`Definitions/Def_GroupCohomology_CyclicCarry.lean`

definition module

Discrete logarithm, carry 2-cochain and cyclic invariant

Three definitions set up an explicit cochain calculus for a finite cyclic group. Throughout, G is a group, s \in G an element with the hypotheses hs, that every g \in G lies in Subgroup.zpowers s, and hfin, that s has finite order; thus G is cyclic of order n = orderOf s, generated by s.

cyclicLog s hs hfin g is the discrete logarithm of g to base s, a natural number: it is obtained by transporting g, viewed as an element of the subgroup of powers of s via hs, through the inverse of Mathlib's bijection finEquivZPowers between Fin (orderOf s) and that subgroup, and then coercing to \mathbb{N}. So it is the unique exponent in [0, n) with s^{\mathrm{cyclicLog}(g)} = g.

For a representation A of G over \mathbb{Z} and an element a of A, carryFun s hs hfin a is the inhomogeneous 2-cochain G \times G \to A whose value at (g, h) is a when n \le \mathrm{cyclicLog}(g) + \mathrm{cyclicLog}(h) and 0 otherwise: the "carry" occurring when the two logarithms are added in \mathbb{Z}/n.

In the other direction, cyclicInv s c, defined for an arbitrary function c : G \times G \to A, is the element \sum_{i < n} c(s^i, s) of A; on a 2-cocycle this is the classical cyclic invariant, and it depends on s only through s itself and n.

Relation to Mathlib

The discrete logarithm is read off from Mathlib's finEquivZPowers; the carry cochain and the cyclic invariant of a 2-cochain are the project's own notions, with no Mathlib counterpart.

Where it is used

These cochains support the explicit description of H^2 of a finite cyclic group: every 2-cocycle is cohomologous to the carry cocycle attached to its cyclic invariant, carry classes add, vanish exactly on norms, and transform predictably under restriction to a subgroup \langle s^f \rangle. This is the computational form in which the cyclic-group (local) cohomology input to the Galois-cohomological arguments is handled.

References

J.-P. Serre, Local Fields, Graduate Texts in Mathematics 67, Springer, 1979
J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, Grundlehren der mathematischen Wissenschaften 323, Springer, 2nd ed., 2008

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

26 lines
3 declarations
used in the statements of 29 theorems and imported by 45 proofs
imports 0 definition modules

Source file: Definitions/Def_GroupCohomology_CyclicCarry.lean

Imports

only Mathlib

Imported by

Source

import Mathlib

set_option autoImplicit false

open CategoryTheory groupCohomology

namespace groupCohomology

section Carry

variable {G : Type} [Group G]

noncomputable def cyclicLog (s : G) (hs : ∀ g : G, g ∈ Subgroup.zpowers s) (hfin : IsOfFinOrder s) (g : G) : ℕ :=
  ((finEquivZPowers hfin).symm ⟨g, hs g⟩ : Fin (orderOf s))

noncomputable def carryFun (s : G) (hs : ∀ g : G, g ∈ Subgroup.zpowers s) (hfin : IsOfFinOrder s)
    {A : Rep ℤ G} (a : A) : G × G → A :=
  fun p => if orderOf s ≤ cyclicLog s hs hfin p.1 + cyclicLog s hs hfin p.2 then a else 0

noncomputable def cyclicInv (s : G) {A : Rep ℤ G} (c : G × G → A) : A :=
  ∑ i ∈ Finset.range (orderOf s), c (s ^ i, s)

end Carry

end groupCohomology

Definitions/Def_GroupCohomology_CyclicCarry.lean