CommutatorEnvelope.lean

1 import PaperXI.CocycleQuotient
2 
3 /-! Exact universal properties of the quotient detected by the scalar
4 commutator. A pairing descends through A/L precisely when L lies in its
5 radical; that descended pairing is nondegenerate precisely at the radical. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CommutatorEnvelope
9 open CocycleCommutator
10 
11 variable {A C : Type*} [CommGroup A] [CommGroup C]
12 
13 /-- The character map descends through any subgroup of the radical. -/
14 def descendedCharacter (c : Cocycle A C) (L : Subgroup A) (hL : L ≤ radical c) :
15     (A ⧸ L) →* (A →* C) := QuotientGroup.lift L (characterMap c) hL
16 
17 @[simp] theorem descendedCharacter_mk (c : Cocycle A C) (L : Subgroup A)
18     (hL : L ≤ radical c) (a b : A) :
19     descendedCharacter c L hL (QuotientGroup.mk a) b = commutator c a b := rfl
20 
21 theorem le_descendedCharacter_ker (c : Cocycle A C) (L : Subgroup A)
22     (hL : L ≤ radical c) (z : A ⧸ L) : L ≤ (descendedCharacter c L hL z).ker := by
23   induction z using QuotientGroup.induction_on with | H a =>
24     intro b hb
25     change commutator c a b = 1
26     rw [commutator_swap, (mem_radical_iff c b).1 (hL hb) a, inv_one]
27 
28 /-- The literal commutator pairing on an arbitrary admissible quotient. -/
29 def descendedPairing (c : Cocycle A C) (L : Subgroup A) (hL : L ≤ radical c) :
30     (A ⧸ L) →* ((A ⧸ L) →* C) where
31   toFun z := QuotientGroup.lift L (descendedCharacter c L hL z)
32     (le_descendedCharacter_ker c L hL z)
33   map_one' := by
34     apply MonoidHom.ext
35     intro z
36     induction z using QuotientGroup.induction_on with | H a =>
37       change descendedCharacter c L hL 1 a = 1
38       simp
39   map_mul' x y := by
40     apply MonoidHom.ext
41     intro z
42     induction z using QuotientGroup.induction_on with | H a =>
43       change descendedCharacter c L hL (x * y) a =
44         descendedCharacter c L hL x a * descendedCharacter c L hL y a
45       rw [map_mul]
46       rfl
47 
48 @[simp] theorem descendedPairing_mk (c : Cocycle A C) (L : Subgroup A)
49     (hL : L ≤ radical c) (a b : A) :
50     descendedPairing c L hL (QuotientGroup.mk a) (QuotientGroup.mk b) =
51       commutator c a b := rfl
52 
53 /-- The exact condition for the pairing to descend through both quotient variables. -/
54 theorem descends_iff (c : Cocycle A C) (L : Subgroup A) :
55     (∃ B : (A ⧸ L) →* ((A ⧸ L) →* C),
56       ∀ a b, B (QuotientGroup.mk a) (QuotientGroup.mk b) = commutator c a b) ↔
57       L ≤ radical c := by
58   constructor
59   · rintro ⟨B, hB⟩ a ha
60     apply (mem_radical_iff c a).2
61     intro b
62     rw [← hB, (QuotientGroup.eq_one_iff a).2 ha, map_one]
63     rfl
64   · intro hL
65     exact ⟨descendedPairing c L hL, descendedPairing_mk c L hL⟩
66 
67 /-- The pairing on a specified quotient is uniquely determined on representatives. -/
68 theorem descendedPairing_unique (c : Cocycle A C) (L : Subgroup A)
69     (hL : L ≤ radical c) (B : (A ⧸ L) →* ((A ⧸ L) →* C))
70     (hB : ∀ a b, B (QuotientGroup.mk a) (QuotientGroup.mk b) = commutator c a b) :
71     B = descendedPairing c L hL := by
72   apply MonoidHom.ext
73   intro x
74   apply MonoidHom.ext
75   intro y
76   induction x using QuotientGroup.induction_on with | H a =>
77     induction y using QuotientGroup.induction_on with | H b =>
78       exact hB a b
79 
80 /-- The complete unique-descent statement. -/
81 theorem existsUnique_descendedPairing (c : Cocycle A C) (L : Subgroup A)
82     (hL : L ≤ radical c) :
83     ∃! B : (A ⧸ L) →* ((A ⧸ L) →* C),
84       ∀ a b, B (QuotientGroup.mk a) (QuotientGroup.mk b) = commutator c a b :=
85   ⟨descendedPairing c L hL, descendedPairing_mk c L hL,
86     fun B hB => descendedPairing_unique c L hL B hB⟩
87 
88 /-- The descended pairing is alternating on its actual quotient. -/
89 theorem descendedPairing_self (c : Cocycle A C) (L : Subgroup A)
90     (hL : L ≤ radical c) (z : A ⧸ L) : descendedPairing c L hL z z = 1 := by
91   induction z using QuotientGroup.induction_on with | H a =>
92     exact commutator_self c a
93 
94 /-- Nondegeneracy of the descended pairing is equivalent to quotienting by the full radical. -/
95 theorem nondegenerate_iff (c : Cocycle A C) (L : Subgroup A) (hL : L ≤ radical c) :
96     (∀ x : A ⧸ L, (∀ y, descendedPairing c L hL x y = 1) → x = 1) ↔
97       L = radical c := by
98   constructor
99   · intro h
100     apply le_antisymm hL
101     intro a ha
102     apply (QuotientGroup.eq_one_iff a).1
103     apply h
104     intro y
105     induction y using QuotientGroup.induction_on with | H b =>
106       exact (mem_radical_iff c a).1 ha b
107   · intro h x hx
108     induction x using QuotientGroup.induction_on with | H a =>
109       apply (QuotientGroup.eq_one_iff a).2
110       rw [h]
111       apply (mem_radical_iff c a).2
112       intro b
113       exact hx (QuotientGroup.mk b)
114 
115 /-- Every admissible quotient maps canonically onto the radical quotient. -/
116 def quotientFactor (c : Cocycle A C) (L : Subgroup A) (hL : L ≤ radical c) :
117     (A ⧸ L) →* (A ⧸ radical c) :=
118   QuotientGroup.map L (radical c) (MonoidHom.id A) (by simpa using hL)
119 
120 @[simp] theorem quotientFactor_mk (c : Cocycle A C) (L : Subgroup A)
121     (hL : L ≤ radical c) (a : A) :
122     quotientFactor c L hL (QuotientGroup.mk a) = QuotientGroup.mk a := rfl
123 
124 /-- The canonical comparison is surjective. -/
125 theorem quotientFactor_surjective (c : Cocycle A C) (L : Subgroup A)
126     (hL : L ≤ radical c) : Function.Surjective (quotientFactor c L hL) := by
127   intro y
128   induction y using QuotientGroup.induction_on with | H a =>
129     exact ⟨QuotientGroup.mk a, rfl⟩
130 
131 /-- The comparison preserves the literal descended pairings. -/
132 theorem quotientFactor_pairing (c : Cocycle A C) (L : Subgroup A)
133     (hL : L ≤ radical c) (x y : A ⧸ L) :
134     quotientPairing c (quotientFactor c L hL x) (quotientFactor c L hL y) =
135       descendedPairing c L hL x y := by
136   induction x using QuotientGroup.induction_on with | H a =>
137     induction y using QuotientGroup.induction_on with | H b => rfl
138 
139 /-- The map to the radical quotient is the unique factorization of its quotient map. -/
140 theorem existsUnique_quotientFactor (c : Cocycle A C) (L : Subgroup A)
141     (hL : L ≤ radical c) :
142     ∃! q : (A ⧸ L) →* (A ⧸ radical c),
143       ∀ a, q (QuotientGroup.mk a) = QuotientGroup.mk a := by
144   refine ⟨quotientFactor c L hL, quotientFactor_mk c L hL, ?_⟩
145   intro q hq
146   apply MonoidHom.ext
147   intro x
148   induction x using QuotientGroup.induction_on with | H a => exact hq a
149 
150 /-- The character map factors uniquely and injectively through the radical quotient. -/
151 theorem existsUnique_injective_characterFactor (c : Cocycle A C) :
152     ∃! f : (A ⧸ radical c) →* (A →* C),
153       Function.Injective f ∧ ∀ a, f (QuotientGroup.mk a) = characterMap c a := by
154   refine ⟨quotientCharacter c, ⟨quotientCharacter_injective c, fun _ => rfl⟩, ?_⟩
155   intro f hf
156   apply MonoidHom.ext
157   intro x
158   induction x using QuotientGroup.induction_on with | H a => exact hf.2 a
159 
160 end PaperXI.CommutatorEnvelope

Back to source controls