RigidLocalSystems

Lean formalization toward Katz's Rigid Local Systems, using mathlib.

Current definitions

Import RigidLocalSystems and open the namespace RigidLocalSystems.

• LocalSystem K X is a functor from the fundamental groupoid of X to FGModuleCat K. Over a field, its fibers are finite-dimensional vector spaces. Its morphisms are natural transformations; F ≅ G is a natural isomorphism.
• LocalSystem.fiber, transport, constant, and pullback provide fibers, parallel transport, constant systems, and pullback along continuous maps.
• Given maps j i : C(D i, U), SameLocalMonodromy j F G means ∀ i, Nonempty (F.pullback (j i) ≅ G.pullback (j i)).
• PhysicallyRigid j F means every local system G with the same local monodromy is globally isomorphic to F. Competitors need not be irreducible.
• LocalSystem.IsIrreducible F means F is a simple object of this category. It excludes the zero object and uses actual categorical subobjects.

For Katz §§1.0.2–1.0.3, take the index type to be the finite nonempty set of punctures and the maps j i to be punctured-disc inclusions into U. The definitions allow general families of continuous maps; they do not construct punctured discs or assert that arbitrary maps are boundary neighborhoods.

Proved: reflexivity, symmetry, and transitivity of SameLocalMonodromy; global isomorphism implies local equivalence; physical rigidity is invariant under isomorphism; for a rigid system, local equivalence is equivalent to global isomorphism.

Progress on Theorem 1.1.2

Both directions are proved for irreducible complex monodromy tuples, in MonodromyTuple.physicallyRigid_iff_index_eq_two. This theorem has no additional cohomological or dimension hypotheses. The full local-system/sheaf formulation is not yet proved: the comparison theorems remain. See the proof status for the exact remaining obligations.

• Irreducible.lean proves constancy of rank along paths, finite-dimensionality of Hom spaces on path-connected bases, the equal-rank nonzero-morphism argument, and Schur's endomorphism-dimension formula.
• MonodromyTuple.lean proves the group-theoretic centralizer factorization behind the converse's orbit argument, using the full conjugating group.
• SpecialLinearConjugacy.lean proves that simultaneous conjugators can be chosen in SL over an algebraically closed field in positive rank.
• ConjugatorAction.lean constructs the action of SL × ∏ Z(Aᵢ) on the product-one fiber, proves equivariance of the SL-valued product map, and proves that tuple rigidity is equivalent to transitivity of this action.
• CommutingAlgebra.lean identifies centralizer groups with units of commuting algebras and describes invertibility by nonvanishing of the determinant.
• LocalIntertwiner.lean constructs the linear isomorphisms for local Hom spaces. NumericalIndex.lean uses them to prove local-conjugacy invariance of the matrix index and equality of the local Hom and End formulas.
• CentralizerDensity.lean proves that polynomials on a commuting algebra over an infinite field are determined by their values on invertible elements. This does not yet prove equality of algebraic-geometric dimensions.
• ParabolicComplex.lean constructs the algebraic complex of two monodromy tuples and proves that the composite differential vanishes by telescoping. LinearComplexEuler.lean proves Euler–Poincaré for finite-dimensional three-term complexes. ParabolicEuler.lean identifies the matrix index with dim H⁰ − dim H¹ + dim H² for locally conjugate tuples, using actual kernels and quotients.
• ParabolicDuality.lean uses the trace pairing to identify H²(A,B) with the dual of simultaneous intertwiners from B to A. It proves the Euler formula rig(A) = dim Hom(A,B) − dim H¹(A,B) + dim Hom(B,A) for locally conjugate tuples. Comparison with sheaf cohomology remains unproved.
• TupleIrreducible.lean defines irreducibility using invariant subspaces and proves the forward criterion: an irreducible tuple of index two is physically rigid. The tuple result assumes no unproved cohomological identifications.
• TupleSchur.lean proves that endomorphisms of an irreducible tuple are scalar over an algebraically closed field. It derives rig(A) = 2 − dim H¹(A,A), the upper bound rig(A) ≤ 2, and rigidity when H¹ has dimension zero.
• ConstraintLinearization.lean and ProductDerivative.lean identify the actual strict derivative of Katz's product map and prove its surjectivity onto the trace-zero matrices at an irreducible tuple.
• ReducedConstraint.lean constructs local coordinates on the product-one fiber by the implicit function theorem. OrbitLinearization.lean computes the symmetry rank and the dimension defect 2 − rig(A).
• OrbitParameters.lean covers a rigid fiber with finitely many polynomial parametrizations of dimension n² − 1 + ∑ dim z(Aᵢ).
• TupleConverse.lean compares dimensions using Hausdorff dimension and proves the converse. It exports physical rigidity iff index two, iff vanishing of the first parabolic cohomology dimension, and iff linearized exactness.
• Theorem112.lean proves the forward argument conditional on an explicit numerical invariance hypothesis, plus the final converse dimension arithmetic. Its homEulerExpression is not a definition of sheaf Euler characteristic.

Scope

This uses the monodromy model of local systems. The comparison with locally constant sheaves on suitably nice spaces, the punctured-curve geometry, the representation-theoretic comparison for irreducibility, and the identification of parabolic cohomology with Hⁱ(ℙ¹,j_* Hom) remain to be formalized. No such results are assumed as axioms.

References are kept locally in references/Katz.pdf, references/retypesetted.pdf, and references/erratum.png.

Build

Run lake build (Lean and mathlib are pinned in the project configuration).