CocycleQuotient.lean

1 import PaperXI.CocycleCommutator
2 
3 /-! Paper XI, Proposition 8.2: the actual quotient by the commutator radical. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.CocycleCommutator
7 
8 variable {A C : Type*} [CommGroup A] [CommGroup C]
9 
10 /-- First descent: characters indexed by the actual radical quotient. -/
11 def quotientCharacter (c : Cocycle A C) : A ⧸ radical c →* (A →* C) :=
12   QuotientGroup.kerLift (characterMap c)
13 
14 @[simp] theorem quotientCharacter_mk (c : Cocycle A C) (a b : A) :
15     quotientCharacter c (QuotientGroup.mk a) b = commutator c a b := rfl
16 
17 theorem radical_le_quotientCharacter_ker (c : Cocycle A C)
18     (z : A ⧸ radical c) : radical c ≤ (quotientCharacter c z).ker := by
19   induction z using QuotientGroup.induction_on with | H a =>
20     intro b hb
21     change commutator c a b = 1
22     rw [commutator_swap, (mem_radical_iff c b).mp hb a, inv_one]
23 
24 /-- The commutator descends in both variables to the radical quotient. -/
25 def quotientPairing (c : Cocycle A C) :
26     (A ⧸ radical c) →* ((A ⧸ radical c) →* C) where
27   toFun z := QuotientGroup.lift (radical c) (quotientCharacter c z)
28     (radical_le_quotientCharacter_ker c z)
29   map_one' := by
30     apply MonoidHom.ext
31     intro z
32     induction z using QuotientGroup.induction_on with | H a =>
33       change quotientCharacter c 1 a = 1
34       simp
35   map_mul' x y := by
36     apply MonoidHom.ext
37     intro z
38     induction z using QuotientGroup.induction_on with | H a =>
39       change quotientCharacter c (x * y) a = quotientCharacter c x a * quotientCharacter c y a
40       rw [map_mul]
41       rfl
42 
43 @[simp] theorem quotientPairing_mk (c : Cocycle A C) (a b : A) :
44     quotientPairing c (QuotientGroup.mk a) (QuotientGroup.mk b) = commutator c a b := rfl
45 
46 /-- Alternation is inherited by the descended pairing. -/
47 theorem quotientPairing_self (c : Cocycle A C) (z : A ⧸ radical c) :
48     quotientPairing c z z = 1 := by
49   induction z using QuotientGroup.induction_on with | H a =>
50     exact commutator_self c a
51 
52 theorem quotientPairing_swap (c : Cocycle A C) (x y : A ⧸ radical c) :
53     quotientPairing c y x = (quotientPairing c x y)⁻¹ := by
54   induction x using QuotientGroup.induction_on with | H a =>
55     induction y using QuotientGroup.induction_on with | H b =>
56       exact commutator_swap c a b
57 
58 /-- The quotient pairing has trivial left radical, proved from the quotient
59 relation and the original cocycle rather than assumed as data. -/
60 theorem quotientPairing_nondegenerate_left (c : Cocycle A C) (z : A ⧸ radical c) :
61     (∀ w, quotientPairing c z w = 1) ↔ z = 1 := by
62   induction z using QuotientGroup.induction_on with | H a =>
63     constructor
64     · intro h
65       apply (QuotientGroup.eq_one_iff a).2
66       apply (mem_radical_iff c a).2
67       intro b
68       exact h (QuotientGroup.mk b)
69     · intro h w
70       rw [h, map_one]
71       rfl
72 
73 /-- The quotient pairing also has trivial right radical. -/
74 theorem quotientPairing_nondegenerate_right (c : Cocycle A C) (z : A ⧸ radical c) :
75     (∀ w, quotientPairing c w z = 1) ↔ z = 1 := by
76   rw [← quotientPairing_nondegenerate_left c z]
77   constructor <;> intro h w
78   · rw [quotientPairing_swap, h, inv_one]
79   · rw [quotientPairing_swap, h, inv_one]
80 
81 /-- Nondegeneracy can equivalently be read as injectivity into the character group. -/
82 theorem quotientCharacter_injective (c : Cocycle A C) :
83     Function.Injective (quotientCharacter c) := QuotientGroup.kerLift_injective _
84 
85 end PaperXI.CocycleCommutator

Back to source controls