FiniteGroupCohomology.lean

1 import Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
2 import Mathlib.Algebra.Field.ZMod
3 import Mathlib.Data.Fintype.Perm
4 
5 /-!
6 # Low-degree cohomology for groups of invertible finite order
7 
8 The averaging argument is connected to Mathlib's actual cohomology of the
9 inhomogeneous cochain complex through `H1π` and `H1_induction_on`.
10 -/
11 
12 noncomputable section
13 
14 set_option maxHeartbeats 800000
15 
16 namespace PaperXII.FiniteGroupCohomology
17 
18 open CategoryTheory Representation groupCohomology
19 
20 universe u
21 
22 variable {K G : Type u} [Field K] [Group G] [Fintype G]
23 
24 /-- An explicit primitive for a one-cocycle. -/
25 def averagingPrimitive (A : Rep K G) (f : cocycles₁ A) : A :=
26   - (Fintype.card G : K)⁻¹ • ∑ g : G, f g
27 
28 /-- Summing the cocycle identity over a finite group. -/
29 theorem cocycle_sum_identity (A : Rep K G) (f : cocycles₁ A) (g : G) :
30     (Fintype.card G : K) • f g = (∑ h : G, f h) - A.ρ g (∑ h : G, f h) := by
31   have h := congrArg (fun q : G → A => ∑ h : G, q h)
32     (funext ((mem_cocycles₁_iff (f : G → A)).mp f.property g))
33   simp only [Finset.sum_add_distrib, Finset.sum_const, Finset.card_univ,
34     ← map_sum, ← Nat.cast_smul_eq_nsmul K] at h
35   have hshift : (∑ h : G, f (g * h)) = ∑ h : G, f h :=
36     Fintype.sum_equiv (Equiv.mulLeft g) _ _ (fun _ => rfl)
37   rw [hshift] at h
38   exact eq_sub_iff_add_eq.mpr (by simpa only [add_comm] using h.symm)
39 
40 /-- Averaging produces an actual coboundary, with no dimension assumption. -/
41 theorem averagingPrimitive_spec (A : Rep K G) (hcard : (Fintype.card G : K) ≠ 0)
42     (f : cocycles₁ A) (g : G) :
43     A.ρ g (averagingPrimitive A f) - averagingPrimitive A f = f g := by
44   calc
45     A.ρ g (averagingPrimitive A f) - averagingPrimitive A f =
46         (Fintype.card G : K)⁻¹ • ((∑ h : G, f h) - A.ρ g (∑ h : G, f h)) := by
47       simp only [averagingPrimitive]
48       rw [LinearMap.map_smul]
49       simp only [neg_smul, smul_sub]
50       abel
51     _ = (Fintype.card G : K)⁻¹ • ((Fintype.card G : K) • f g) := by
52       rw [← cocycle_sum_identity A f g]
53     _ = f g := by rw [smul_smul, inv_mul_cancel₀ hcard, one_smul]
54 
55 /-- All one-cocycles are coboundaries for a group of invertible order. -/
56 theorem cocycles₁_eq_coboundaries₁ (A : Rep K G)
57     (hcard : (Fintype.card G : K) ≠ 0) : cocycles₁ A = coboundaries₁ A := by
58   apply le_antisymm
59   · intro f hf
60     refine ⟨averagingPrimitive A ⟨f, hf⟩, ?_⟩
61     funext g
62     exact averagingPrimitive_spec A hcard ⟨f, hf⟩ g
63   · exact coboundaries₁_le_cocycles₁ A
64 
65 /-- Every element of Mathlib's first group cohomology is zero. -/
66 theorem h1_eq_zero (A : Rep K G) (hcard : (Fintype.card G : K) ≠ 0)
67     (x : groupCohomology A 1) : x = 0 := by
68   induction x using H1_induction_on with
69   | h f =>
70     apply (H1π_eq_zero_iff f).mpr
71     rw [← cocycles₁_eq_coboundaries₁ A hcard]
72     exact f.property
73 
74 /-- The first cohomology group itself is the zero module. -/
75 theorem h1_subsingleton (A : Rep K G) (hcard : (Fintype.card G : K) ≠ 0) :
76     Subsingleton (groupCohomology A 1) :=
77   ⟨fun x y => (h1_eq_zero A hcard x).trans (h1_eq_zero A hcard y).symm⟩
78 
79 omit [Fintype G] in
80 /-- Vanishing of degree zero is precisely vanishing of actual invariants. -/
81 theorem h0_subsingleton_iff_invariants_eq_bot (A : Rep K G) :
82     Subsingleton (groupCohomology A 0) ↔ A.ρ.invariants = ⊥ :=
83   (H0Iso A).toLinearEquiv.toEquiv.subsingleton_congr.trans
84     Submodule.subsingleton_iff_eq_bot
85 
86 omit [Fintype G] in
87 /-- A usable zero-invariants criterion for degree-zero cohomology. -/
88 theorem h0_subsingleton_of_fixed_eq_zero (A : Rep K G)
89     (hfixed : ∀ v : A, (∀ g : G, A.ρ g v = v) → v = 0) :
90     Subsingleton (groupCohomology A 0) := by
91   apply (h0_subsingleton_iff_invariants_eq_bot A).mpr
92   apply (Submodule.eq_bot_iff _).mpr
93   intro v hv
94   exact hfixed v ((mem_invariants A.ρ v).mp hv)
95 
96 /-- The symmetric group on three letters has order invertible in `F₇`. -/
97 theorem s3_order_nonzero : (Fintype.card (Equiv.Perm (Fin 3)) : ZMod 7) ≠ 0 := by
98   norm_num [Fintype.card_perm, Nat.factorial]
99   decide
100 
101 /-- Actual first group cohomology vanishes for every `F₇` representation of `S₃`. -/
102 theorem s3_h1_subsingleton (A : Rep (ZMod 7) (Equiv.Perm (Fin 3))) :
103     Subsingleton (groupCohomology A 1) := by
104   have : Fact (Nat.Prime 7) := ⟨by decide⟩
105   exact h1_subsingleton A s3_order_nonzero
106 
107 end PaperXII.FiniteGroupCohomology

Back to source controls