NYLL
Module

ChosenPlaceAction.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Cohomology.SPlaces.OutsideIntegralInduced.ChosenPlaceAction
11 declarations indexed from sourceView source ↗

Module documentation

The action at a chosen finite place

This file exposes the decomposition-group action and the direct local cohomology endpoint used by the integral induced-block construction. Keeping this localization boundary in a lower leaf prevents downstream transport proofs from elaborating it together with the tensor-block API.

Imports6
Imported by10

Declarations

abbrev

ChosenFinitePlaceDecompositionGroup

L46 ↗
Documentation

The decomposition group at the chosen extension of a finite place.

Source context 11 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section ChosenFinitePlace
Lean source · statement
abbrev ChosenFinitePlaceDecompositionGroup
    (w₀ : HeightOneSpectrum (𝓞 K))
abbrev

ChosenFinitePlaceLocalizedIntegerUnits

L52 ↗
Documentation

Integer units in the chosen localized completion.

Source context 11 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section ChosenFinitePlace
Lean source · statement
abbrev ChosenFinitePlaceLocalizedIntegerUnits
    (w₀ : HeightOneSpectrum (𝓞 K))
abbrev

ChosenFinitePlaceLocalizedFieldUnits

L58 ↗
Documentation

Field units in the chosen localized completion.

Source context 11 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section ChosenFinitePlace
Lean source · statement
abbrev ChosenFinitePlaceLocalizedFieldUnits
    (w₀ : HeightOneSpectrum (𝓞 K))
def

chosenFinitePlaceDecompositionGroupIntegerUnitsAction

L68 ↗
Documentation

The decomposition-group action on the chosen local integer units.

The named action is the boundary at which dependent induced-module declarations stop expanding the chosen-localization construction.

Source context 11 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section ChosenFinitePlace
Lean source · statement
def
    chosenFinitePlaceDecompositionGroupIntegerUnitsAction
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction
      (ChosenFinitePlaceDecompositionGroup
        (K := K) (L := L) w₀)
      (ChosenFinitePlaceLocalizedIntegerUnits
        (K := K) (L := L) w₀)
def

chosenFinitePlaceDecompositionGroupLocalUnitsAction

L85 ↗
Documentation

The decomposition-group action on the chosen local field units.

Source context 11 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section ChosenFinitePlace
Lean source · statement
def chosenFinitePlaceDecompositionGroupLocalUnitsAction
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction
      (ChosenFinitePlaceDecompositionGroup
        (K := K) (L := L) w₀)
      (ChosenFinitePlaceLocalizedFieldUnits
        (K := K) (L := L) w₀)
abbrev

ChosenFinitePlaceInducedIntegerUnits

L98 ↗
Documentation

The induced module of integer units at the chosen finite place.

Source context 11 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section ChosenFinitePlace
Lean source · statement
abbrev ChosenFinitePlaceInducedIntegerUnits
    (w₀ : HeightOneSpectrum (𝓞 K))
abbrev

ChosenFinitePlaceLocalPlaceBlock

L112 ↗
Documentation

The local multiplicative block attached to the chosen finite place.

Source context 11 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section ChosenFinitePlace
Lean source · statement
abbrev ChosenFinitePlaceLocalPlaceBlock
    (w₀ : HeightOneSpectrum (𝓞 K))
def

chosenFinitePlaceInducedIntegerUnitsAction

L121 ↗
Documentation

The global action on the chosen induced integer-unit block.

Source context 11 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section ChosenFinitePlace
Lean source · statement
def chosenFinitePlaceInducedIntegerUnitsAction
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction (L ≃ₐ[K] L)
      (ChosenFinitePlaceInducedIntegerUnits
        (K := K) (L := L) w₀)
def

chosenFinitePlaceLocalPlaceBlockAction

L139 ↗
Documentation

The global action on the chosen local multiplicative block.

Source context 11 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section ChosenFinitePlace
Lean source · statement
def chosenFinitePlaceLocalPlaceBlockAction
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction (L ≃ₐ[K] L)
      (ChosenFinitePlaceLocalPlaceBlock
        (K := K) (L := L) w₀)
