Module

FiniteCyclicBaseUnitCarry.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FiniteCyclicBaseUnitCarry

3 declarations indexed from sourceView source ↗

Module documentation

Base-unit carry classes in finite cyclic unit cohomology

This file evaluates the normalized carry cocycle whose coefficient is a unit from the base field. Under the finite-cyclic H²--norm-quotient comparison, its class is exactly the corresponding norm class.

Imports2

Imported by3

def

finiteCyclicBaseUnitFixed

L29 ↗

ClassFieldTower.Martinet.Shafarevich.finiteCyclicBaseUnitFixed

Documentation

A base-field unit embedded in a finite Galois extension, bundled as a fixed point for an arbitrary Galois automorphism.

Source context 5 commands

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

open CategoryTheory Representation
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalFieldTheory
noncomputable section

Lean source · statement

def finiteCyclicBaseUnitFixed
    (K L : Type) [Field K] [Field L] [Algebra K L]
    (g : Gal(L/K)) (a : Kˣ) :
    LinearMap.ker
      ((Rep.ofAlgebraAutOnUnits K L).ρ g - LinearMap.id)

theorem

finiteCyclicGeneratorFixedBaseUnit_baseUnitFixed

L47 ↗

ClassFieldTower.Martinet.Shafarevich.finiteCyclicGeneratorFixedBaseUnit_baseUnitFixed

Documentation

Recovering the base-field unit from its embedded invariant representative is the identity.

Source context 5 commands

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

open CategoryTheory Representation
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalFieldTheory
noncomputable section

Lean source · statement

theorem finiteCyclicGeneratorFixedBaseUnit_baseUnitFixed
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (g : Gal(L/K))
    (hg : ∀ sigma : Gal(L / K), sigma ∈ Subgroup.zpowers g)
    (a : Kˣ) :
    finiteCyclicGeneratorFixedBaseUnit K L g hg
        (finiteCyclicBaseUnitFixed K L g a) = a

theorem

finiteCyclicUnitsH2IsoNormQuotient_carry_baseUnit

L67 ↗

ClassFieldTower.Martinet.Shafarevich.finiteCyclicUnitsH2IsoNormQuotient_carry_baseUnit

Documentation

The normalized carry class with a base-unit coefficient evaluates to the norm class of that base unit.

Source context 5 commands

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

open CategoryTheory Representation
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open CyclicCohomology LocalFieldTheory
noncomputable section

Lean source · full declaration

theorem finiteCyclicUnitsH2IsoNormQuotient_carry_baseUnit
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (g : Gal(L/K))
    (hg : ∀ sigma : Gal(L / K), sigma ∈ Subgroup.zpowers g)
    (a : Kˣ) :
    letI := AlgEquiv.fintype K L
    let : IsCyclic (Gal(L / K)) :=
      CyclicCohomology.isCyclic_of_generator g hg
    letI : CommGroup (Gal(L / K)) := IsCyclic.commGroup
    (finiteCyclicUnitsH2IsoNormQuotient K L g hg).hom
        (groupCohomology.H2π (Rep.ofAlgebraAutOnUnits K L)
          (finiteCyclicCarryTwoCocycle (Rep.ofAlgebraAutOnUnits K L)
            g hg (finiteCyclicBaseUnitFixed K L g a))) =
      Additive.ofMul (normClass K L a) := by
  dsimp only
  let := AlgEquiv.fintype K L
  let : IsCyclic (Gal(L / K)) :=
    CyclicCohomology.isCyclic_of_generator g hg
  let : CommGroup (Gal(L / K)) := IsCyclic.commGroup
  let A := Rep.ofAlgebraAutOnUnits K L
  let baseUnitFixed :
      LinearMap.ker (Rep.applyAsHom A g - 𝟙 A).hom.toLinearMap :=
    Eq.mp (by rfl) (finiteCyclicBaseUnitFixed K L g a)
  change
    (finiteCyclicUnitsH2IsoNormQuotient K L g hg).hom
        (groupCohomology.H2π A
          (finiteCyclicCarryTwoCocycle A g hg baseUnitFixed)) = _
  rw [H2π_finiteCyclicCarryTwoCocycle]
  change
    (finiteCyclicUnitsH2IsoNormQuotient K L g hg).hom
        (finiteCyclicUnitsH2PeriodicClass K L g hg
          (finiteCyclicBaseUnitFixed K L g a)) = _
  rw [finiteCyclicUnitsH2IsoNormQuotient_periodicClass,
    finiteCyclicGeneratorFixedBaseUnit_baseUnitFixed]

Module documentation

Base-unit carry classes in finite cyclic unit cohomology

Declarations

finiteCyclicBaseUnitFixed

finiteCyclicGeneratorFixedBaseUnit_baseUnitFixed

finiteCyclicUnitsH2IsoNormQuotient_carry_baseUnit