Nyll.GaloisCohomology.ProP.H2CocycleExtensionKernelCharacter

Module documentation

Splitting a cocycle extension with a coefficient-kernel character

A continuous character which is the identity on the explicit coefficient kernel constructs a continuous section by correcting the zero-coordinate lift. The prime-to-index restriction leaf supplies this character from the actual finite-index transfer.

theorem

π_eq_zero_of_kernelCharacter

L32 ↗

ClassFieldTower.ProP.H2CocycleExtension.π_eq_zero_of_kernelCharacter

Documentation

A coefficient-kernel retraction gives an explicit continuous section and kills the class.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open CategoryTheory TopRep ContRepresentation FreeProPH2Cocycle
noncomputable section
universe u
variable {p : ℕ} [Fact p.Prime]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [LocallyCompactSpace G]

Lean source · statement

theorem H2CocycleExtension.π_eq_zero_of_kernelCharacter
    (z : Cohomology.trivialZModPCocyclesLifted p G 2)
    (χ : H2CocycleExtension z →ₜ* Multiplicative (ZMod p))
    (hχ : ∀ a : A p, χ ⟨a, 1⟩ = Multiplicative.ofAdd a.down) :
    ContinuousCohomology.π (Cohomology.trivialZModPLifted p G) 2 z = 0

Module documentation

Splitting a cocycle extension with a coefficient-kernel character

Declarations

π_eq_zero_of_kernelCharacter