Module

UnramifiedKummerFieldUnitsH2.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.UnramifiedKummerFieldUnitsH2

6 declarations indexed from sourceView source ↗

Module documentation

Kummer H² dies in field units at an unramified p-extension

The two coefficient paths into actual relative ideles coincide: Kummer coefficients through everywhere-integral ideles, or through field units. The first has zero H² by the proved local block and restricted-product construction. Injectivity of field-unit H² into idele H² then supplies an actual field-unit primitive. Neither an idele primitive nor a comparison of coefficient maps is an additional hypothesis.

Imports3

Imported by3

instance

kummerFieldUnitsH2SupportedAction

L36 ↗

ClassFieldTower.Martinet.Shafarevich.kummerFieldUnitsH2SupportedAction

Source context 9 commands

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

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

Lean source · statement

instance kummerFieldUnitsH2SupportedAction : MulDistribMulAction Gal(L / K)
    (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) ∅)

instance

kummerFieldUnitsH2IdeleAction

L40 ↗

ClassFieldTower.Martinet.Shafarevich.kummerFieldUnitsH2IdeleAction

Source context 10 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local instance kummerFieldUnitsH2SupportedAction : MulDistribMulAction Gal(L / K)
    (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) ∅) :=
  relativeIdeleLocalTensorDecompositionSupportedSubgroupAction (K := K) (L := L) ∅

Lean source · statement

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

def

finiteSupportedIdeleInclusionRepHom

L46 ↗

ClassFieldTower.Martinet.Shafarevich.finiteSupportedIdeleInclusionRepHom

Documentation

Actual inclusion of everywhere-integral ideles into relative ideles, as a morphism of the canonical Galois representations.

Source context 11 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local instance kummerFieldUnitsH2SupportedAction : MulDistribMulAction Gal(L / K)
    (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) ∅) :=
  relativeIdeleLocalTensorDecompositionSupportedSubgroupAction (K := K) (L := L) ∅
local instance kummerFieldUnitsH2IdeleAction :
    MulDistribMulAction Gal(L/K) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L

Lean source · statement

def finiteSupportedIdeleInclusionRepHom :
    Rep.ofMulDistribMulAction Gal(L / K)
        (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) ∅) ⟶
      (finiteIdeleShortComplex K L).X₂

theorem

finiteKummerSupportedIdeleRepHom_factor

L58 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerSupportedIdeleRepHom_factor

Documentation

The two actual Kummer-to-idele coefficient paths agree pointwise.

Source context 13 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local instance kummerFieldUnitsH2SupportedAction : MulDistribMulAction Gal(L / K)
    (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) ∅) :=
  relativeIdeleLocalTensorDecompositionSupportedSubgroupAction (K := K) (L := L) ∅
local instance kummerFieldUnitsH2IdeleAction :
    MulDistribMulAction Gal(L/K) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
variable (n : ℕ+) [Fact (n : ℕ).Prime]
omit [IsGalois K L] [Fact (n : ℕ).Prime] in

Lean source · statement

theorem finiteKummerSupportedIdeleRepHom_factor
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    finiteKummerSupportedIdeleRepHom K L n hmu ≫ finiteSupportedIdeleInclusionRepHom K L =
      finiteKummerCoefficientRepHom K L n hmu ≫ finiteFieldUnitsIdeleRepHom K L

theorem

unramifiedFiniteKummerCoefficientH2Map_eq_zero

L67 ↗

ClassFieldTower.Martinet.Shafarevich.unramifiedFiniteKummerCoefficientH2Map_eq_zero

Documentation

Kummer classes in degree two vanish after passage to field units in an everywhere-unramified finite Galois p-extension.

Source context 12 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local instance kummerFieldUnitsH2SupportedAction : MulDistribMulAction Gal(L / K)
    (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) ∅) :=
  relativeIdeleLocalTensorDecompositionSupportedSubgroupAction (K := K) (L := L) ∅
local instance kummerFieldUnitsH2IdeleAction :
    MulDistribMulAction Gal(L/K) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
variable (n : ℕ+) [Fact (n : ℕ).Prime]

Lean source · statement

theorem unramifiedFiniteKummerCoefficientH2Map_eq_zero
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hP : IsPGroup (n : ℕ) Gal(L/K))
    (hfin : ∀ v : HeightOneSpectrum (𝓞 K), ChosenFinitePlaceIsUnramified (K := K) (L := L) v)
    (hinf : ∀ v : InfinitePlace K, (chosenInfinitePlaceAbove (L := L) v).IsUnramified K)
    (x : groupCohomology (Rep.trivial ℤ Gal(L / K) (ULift (ZMod (n : ℕ)))) 2) :
    (finiteKummerCoefficientH2Map K L n hmu).hom x = 0

theorem

unramifiedFiniteKummerTwoCocycle_isFieldUnitsCoboundary

L123 ↗

ClassFieldTower.Martinet.Shafarevich.unramifiedFiniteKummerTwoCocycle_isFieldUnitsCoboundary

Documentation

Every finite Kummer two-cocycle admits an actual field-unit primitive in an everywhere-unramified finite Galois p-extension.

Source context 12 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local instance kummerFieldUnitsH2SupportedAction : MulDistribMulAction Gal(L / K)
    (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) ∅) :=
  relativeIdeleLocalTensorDecompositionSupportedSubgroupAction (K := K) (L := L) ∅
local instance kummerFieldUnitsH2IdeleAction :
    MulDistribMulAction Gal(L/K) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
variable (n : ℕ+) [Fact (n : ℕ).Prime]

Lean source · statement

theorem unramifiedFiniteKummerTwoCocycle_isFieldUnitsCoboundary
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hP : IsPGroup (n : ℕ) Gal(L/K))
    (hfin : ∀ v : HeightOneSpectrum (𝓞 K), ChosenFinitePlaceIsUnramified (K := K) (L := L) v)
    (hinf : ∀ v : InfinitePlace K, (chosenInfinitePlaceAbove (L := L) v).IsUnramified K)
    (c : groupCohomology.cocycles₂ (Rep.trivial ℤ Gal(L / K) (ULift (ZMod (n : ℕ))))) :
    ∃ b : Gal(L / K) → Additive Lˣ,
      (groupCohomology.d₁₂ (Rep.ofAlgebraAutOnUnits K L)).hom b =
        (groupCohomology.mapCocycles₂ (MonoidHom.id Gal(L / K))
          (finiteKummerCoefficientRepHom K L n hmu) c).1

Module documentation

Kummer H² dies in field units at an unramified p-extension

Declarations

kummerFieldUnitsH2SupportedAction

kummerFieldUnitsH2IdeleAction

finiteSupportedIdeleInclusionRepHom

finiteKummerSupportedIdeleRepHom_factor

unramifiedFiniteKummerCoefficientH2Map_eq_zero

unramifiedFiniteKummerTwoCocycle_isFieldUnitsCoboundary