Module

FiniteFieldUnitsIdelePrimitive.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.FiniteFieldUnitsIdelePrimitive

8 declarations indexed from sourceView source ↗

Module documentation

Recovering a field-unit primitive from an idele primitive

The actual field-unit embedding factors through the principal-idele representation isomorphism. Its degree-two map is therefore injective in a finite Galois p-extension. An explicit idele primitive of a field-unit cocycle consequently supplies a field-unit primitive, the input needed for the subsequent Hilbert-90 and Kummer correction.

Imports2

Imported by3

instance

(anonymous instance)

L32 ↗

Source context 7 commands

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

open CategoryTheory NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology LocalClassFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [Algebra K L]

Lean source · statement

instance : MulDistribMulAction (Gal(L/K)) Lˣ

instance

(anonymous instance)

L35 ↗

Source context 8 commands

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

open CategoryTheory NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology LocalClassFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [Algebra K L]
local instance : MulDistribMulAction (Gal(L/K)) Lˣ :=
  galoisGroupFieldUnitsMulDistribMulAction K L

Lean source · statement

instance : MulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup K L)

instance

(anonymous instance)

L38 ↗

Source context 9 commands

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

open CategoryTheory NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology LocalClassFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [Algebra K L]
local instance : MulDistribMulAction (Gal(L/K)) Lˣ :=
  galoisGroupFieldUnitsMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L

Lean source · statement

instance : MulDistribMulAction (Gal(L/K))
    (RelativeIdeleGroup.principalSubgroup K L)

def

finiteFieldUnitsIdeleRepHom

L43 ↗

ClassFieldTower.Martinet.Shafarevich.finiteFieldUnitsIdeleRepHom

Documentation

The actual diagonal embedding of field units as a representation map.

Source context 10 commands

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

open CategoryTheory NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology LocalClassFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [Algebra K L]
local instance : MulDistribMulAction (Gal(L/K)) Lˣ :=
  galoisGroupFieldUnitsMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K))
    (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L

Lean source · statement

def finiteFieldUnitsIdeleRepHom :
    Rep.ofMulDistribMulAction (Gal(L/K)) Lˣ ⟶
      (finiteIdeleShortComplex K L).X₂

def

fieldUnitsPrincipalIdeleRepIso

L49 ↗

ClassFieldTower.Martinet.Shafarevich.fieldUnitsPrincipalIdeleRepIso

Source context 10 commands

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

open CategoryTheory NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology LocalClassFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [Algebra K L]
local instance : MulDistribMulAction (Gal(L/K)) Lˣ :=
  galoisGroupFieldUnitsMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K))
    (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L

Lean source · statement

def fieldUnitsPrincipalIdeleRepIso :
    Rep.ofMulDistribMulAction (Gal(L/K)) Lˣ ≅ (finiteIdeleShortComplex K L).X₁

theorem

finiteFieldUnitsIdeleRepHom_factor

L58 ↗

ClassFieldTower.Martinet.Shafarevich.finiteFieldUnitsIdeleRepHom_factor

Source context 10 commands

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

open CategoryTheory NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology LocalClassFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [Algebra K L]
local instance : MulDistribMulAction (Gal(L/K)) Lˣ :=
  galoisGroupFieldUnitsMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K))
    (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L

Lean source · statement

theorem finiteFieldUnitsIdeleRepHom_factor :
    finiteFieldUnitsIdeleRepHom K L =
      (fieldUnitsPrincipalIdeleRepIso K L).hom ≫ (finiteIdeleShortComplex K L).f

theorem

finiteFieldUnitsIdeleH2Map_injective_of_isPGroup

L66 ↗

ClassFieldTower.Martinet.Shafarevich.finiteFieldUnitsIdeleH2Map_injective_of_isPGroup

Documentation

The field-unit-to-idele map is injective in degree two for a finite Galois p-extension, by the proved idele-class degree-one vanishing.

Source context 10 commands

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

open CategoryTheory NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology LocalClassFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [Algebra K L]
local instance : MulDistribMulAction (Gal(L/K)) Lˣ :=
  galoisGroupFieldUnitsMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K))
    (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L

Lean source · statement

theorem finiteFieldUnitsIdeleH2Map_injective_of_isPGroup
    [NumberField L] [FiniteDimensional K L] [IsGalois K L]
    {p : ℕ} [Fact p.Prime] (hP : IsPGroup p (Gal(L/K))) :
    Function.Injective
      (groupCohomology.map
        (A := Rep.ofMulDistribMulAction (Gal(L/K)) Lˣ)
        (B := (finiteIdeleShortComplex K L).X₂)
        (MonoidHom.id (Gal(L/K))) (finiteFieldUnitsIdeleRepHom K L) 2).hom

theorem

finiteFieldUnitsTwoCocycle_isCoboundary_of_idelePrimitive

L84 ↗

ClassFieldTower.Martinet.Shafarevich.finiteFieldUnitsTwoCocycle_isCoboundary_of_idelePrimitive

Documentation

An explicit idele primitive of a field-unit cocycle yields an actual field-unit primitive. The idele primitive is the one constructed by the unramified local-unit and restricted-product argument.

Source context 10 commands

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

open CategoryTheory NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology LocalClassFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [Algebra K L]
local instance : MulDistribMulAction (Gal(L/K)) Lˣ :=
  galoisGroupFieldUnitsMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K))
    (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L

Lean source · statement

theorem finiteFieldUnitsTwoCocycle_isCoboundary_of_idelePrimitive
    [NumberField L] [FiniteDimensional K L] [IsGalois K L]
    {p : ℕ} [Fact p.Prime] (hP : IsPGroup p (Gal(L/K)))
    (c : groupCohomology.cocycles₂ (Rep.ofMulDistribMulAction (Gal(L/K)) Lˣ))
    (b : Gal(L/K) → Additive (RelativeIdeleGroup K L))
    (hb : (groupCohomology.d₁₂
        (Rep.ofMulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup K L))).hom b =
      (groupCohomology.mapCocycles₂ (MonoidHom.id (Gal(L/K)))
        (finiteFieldUnitsIdeleRepHom K L) c).1) :
    ∃ a : Gal(L/K) → Additive Lˣ,
      (groupCohomology.d₁₂ (Rep.ofMulDistribMulAction (Gal(L/K)) Lˣ)).hom a = c.1

Module documentation

Recovering a field-unit primitive from an idele primitive

Declarations