DyadicProjectorsResidual.lean

1 import PaperXII.DyadicProjectors
2 import PaperXII.ResidualAugmentation
3 import Mathlib.RingTheory.Ideal.Quotient.Operations
4 
5 set_option autoImplicit false
6 
7 /-! Paper XII, Proposition 11.1: the actual residual dual-number algebra. -/
8 namespace PaperXII.DyadicProjectors.Residual
9 
10 abbrev k := ZMod 2
11 
12 noncomputable def squareIdeal : Ideal (Polynomial k) :=
13   Ideal.span {Polynomial.X ^ 2}
14 
15 abbrev Dual := Polynomial k ⧸ squareIdeal
16 
17 noncomputable def X : Dual := Ideal.Quotient.mk squareIdeal Polynomial.X
18 
19 theorem X_sq : X * X = 0 := by
20   change Ideal.Quotient.mk squareIdeal Polynomial.X *
21     Ideal.Quotient.mk squareIdeal Polynomial.X = 0
22   rw [← map_mul, ← pow_two, Ideal.Quotient.eq_zero_iff_mem]
23   exact Ideal.subset_span (Set.mem_singleton _)
24 
25 theorem one_add_X_sq : (1 + X) * (1 + X) = 1 := by
26   have htwo : (2 : Dual) = 0 := by
27     have hz : (2 : k) = 0 := by decide
28     calc
29       (2 : Dual) = (algebraMap k Dual) (2 : k) := (map_ofNat _ _).symm
30       _ = (algebraMap k Dual) 0 := congrArg _ hz
31       _ = 0 := map_zero _
32   calc
33     (1 + X) * (1 + X) = 1 + 2 * X + X * X := by ring
34     _ = 1 := by rw [htwo, X_sq]; ring
35 
36 noncomputable def cyclicMap : G →* Dual where
37   toFun h := if h = 1 then 1 else 1 + X
38   map_one' := by simp
39   map_mul' a b := by
40     rcases group_cases a with rfl | rfl <;> rcases group_cases b with rfl | rfl <;>
41       simp [g_mul_g, g_ne_one, one_add_X_sq]
42 
43 /-- The group generator is sent to 1+X. -/
44 noncomputable def toDual : MonoidAlgebra k G →ₐ[k] Dual :=
45   MonoidAlgebra.lift k Dual G cyclicMap
46 
47 theorem generator_toDual : toDual (generator (K := k)) = 1 + X := by
48   simp [toDual, generator, cyclicMap, g_ne_one]
49 
50 theorem augmentation_generator_sq :
51     (generator (K := k) - 1) * (generator - 1) = 0 := by
52   have hgen : generator (K := k) * generator = 1 := by
53     simp [generator, MonoidAlgebra.single_mul_single, g_mul_g, MonoidAlgebra.one_def]
54   have htwo : (2 : MonoidAlgebra k G) = 0 := by
55     have hz : (2 : k) = 0 := by decide
56     calc
57       (2 : MonoidAlgebra k G) = (algebraMap k (MonoidAlgebra k G)) (2 : k) :=
58         (map_ofNat _ _).symm
59       _ = (algebraMap k (MonoidAlgebra k G)) 0 := congrArg _ hz
60       _ = 0 := map_zero _
61   calc
62     (generator (K := k) - 1) * (generator - 1) =
63       generator * generator - 2 * generator + 1 := by ring
64     _ = 0 := by rw [hgen, htwo]; simpa only [zero_mul, sub_zero, one_add_one_eq_two] using htwo
65 
66 noncomputable def fromDual : Dual →ₐ[k] MonoidAlgebra k G :=
67   Ideal.Quotient.liftₐ squareIdeal (Polynomial.aeval (generator - 1)) (by
68     change squareIdeal ≤ RingHom.ker (Polynomial.aeval (generator - 1)).toRingHom
69     apply Ideal.span_le.mpr
70     rintro _ rfl
71     change (Polynomial.aeval (generator (K := k) - 1)) (Polynomial.X ^ 2) = 0
72     simp [pow_two, augmentation_generator_sq])
73 
74 theorem X_fromDual : fromDual X = generator - 1 := by
75   change (Polynomial.aeval (generator (K := k) - 1)) Polynomial.X = _
76   exact Polynomial.aeval_X _
77 
78 theorem fromDual_comp_toDual : fromDual.comp toDual = AlgHom.id k (MonoidAlgebra k G) := by
79   apply MonoidAlgebra.algHom_ext
80   · intro h
81     rcases group_cases h with rfl | rfl
82     · simp [toDual, cyclicMap, MonoidAlgebra.one_def]
83     · change fromDual (toDual (generator (K := k))) = generator
84       rw [generator_toDual, map_add, map_one, X_fromDual]
85       ring
86   · exact Subsingleton.elim _ _
87 
88 theorem toDual_comp_fromDual : toDual.comp fromDual = AlgHom.id k Dual := by
89   apply Ideal.Quotient.algHom_ext
90   apply Polynomial.algHom_ext
91   change toDual (fromDual X) = X
92   rw [X_fromDual, map_sub, map_one, generator_toDual]
93   ring
94 
95 /-- The residual algebra is exactly the dual-number quotient, via X=g−1. -/
96 noncomputable def dualNumberEquiv : MonoidAlgebra k G ≃ₐ[k] Dual :=
97   AlgEquiv.ofAlgHom toDual fromDual toDual_comp_fromDual fromDual_comp_toDual
98 
99 theorem dualNumberEquiv_generator : dualNumberEquiv (generator (K := k) - 1) = X := by
100   change toDual (generator (K := k) - 1) = X
101   rw [map_sub, map_one, generator_toDual]
102   ring
103 
104 theorem cyclic_is_two_group : IsPGroup 2 G := by
105   intro h
106   refine ⟨1, ?_⟩
107   rcases group_cases h with rfl | rfl <;> simp [pow_two, g_mul_g]
108 
109 theorem groupAlgebra_isLocalRing : IsLocalRing (MonoidAlgebra k G) :=
110   PaperXII.ResidualAugmentation.isLocalRing (k := k) cyclic_is_two_group
111 
112 theorem groupAlgebra_idempotent (e : MonoidAlgebra k G) (he : e * e = e) :
113     e = 0 ∨ e = 1 :=
114   PaperXII.ResidualAugmentation.idempotent_eq_zero_or_one cyclic_is_two_group e he
115 
116 theorem dual_isLocalRing : IsLocalRing Dual := by
117   let := groupAlgebra_isLocalRing
118   exact dualNumberEquiv.toRingEquiv.isLocalRing
119 
120 theorem dual_idempotent (e : Dual) (he : e * e = e) : e = 0 ∨ e = 1 := by
121   let := dual_isLocalRing
122   exact PaperXII.LocalIdempotents.eq_zero_or_one e he
123 
124 end PaperXII.DyadicProjectors.Residual

Back to source controls