Crossed homomorphisms twisted by a unit-valued function

Let H be a multiplicative type, R a semiring and χ : H → Rˣ a unit-valued function. A function F : H → R is a crossed homomorphism for χ when

F (x * y) = χ x * F y + F x

for all x y : H (TauCeti.IsCrossedHom). When H is a group and χ : H →* Rˣ is a character, these are exactly the 1-cocycles for the action of H on R through χ, written without a module structure on R.

This file develops the elementary calculus for arbitrary unit-valued twists. Over a monoid and an additively cancellative semiring, crossed homomorphisms vanish at 1, their values at natural powers are geometric sums, and they are additive on products where the twist is trivial. Over a group and a ring, their values at inverses are determined by their values at the original elements. Only the commutator formula needs a multiplicative character.

Continuous crossed homomorphisms and uniqueness on topological generating sets are treated in TauCeti/Topology/Algebra/Group/CrossedHom.lean. For R = ℤ_p, their values on a minimal generating tuple are what Labute's prescription property of a continuous character prescribes.

Main definitions

• TauCeti.IsCrossedHom: F : H → R is a crossed homomorphism for the unit-valued χ.

Main results

• TauCeti.IsCrossedHom.ringHom_comp: composing with a semiring homomorphism φ gives a crossed homomorphism for Units.map φ ∘ χ.
• TauCeti.IsCrossedHom.map_pow: F (x ^ k) = (1 + χ x + ⋯ + χ x ^ (k - 1)) * F x.
• TauCeti.IsCrossedHom.map_list_prod_of_forall_eq_one: on a product of elements on which χ is trivial, F is additive.
• TauCeti.IsCrossedHom.map_commutatorElement: for a character into a commutative ring, F ⁅x, y⁆ = (χ x - 1) * F y - (χ y - 1) * F x.

References

• J.-P. Serre, Galois Cohomology, Ch. I, §2.3.
• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, §2.

def TauCeti.IsCrossedHom {H : Type u_1} [Mul H] {R : Type u_2} [Semiring R] (χ : H → Rˣ) (F : H → R) : Prop

A function F : H → R is a crossed homomorphism for the unit-valued function χ when F (x * y) = χ x * F y + F x for all x y : H. Here χ is any function H → Rˣ; when H is a group and χ : H →* Rˣ is a character, this is the 1-cocycle condition for the action of H on R through χ.

Equations

• TauCeti.IsCrossedHom χ F = ∀ (x y : H), F (x * y) = ↑(χ x) * F y + F x

theorem TauCeti.isCrossedHom_iff {H : Type u_1} [Mul H] {R : Type u_2} [Semiring R] {χ : H → Rˣ} {F : H → R} : IsCrossedHom χ F ↔ ∀ (x y : H), F (x * y) = ↑(χ x) * F y + F x

The defining property of IsCrossedHom.

theorem TauCeti.IsCrossedHom.map_mul {H : Type u_1} [Mul H] {R : Type u_2} [Semiring R] {χ : H → Rˣ} {F : H → R} (hF : IsCrossedHom χ F) (x y : H) : F (x * y) = ↑(χ x) * F y + F x

The cocycle identity of a crossed homomorphism.

theorem TauCeti.IsCrossedHom.comp {H : Type u_1} [Mul H] {R : Type u_2} [Semiring R] {χ : H → Rˣ} {F : H → R} (hF : IsCrossedHom χ F) {H' : Type u_3} [Mul H'] {F'' : Type u_4} [FunLike F'' H' H] [MulHomClass F'' H' H] (φ : F'') {χ' : H' → Rˣ} (hχ' : ∀ (x : H'), χ' x = χ (φ x)) : IsCrossedHom χ' (F ∘ ⇑φ)

Precomposing a crossed homomorphism with a multiplicative map gives a crossed homomorphism for the precomposed unit-valued twist.

theorem TauCeti.IsCrossedHom.ringHom_comp {H : Type u_1} [Mul H] {R : Type u_2} [Semiring R] {χ : H → Rˣ} {F : H → R} (hF : IsCrossedHom χ F) {S : Type u_3} [Semiring S] (φ : R →+* S) : IsCrossedHom (⇑(Units.map ↑φ) ∘ χ) (⇑φ ∘ F)

Composing a crossed homomorphism with a semiring homomorphism φ : R →+* S gives a crossed homomorphism for the unit-valued twist Units.map φ ∘ χ.

theorem TauCeti.IsCrossedHom.map_one {H : Type u_1} [MulOneClass H] {R : Type u_2} [Semiring R] [IsLeftCancelAdd R] {χ : H → Rˣ} {F : H → R} (hF : IsCrossedHom χ F) : F 1 = 0

A crossed homomorphism into an additively cancellative semiring vanishes at 1, even when its twist is not multiplicative.

theorem TauCeti.IsCrossedHom.map_list_prod_of_forall_eq_one {H : Type u_1} [MulOneClass H] {R : Type u_2} [Semiring R] [IsLeftCancelAdd R] {χ : H → Rˣ} {F : H → R} (hF : IsCrossedHom χ F) {l : List H} (hl : ∀ a ∈ l, χ a = 1) : F l.prod = (List.map F l).sum

On a product of elements where the twist is trivial, a crossed homomorphism is additive.

theorem TauCeti.IsCrossedHom.map_pow {H : Type u_1} [Monoid H] {R : Type u_2} [Semiring R] [IsLeftCancelAdd R] {χ : H → Rˣ} {F : H → R} (hF : IsCrossedHom χ F) (x : H) (k : ℕ) : F (x ^ k) = (∑ j ∈ Finset.range k, ↑(χ x) ^ j) * F x

The value of a crossed homomorphism at a power is a geometric sum in the twist times the value at the base.

theorem TauCeti.IsCrossedHom.map_pow_of_eq_one {H : Type u_1} [Monoid H] {R : Type u_2} [Semiring R] [IsLeftCancelAdd R] {χ : H → Rˣ} {F : H → R} (hF : IsCrossedHom χ F) {x : H} (hx : χ x = 1) (k : ℕ) : F (x ^ k) = ↑k * F x

On an element where the twist is trivial, a crossed homomorphism is additive along powers: F (x ^ k) = k * F x.

theorem TauCeti.IsCrossedHom.mul_map_inv {H : Type u_1} [Group H] {R : Type u_2} [Ring R] {χ : H → Rˣ} {F : H → R} (hF : IsCrossedHom χ F) (x : H) : ↑(χ x) * F x⁻¹ = -F x

The value of a crossed homomorphism at an inverse, multiplied through by the twist.

theorem TauCeti.IsCrossedHom.map_inv {H : Type u_1} [Group H] {R : Type u_2} [Ring R] {χ : H → Rˣ} {F : H → R} (hF : IsCrossedHom χ F) (x : H) : F x⁻¹ = -↑(χ x)⁻¹ * F x

The value of a crossed homomorphism at an inverse.

theorem TauCeti.IsCrossedHom.map_commutatorElement {H : Type u_1} [Group H] {R : Type u_2} [CommRing R] {F' : Type u_3} [FunLike F' H Rˣ] [MonoidHomClass F' H Rˣ] {χ : F'} {F : H → R} (hF : IsCrossedHom (⇑χ) F) (x y : H) : F ⁅x, y⁆ = (↑(χ x) - 1) * F y - (↑(χ y) - 1) * F x

The value of a crossed homomorphism on the commutator ⁅x, y⁆ = x * y * x⁻¹ * y⁻¹; the character kills the commutator because Rˣ is commutative.