Module

RelativeTwoCocycle.lean

Nyll.GaloisCohomology.Kummer.RelativeTwoCocycle

2 declarations indexed from sourceView source ↗

Module documentation

Relative representatives of degree-two cohomology classes

Restriction-zero classes have representatives which vanish pointwise on the subgroup. Their conjugation defect is an actual degree-one cocycle, the input for Hilbert 90 in finite Galois descent.

Imports4

Mathlib.RepresentationTheory.Rep.Res
Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Mathlib.Tactic.Abel

Imported by3

theorem

exists_relativeTwoCocycle

L32 ↗

ClassFieldTower.Cohomology.exists_relativeTwoCocycle

Documentation

Replace a restriction-zero class by a cohomologous cocycle that vanishes on both subgroup arguments. No normality is needed for this first step.

Source context 6 commands

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

open CategoryTheory
open Rep
open groupCohomology
namespace ClassFieldTower.Cohomology
noncomputable section
variable {k G : Type} [CommRing k] [Group G]

Lean source · statement

theorem exists_relativeTwoCocycle
    (A : Rep k G) (S : Subgroup G) (z : cocycles₂ A)
    (hz : groupCohomology.map S.subtype (𝟙 (res S.subtype A)) 2 (H2π A z) = 0) :
    ∃ z' : cocycles₂ A, H2π A z' = H2π A z ∧
      ∀ n m : S, z' ((n : G), (m : G)) = 0

def

relativeTwoCocycleConjugation

L69 ↗

ClassFieldTower.Cohomology.relativeTwoCocycleConjugation