theorem

chosenFinitePlaceDecompositionGroupIntegerUnitsAction_smul_eq_pullback

L160 ↗
Documentation

On the actual chosen localization, the decomposition-group action on integer units is the pullback of the local Galois action along the canonical decomposition equivalence. Both sides are evaluated with the valued-field and integral-closure data used by LocalInduction.

Source context 12 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section ChosenFinitePlace
omit [NumberField L] in
Lean source · full declaration
theorem
    chosenFinitePlaceDecompositionGroupIntegerUnitsAction_smul_eq_pullback
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    let vK := HeightOneSpectrum.adicAbv K w₀
    let w := chosenFinitePlaceExtension (L := L) w₀
    let E := ChosenFinitePlaceLocalizedCompletion
      (K := K) (L := L) w₀
    let eLocal :=
      decompositionGroupEquivAlgebraicLocalizationAut
        vK
        (RayClass.adicAbv_isNontrivial w₀)
        w
    letI : MulDistribMulAction
        (Gal(E / vK.Completion)) 𝒪[E]ˣ :=
      galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure
        vK.Completion E
    ∀ (σ : absoluteValueDecompositionGroup K w.1)
      (x : 𝒪[E]ˣ),
      (chosenFinitePlaceDecompositionGroupIntegerUnitsAction
        (K := K) (L := L) w₀).smul σ x =
        (MulDistribMulAction.compHom
          𝒪[E]ˣ eLocal.toMonoidHom).smul σ x := by
  unfold chosenFinitePlaceDecompositionGroupIntegerUnitsAction
  dsimp
  intro σ x
  rfl
theorem

chosenFinitePlaceLocalizedIntegerUnits_unramifiedHerbrand_subsingleton

L192 ↗
Documentation

The actual completion selected over a finite place has trivial low-degree Herbrand cohomology on its integer units whenever that local extension is unramified. All valued-local-field and integer-ring structures here are the canonical instances exported by ChosenLocalization.

Source context 12 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section ChosenFinitePlace
omit [NumberField L] in
Lean source · full declaration
theorem chosenFinitePlaceLocalizedIntegerUnits_unramifiedHerbrand_subsingleton
    (w₀ : HeightOneSpectrum (𝓞 K))
    (g : ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) w₀
      ≃ₐ[ChosenFinitePlaceBaseCompletion (K := K) w₀]
      ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) w₀)
    (hg : ∀ τ : Gal(
      ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) w₀ /
      ChosenFinitePlaceBaseCompletion (K := K) w₀),
      τ ∈ Subgroup.zpowers g)
    (hunram : ChosenFinitePlaceIsUnramified
      (K := K) (L := L) w₀) :
    letI : MulDistribMulAction
        (Gal(
          ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) w₀ /
          ChosenFinitePlaceBaseCompletion (K := K) w₀))
        𝒪[ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) w₀]ˣ :=
      galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure
        (ChosenFinitePlaceBaseCompletion (K := K) w₀)
        (ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) w₀)
    Subsingleton
        (HerbrandH0
          (Gal(
            ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) w₀ /
            ChosenFinitePlaceBaseCompletion (K := K) w₀))
          𝒪[ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) w₀]ˣ) ∧
      Subsingleton
        (HerbrandHMinusOne
          (Gal(
            ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) w₀ /
            ChosenFinitePlaceBaseCompletion (K := K) w₀))
          𝒪[ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) w₀]ˣ g) := by
  let vK := HeightOneSpectrum.adicAbv K w₀
  let E := ChosenFinitePlaceLocalizedCompletion
    (K := K) (L := L) w₀
  let :
      IsNonarchimedeanLocalField.IsUnramifiedValuedExtension
        vK.Completion E := by
    simpa [ChosenFinitePlaceIsUnramified] using hunram
  exact
    unramifiedLocalIntegerUnitsHerbrand_subsingleton
      vK.Completion E g hg

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.