Module

FiniteCyclicCarryCoefficientNorm.lean

Nyll.GaloisCohomology.ProP.FiniteCyclicCarryCoefficientNorm

1 declaration indexed from sourceView source ↗

Module documentation

Vanishing of a coefficient-changed cyclic carry class

A coefficient morphism sends the carry cocycle of a fixed element to the carry cocycle of its image. If that image is the norm of an actual element in the target representation, the resulting degree-two cohomology class is zero.

Imports5

Nyll.GaloisCohomology.ProP.FiniteCyclicCarryCocycle
Nyll.GaloisCohomology.ProP.FiniteCyclicBarPeriodicH2Comparison
Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Mathlib.RepresentationTheory.Rep.Basic

Imported by2

theorem

finiteCyclicCarry_coefficientMap_eq_zero_of_norm

L30 ↗

ClassFieldTower.Cohomology.finiteCyclicCarry_coefficientMap_eq_zero_of_norm

Documentation

A concrete norm preimage kills the coefficient-changed cyclic carry class.

Source context 4 commands

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

open CategoryTheory
namespace ClassFieldTower.Cohomology
universe u
variable {R G : Type u} [CommRing R] [CommGroup G] [Fintype G]

Lean source · statement

theorem finiteCyclicCarry_coefficientMap_eq_zero_of_norm
    (A B : Rep R G) (g : G) (hg : ∀ x : G, x ∈ Subgroup.zpowers g)
    (φ : A ⟶ B)
    (a : LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap)
    (b : B) (hb : B.norm.hom b = φ.hom a.1) :
    groupCohomology.map (MonoidHom.id G) φ 2
        (groupCohomology.H2π A (finiteCyclicCarryTwoCocycle A g hg a)) = 0

Module documentation

Vanishing of a coefficient-changed cyclic carry class

Declarations

finiteCyclicCarry_coefficientMap_eq_zero_of_norm