CentralProductFactors.lean

1 import PaperXI.CentralProduct
2 import Mathlib.Algebra.Group.Pi.Lemmas
3 
4 /-! The factor injections and the empty-family center of the actual finite central product. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.CentralProduct
8 
9 variable {S Z : Type*} [Fintype S] [DecidableEq S] [CommGroup Z]
10 variable {H A : S → Type*} [∀ s, _root_.Group (H s)] [∀ s, CommGroup (A s)]
11 variable (D : ∀ s, CentralExtension.Datum Z (H s) (A s))
12 
13 def factor (s : S) : H s →* Group D :=
14   (mk D).comp ((MonoidHom.inr Z (∀ s, H s)).comp (MonoidHom.mulSingle H s))
15 
16 @[simp] theorem factor_apply (s : S) (h : H s) :
17     factor D s h = mk D (1, Pi.mulSingle s h) := by
18   rfl
19 
20 @[simp] theorem projection_factor (s : S) (h : H s) :
21     projection D (factor D s h) = Pi.mulSingle s ((D s).q h) := by
22   rw [factor_apply, projection_mk]
23   ext t
24   by_cases hst : s = t
25   · subst t; simp
26   · simp [Pi.mulSingle_eq_of_ne (Ne.symm hst)]
27 
28 @[simp] theorem factor_center (s : S) (z : Z) :
29     factor D s ((D s).i z) = center D z := by
30   have hw : (fun t => (D t).i (Pi.mulSingle (M := fun _ : S => Z) s z t)) = Pi.mulSingle s ((D s).i z) := by
31     funext t
32     by_cases hst : s = t
33     · subst t; simp
34     · simp [Pi.mulSingle_eq_of_ne (Ne.symm hst)]
35   rw [factor_apply, ← hw, mk_centers]
36   congr 1
37   rw [Finset.prod_eq_single s]
38   · simp
39   · intro t _ hts
40     exact Pi.mulSingle_eq_of_ne (M := fun _ : S => Z) hts z
41   · simp
42 
43 theorem factor_injective (s : S) : Function.Injective (factor D s) := by
44   apply (MonoidHom.ker_eq_bot_iff _).mp
45   rw [Subgroup.eq_bot_iff_forall]
46   intro h hh
47   have hq : (D s).q h = 1 := by
48     have heq := congrArg (fun x => projection D x s) hh
49     simpa using heq
50   have hi : h ∈ (D s).i.range := by
51     rw [(D s).range_i_eq_ker_q]
52     exact hq
53   obtain ⟨z, rfl⟩ := hi
54   have hz : z = 1 := by
55     apply center_injective D
56     change factor D s ((D s).i z) = 1 at hh
57     rw [factor_center] at hh
58     simpa only [map_one] using hh
59   simp [hz]
60 
61 theorem factor_commute (s t : S) (hst : s ≠ t) (h : H s) (k : H t) :
62     Commute (factor D s h) (factor D t k) := by
63   have hcomm : Commute (Pi.mulSingle s h) (Pi.mulSingle t k) :=
64     Pi.mulSingle_commute hst h k
65   have hcomm' : Commute ((1 : Z), Pi.mulSingle s h) (1, Pi.mulSingle t k) := by
66     exact Prod.ext (by simp) hcomm.eq
67   change factor D s h * factor D t k = factor D t k * factor D s h
68   rw [factor_apply, factor_apply, ← map_mul, ← map_mul]
69   exact congrArg (mk D) hcomm'.eq
70 
71 omit [DecidableEq S] in
72 theorem center_surjective_of_isEmpty [IsEmpty S] : Function.Surjective (center D) := by
73   intro x
74   have hq : projection D x = 1 := Subsingleton.elim _ _
75   have hx : x ∈ (center D).range := by
76     rw [range_center_eq_ker_projection]
77     exact hq
78   exact hx
79 
80 /-- An empty family retains exactly one copy of the central group. -/
81 def emptyEquiv [IsEmpty S] : Group D ≃* Z :=
82   (MulEquiv.ofBijective (center D)
83     ⟨center_injective D, center_surjective_of_isEmpty D⟩).symm
84 
85 omit [DecidableEq S] in
86 @[simp] theorem emptyEquiv_center [IsEmpty S] (z : Z) :
87     emptyEquiv D (center D z) = z := (emptyEquiv D).apply_symm_apply z
88 
89 end PaperXI.CentralProduct

Back to source controls