The carry cocycle of a character

Let G be a topological group, M a topological G-module, χ : G → ℚ/ℤ a character with open kernel and a ∈ M^G an invariant. Write χ'(g) ∈ [0, 1) for the representative of χ(g). Then

(g, h) ↦ (χ'(g) + χ'(h) - χ'(gh)) • a = ⌊χ'(g) + χ'(h)⌋ • a

is a continuous 2-cocycle, the carry cocycle characterCarryCocycle χ hχ a of χ and a. Classically, its class is the cup product a ∪ δχ of a ∈ H⁰(G, M) with the image δχ of χ ∈ H¹(G, ℚ/ℤ) under the connecting map of 0 → ℤ → ℚ → ℚ/ℤ → 0: the integer-valued cochain (g, h) ↦ χ'(g) + χ'(h) - χ'(gh) is the coboundary of the rational lift χ' of χ. When G is cyclic of order n and χ sends a generator g to 1 / n, its value at (gⁱ, gʲ), for i, j < n, is a if n ≤ i + j and 0 otherwise (characterCarry_eq_ite): these are the values of the carry cocycle of a at g that represents the two-periodicity class of a.

The class is additive in a by construction and additive in χ (characterCarryCocycle_add_character), and the cocycle is natural along compatible pairs (cocyclesMap2_characterCarryCocycle). Naturality is what computes the localizations of a global carry class at the places of a number field, and additivity in χ reduces the local computation to a character taking the value 1 / n on a generator.

The cocycle construction and its naturality only require separately continuous multiplication on the groups: the open kernel makes the character locally constant. The cohomology map explicitMap2_characterCarryCocycle requires jointly continuous multiplication and continuous actions, as does the degree-two cohomology carrier H2.

Main definitions

• TauCeti.ContCohomology.characterCarry χ g h: the integer ⌊χ'(g) + χ'(h)⌋.
• TauCeti.ContCohomology.characterCarryCocycle χ hχ: the carry cocycle of χ, additive in the invariant a.

Main results

• TauCeti.ContCohomology.intCast_characterCarry: ⌊χ'(g) + χ'(h)⌋ = χ'(g) + χ'(h) - χ'(gh).
• TauCeti.ContCohomology.characterCarry_mul_add: the carry is an integer 2-cocycle.
• TauCeti.ContCohomology.characterCarry_eq_ite: if χ(g) and χ(h) are the classes of i / n and j / n with i, j < n, the carry is 1 if n ≤ i + j and 0 otherwise.
• TauCeti.ContCohomology.cocyclesMap2_characterCarryCocycle: pulling back the carry cocycle of χ and a along a compatible pair (φ, f) gives the carry cocycle of χ ∘ φ and f a.
• TauCeti.ContCohomology.characterCarryCocycle_add_character, TauCeti.ContCohomology.characterCarryCocycle_zsmul_character: the class of the carry cocycle is additive in the character.

References

• J.-P. Serre, Local Fields, Chapter XIV, §1.
• J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter VII (Tate, Global Class Field Theory), §1.

noncomputable def TauCeti.ContCohomology.characterCarry {G : Type u} [Group G] (χ : Additive G →+ AddCircle 1) (g h : G) : ℤ

The carry of a character χ : G → ℚ/ℤ at (g, h): the integer ⌊χ'(g) + χ'(h)⌋, where χ'(x) ∈ [0, 1) is the representative of χ(x). It is χ'(g) + χ'(h) - χ'(gh) (intCast_characterCarry).

theorem TauCeti.ContCohomology.intCast_characterCarry {G : Type u} [Group G] (χ : Additive G →+ AddCircle 1) (g h : G) : ↑(characterCarry χ g h) = ↑((AddCircle.equivIco 1 0) (χ (Additive.ofMul g))) + ↑((AddCircle.equivIco 1 0) (χ (Additive.ofMul h))) - ↑((AddCircle.equivIco 1 0) (χ (Additive.ofMul (g * h))))

The carry of χ at (g, h) is the defect χ'(g) + χ'(h) - χ'(gh) of additivity of the representatives in [0, 1).

theorem TauCeti.ContCohomology.characterCarry_eq_ite {G : Type u} [Group G] (χ : Additive G →+ AddCircle 1) {g h : G} {n i j : ℕ} (hi : i < n) (hj : j < n) (hg : χ (Additive.ofMul g) = ↑(↑i / ↑n)) (hh : χ (Additive.ofMul h) = ↑(↑j / ↑n)) : characterCarry χ g h = if n ≤ i + j then 1 else 0

The carry on classes of fractions: if χ(g) and χ(h) are the classes of i / n and j / n with i, j < n, the carry of χ at (g, h) is 1 if n ≤ i + j and 0 otherwise.

@[simp]

theorem TauCeti.ContCohomology.characterCarry_zero {G : Type u} [Group G] (g h : G) : characterCarry 0 g h = 0

The zero character has no carries.

@[simp]

theorem TauCeti.ContCohomology.characterCarry_comp {G : Type u} [Group G] {H : Type u_1} [Group H] (χ : Additive G →+ AddCircle 1) (φ : H →* G) (h k : H) : characterCarry (χ.comp (MonoidHom.toAdditive φ)) h k = characterCarry χ (φ h) (φ k)

The carry of a character composed with a homomorphism is the carry at the images.

theorem TauCeti.ContCohomology.characterCarry_mul_add {G : Type u} [Group G] (χ : Additive G →+ AddCircle 1) (g h j : G) : characterCarry χ (g * h) j + characterCarry χ g h = characterCarry χ h j + characterCarry χ g (h * j)

The carry is an integer 2-cocycle: c(gh, j) + c(g, h) = c(h, j) + c(g, hj) for the carry c of a character. In ℚ both sides telescope to χ'(g) + χ'(h) + χ'(j) - χ'(ghj).

noncomputable def TauCeti.ContCohomology.characterCarryCocycle {G : Type u} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] (χ : Additive G →+ AddCircle 1) (hχ : IsOpen ↑χ.ker) : ↥(H0 G M) →+ ↥(Z2 G M)

