FamilyBoundary.lean

1 import PaperX.FamilyRigidity
2 import PaperX.SummandBoundary
3 
4 /-! Independent idempotent lifting does not preserve a decomposition.  The
5 examples use an actual rank-two Z_2 carrier with trivial C2 action. Distinct
6 complete families with the same reduction can nevertheless be conjugate by a
7 matrix congruent to the identity. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperX.FamilyBoundary
11 open scoped Matrix BigOperators
12 open PaperX.RepresentationLimits PaperX.CompletionExamples
13 open PaperX.PrecisionExamples PaperX.OrthogonalProjectors
14 
15 private theorem modTwo_two : modTwo (2 : ℤ_[2]) = 0 := by
16   rw [show (2 : ℤ_[2]) = 1 + 1 by norm_num, map_add, map_one]
17   decide +kernel
18 
19 abbrev trivialCarrier : MatrixRep ℤ_[2] C2 (Fin 2) := 1
20 
21 def leftProjector : Matrix (Fin 2) (Fin 2) ℤ_[2] := !![1, 0; 0, 0]
22 def skewRight (b : ℤ_[2]) : Matrix (Fin 2) (Fin 2) ℤ_[2] := !![0, b; 0, 1]
23 def adjustedLeft (b : ℤ_[2]) : Matrix (Fin 2) (Fin 2) ℤ_[2] := !![1, -b; 0, 0]
24 def shear (b : ℤ_[2]) : Matrix (Fin 2) (Fin 2) ℤ_[2] := !![1, b; 0, 1]
25 
26 theorem independent_idempotents (b : ℤ_[2]) :
27     leftProjector * leftProjector = leftProjector ∧
28       skewRight b * skewRight b = skewRight b := by
29   constructor <;> ext i j <;> fin_cases i <;> fin_cases j <;>
30     simp [leftProjector, skewRight, Matrix.mul_apply, Fin.sum_univ_succ]
31 
32 theorem independent_lifts_same_reduction :
33     (skewRight 2).map modTwo = (skewRight 0).map modTwo := by
34   ext i j
35   fin_cases i <;> fin_cases j <;> norm_num [skewRight, modTwo_two]
36 
37 theorem independent_lifts_not_orthogonal : leftProjector * skewRight 2 ≠ 0 := by
38   intro h
39   have h01 := congrArg (fun M : Matrix (Fin 2) (Fin 2) ℤ_[2] => M 0 1) h
40   norm_num [leftProjector, skewRight, Matrix.mul_apply, Fin.sum_univ_succ] at h01
41 
42 theorem independent_lifts_not_total : leftProjector + skewRight 2 ≠ 1 := by
43   intro h
44   have h01 := congrArg (fun M : Matrix (Fin 2) (Fin 2) ℤ_[2] => M 0 1) h
45   norm_num [leftProjector, skewRight] at h01
46 
47 /-- Both independent lifts are genuine equivariant idempotents. -/
48 theorem independent_lifts_commute (b : ℤ_[2]) (g : C2) :
49     trivialCarrier g * leftProjector = leftProjector * trivialCarrier g ∧
50       trivialCarrier g * skewRight b = skewRight b * trivialCarrier g := by
51   simp [trivialCarrier]
52 
53 def familyMatrix (b : ℤ_[2]) (i : Fin 2) : Matrix (Fin 2) (Fin 2) ℤ_[2] :=
54   if i = 0 then adjustedLeft b else skewRight b
55 
56 theorem familyMatrix_idempotent (b : ℤ_[2]) (i : Fin 2) :
57     familyMatrix b i * familyMatrix b i = familyMatrix b i := by
58   fin_cases i <;> ext a c <;> fin_cases a <;> fin_cases c <;>
59     simp [familyMatrix, adjustedLeft, skewRight, Matrix.mul_apply, Fin.sum_univ_succ]
60 
61 theorem familyMatrix_orthogonal (b : ℤ_[2]) (i j : Fin 2) (h : i ≠ j) :
62     familyMatrix b i * familyMatrix b j = 0 := by
63   fin_cases i <;> fin_cases j
64   all_goals try contradiction
65   all_goals ext a c; fin_cases a <;> fin_cases c <;>
66     simp [familyMatrix, adjustedLeft, skewRight, Matrix.mul_apply, Fin.sum_univ_succ]
67 
68 theorem familyMatrix_total (b : ℤ_[2]) : ∑ i : Fin 2, familyMatrix b i = 1 := by
69   ext a c
70   fin_cases a <;> fin_cases c <;>
71     simp [familyMatrix, adjustedLeft, skewRight, Fin.sum_univ_succ]
72 
73 def splitFamily (b : ℤ_[2]) : Family trivialCarrier (Fin 2) where
74   projector i := {
75     matrix := familyMatrix b i
76     idempotent := familyMatrix_idempotent b i
77     commutes := by intro g; simp [trivialCarrier] }
78   orthogonal := familyMatrix_orthogonal b
79   total := familyMatrix_total b
80 
81 theorem complete_families_same_reduction (i : Fin 2) :
82     ((splitFamily 2).projector i).matrix.map modTwo =
83       ((splitFamily 0).projector i).matrix.map modTwo := by
84   fin_cases i <;> ext a c <;> fin_cases a <;> fin_cases c <;>
85     norm_num [splitFamily, familyMatrix, adjustedLeft, skewRight, modTwo_two]
86 
87 theorem complete_families_distinct : splitFamily 2 ≠ splitFamily 0 := by
88   intro h
89   have h01 := congrArg (fun E : Family trivialCarrier (Fin 2) =>
90     (E.projector 1).matrix 0 1) h
91   norm_num [splitFamily, familyMatrix, skewRight] at h01
92 
93 theorem shear_inverse (b : ℤ_[2]) : shear b * shear (-b) = 1 ∧
94     shear (-b) * shear b = 1 := by
95   constructor <;> ext i j <;> fin_cases i <;> fin_cases j <;>
96     simp [shear, Matrix.mul_apply, Fin.sum_univ_succ]
97 
98 def shearUnit (b : ℤ_[2]) : (Matrix (Fin 2) (Fin 2) ℤ_[2])ˣ where
99   val := shear b
100   inv := shear (-b)
101   val_inv := (shear_inverse b).1
102   inv_val := (shear_inverse b).2
103 
104 theorem shear_preserves_labels (b : ℤ_[2]) (i : Fin 2) :
105     shear b * ((splitFamily 0).projector i).matrix =
106       ((splitFamily b).projector i).matrix * shear b := by
107   fin_cases i <;> ext a c <;> fin_cases a <;> fin_cases c <;>
108     simp [splitFamily, familyMatrix, adjustedLeft, skewRight, shear,
109       Matrix.mul_apply, Fin.sum_univ_succ]
110 
111 theorem shear_congruent_identity : (shear 2).map modTwo = 1 := by
112   ext i j
113   fin_cases i <;> fin_cases j <;> norm_num [shear, modTwo_two]
114 
115 /-- Nonuniqueness is compatible with the precise labeled conjugacy conclusion. -/
116 theorem distinct_families_have_identity_congruent_equivariant_conjugacy :
117     splitFamily 2 ≠ splitFamily 0 ∧
118     ∃ U : (Matrix (Fin 2) (Fin 2) ℤ_[2])ˣ,
119       (U : Matrix (Fin 2) (Fin 2) ℤ_[2]).map modTwo = 1 ∧
120       (∀ g : C2, trivialCarrier g * U = U * trivialCarrier g) ∧
121       ∀ i : Fin 2, (U : Matrix (Fin 2) (Fin 2) ℤ_[2]) *
122           ((splitFamily 0).projector i).matrix =
123         ((splitFamily 2).projector i).matrix * U := by
124   refine ⟨complete_families_distinct, shearUnit 2, shear_congruent_identity, ?_,
125     shear_preserves_labels 2⟩
126   intro g
127   simp [trivialCarrier]
128 
129 /-- The general rigidity theorem applies to the two explicit distinct families. -/
130 theorem generic_rigidity_on_distinct_families :
131     ∃ U : (Matrix (Fin 2) (Fin 2) ℤ_[2])ˣ,
132       (U : Matrix (Fin 2) (Fin 2) ℤ_[2]) =
133         FamilyRigidity.comparison (splitFamily 0) (splitFamily 2) ∧
134       (U : Matrix (Fin 2) (Fin 2) ℤ_[2]).map
135         (Ideal.Quotient.mk (twoIdeal^1)) = 1 ∧
136       (∀ g : C2, trivialCarrier g * (U : Matrix (Fin 2) (Fin 2) ℤ_[2]) =
137         (U : Matrix (Fin 2) (Fin 2) ℤ_[2]) * trivialCarrier g) ∧
138       ∀ i : Fin 2, (U : Matrix (Fin 2) (Fin 2) ℤ_[2]) *
139           ((splitFamily 0).projector i).matrix *
140           (↑(U⁻¹) : Matrix (Fin 2) (Fin 2) ℤ_[2]) =
141         ((splitFamily 2).projector i).matrix := by
142   apply FamilyRigidity.exists_conjugating_unit_of_reduction (2 : ℤ_[2])
143     PadicInt.irreducible_p.not_isUnit 1 (by decide) (splitFamily 0) (splitFamily 2)
144   intro i
145   apply (quotient_matrices_eq_iff 1 _ _).mpr
146   have htwo : PadicInt.toZModPow 1 (2 : ℤ_[2]) = 0 := by
147     rw [show (2 : ℤ_[2]) = 1 + 1 by norm_num, map_add, map_one]
148     decide +kernel
149   fin_cases i <;> ext a c <;> fin_cases a <;> fin_cases c <;>
150     norm_num [splitFamily, familyMatrix, adjustedLeft, skewRight, htwo]
151 
152 end PaperX.FamilyBoundary

Back to source controls