Module

Spine.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Cohomology.SPlaces.OutsideIntegralInduced.LocalInduction.Spine

10 declarations indexed from sourceView source ↗

Module documentation

Shared completion spine for integral local induction

This file names the coherent algebra, valuation, and integral-closure structures used by every integral local-induction leaf.

Imports3

Imported by8

def

extensionCompletionAlgebra

L43 ↗

LocalInductionInternal.extensionCompletionAlgebra

Documentation

The base-field algebra structure on the chosen extension completion.

Source context 10 commands

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

open scoped NumberField TensorProduct ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace LocalInductionInternal
variable (vK : AbsoluteValue K ℝ)
    (w : AbsoluteValueExtension vK L)

Lean source · statement

def extensionCompletionAlgebra :
    Algebra K w.1.Completion

def

extensionCompletionSMul

L49 ↗

LocalInductionInternal.extensionCompletionSMul

Documentation

The scalar action underlying extensionCompletionAlgebra.

Source context 10 commands

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

open scoped NumberField TensorProduct ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace LocalInductionInternal
variable (vK : AbsoluteValue K ℝ)
    (w : AbsoluteValueExtension vK L)

Lean source · statement

def extensionCompletionSMul :
    SMul K w.1.Completion

def

completionAlgebra

L56 ↗

LocalInductionInternal.completionAlgebra

Documentation

The completed-base algebra structure on the chosen extension completion.

Source context 10 commands

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

open scoped NumberField TensorProduct ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace LocalInductionInternal
variable (vK : AbsoluteValue K ℝ)
    (w : AbsoluteValueExtension vK L)

Lean source · statement

def completionAlgebra :
    Algebra vK.Completion w.1.Completion

def

baseValued

L62 ↗

LocalInductionInternal.baseValued

Documentation

The canonical valued structure on the completed base place.

Source context 10 commands

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

open scoped NumberField TensorProduct ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace LocalInductionInternal
variable (vK : AbsoluteValue K ℝ)
    (w : AbsoluteValueExtension vK L)

Lean source · statement

def baseValued
    (hvKna : IsNonarchimedean (vK : K → ℝ)) :
    Valued vK.Completion ℝ≥0

def

baseValuativeRel

L69 ↗

LocalInductionInternal.baseValuativeRel

Documentation

The canonical valuative relation on the completed base place.

Source context 10 commands

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

open scoped NumberField TensorProduct ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace LocalInductionInternal
variable (vK : AbsoluteValue K ℝ)
    (w : AbsoluteValueExtension vK L)

Lean source · full declaration

def baseValuativeRel
    (hvKna : IsNonarchimedean (vK : K → ℝ)) :
    letI : Valued vK.Completion ℝ≥0 := baseValued vK hvKna
    ValuativeRel vK.Completion :=
  finitePlaceCompletionValuativeRel vK hvKna

def

localizedValued

L77 ↗

LocalInductionInternal.localizedValued

Documentation

The canonical valued structure on the chosen localized completion.

Source context 10 commands

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

open scoped NumberField TensorProduct ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace LocalInductionInternal
variable (vK : AbsoluteValue K ℝ)
    (w : AbsoluteValueExtension vK L)

Lean source · statement

def localizedValued
    (hvKna : IsNonarchimedean (vK : K → ℝ)) :
    Valued (LocalizedCompletion vK w) ℝ≥0

def

localizedValuativeRel

L84 ↗

LocalInductionInternal.localizedValuativeRel

Documentation

The canonical valuative relation on the chosen localized completion.

Source context 10 commands

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

open scoped NumberField TensorProduct ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace LocalInductionInternal
variable (vK : AbsoluteValue K ℝ)
    (w : AbsoluteValueExtension vK L)

Lean source · full declaration

def localizedValuativeRel
    (hvKna : IsNonarchimedean (vK : K → ℝ)) :
    letI : Valued (LocalizedCompletion vK w) ℝ≥0 :=
      localizedValued vK w hvKna
    ValuativeRel (LocalizedCompletion vK w) :=
  localizedCompletionFinitePlaceValuativeRel vK w hvKna

def

integerAlgebra

L94 ↗

LocalInductionInternal.integerAlgebra

Documentation

The canonical algebra of the localized completion over the completed base valuation ring.

Source context 10 commands

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

open scoped NumberField TensorProduct ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace LocalInductionInternal
variable (vK : AbsoluteValue K ℝ)
    (w : AbsoluteValueExtension vK L)

Lean source · full declaration

