Module

FiniteKummerSPlaceLocalization.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.FiniteKummerSPlaceLocalization

8 declarations indexed from sourceView source ↗

Module documentation

Finite Kummer coefficients in an arbitrary finite idele support

Roots of unity are integral at every finite place. The empty-support coefficient map therefore factors through each prescribed finite support, without changing the principal idele in the full idele representation.

Imports9

Imported by2

instance

finiteKummerSPlaceSupportedAction

L38 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerSPlaceSupportedAction

Source context 8 commands

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

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

Lean source · statement

instance finiteKummerSPlaceSupportedAction
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    MulDistribMulAction Gal(L / K)
      (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S)

instance

finiteKummerSPlaceIdeleAction

L44 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerSPlaceIdeleAction

Source context 9 commands

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

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

Lean source · statement

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

def

finiteKummerSSupportedIdeleRepHom

L49 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerSSupportedIdeleRepHom

Documentation

Roots of unity mapped into any prescribed finite idele support.

Source context 10 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L]
local instance finiteKummerSPlaceSupportedAction
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    MulDistribMulAction Gal(L / K)
      (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S) :=
  relativeIdeleLocalTensorDecompositionSupportedSubgroupAction (K := K) (L := L) S
local instance finiteKummerSPlaceIdeleAction :
    MulDistribMulAction Gal(L / K) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L

Lean source · statement

def finiteKummerSSupportedIdeleRepHom
    (S : Finset (HeightOneSpectrum (𝓞 K))) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    Rep.trivial ℤ Gal(L / K) (ULift (ZMod (n : ℕ))) ⟶
      Rep.ofMulDistribMulAction Gal(L / K)
        (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S)

def

finiteSSupportedIdeleInclusionRepHom

L74 ↗

ClassFieldTower.Martinet.Shafarevich.finiteSSupportedIdeleInclusionRepHom

Documentation

The actual inclusion of finite-support ideles in all relative ideles.

Source context 10 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L]
local instance finiteKummerSPlaceSupportedAction
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    MulDistribMulAction Gal(L / K)
      (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S) :=
  relativeIdeleLocalTensorDecompositionSupportedSubgroupAction (K := K) (L := L) S
local instance finiteKummerSPlaceIdeleAction :
    MulDistribMulAction Gal(L / K) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L

Lean source · statement

def finiteSSupportedIdeleInclusionRepHom
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Rep.ofMulDistribMulAction Gal(L / K)
        (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S) ⟶
      (finiteIdeleShortComplex K L).X₂

theorem

finiteKummerSSupportedIdeleRepHom_factor

L85 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerSSupportedIdeleRepHom_factor

Documentation

Passing a Kummer coefficient through the supported subgroup or through field units gives the same actual principal idele.

Source context 10 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L]
local instance finiteKummerSPlaceSupportedAction
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    MulDistribMulAction Gal(L / K)
      (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S) :=
  relativeIdeleLocalTensorDecompositionSupportedSubgroupAction (K := K) (L := L) S
local instance finiteKummerSPlaceIdeleAction :
    MulDistribMulAction Gal(L / K) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L

Lean source · statement

theorem finiteKummerSSupportedIdeleRepHom_factor
    (S : Finset (HeightOneSpectrum (𝓞 K))) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    finiteKummerSSupportedIdeleRepHom K L S n hmu ≫
        finiteSSupportedIdeleInclusionRepHom K L S =
      finiteKummerCoefficientRepHom K L n hmu ≫ finiteFieldUnitsIdeleRepHom K L

instance

finiteKummerSPlaceTensorAction

L97 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerSPlaceTensorAction

Source context 11 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L]
local instance finiteKummerSPlaceSupportedAction
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    MulDistribMulAction Gal(L / K)
      (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S) :=
  relativeIdeleLocalTensorDecompositionSupportedSubgroupAction (K := K) (L := L) S
local instance finiteKummerSPlaceIdeleAction :
    MulDistribMulAction Gal(L / K) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
variable [IsGalois K L]

Lean source · statement

instance finiteKummerSPlaceTensorAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (v.adicCompletion K ⊗[K] L)ˣ

def

finiteKummerSPlaceH2Localization

L103 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerSPlaceH2Localization

Documentation

The actual finite Kummer class localized at the finite tensor blocks in the chosen exceptional support.

Source context 12 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L]
local instance finiteKummerSPlaceSupportedAction
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    MulDistribMulAction Gal(L / K)
      (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S) :=
  relativeIdeleLocalTensorDecompositionSupportedSubgroupAction (K := K) (L := L) S
local instance finiteKummerSPlaceIdeleAction :
    MulDistribMulAction Gal(L / K) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
variable [IsGalois K L]
local instance finiteKummerSPlaceTensorAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (v.adicCompletion K ⊗[K] L)ˣ :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.adicCompletion K)

Lean source · statement

def finiteKummerSPlaceH2Localization
    (S : Finset (HeightOneSpectrum (𝓞 K))) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    groupCohomology (Rep.trivial ℤ Gal(L / K) (ULift (ZMod (n : ℕ)))) 2 →+
      ∀ v : {v : HeightOneSpectrum (𝓞 K) // v ∈ S},
        groupCohomology
          (Rep.ofMulDistribMulAction Gal(L / K) (v.1.adicCompletion K ⊗[K] L)ˣ) 2

theorem

finiteKummerSPlaceH2Localization_ker_le

L117 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerSPlaceH2Localization_ker_le

Documentation

A Kummer class vanishing at all exceptional finite coordinates dies in field-unit cohomology when the other local blocks are unramified. This is a kernel containment, not injectivity of the Kummer coefficient map.

Source context 12 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology CyclicCohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L]
local instance finiteKummerSPlaceSupportedAction
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    MulDistribMulAction Gal(L / K)
      (relativeIdeleLocalTensorDecompositionSupportedSubgroup (K := K) (L := L) S) :=
  relativeIdeleLocalTensorDecompositionSupportedSubgroupAction (K := K) (L := L) S
local instance finiteKummerSPlaceIdeleAction :
    MulDistribMulAction Gal(L / K) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
variable [IsGalois K L]
local instance finiteKummerSPlaceTensorAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (v.adicCompletion K ⊗[K] L)ˣ :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.adicCompletion K)

Lean source · statement

theorem finiteKummerSPlaceH2Localization_ker_le
    (S : Finset (HeightOneSpectrum (𝓞 K))) (n : ℕ+) [Fact (n : ℕ).Prime]
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (hP : IsPGroup (n : ℕ) Gal(L/K))
    (hfin : ∀ v : HeightOneSpectrum (𝓞 K), v ∉ S →
      ChosenFinitePlaceIsUnramified (K := K) (L := L) v)
    (hinf : ∀ v : InfinitePlace K, (chosenInfinitePlaceAbove (L := L) v).IsUnramified K) :
    (finiteKummerSPlaceH2Localization K L S n hmu).ker ≤
      (finiteKummerCoefficientH2Map K L n hmu).hom.toAddMonoidHom.ker

Module documentation

Finite Kummer coefficients in an arbitrary finite idele support

Declarations