Identities of unbundled 1-cocycles

Facts about a 1-cocycle f : G → M in the sense of Mathlib's unbundled groupCohomology.IsCocycle₁, which need no topology and no representation:

• groupCohomology.smul_apply_inv_mul_mul_of_isCocycle₁: conjugating the argument by k and then acting by k adds m • f k - f k to the value at m, for any scalar multiplication of G on M: k • f (k⁻¹ * m * k) = m • f k - f k + f m.

• groupCohomology.smul_zero_of_isCocycle₁: an action admitting a 1-cocycle fixes 0.

• groupCohomology.zeroLocus: the zero locus {g | f g = 0} is a subgroup of G, for any group action (not necessarily distributive) admitting the cocycle. As a set it is f ⁻¹' {0} (groupCohomology.coe_zeroLocus). GroupCohomology/Cocycle/Topology.lean shows it is closed when f is continuous into a T1 space, and deduces that such an f vanishing on a topological generating set vanishes everywhere.

• TauCeti.isCocycle₁_ext_of_forall_mem_zpowers: a one-cocycle on a cyclic group is determined by its value at a generator.

• TauCeti.groupNorm: the sum of the scalar actions of a finite group, as an additive homomorphism, with no topology or representation required. For a finite normal subgroup it commutes with the action of the ambient group (TauCeti.groupNorm_smul), and so is a G-equivariant additive endomorphism (TauCeti.groupNormHom).

• TauCeti.sum_smul_apply_eq_zero_of_isCocycle₁: on a finite group, the group norm kills every value of a one-cocycle.

Continuous cohomology uses the conjugation identity in the five-term sequence and in transgression, and the cyclic-group facts in the vanishing criterion.

theorem groupCohomology.smul_apply_inv_mul_mul_of_isCocycle₁ {G : Type u_1} {M : Type u_2} [Group G] [AddCommGroup M] [SMul G M] {c : G → M} (hc : IsCocycle₁ c) (k m : G) : k • c (k⁻¹ * m * k) = m • c k - c k + c m

Conjugating the argument of a 1-cocycle by k and then acting by k adds m • c k - c k to its value at m: k • c (k⁻¹ * m * k) = m • c k - c k + c m. Only a scalar multiplication of G on M is needed, not an action.

theorem groupCohomology.smul_zero_of_isCocycle₁ {G : Type u_1} {M : Type u_2} [Monoid G] [AddCommGroup M] [MulAction G M] {f : G → M} (hf : IsCocycle₁ f) (g : G) : g • 0 = 0

A monoid action on an additive group that admits a 1-cocycle fixes 0.

def groupCohomology.zeroLocus {G : Type u_1} {M : Type u_2} [Group G] [AddCommGroup M] [MulAction G M] {f : G → M} (hf : IsCocycle₁ f) : Subgroup G

The zero locus of a 1-cocycle, {g | f g = 0}, as a subgroup of G, for any group action (not necessarily distributive).

Equations

• groupCohomology.zeroLocus hf = { carrier := {g : G | f g = 0}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem groupCohomology.mem_zeroLocus {G : Type u_1} {M : Type u_2} [Group G] [AddCommGroup M] [MulAction G M] {f : G → M} (hf : IsCocycle₁ f) {g : G} : g ∈ zeroLocus hf ↔ f g = 0

An element lies in the zero locus of a 1-cocycle exactly when the cocycle vanishes there.

@[simp]

theorem groupCohomology.coe_zeroLocus {G : Type u_1} {M : Type u_2} [Group G] [AddCommGroup M] [MulAction G M] {f : G → M} (hf : IsCocycle₁ f) : ↑(zeroLocus hf) = f ⁻¹' {0}

The zero locus of a 1-cocycle is the preimage of 0.

def TauCeti.groupNorm (G : Type u_1) (M : Type u_2) [Fintype G] [AddCommMonoid M] [DistribSMul G M] : M →+ M

The group norm, m ↦ ∑ x, x • m, as an additive homomorphism. It needs only a finite scalar type and distributive scalar multiplication on an additive commutative monoid.

Equations

• TauCeti.groupNorm G M = ∑ x : G, DistribSMul.toAddMonoidHom M x

@[simp]

theorem TauCeti.groupNorm_apply (G : Type u_1) (M : Type u_2) [Fintype G] [AddCommMonoid M] [DistribSMul G M] (m : M) : (groupNorm G M) m = ∑ x : G, x • m

Applying the group norm sums the scalar translates of the argument.

theorem TauCeti.groupNorm_smul {G : Type u_1} {M : Type u_2} [Group G] [AddCommMonoid M] [DistribMulAction G M] (N : Subgroup G) [N.Normal] [Fintype ↥N] (g : G) (m : M) : (groupNorm (↥N) M) (g • m) = g • (groupNorm (↥N) M) m

The norm of a finite normal subgroup N of G commutes with the action of G: conjugation by g permutes N.

def TauCeti.groupNormHom {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] [Fintype ↥N] (M : Type u_2) [AddCommMonoid M] [DistribMulAction G M] : M →+[G] M

The norm of a finite normal subgroup N of G, as a G-equivariant additive endomorphism of M (TauCeti.groupNorm_smul).

Equations

• TauCeti.groupNormHom N M = { toFun := (↑(TauCeti.groupNorm (↥N) M)).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.groupNormHom_apply {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] [Fintype ↥N] (M : Type u_2) [AddCommMonoid M] [DistribMulAction G M] (m : M) : (groupNormHom N M) m = (groupNorm (↥N) M) m

The equivariant norm groupNormHom N M is the group norm of N.

theorem TauCeti.isCocycle₁_ext_of_forall_mem_zpowers {G : Type u_1} {M : Type u_2} [Group G] [AddCommGroup M] [MulAction G M] {f f' : G → M} (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (hf : groupCohomology.IsCocycle₁ f) (hf' : groupCohomology.IsCocycle₁ f') (h : f g = f' g) : f = f'

Two one-cocycles on a cyclic group agree if they agree at a generator. No finiteness or continuity hypothesis is needed, and the action need not be distributive.

theorem TauCeti.sum_smul_apply_eq_zero_of_isCocycle₁ {G : Type u_1} {M : Type u_2} [Group G] [AddCommGroup M] [SMul G M] [Fintype G] {f : G → M} (g : G) (hf : groupCohomology.IsCocycle₁ f) : ∑ x : G, x • f g = 0

The value of a one-cocycle on a finite group lies in the kernel of the group norm. This holds at every group element, not just at a cyclic generator. Even associativity and distributivity of the scalar multiplication are unnecessary for this identity.