CocycleClass.lean

1 import PaperXI.CocycleCommutator
2 
3 /-! The explicit quotient of normalized cocycles by normalized scalar coboundaries.
4 This is a concrete cohomological-class model; no identification with a separate
5 Mathlib group-cohomology construction is assumed. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CocycleClass
9 
10 open CocycleCommutator
11 variable {A B C : Type*} [CommGroup A] [CommGroup B] [CommGroup C]
12 
13 /-- Equality of actual cocycle coefficients determines the cocycle. -/
14 theorem cocycle_ext {c d : Cocycle A C} (h : ∀ a b, c.coeff a b = d.coeff a b) : c = d := by
15   cases c
16   cases d
17   congr
18   funext a b
19   exact h a b
20 
21 @[simp] theorem rescale_one (c : Cocycle A C) : rescale c (fun _ => 1) = c := by
22   apply cocycle_ext
23   intro a b
24   simp [rescale]
25 
26 /-- Successive scalar changes multiply their actual cochains. -/
27 theorem rescale_trans (c : Cocycle A C) (s t : A → C) :
28     rescale (rescale c s) t = rescale c (fun a => s a * t a) := by
29   apply cocycle_ext
30   intro a b
31   simp [rescale, div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm]
32 
33 /-- Normalized cocycles, retaining the actual multiplication coefficients. -/
34 abbrev NormalizedCocycle (A C : Type*) [CommGroup A] [CommGroup C] :=
35   {c : Cocycle A C // Normalized c}
36 
37 /-- An explicit normalized cochain relates the second cocycle to the first. -/
38 def Related (c d : NormalizedCocycle A C) : Prop :=
39   ∃ s : A → C, s 1 = 1 ∧ d.val = rescale c.val s
40 
41 theorem related_refl (c : NormalizedCocycle A C) : Related c c :=
42   ⟨fun _ => 1, rfl, (rescale_one c.val).symm⟩
43 
44 theorem related_symm {c d : NormalizedCocycle A C} (h : Related c d) : Related d c := by
45   obtain ⟨s, hs, hd⟩ := h
46   refine ⟨fun a => (s a)⁻¹, by simp [hs], ?_⟩
47   rw [hd, rescale_trans]
48   simp
49 
50 theorem related_trans {c d e : NormalizedCocycle A C}
51     (hcd : Related c d) (hde : Related d e) : Related c e := by
52   obtain ⟨s, hs, hd⟩ := hcd
53   obtain ⟨t, ht, he⟩ := hde
54   refine ⟨fun a => s a * t a, by simp [hs, ht], ?_⟩
55   rw [he, hd, rescale_trans]
56 
57 /-- The equivalence relation is proved directly from scalar changes. -/
58 def coboundarySetoid (A C : Type*) [CommGroup A] [CommGroup C] :
59     Setoid (NormalizedCocycle A C) where
60   r := Related
61   iseqv := ⟨related_refl, related_symm, related_trans⟩
62 
63 /-- The concrete normalized-cocycle class space. -/
64 def Class (A C : Type*) [CommGroup A] [CommGroup C] := Quotient (coboundarySetoid A C)
65 
66 /-- The class of the actual normalized cocycle. -/
67 def of (c : Cocycle A C) (hc : Normalized c) : Class A C :=
68   Quotient.mk (coboundarySetoid A C) ⟨c, hc⟩
69 
70 /-- Class equality is exactly the existence of an explicit normalized coboundary. -/
71 theorem of_eq_iff (c d : Cocycle A C) (hc : Normalized c) (hd : Normalized d) :
72     of c hc = of d hd ↔ ∃ s : A → C, s 1 = 1 ∧ d = rescale c s :=
73   Quotient.eq
74 
75 /-- A proved rescaling identity gives equality of the actual cocycle classes. -/
76 theorem of_eq_of_rescale (c d : Cocycle A C) (hc : Normalized c) (hd : Normalized d)
77     (s : A → C) (hs : s 1 = 1) (h : d = rescale c s) : of c hc = of d hd :=
78   (of_eq_iff c d hc hd).mpr ⟨s, hs, h⟩
79 
80 @[simp] theorem of_rescale (c : Cocycle A C) (hc : Normalized c)
81     (s : A → C) (hs : s 1 = 1) :
82     of (rescale c s) (normalized_rescale c hc s hs) = of c hc :=
83   (of_eq_of_rescale c (rescale c s) hc (normalized_rescale c hc s hs) s hs rfl).symm
84 
85 /-- The alternating commutator descends to actual cocycle classes. -/
86 def commutator : Class A C → A → A → C :=
87   Quotient.lift (fun c : NormalizedCocycle A C => CocycleCommutator.commutator c.val)
88     (by
89       intro c d h
90       obtain ⟨s, _, hd⟩ := h
91       rw [hd]
92       funext a b
93       exact (commutator_rescale c.val s a b).symm)
94 
95 @[simp] theorem commutator_of (c : Cocycle A C) (hc : Normalized c) (a b : A) :
96     commutator (of c hc) a b = CocycleCommutator.commutator c a b := rfl
97 
98 /-- The radical subgroup is independent of the chosen representative. -/
99 def radical : Class A C → Subgroup A :=
100   Quotient.lift (fun c : NormalizedCocycle A C => CocycleCommutator.radical c.val)
101     (by
102       intro c d h
103       obtain ⟨s, _, hd⟩ := h
104       rw [hd]
105       exact (radical_rescale c.val s).symm)
106 
107 @[simp] theorem radical_of (c : Cocycle A C) (hc : Normalized c) :
108     radical (of c hc) = CocycleCommutator.radical c := rfl
109 
110 /-- Pull back the actual coefficient function along an index-group homomorphism. -/
111 def pullbackCocycle (f : B →* A) (c : Cocycle A C) : Cocycle B C where
112   coeff a b := c.coeff (f a) (f b)
113   assoc a b d := by simpa using c.assoc (f a) (f b) (f d)
114 
115 theorem normalized_pullback (f : B →* A) (c : Cocycle A C) (hc : Normalized c) :
116     Normalized (pullbackCocycle f c) := by
117   constructor <;> intro a <;> simp [pullbackCocycle, hc.1, hc.2]
118 
119 theorem pullback_rescale (f : B →* A) (c : Cocycle A C) (s : A → C) :
120     pullbackCocycle f (rescale c s) = rescale (pullbackCocycle f c) (s ∘ f) := by
121   apply cocycle_ext
122   intro a b
123   simp [pullbackCocycle, rescale]
124 
125 /-- The induced contravariant map on actual normalized-cocycle classes. -/
126 def pullback (f : B →* A) : Class A C → Class B C :=
127   Quotient.map (fun c : NormalizedCocycle A C =>
128     ⟨pullbackCocycle f c.val, normalized_pullback f c.val c.property⟩)
129     (by
130       intro c d h
131       obtain ⟨s, hs, hd⟩ := h
132       refine ⟨s ∘ f, by simpa using hs, ?_⟩
133       change pullbackCocycle f d.val = _
134       rw [hd, pullback_rescale])
135 
136 @[simp] theorem pullback_of (f : B →* A) (c : Cocycle A C) (hc : Normalized c) :
137     pullback f (of c hc) = of (pullbackCocycle f c) (normalized_pullback f c hc) := rfl
138 
139 /-- Relabeling the index group by a genuine isomorphism induces a class equivalence. -/
140 def congrEquiv (e : A ≃* B) : Class A C ≃ Class B C where
141   toFun := pullback e.symm.toMonoidHom
142   invFun := pullback e.toMonoidHom
143   left_inv q := by
144     refine Quotient.inductionOn q ?_
145     intro c
146     change of (pullbackCocycle e.toMonoidHom (pullbackCocycle e.symm.toMonoidHom c.val)) _ = of c.val c.property
147     have h : pullbackCocycle e.toMonoidHom (pullbackCocycle e.symm.toMonoidHom c.val) = c.val := by
148       apply cocycle_ext
149       intro a b
150       simp [pullbackCocycle]
151     apply Quotient.sound
152     exact ⟨fun _ => 1, rfl, by simpa using h.symm⟩
153   right_inv q := by
154     refine Quotient.inductionOn q ?_
155     intro c
156     change of (pullbackCocycle e.symm.toMonoidHom (pullbackCocycle e.toMonoidHom c.val)) _ = of c.val c.property
157     have h : pullbackCocycle e.symm.toMonoidHom (pullbackCocycle e.toMonoidHom c.val) = c.val := by
158       apply cocycle_ext
159       intro a b
160       simp [pullbackCocycle]
161     apply Quotient.sound
162     exact ⟨fun _ => 1, rfl, by simpa using h.symm⟩
163 
164 @[simp] theorem congrEquiv_of (e : A ≃* B) (c : Cocycle A C) (hc : Normalized c) :
165     congrEquiv e (of c hc) =
166       of (pullbackCocycle e.symm.toMonoidHom c) (normalized_pullback e.symm.toMonoidHom c hc) := rfl
167 
168 end PaperXI.CocycleClass

Back to source controls