CentralProduct.lean

1 import PaperXI.CentralExtension
2 import Mathlib.GroupTheory.QuotientGroup.Basic
3 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
4 
5 /-! The finite central product, with an explicit central factor so that the empty
6 family has the correct tensor-unit center. The group is an actual quotient. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.CentralProduct
10 
11 variable {S Z : Type*} [Fintype S] [CommGroup Z]
12 variable {H A : S → Type*} [∀ s, _root_.Group (H s)] [∀ s, CommGroup (A s)]
13 variable (D : ∀ s, CentralExtension.Datum Z (H s) (A s))
14 
15 abbrev Ambient := Z × (∀ s, H s)
16 
17 /-- The balancing relation identifies each factor center with the retained center. -/
18 def balanced : (S → Z) →* Ambient (Z := Z) (H := H) where
19   toFun z := ((∏ s, z s)⁻¹, fun s => (D s).i (z s))
20   map_one' := by ext <;> simp
21   map_mul' x y := by ext <;> simp [Finset.prod_mul_distrib, mul_comm]
22 
23 def relation : Subgroup (Ambient (Z := Z) (H := H)) := (balanced D).range
24 
25 theorem balanced_central (z : S → Z) (x : Ambient (Z := Z) (H := H)) :
26     balanced D z * x = x * balanced D z := by
27   apply Prod.ext
28   · exact mul_comm _ _
29   · funext s
30     exact (D s).central (z s) (x.2 s)
31 
32 instance relation_normal : (relation D).Normal where
33   conj_mem n hn g := by
34     obtain ⟨z, rfl⟩ := hn
35     refine ⟨z, ?_⟩
36     rw [← balanced_central D z g, mul_inv_cancel_right]
37 
38 /-- The central product of the finite family, including an empty family. -/
39 def Group := Ambient (Z := Z) (H := H) ⧸ relation D
40 
41 instance : _root_.Group (Group D) := inferInstanceAs (_root_.Group (_ ⧸ relation D))
42 
43 def mk : Ambient (Z := Z) (H := H) →* Group D := QuotientGroup.mk' (relation D)
44 
45 theorem mk_surjective : Function.Surjective (mk D) := QuotientGroup.mk'_surjective _
46 
47 @[simp] theorem mk_balanced (z : S → Z) : mk D (balanced D z) = 1 :=
48   (QuotientGroup.eq_one_iff _).2 ⟨z, rfl⟩
49 
50 def center : Z →* Group D := (mk D).comp (MonoidHom.inl Z (∀ s, H s))
51 
52 @[simp] theorem center_apply (z : Z) : center D z = mk D (z, 1) := rfl
53 
54 theorem center_injective : Function.Injective (center D) := by
55   apply (MonoidHom.ker_eq_bot_iff _).mp
56   apply le_antisymm
57   · intro z hz
58     change z = 1
59     have hz' : (z, (1 : ∀ s, H s)) ∈ relation D :=
60       (QuotientGroup.eq_one_iff _).1 hz
61     obtain ⟨w, hw⟩ := hz'
62     have hw1 : w = 1 := by
63       funext s
64       apply (D s).i_injective
65       simpa [balanced] using congr_fun (congr_arg Prod.snd hw) s
66     simpa [hw1, balanced] using (congr_arg Prod.fst hw).symm
67   · exact bot_le
68 
69 def ambientProjection : Ambient (Z := Z) (H := H) →* (∀ s, A s) where
70   toFun x s := (D s).q (x.2 s)
71   map_one' := by ext s; simp
72   map_mul' x y := by ext s; simp
73 
74 theorem relation_le_ker_projection : relation D ≤ (ambientProjection D).ker := by
75   rintro x ⟨z, rfl⟩
76   ext s
77   exact CentralExtension.q_i (D s) (z s)
78 
79 def projection : Group D →* (∀ s, A s) :=
80   QuotientGroup.lift (relation D) (ambientProjection D) (relation_le_ker_projection D)
81 
82 @[simp] theorem projection_mk (x : Ambient (Z := Z) (H := H)) :
83     projection D (mk D x) = fun s => (D s).q (x.2 s) := rfl
84 
85 @[simp] theorem projection_center (z : Z) : projection D (center D z) = 1 := by
86   ext s
87   simp [center_apply]
88 
89 theorem projection_surjective : Function.Surjective (projection D) := by
90   intro a
91   refine ⟨mk D (1, fun s => CentralExtension.sectionMap (D s) (a s)), ?_⟩
92   ext s
93   exact CentralExtension.q_section (D s) (a s)
94 
95 /-- All factor-center tuples collapse to their product in the one retained center. -/
96 theorem mk_centers (z : Z) (w : S → Z) :
97     mk D (z, fun s => (D s).i (w s)) = center D (z * ∏ s, w s) := by
98   have h : (z, fun s => (D s).i (w s)) =
99       (z * ∏ s, w s, (1 : ∀ s, H s)) * balanced D w := by
100     apply Prod.ext
101     · simp [balanced, mul_assoc]
102     · simp [balanced]
103   rw [h, map_mul, mk_balanced, mul_one, center_apply]
104 
105 theorem range_center_eq_ker_projection : (center D).range = (projection D).ker := by
106   apply le_antisymm
107   · rintro x ⟨z, rfl⟩
108     exact projection_center D z
109   · intro x hx
110     obtain ⟨⟨z, h⟩, rfl⟩ := mk_surjective D x
111     have hh : ∀ s, ∃ w, (D s).i w = h s := by
112       intro s
113       have hs : h s ∈ (D s).q.ker := congr_fun hx s
114       rw [← (D s).range_i_eq_ker_q] at hs
115       exact hs
116     choose w hw using hh
117     refine ⟨z * ∏ s, w s, ?_⟩
118     rw [← mk_centers D z w]
119     congr 1
120     exact Prod.ext rfl (funext hw)
121 
122 theorem center_commutes (z : Z) (x : Group D) :
123     center D z * x = x * center D z := by
124   obtain ⟨x, rfl⟩ := mk_surjective D x
125   rw [center_apply, ← map_mul, ← map_mul]
126   congr 1
127   apply Prod.ext
128   · exact mul_comm _ _
129   · simp
130 
131 def datum : CentralExtension.Datum Z (Group D) (∀ s, A s) where
132   i := center D
133   q := projection D
134   i_injective := center_injective D
135   q_surjective := projection_surjective D
136   range_i_eq_ker_q := range_center_eq_ker_projection D
137   central := center_commutes D
138 
139 @[simp] theorem datum_i (z : Z) : (datum D).i z = center D z := rfl
140 
141 @[simp] theorem datum_q (x : Group D) : (datum D).q x = projection D x := rfl
142 
143 /-- Universal descent of an actual ambient homomorphism killing the balances. -/
144 def descend {G : Type*} [Monoid G] (f : Ambient (Z := Z) (H := H) →* G)
145     (hf : ∀ z : S → Z, f (balanced D z) = 1) : Group D →* G :=
146   QuotientGroup.lift (relation D) f (by rintro x ⟨z, rfl⟩; exact hf z)
147 
148 @[simp] theorem descend_mk {G : Type*} [Monoid G]
149     (f : Ambient (Z := Z) (H := H) →* G)
150     (hf : ∀ z : S → Z, f (balanced D z) = 1)
151     (x : Ambient (Z := Z) (H := H)) : descend D f hf (mk D x) = f x := rfl
152 
153 theorem hom_ext {G : Type*} [Monoid G] {f g : Group D →* G}
154     (h : f.comp (mk D) = g.comp (mk D)) : f = g := by
155   ext x
156   obtain ⟨x, rfl⟩ := mk_surjective D x
157   exact DFunLike.congr_fun h x
158 
159 end PaperXI.CentralProduct

Back to source controls