def integerAlgebra
    (hvKna : IsNonarchimedean (vK : K → ℝ)) :
    letI := extensionCompletionAlgebra vK w
    letI : SMul K w.1.Completion := extensionCompletionSMul vK w
    letI := completionAlgebra vK w
    letI : Valued vK.Completion ℝ≥0 := baseValued vK hvKna
    letI : ValuativeRel vK.Completion := baseValuativeRel vK hvKna
    letI : Valued (LocalizedCompletion vK w) ℝ≥0 :=
      localizedValued vK w hvKna
    letI : ValuativeRel (LocalizedCompletion vK w) :=
      localizedValuativeRel vK w hvKna
    Algebra 𝒪[vK.Completion] (LocalizedCompletion vK w) := by
  letI := extensionCompletionAlgebra vK w
  letI : SMul K w.1.Completion := extensionCompletionSMul vK w
  letI := completionAlgebra vK w
  letI : Valued vK.Completion ℝ≥0 := baseValued vK hvKna
  letI : ValuativeRel vK.Completion := baseValuativeRel vK hvKna
  letI : Valued (LocalizedCompletion vK w) ℝ≥0 :=
    localizedValued vK w hvKna
  letI : ValuativeRel (LocalizedCompletion vK w) :=
    localizedValuativeRel vK w hvKna
  exact Algebra.ofSubsemiring 𝒪[vK.Completion]

theorem

valuationHasExtension

L121 ↗

LocalInductionInternal.valuationHasExtension

Documentation

The canonical valuation-extension certificate for the integral local-induction completion pair.

Source context 11 commands

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

open scoped NumberField TensorProduct ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace LocalInductionInternal
variable (vK : AbsoluteValue K ℝ)
    (w : AbsoluteValueExtension vK L)
omit [NumberField K] [NumberField L] [FiniteDimensional K L]
    [IsGalois K L] in

Lean source · full declaration

theorem valuationHasExtension
    (hvKna : IsNonarchimedean (vK : K → ℝ)) :
    letI := extensionCompletionAlgebra vK w
    letI : SMul K w.1.Completion := extensionCompletionSMul vK w
    letI := completionAlgebra vK w
    letI : Valued vK.Completion ℝ≥0 := baseValued vK hvKna
    letI : ValuativeRel vK.Completion := baseValuativeRel vK hvKna
    letI : Valued (LocalizedCompletion vK w) ℝ≥0 :=
      localizedValued vK w hvKna
    letI : ValuativeRel (LocalizedCompletion vK w) :=
      localizedValuativeRel vK w hvKna
    Valuation.HasExtension
      (ValuativeRel.valuation vK.Completion)
      (ValuativeRel.valuation (LocalizedCompletion vK w)) :=
  localizedCompletionValuationHasExtension vK w hvKna

theorem

isIntegralClosure

L140 ↗

LocalInductionInternal.isIntegralClosure

Documentation

The canonical integral-closure certificate for the integral local-induction completion pair.

Source context 11 commands

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

open scoped NumberField TensorProduct ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open LocalClassFieldTheory
open LocalFieldTheory
variable
    {K : Type} {L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
namespace LocalInductionInternal
variable (vK : AbsoluteValue K ℝ)
    (w : AbsoluteValueExtension vK L)
omit [NumberField K] [NumberField L] [IsGalois K L] in

Lean source · full declaration

theorem isIntegralClosure
    (hvK : vK.IsNontrivial)
    (hvKna : IsNonarchimedean (vK : K → ℝ)) :
    letI := extensionCompletionAlgebra vK w
    letI : SMul K w.1.Completion := extensionCompletionSMul vK w
    letI := completionAlgebra vK w
    letI : Valued vK.Completion ℝ≥0 := baseValued vK hvKna
    letI : ValuativeRel vK.Completion := baseValuativeRel vK hvKna
    letI : Valued (LocalizedCompletion vK w) ℝ≥0 :=
      localizedValued vK w hvKna
    letI : ValuativeRel (LocalizedCompletion vK w) :=
      localizedValuativeRel vK w hvKna
    letI : Algebra 𝒪[vK.Completion] (LocalizedCompletion vK w) :=
      integerAlgebra vK w hvKna
    letI := valuationHasExtension vK w hvKna
    IsIntegralClosure
      𝒪[LocalizedCompletion vK w]
      𝒪[vK.Completion]
      (LocalizedCompletion vK w) :=
  localizedCompletionIsIntegralClosureWithExtension
    vK w hvK hvKna

Module documentation

Shared completion spine for integral local induction

Declarations