SplitTemplateRigidity.lean

1 import PaperX.MatrixSpanBound
2 import PaperX.IntegralActionSpan
3 
4 /-! A uniform determinant detector inferred from a fixed split irreducible template.
5 Irreducibility and the scalar-commutant property concern the actual fraction-field
6 representation. Full action span and a detecting depth are conclusions, not inputs. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.SplitTemplateRigidity
10 open PaperX.RepresentationLimits PaperX.RepresentationClasses PaperX.IntegralActionSpan
11 open scoped MonoidAlgebra
12 variable {R K G n : Type*} [CommRing R] [IsDomain R]
13   [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K]
14   [Group G] [Fintype n] [DecidableEq n]
15 
16 /-- One determinant depth works for every integral member of the field-isomorphism
17 class of a fixed split irreducible template. The source group need not be finite. -/
18 theorem uniform_detector_of_split_irreducible (τ : MatrixRep R G n)
19     [Representation.IsIrreducible
20       (matrixRepresentation (changeCoefficients (algebraMap R K) τ))]
21     (hscalar : Function.Surjective (algebraMap K (Module.End K[G]
22       (matrixRepresentation (changeCoefficients (algebraMap R K) τ)).asModule)))
23     (π : R) (hπ : Irreducible π) :
24     ∃ c : ℕ, ∀ ρ : MatrixRep R G n,
25       Conjugate (changeCoefficients (algebraMap R K) τ)
26         (changeCoefficients (algebraMap R K) ρ) →
27       ∃ P : Matrix n n R, (∀ g, ρ g * P = P * τ g) ∧
28         (P.map (Ideal.Quotient.mk
29           ((Ideal.span {π}) ^ (c * Fintype.card n + 1)))).det ≠ 0 := by
30   have hs := matrix_span_eq_top_of_split_irreducible
31     (changeCoefficients (algebraMap R K) τ) hscalar
32   exact MatrixSpanBound.uniform_detector_for_conjugates τ π hπ hs
33 
34 end PaperX.SplitTemplateRigidity

Back to source controls