CentralProductComparison.lean

1 import PaperXI.CentralProductFactors
2 import Mathlib.GroupTheory.NoncommPiCoprod
3 import Mathlib.GroupTheory.NoncommCoprod
4 
5 /-! Actual compatible factor embeddings construct the comparison with a declared
6 full central extension. The desired group isomorphism is derived from exactness. -/
7 set_option autoImplicit false
8 set_option backward.isDefEq.respectTransparency false
9 noncomputable section
10 namespace PaperXI.CentralProductComparison
11 
12 variable {S Z G : Type*} [Fintype S] [DecidableEq S] [CommGroup Z] [Group G]
13 variable {H A : S → Type*} [∀ s, Group (H s)] [∀ s, CommGroup (A s)]
14 variable (D : ∀ s, CentralExtension.Datum Z (H s) (A s))
15 variable (E : CentralExtension.Datum Z G (∀ s, A s))
16 variable (j : ∀ s, H s →* G)
17 variable (hc : Pairwise fun s t => ∀ h k, Commute (j s h) (j t k))
18 variable (hi : ∀ s z, j s ((D s).i z) = E.i z)
19 variable (hq : ∀ s h, E.q (j s h) = Pi.mulSingle s ((D s).q h))
20 
21 /-- The finite commuting product of the actual factor images. -/
22 def factors : (∀ s, H s) →* G := MonoidHom.noncommPiCoprod j hc
23 
24 @[simp] theorem factors_single (s : S) (h : H s) :
25     factors j hc (Pi.mulSingle s h) = j s h :=
26   MonoidHom.noncommPiCoprod_mulSingle j s h
27 
28 include hq in
29 /-- Coordinate projection of the actual factor product is the prescribed tuple. -/
30 theorem factors_projection (h : ∀ s, H s) :
31     E.q (factors j hc h) = fun s => (D s).q (h s) := by
32   have he : E.q.comp (factors j hc) = MonoidHom.pi (fun s => (D s).q.comp
33       (Pi.evalMonoidHom H s)) := by
34     apply MonoidHom.pi_ext
35     intro s x
36     change E.q (factors j hc (Pi.mulSingle s x)) = fun t => (D t).q (Pi.mulSingle s x t)
37     rw [factors_single, hq]
38     ext t
39     by_cases ht : t = s
40     · subst t; simp
41     · simp [Pi.mulSingle_eq_of_ne ht]
42   exact DFunLike.congr_fun he h
43 
44 /-- Product of the central coordinates as a homomorphism. -/
45 def centerProduct : (S → Z) →* Z where
46   toFun z := ∏ s, z s
47   map_one' := by simp
48   map_mul' x y := by simp [Finset.prod_mul_distrib]
49 
50 include hi in
51 /-- The factor centers multiply in the single declared total center. -/
52 theorem factors_centers (z : S → Z) :
53     factors j hc (fun s => (D s).i (z s)) = E.i (∏ s, z s) := by
54   have he : (factors j hc).comp (MonoidHom.pi (fun s => (D s).i.comp
55       (Pi.evalMonoidHom (fun _ : S => Z) s))) = E.i.comp (centerProduct (S := S)) := by
56     apply MonoidHom.pi_ext
57     intro s x
58     have ht : (fun t => (D t).i (Pi.mulSingle (M := fun _ : S => Z) s x t)) =
59         Pi.mulSingle s ((D s).i x) := by
60       funext t
61       by_cases hts : t = s
62       · subst t; simp
63       · simp [Pi.mulSingle_eq_of_ne hts]
64     change factors j hc (fun t => (D t).i (Pi.mulSingle (M := fun _ : S => Z) s x t)) =
65       E.i (centerProduct (Pi.mulSingle s x))
66     rw [ht, factors_single, hi]
67     congr 1
68     simp [centerProduct]
69   exact DFunLike.congr_fun he z
70 
71 /-- Actual ambient map, retaining the center also in the empty family. -/
72 def ambient : CentralProduct.Ambient (Z := Z) (H := H) →* G :=
73   E.i.noncommCoprod (factors j hc) (fun z h => E.central z (factors j hc h))
74 
75 omit [DecidableEq S] in
76 @[simp] theorem ambient_apply (z : Z) (h : ∀ s, H s) :
77     ambient E j hc (z,h) = E.i z * factors j hc h := rfl
78 
79 include hi in
80 /-- The balancing relations vanish, by compatibility of the actual central inclusions. -/
81 theorem ambient_balanced (z : S → Z) :
82     ambient E j hc (CentralProduct.balanced D z) = 1 := by
83   change E.i ((∏ s, z s)⁻¹) * factors j hc (fun s => (D s).i (z s)) = 1
84   rw [factors_centers D E j hc hi, ← map_mul, inv_mul_cancel, map_one]
85 
86 /-- The comparison descends through the actual quotient. -/
87 def comparison : CentralProduct.Group D →* G :=
88   CentralProduct.descend D (ambient E j hc) (ambient_balanced D E j hc hi)
89 
90 @[simp] theorem comparison_mk (z : Z) (h : ∀ s, H s) :
91     comparison D E j hc hi (CentralProduct.mk D (z,h)) = E.i z * factors j hc h := rfl
92 
93 @[simp] theorem comparison_center (z : Z) :
94     comparison D E j hc hi (CentralProduct.center D z) = E.i z := by
95   simp [CentralProduct.center_apply]
96 
97 include hq in
98 /-- The comparison induces the identity on the actual quotient coordinates. -/
99 theorem comparison_projection (x : CentralProduct.Group D) :
100     E.q (comparison D E j hc hi x) = CentralProduct.projection D x := by
101   obtain ⟨⟨z,h⟩, rfl⟩ := CentralProduct.mk_surjective D x
102   simp only [comparison_mk, map_mul, CentralExtension.q_i, one_mul,
103     CentralProduct.projection_mk]
104   exact factors_projection D E j hc hq h
105 
106 include hq in
107 /-- Exactness on both sides proves injectivity, without a dimension surrogate. -/
108 theorem comparison_injective : Function.Injective (comparison D E j hc hi) := by
109   apply (MonoidHom.ker_eq_bot_iff _).mp
110   rw [Subgroup.eq_bot_iff_forall]
111   intro x hx
112   change comparison D E j hc hi x = 1 at hx
113   have hxq : CentralProduct.projection D x = 1 := by
114     rw [← comparison_projection D E j hc hi hq, hx, map_one]
115   have hm : x ∈ (CentralProduct.center D).range := by
116     rw [CentralProduct.range_center_eq_ker_projection]
117     exact hxq
118   obtain ⟨z, rfl⟩ := hm
119   have hz : z = 1 := by
120     apply E.i_injective
121     simpa only [comparison_center, map_one] using hx
122   rw [hz, map_one]
123 
124 include hq in
125 /-- Surjectivity follows by matching quotient coordinates and correcting the central difference. -/
126 theorem comparison_surjective : Function.Surjective (comparison D E j hc hi) := by
127   intro g
128   obtain ⟨x, hx⟩ := CentralProduct.projection_surjective D (E.q g)
129   have hk : g * (comparison D E j hc hi x)⁻¹ ∈ E.q.ker := by
130     change E.q (g * (comparison D E j hc hi x)⁻¹) = 1
131     rw [map_mul, map_inv, comparison_projection D E j hc hi hq, hx, mul_inv_cancel]
132   rw [← E.range_i_eq_ker_q] at hk
133   obtain ⟨z, hz⟩ := hk
134   refine ⟨CentralProduct.center D z * x, ?_⟩
135   rw [map_mul, comparison_center, hz, inv_mul_cancel_right]
136 
137 /-- Actual full-envelope group comparison from compatible factor embeddings. -/
138 def equiv : CentralProduct.Group D ≃* G :=
139   MulEquiv.ofBijective (comparison D E j hc hi)
140     ⟨comparison_injective D E j hc hi hq, comparison_surjective D E j hc hi hq⟩
141 
142 @[simp] theorem equiv_center (z : Z) :
143     equiv D E j hc hi hq (CentralProduct.center D z) = E.i z :=
144   comparison_center D E j hc hi z
145 
146 @[simp] theorem equiv_mk (z : Z) (h : ∀ s, H s) :
147     equiv D E j hc hi hq (CentralProduct.mk D (z,h)) = E.i z * factors j hc h := rfl
148 
149 end PaperXI.CentralProductComparison

Back to source controls