The carry cocycle of a character χ : G → ℚ/ℤ with open kernel and an invariant a ∈ M^G: the continuous 2-cocycle (g, h) ↦ ⌊χ'(g) + χ'(h)⌋ • a, where χ'(x) ∈ [0, 1) represents χ(x) (characterCarryCocycle_apply). It is additive in a.

@[simp]

theorem TauCeti.ContCohomology.characterCarryCocycle_apply {G : Type u} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] (χ : Additive G →+ AddCircle 1) (hχ : IsOpen ↑χ.ker) (a : ↥(H0 G M)) (g h : G) : ↑((characterCarryCocycle χ hχ) a) (g, h) = characterCarry χ g h • ↑a

The value of the carry cocycle of χ and a at (g, h) is the carry of χ times a.

theorem TauCeti.ContCohomology.cocyclesMap2_characterCarryCocycle {G : Type u} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {H : Type uH} [Group H] [TopologicalSpace H] [SeparatelyContinuousMul H] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction H N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (χ : Additive G →+ AddCircle 1) (hχ : IsOpen ↑χ.ker) (a : ↥(H0 G M)) : (cocyclesMap2 G M H N φ f hf hequiv) ((characterCarryCocycle χ hχ) a) = (characterCarryCocycle (χ.comp (MonoidHom.toAdditive ↑φ)) ⋯) ((explicitMap0 G M (↑φ) f hequiv) a)

Naturality of the carry cocycle. Pulling back the carry cocycle of χ and a along a compatible pair (φ, f) gives the carry cocycle of χ ∘ φ and f a.

theorem TauCeti.ContCohomology.characterCarryCocycle_add_character {G : Type u} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {χ₁ χ₂ : Additive G →+ AddCircle 1} (hχ₁ : IsOpen ↑χ₁.ker) (hχ₂ : IsOpen ↑χ₂.ker) (a : ↥(H0 G M)) : ↑((characterCarryCocycle (χ₁ + χ₂) ⋯) a) = ↑((characterCarryCocycle χ₁ hχ₁) a) + ↑((characterCarryCocycle χ₂ hχ₂) a)

The class of the carry cocycle is additive in the character. The carry cocycles of χ₁ + χ₂, χ₁ and χ₂ differ by the coboundary of g ↦ ⌊χ₁'(g) + χ₂'(g)⌋ • a. The classes are read in the quotient of Z² by the continuous coboundaries lying in Z², which is H2 G M whenever the latter is defined.

@[simp]

theorem TauCeti.ContCohomology.characterCarryCocycle_zero_character {G : Type u} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] (a : ↥(H0 G M)) : (characterCarryCocycle 0 ⋯) a = 0

The carry cocycle of the zero character vanishes.

theorem TauCeti.ContCohomology.characterCarryCocycle_zsmul_character {G : Type u} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {χ : Additive G →+ AddCircle 1} (hχ : IsOpen ↑χ.ker) (k : ℤ) (a : ↥(H0 G M)) : ↑((characterCarryCocycle (k • χ) ⋯) a) = k • ↑((characterCarryCocycle χ hχ) a)

The class of the carry cocycle is additive in the character: integer multiples.

theorem TauCeti.ContCohomology.explicitMap2_characterCarryCocycle {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {H : Type uH} [Group H] [TopologicalSpace H] [ContinuousMul H] [ContinuousSMul G M] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (χ : Additive G →+ AddCircle 1) (hχ : IsOpen ↑χ.ker) (a : ↥(H0 G M)) : (explicitMap2 G M H N φ f hf hequiv) ↑((characterCarryCocycle χ hχ) a) = ↑((characterCarryCocycle (χ.comp (MonoidHom.toAdditive ↑φ)) ⋯) ((explicitMap0 G M (↑φ) f hequiv) a))

Naturality of the carry class. Pulling back the cohomology class of the carry cocycle of χ and a along a compatible pair (φ, f) gives the carry class of χ ∘ φ and f a.

This is the degree-two cohomology form of cocyclesMap2_characterCarryCocycle.

theorem TauCeti.ContCohomology.explicitMap2_characterCarryCocycle_eq_zero {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] {H : Type uH} [Group H] [TopologicalSpace H] [ContinuousMul H] [ContinuousSMul G M] {N : Type uN} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (χ : Additive G →+ AddCircle 1) (hχ : IsOpen ↑χ.ker) (a : ↥(H0 G M)) (ha : f ↑a = 0) : (explicitMap2 G M H N φ f hf hequiv) ↑((characterCarryCocycle χ hχ) a) = 0

A carry class pulled back to a coefficient where its invariant vanishes is zero: if the compatible pair (φ, f) sends the invariant a to 0, it sends the carry class of χ and a to 0.