FamilyRigidity.lean

1 import PaperX.OrthogonalProjectors
2 import PaperX.PrecisionAveraging
3 
4 /-! Complete labeled projector decompositions with the same positive reduction
5 are conjugate by an equivariant integral unit congruent to the identity.
6 The carrier group need not be finite and the coefficient ring need not be complete. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperX.FamilyRigidity
10 open PaperX.RepresentationLimits PaperX.MatrixProjector PaperX.OrthogonalProjectors
11 open scoped BigOperators
12 
13 variable {R Γ ι J : Type*} [CommRing R] [Group Γ]
14   [Fintype ι] [DecidableEq ι] [Fintype J]
15 variable {ρ : MatrixRep R Γ ι}
16 
17 /-- The change of decomposition respects each label separately. -/
18 def comparison (E F : Family ρ J) : Matrix ι ι R :=
19   ∑ i, (F.projector i).matrix * (E.projector i).matrix
20 
21 theorem comparison_right (E F : Family ρ J) (j : J) :
22     comparison E F * (E.projector j).matrix =
23       (F.projector j).matrix * (E.projector j).matrix := by
24   classical
25   unfold comparison
26   rw [Finset.sum_mul]
27   simp only [mul_assoc, E.product]
28   simp
29 
30 theorem comparison_left (E F : Family ρ J) (j : J) :
31     (F.projector j).matrix * comparison E F =
32       (F.projector j).matrix * (E.projector j).matrix := by
33   classical
34   unfold comparison
35   rw [Finset.mul_sum]
36   simp only [← mul_assoc, F.product]
37   simp
38 
39 theorem comparison_intertwines (E F : Family ρ J) (j : J) :
40     comparison E F * (E.projector j).matrix =
41       (F.projector j).matrix * comparison E F :=
42   (comparison_right E F j).trans (comparison_left E F j).symm
43 
44 theorem comparison_commutes (E F : Family ρ J) (g : Γ) :
45     ρ g * comparison E F = comparison E F * ρ g := by
46   unfold comparison
47   rw [Finset.mul_sum, Finset.sum_mul]
48   apply Finset.sum_congr rfl
49   intro i _
50   rw [← mul_assoc, (F.projector i).commutes, mul_assoc,
51     (E.projector i).commutes, ← mul_assoc]
52 
53 /-- Equal reductions of each labeled projector force the comparison to reduce
54 to the identity; equality of unlabeled sets is not the hypothesis. -/
55 theorem comparison_map {S : Type*} [CommRing S] (f : R →+* S)
56     (E F : Family ρ J)
57     (hEF : ∀ i, (E.projector i).matrix.map f = (F.projector i).matrix.map f) :
58     (comparison E F).map f = 1 := by
59   change f.mapMatrix (∑ i, (F.projector i).matrix * (E.projector i).matrix) = 1
60   rw [map_sum]
61   have hterm (i : J) :
62       f.mapMatrix ((F.projector i).matrix * (E.projector i).matrix) =
63         f.mapMatrix (F.projector i).matrix := by
64     change ((F.projector i).matrix * (E.projector i).matrix).map f = _
65     rw [Matrix.map_mul, hEF, ← Matrix.map_mul, (F.projector i).idempotent]
66     rfl
67   simp only [hterm]
68   rw [← map_sum, F.total, map_one]
69 
70 /-- A unit-reflecting coefficient map suffices for simultaneous rigidity. -/
71 theorem exists_conjugating_unit {S : Type*} [CommRing S] (f : R →+* S)
72     [IsLocalHom f] (E F : Family ρ J)
73     (hEF : ∀ i, (E.projector i).matrix.map f = (F.projector i).matrix.map f) :
74     ∃ U : (Matrix ι ι R)ˣ,
75       (U : Matrix ι ι R) = comparison E F ∧
76       (U : Matrix ι ι R).map f = 1 ∧
77       (∀ g, ρ g * (U : Matrix ι ι R) = (U : Matrix ι ι R) * ρ g) ∧
78       (∀ j, (U : Matrix ι ι R) * (E.projector j).matrix *
79         (↑(U⁻¹) : Matrix ι ι R) = (F.projector j).matrix) := by
80   have hm := comparison_map f E F hEF
81   have hu : IsUnit (comparison E F) :=
82     PaperX.FiniteGroupAveraging.matrix_isUnit_of_map f _ (hm.symm ▸ isUnit_one)
83   obtain ⟨U, hU⟩ := hu
84   refine ⟨U, hU, by simpa only [hU] using hm, ?_, ?_⟩
85   · intro g
86     simpa only [hU] using comparison_commutes E F g
87   · intro j
88     have hj : (U : Matrix ι ι R) * (E.projector j).matrix =
89         (F.projector j).matrix * (U : Matrix ι ι R) := by
90       simpa only [hU] using comparison_intertwines E F j
91     rw [hj, mul_assoc, Units.mul_inv, mul_one]
92 
93 /-- Positive precision determines a complete labeled decomposition up to an
94 equivariant change of basis congruent to the identity at that same precision.
95 There is no extra loss depending on the number of projectors. -/
96 theorem exists_conjugating_unit_of_reduction [IsLocalRing R]
97     (π : R) (hπ : ¬ IsUnit π) (k : ℕ) (hk : 0 < k)
98     (E F : Family ρ J)
99     (hEF : ∀ i,
100       (E.projector i).matrix.map (Ideal.Quotient.mk ((Ideal.span {π})^k)) =
101       (F.projector i).matrix.map (Ideal.Quotient.mk ((Ideal.span {π})^k))) :
102     ∃ U : (Matrix ι ι R)ˣ,
103       (U : Matrix ι ι R) = comparison E F ∧
104       (U : Matrix ι ι R).map (Ideal.Quotient.mk ((Ideal.span {π})^k)) = 1 ∧
105       (∀ g, ρ g * (U : Matrix ι ι R) = (U : Matrix ι ι R) * ρ g) ∧
106       (∀ j, (U : Matrix ι ι R) * (E.projector j).matrix *
107         (↑(U⁻¹) : Matrix ι ι R) = (F.projector j).matrix) := by
108   let := PaperX.PrecisionAveraging.positive_quotient_local π hπ k hk
109   exact exists_conjugating_unit _ E F hEF
110 
111 /-- A projector intertwiner maps the actual image into the corresponding image. -/
112 theorem mulVec_mem_image (E F : Projector ρ) (A : Matrix ι ι R)
113     (hA : A * E.matrix = F.matrix * A) (v : E.image.toSubmodule) :
114     A.mulVec (v : ι → R) ∈ F.image.toSubmodule := by
115   rw [F.image_iff, Matrix.mulVec_mulVec, ← hA, ← Matrix.mulVec_mulVec,
116     (E.image_iff _).mp v.property]
117 
118 theorem inverse_intertwines (E F : Projector ρ) (U : (Matrix ι ι R)ˣ)
119     (hU : (U : Matrix ι ι R) * E.matrix = F.matrix * (U : Matrix ι ι R)) :
120     (↑(U⁻¹) : Matrix ι ι R) * F.matrix =
121       E.matrix * (↑(U⁻¹) : Matrix ι ι R) := by
122   calc
123     (↑(U⁻¹) : Matrix ι ι R) * F.matrix =
124         (↑(U⁻¹) : Matrix ι ι R) * (F.matrix * (U : Matrix ι ι R)) *
125           (↑(U⁻¹) : Matrix ι ι R) := by simp [mul_assoc]
126     _ = (↑(U⁻¹) : Matrix ι ι R) * ((U : Matrix ι ι R) * E.matrix) *
127           (↑(U⁻¹) : Matrix ι ι R) := by rw [hU]
128     _ = E.matrix * (↑(U⁻¹) : Matrix ι ι R) := by simp [← mul_assoc]
129 
130 /-- Simultaneous conjugacy restricts to actual linear isomorphisms of images. -/
131 def imageEquiv (E F : Projector ρ) (U : (Matrix ι ι R)ˣ)
132     (hU : (U : Matrix ι ι R) * E.matrix = F.matrix * (U : Matrix ι ι R)) :
133     E.image.toSubmodule ≃ₗ[R] F.image.toSubmodule where
134   toFun v := ⟨(U : Matrix ι ι R).mulVec v, mulVec_mem_image E F U hU v⟩
135   invFun v := ⟨(↑(U⁻¹) : Matrix ι ι R).mulVec v,
136     mulVec_mem_image F E (↑(U⁻¹)) (inverse_intertwines E F U hU) v⟩
137   left_inv v := by
138     apply Subtype.ext
139     change (↑(U⁻¹) : Matrix ι ι R).mulVec ((U : Matrix ι ι R).mulVec v) = v
140     rw [Matrix.mulVec_mulVec, Units.inv_mul, Matrix.one_mulVec]
141   right_inv v := by
142     apply Subtype.ext
143     change (U : Matrix ι ι R).mulVec ((↑(U⁻¹) : Matrix ι ι R).mulVec v) = v
144     rw [Matrix.mulVec_mulVec, Units.mul_inv, Matrix.one_mulVec]
145   map_add' v w := by
146     apply Subtype.ext
147     exact Matrix.mulVec_add _ _ _
148   map_smul' a v := by
149     apply Subtype.ext
150     exact Matrix.mulVec_smul _ _ _
151 
152 theorem imageEquiv_apply (E F : Projector ρ) (U : (Matrix ι ι R)ˣ)
153     (hU : (U : Matrix ι ι R) * E.matrix = F.matrix * (U : Matrix ι ι R))
154     (v : E.image.toSubmodule) :
155     (imageEquiv E F U hU v : ι → R) = (U : Matrix ι ι R).mulVec v := rfl
156 
157 /-- The image isomorphism respects the inherited carrier representation. -/
158 theorem imageEquiv_equivariant (E F : Projector ρ) (U : (Matrix ι ι R)ˣ)
159     (hU : (U : Matrix ι ι R) * E.matrix = F.matrix * (U : Matrix ι ι R))
160     (hρ : ∀ g, ρ g * (U : Matrix ι ι R) = (U : Matrix ι ι R) * ρ g)
161     (g : Γ) (v : E.image.toSubmodule) :
162     imageEquiv E F U hU (E.image.toRepresentation g v) =
163       F.image.toRepresentation g (imageEquiv E F U hU v) := by
164   apply Subtype.ext
165   change (U : Matrix ι ι R).mulVec ((ρ g).mulVec (v : ι → R)) =
166     (ρ g).mulVec ((U : Matrix ι ι R).mulVec (v : ι → R))
167   rw [Matrix.mulVec_mulVec, Matrix.mulVec_mulVec, hρ]
168 
169 end PaperX.FamilyRigidity

Back to source controls