FamilyClassification.lean

1 import PaperX.OrthogonalLifting
2 import PaperX.FamilySummands
3 import PaperX.FamilyRigidity
4 
5 /-! End-to-end finite-depth existence and labeled conjugacy classification
6 inside a supplied complete local finite-group carrier. -/
7 set_option autoImplicit false
8 namespace PaperX.FamilyClassification
9 open PaperX.RepresentationLimits PaperX.OrthogonalProjectors
10 
11 variable {R Γ ι J : Type*} [CommRing R] [IsDomain R] [IsLocalRing R]
12   [Group Γ] [Fintype Γ] [Fintype ι] [DecidableEq ι] [Fintype J]
13 
14 /-- Every allowed deep family has a lift, and all lifts of its retained
15 reduction are equivariantly conjugate by a unit equal to the identity there. -/
16 theorem exists_family_unique_up_to_conjugacy
17     (π : R) [IsAdicComplete (Ideal.span {π}) R] (hπ : ¬ IsUnit π)
18     (e k : ℕ) (hk : 0 < k) (ρ : MatrixRep R Γ ι)
19     (hΓ : (Fintype.card Γ : R) ≠ 0)
20     (hdiv : (Fintype.card Γ : R) ∣ π^e)
21     (Q : Family (reduce (Ideal.span {π}) ρ (e+k)) J) :
22     ∃ E : Family ρ J,
23       (∀ i, (E.projector i).matrix.map (Ideal.Quotient.mk ((Ideal.span {π})^k)) =
24         (Q.projector i).matrix.map
25           (Ideal.Quotient.factorPow (Ideal.span {π}) (Nat.le_add_left k e))) ∧
26       ∀ F : Family ρ J,
27         (∀ i, (F.projector i).matrix.map (Ideal.Quotient.mk ((Ideal.span {π})^k)) =
28           (Q.projector i).matrix.map
29             (Ideal.Quotient.factorPow (Ideal.span {π}) (Nat.le_add_left k e))) →
30         ∃ U : (Matrix ι ι R)ˣ,
31           (U : Matrix ι ι R) = FamilyRigidity.comparison E F ∧
32           (U : Matrix ι ι R).map (Ideal.Quotient.mk ((Ideal.span {π})^k)) = 1 ∧
33           (∀ g, ρ g * (U : Matrix ι ι R) = (U : Matrix ι ι R) * ρ g) ∧
34           ∀ i, (U : Matrix ι ι R) * (E.projector i).matrix *
35             (↑(U⁻¹) : Matrix ι ι R) = (F.projector i).matrix := by
36   obtain ⟨E, hE⟩ := OrthogonalLifting.exists_family_lift π e k hk ρ hΓ hdiv Q
37   refine ⟨E, hE, fun F hF => ?_⟩
38   exact FamilyRigidity.exists_conjugating_unit_of_reduction π hπ k hk E F
39     (fun i => (hE i).trans (hF i).symm)
40 
41 end PaperX.FamilyClassification

Back to source controls