CentralProductCommutator.lean

1 import PaperXI.CentralProduct
2 import PaperXI.CentralExtensionStructure
3 import Mathlib.Algebra.Group.Pi.Lemmas
4 
5 /-! The actual quotient commutator is the product of the factor commutators.
6 Scalar nondegeneracy is inherited without assuming a faithful central character. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.CentralProduct
10 
11 open CentralExtension CocycleCommutator
12 variable {S Z : Type*} [Fintype S] [CommGroup Z]
13 variable {H A : S → Type*} [∀ s, _root_.Group (H s)] [∀ s, CommGroup (A s)]
14 variable (D : ∀ s, CentralExtension.Datum Z (H s) (A s))
15 
16 theorem commutator_mk (x y : Ambient (Z := Z) (H := H)) :
17     centralCommutator (datum D) (mk D x) (mk D y) =
18       ∏ s, centralCommutator (D s) (x.2 s) (y.2 s) := by
19   apply (datum D).i_injective
20   rw [i_centralCommutator, datum_i, ← map_inv, ← map_inv,
21     ← map_mul, ← map_mul, ← map_mul]
22   have h : x * y * x⁻¹ * y⁻¹ = (1,
23       fun s => (D s).i (centralCommutator (D s) (x.2 s) (y.2 s))) := by
24     apply Prod.ext
25     · change x.1 * y.1 * x.1⁻¹ * y.1⁻¹ = 1
26       simp [mul_assoc]
27     · funext s
28       exact (i_centralCommutator (D s) _ _).symm
29   rw [h, mk_centers, one_mul]
30 
31 /-- The scalar commutator on the actual product quotient factors componentwise. -/
32 theorem scalar_commutator_product (ζ : Z →* ℂˣ) (a b : ∀ s, A s) :
33     commutator (scalarCocycle (datum D) ζ) a b =
34       ∏ s, commutator (scalarCocycle (D s) ζ) (a s) (b s) := by
35   let x : Ambient (Z := Z) (H := H) :=
36     (1, fun s => sectionMap (D s) (a s))
37   let y : Ambient (Z := Z) (H := H) :=
38     (1, fun s => sectionMap (D s) (b s))
39   have hx : (datum D).q (mk D x) = a := by ext s; simp [x]
40   have hy : (datum D).q (mk D y) = b := by ext s; simp [y]
41   rw [← hx, ← hy, scalar_commutator, commutator_mk, map_prod]
42   apply Finset.prod_congr rfl
43   intro s _
44   simpa [x, y] using (scalar_commutator (D s) ζ (sectionMap (D s) (a s))
45     (sectionMap (D s) (b s))).symm
46 
47 /-- Test each coordinate with a single supported quotient element. -/
48 theorem radical_eq_bot (ζ : Z →* ℂˣ)
49     (hnd : ∀ s, radical (scalarCocycle (D s) ζ) = ⊥) :
50     radical (scalarCocycle (datum D) ζ) = ⊥ := by
51   classical
52   rw [Subgroup.eq_bot_iff_forall]
53   intro a ha
54   funext s
55   apply ((Subgroup.eq_bot_iff_forall _).mp (hnd s))
56   rw [mem_radical_iff]
57   intro b
58   have hh := (mem_radical_iff _ _).mp ha (Pi.mulSingle s b)
59   rw [scalar_commutator_product] at hh
60   rw [Finset.prod_eq_single s] at hh
61   · simpa using hh
62   · intro t _ hts
63     simp [Pi.mulSingle_eq_of_ne hts]
64   · simp
65 
66 /-- The full center is exactly the common retained center under the same hypothesis. -/
67 theorem full_center (ζ : Z →* ℂˣ)
68     (hnd : ∀ s, radical (scalarCocycle (D s) ζ) = ⊥) :
69     Subgroup.center (Group D) = (center D).range :=
70   CentralExtension.center_eq_range (datum D) ζ (radical_eq_bot D ζ hnd)
71 
72 end PaperXI.CentralProduct

Back to source controls