CentralExtensionStructure.lean

1 import PaperXI.CentralExtensionCocycle
2 import Mathlib.GroupTheory.Subgroup.Center
3 import Mathlib.SetTheory.Cardinal.Finite
4 
5 /-! Coordinates, cardinality, and intrinsic scalar nondegeneracy of an actual
6 central extension. Faithfulness is an explicit hypothesis when a central-valued
7 nondegeneracy statement is transported through a central character. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.CentralExtension
11 
12 open CocycleCommutator
13 variable {Z H A : Type*} [CommGroup Z] [Group H] [CommGroup A]
14 variable (D : Datum Z H A)
15 
16 /-- The actual normal-coordinate equivalence of underlying types. -/
17 def coordinates : H ≃ Z × A where
18   toFun h := (coordinate D h, D.q h)
19   invFun p := D.i p.1 * sectionMap D p.2
20   left_inv h := (normal_form D h).symm
21   right_inv p := by
22     apply Prod.ext
23     · exact coordinate_eq_of_eq D _ _ _ rfl
24     · simp
25 
26 @[simp] theorem coordinates_apply (h : H) :
27     coordinates D h = (coordinate D h, D.q h) := rfl
28 
29 @[simp] theorem coordinates_symm_apply (z : Z) (a : A) :
30     (coordinates D).symm (z, a) = D.i z * sectionMap D a := rfl
31 
32 include D in
33 theorem finite_middle [Finite Z] [Finite A] : Finite H :=
34   Finite.of_injective (coordinates D) (coordinates D).injective
35 
36 include D in
37 /-- The order of the middle group is the product of kernel and quotient orders. -/
38 theorem natCard_eq : Nat.card H = Nat.card Z * Nat.card A := by
39   rw [Nat.card_congr (coordinates D), Nat.card_prod]
40 
41 include D in
42 theorem card_eq [Fintype H] [Fintype Z] [Fintype A] :
43     Fintype.card H = Fintype.card Z * Fintype.card A := by
44   simpa only [Fintype.card_prod] using Fintype.card_congr (coordinates D)
45 
46 /-- Scalar nondegeneracy can be stated intrinsically on all actual group lifts,
47 without referring to the chosen quotient section. -/
48 theorem radical_scalarCocycle_eq_bot_iff (ζ : Z →* ℂˣ) :
49     radical (scalarCocycle D ζ) = ⊥ ↔
50       ∀ h : H, (∀ k : H, ζ (centralCommutator D h k) = 1) → D.q h = 1 := by
51   rw [Subgroup.eq_bot_iff_forall]
52   constructor
53   · intro hnd h hh
54     apply hnd (D.q h)
55     rw [mem_radical_iff]
56     intro a
57     obtain ⟨k, rfl⟩ := D.q_surjective a
58     rw [scalar_commutator]
59     exact hh k
60   · intro hnd a ha
61     obtain ⟨h, rfl⟩ := D.q_surjective a
62     apply hnd h
63     intro k
64     rw [← scalar_commutator]
65     exact (mem_radical_iff _ _).mp ha (D.q k)
66 
67 /-- A faithful central character carries intrinsic central nondegeneracy to
68 scalar nondegeneracy. Faithfulness cannot be replaced by mere nontriviality. -/
69 theorem radical_scalarCocycle_eq_bot_of_faithful (ζ : Z →* ℂˣ)
70     (hζ : Function.Injective ζ)
71     (hcentral : ∀ h : H, (∀ k : H, centralCommutator D h k = 1) → D.q h = 1) :
72     radical (scalarCocycle D ζ) = ⊥ := by
73   apply (radical_scalarCocycle_eq_bot_iff D ζ).2
74   intro h hh
75   apply hcentral h
76   intro k
77   apply hζ
78   simpa only [map_one] using hh k
79 
80 /-- For a faithful character the scalar and central cocycle radicals coincide. -/
81 theorem radical_scalarCocycle_of_injective (ζ : Z →* ℂˣ)
82     (hζ : Function.Injective ζ) :
83     radical (scalarCocycle D ζ) = radical (centralCocycle D) := by
84   ext a
85   rw [mem_radical_iff, mem_radical_iff]
86   constructor
87   · intro h b
88     apply hζ
89     simpa only [CocycleCommutator.commutator, scalarCocycle_coeff,
90       centralCocycle, map_div, map_one] using h b
91   · intro h b
92     simpa only [CocycleCommutator.commutator, scalarCocycle_coeff,
93       centralCocycle, map_div, map_one] using congrArg ζ (h b)
94 
95 theorem radical_scalarCocycle_eq_bot_of_central (ζ : Z →* ℂˣ)
96     (hζ : Function.Injective ζ) (hcentral : radical (centralCocycle D) = ⊥) :
97     radical (scalarCocycle D ζ) = ⊥ := by
98   rw [radical_scalarCocycle_of_injective D ζ hζ, hcentral]
99 
100 /-- Scalar nondegeneracy forces the distinguished central subgroup to be the
101 full center of the actual middle group. -/
102 theorem center_eq_range (ζ : Z →* ℂˣ)
103     (hnd : radical (scalarCocycle D ζ) = ⊥) : Subgroup.center H = D.i.range := by
104   apply le_antisymm
105   · intro h hh
106     rw [D.range_i_eq_ker_q]
107     apply (radical_scalarCocycle_eq_bot_iff D ζ).1 hnd h
108     intro k
109     have hc : centralCommutator D h k = 1 := by
110       apply D.i_injective
111       rw [i_centralCommutator, map_one, ← (Subgroup.mem_center_iff.mp hh k)]
112       group
113     simp only [hc, map_one]
114   · rintro _ ⟨z, rfl⟩
115     exact Subgroup.mem_center_iff.mpr (fun h => (D.central z h).symm)
116 
117 end PaperXI.CentralExtension

Back to source controls