FamilyExamples.lean

1 import PaperX.OrthogonalLifting
2 import PaperX.SummandExamples
3 
4 /-! A three-summand example with a nonunit finite-group order.  The actual
5 carrier is diag(1,sign,1) over Z_2. An integral shear produces a complete
6 orthogonal family which is equivariant modulo four, but cannot be retained
7 modulo four by any exact equivariant lift. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperX.FamilyExamples
11 open scoped Matrix BigOperators
12 open PaperX.RepresentationLimits PaperX.CompletionExamples
13 open PaperX.PrecisionExamples PaperX.OrthogonalProjectors
14 
15 private theorem modFour_two : modFour (2 : ℤ_[2]) = 2 := by
16   rw [show (2 : ℤ_[2]) = 1 + 1 by norm_num, map_add, map_one]
17   decide +kernel
18 
19 def integerCarrier : MatrixRep ℤ C2 (Fin 3) where
20   toFun g := !![1, 0, 0; 0, signValue g, 0; 0, 0, 1]
21   map_one' := by decide +kernel
22   map_mul' := by decide +kernel
23 
24 def tau3 : MatrixRep ℤ_[2] C2 (Fin 3) :=
25   changeCoefficients (Int.castRingHom ℤ_[2]) integerCarrier
26 
27 theorem tau3_continuous :
28     PaperX.RepresentationTopology.AdicRepContinuous twoIdeal tau3 := by
29   let : TopologicalSpace ℤ_[2] := twoIdeal.adicTopology
30   exact continuous_of_discreteTopology
31 
32 def integerProjectors (i : Fin 3) : Matrix (Fin 3) (Fin 3) ℤ :=
33   ![!![1, -2, 0; 0, 0, 0; 0, 0, 0],
34     !![0, 2, 0; 0, 1, 0; 0, 0, 0],
35     !![0, 0, 0; 0, 0, 0; 0, 0, 1]] i
36 
37 def pAdicProjectors (i : Fin 3) : Matrix (Fin 3) (Fin 3) ℤ_[2] :=
38   (integerProjectors i).map (Int.castRingHom ℤ_[2])
39 
40 theorem integer_idempotent : ∀ i : Fin 3,
41     integerProjectors i * integerProjectors i = integerProjectors i := by
42   decide +kernel
43 
44 theorem integer_orthogonal : ∀ i j : Fin 3, i ≠ j →
45     integerProjectors i * integerProjectors j = 0 := by decide +kernel
46 
47 theorem integer_total : ∑ i : Fin 3, integerProjectors i = 1 := by decide +kernel
48 
49 theorem integer_diagonal : ∀ i : Fin 3, integerProjectors i i i = 1 := by decide +kernel
50 
51 theorem integer_commutes_mod_four : ∀ (g : C2) (i : Fin 3),
52     (integerCarrier g).map (Int.castRingHom (ZMod 4)) *
53         (integerProjectors i).map (Int.castRingHom (ZMod 4)) =
54       (integerProjectors i).map (Int.castRingHom (ZMod 4)) *
55         (integerCarrier g).map (Int.castRingHom (ZMod 4)) := by decide +kernel
56 
57 theorem pAdic_idempotent (i : Fin 3) :
58     pAdicProjectors i * pAdicProjectors i = pAdicProjectors i := by
59   unfold pAdicProjectors
60   rw [← Matrix.map_mul, integer_idempotent]
61 
62 theorem pAdic_orthogonal (i j : Fin 3) (h : i ≠ j) :
63     pAdicProjectors i * pAdicProjectors j = 0 := by
64   unfold pAdicProjectors
65   rw [← Matrix.map_mul, integer_orthogonal i j h]
66   ext a b
67   simp only [Matrix.map_apply, Matrix.zero_apply, map_zero]
68 
69 theorem pAdic_total : ∑ i : Fin 3, pAdicProjectors i = 1 := by
70   change ∑ i : Fin 3, (Int.castRingHom ℤ_[2]).mapMatrix (integerProjectors i) = 1
71   rw [← map_sum, integer_total, map_one]
72 
73 theorem pAdic_diagonal (i : Fin 3) : pAdicProjectors i i i = 1 := by
74   simp only [pAdicProjectors, Matrix.map_apply, integer_diagonal, map_one]
75 
76 theorem pAdic_commutes_mod_four (g : C2) (i : Fin 3) :
77     (tau3 g).map modFour * (pAdicProjectors i).map modFour =
78       (pAdicProjectors i).map modFour * (tau3 g).map modFour := by
79   simpa [tau3, pAdicProjectors, changeCoefficients, Matrix.map_map,
80     Function.comp_def] using integer_commutes_mod_four g i
81 
82 /-- The quotient comparison is independent of the matrix rank. -/
83 theorem quotient_matrices_eq_iff_three (n : ℕ)
84     (A B : Matrix (Fin 3) (Fin 3) ℤ_[2]) :
85     A.map (Ideal.Quotient.mk (twoIdeal^n)) = B.map (Ideal.Quotient.mk (twoIdeal^n)) ↔
86       A.map (PadicInt.toZModPow n) = B.map (PadicInt.toZModPow n) := by
87   constructor
88   · intro h
89     ext i j
90     exact (quotient_eq_iff n _ _).mp (congrArg (fun M => M i j) h)
91   · intro h
92     ext i j
93     exact (quotient_eq_iff n _ _).mpr (congrArg (fun M => M i j) h)
94 
95 theorem pAdic_commutes_quotient (g : C2) (i : Fin 3) :
96     (tau3 g).map (Ideal.Quotient.mk (twoIdeal^2)) *
97         (pAdicProjectors i).map (Ideal.Quotient.mk (twoIdeal^2)) =
98       (pAdicProjectors i).map (Ideal.Quotient.mk (twoIdeal^2)) *
99         (tau3 g).map (Ideal.Quotient.mk (twoIdeal^2)) := by
100   rw [← Matrix.map_mul, ← Matrix.map_mul]
101   apply (quotient_matrices_eq_iff_three 2 _ _).mpr
102   simpa only [Matrix.map_mul] using pAdic_commutes_mod_four g i
103 
104 /-- Three nonzero prescribed orthogonal quotient projectors. -/
105 def inputFamily : Family (reduce twoIdeal tau3 2) (Fin 3) where
106   projector i := {
107     matrix := (pAdicProjectors i).map (Ideal.Quotient.mk (twoIdeal^2))
108     idempotent := by rw [← Matrix.map_mul, pAdic_idempotent]
109     commutes := by intro g; exact pAdic_commutes_quotient g i }
110   orthogonal i j hij := by
111     change (pAdicProjectors i).map _ * (pAdicProjectors j).map _ = 0
112     rw [← Matrix.map_mul, pAdic_orthogonal i j hij]
113     ext a b
114     simp only [Matrix.map_apply, Matrix.zero_apply, map_zero]
115   total := by
116     change ∑ i : Fin 3, (Ideal.Quotient.mk (twoIdeal^2)).mapMatrix (pAdicProjectors i) = 1
117     rw [← map_sum, pAdic_total, map_one]
118 
119 /-- Exact equivariance forces the mixed-sign entry to vanish. -/
120 theorem commuting_upper_right_zero (P : Matrix (Fin 3) (Fin 3) ℤ_[2])
121     (hP : ∀ g : C2, tau3 g * P = P * tau3 g) : P 0 1 = 0 := by
122   have h01 := congrArg (fun M : Matrix (Fin 3) (Fin 3) ℤ_[2] => M 0 1)
123     (hP generator)
124   norm_num [tau3, changeCoefficients, integerCarrier, signValue, generator,
125     Matrix.mul_apply, Fin.sum_univ_succ] at h01
126   have heq : 2 * P 0 1 = 0 := by linear_combination h01
127   exact (mul_eq_zero.mp heq).resolve_left (by norm_num)
128 
129 theorem pAdic_family_not_equivariant :
130     ¬ ∀ (g : C2) (i : Fin 3), tau3 g * pAdicProjectors i =
131       pAdicProjectors i * tau3 g := by
132   intro h
133   have hz := commuting_upper_right_zero (pAdicProjectors 1) (fun g => h g 1)
134   norm_num [pAdicProjectors, integerProjectors] at hz
135 
136 /-- Even one of the three prescribed projectors cannot be retained modulo four.
137 The failure concerns exact equivariance, before asking for orthogonality. -/
138 theorem no_exact_family_retains_mod_four :
139     ¬ ∃ E : Family tau3 (Fin 3), ∀ i : Fin 3,
140       (E.projector i).matrix.map modFour = (pAdicProjectors i).map modFour := by
141   rintro ⟨E, hE⟩
142   have hz := commuting_upper_right_zero (E.projector 1).matrix
143     (E.projector 1).commutes
144   have h01 := congrArg (fun M : Matrix (Fin 3) (Fin 3) (ZMod 4) => M 0 1) (hE 1)
145   norm_num [Matrix.map_apply, pAdicProjectors, integerProjectors, hz, modFour_two] at h01
146   exact (by decide : (0 : ZMod 4) ≠ 2) h01
147 
148 /-- The preserved diagonal witnesses that every output summand is nonzero. -/
149 theorem nonzero_of_reduction (i : Fin 3) (P : Matrix (Fin 3) (Fin 3) ℤ_[2])
150     (hP : P.map (Ideal.Quotient.mk (twoIdeal^1)) =
151       (pAdicProjectors i).map (Ideal.Quotient.mk (twoIdeal^1))) : P ≠ 0 := by
152   intro hz
153   have h := (quotient_matrices_eq_iff_three 1 _ _).mp hP
154   have hii := congrArg (fun M : Matrix (Fin 3) (Fin 3) (ZMod (2^1)) => M i i) h
155   simp only [Matrix.map_apply, pAdic_diagonal, hz, Matrix.zero_apply, map_zero,
156     map_one] at hii
157   exact (by decide : (0 : ZMod (2^1)) ≠ 1) hii
158 
159 /-- The general simultaneous theorem constructs three nonzero exact summands
160 from this mod-four family while retaining its prescribed mod-two reduction.
161 The group order is two, so this tests the nonunit-order case and a family with
162 more than a projector and its complement. -/
163 theorem actual_three_summand_lift :
164     ∃ E : Family tau3 (Fin 3),
165       (∀ i : Fin 3, (E.projector i).matrix.map
166           (Ideal.Quotient.mk (twoIdeal^1)) =
167         (pAdicProjectors i).map (Ideal.Quotient.mk (twoIdeal^1))) ∧
168       ∀ i : Fin 3, (E.projector i).matrix ≠ 0 := by
169   obtain ⟨E, hE⟩ := OrthogonalLifting.exists_family_lift (2 : ℤ_[2]) 1 1
170     (by decide) tau3 group_order_nonzero group_order_divides_two inputFamily
171   have hred (i : Fin 3) : (E.projector i).matrix.map
172         (Ideal.Quotient.mk (twoIdeal^1)) =
173       (pAdicProjectors i).map (Ideal.Quotient.mk (twoIdeal^1)) := by
174     rw [hE]
175     ext a b
176     simp [inputFamily]
177   exact ⟨E, hred, fun i => nonzero_of_reduction i _ (hred i)⟩
178 
179 end PaperX.FamilyExamples

Back to source controls