NYLL
Module

FinitePlaceSeparableEmbedding.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FinitePlaceSeparableEmbedding
6 declarations indexed from sourceView source ↗

Module documentation

The actual global-to-local separable-closure embedding

The chosen algebraic localization embeds the global algebraic closure into the local separable closure. Its pointwise equivariance identifies the actual action used by the decomposition-group comparison. Two canonical scalar towers are each installed once; no valuation preservation is assumed.

Imports1
Imported by2

Declarations

instance

finitePlaceSeparableEmbeddingBaseAlgebra

L30 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceSeparableEmbeddingBaseAlgebra
Source context 9 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations HilbertRamification
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "Kv" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "w" => finitePlaceAbsoluteValueExtension F v
Lean source · statement
instance finitePlaceSeparableEmbeddingBaseAlgebra : Algebra F (SeparableClosure Kv)
instance

finitePlaceSeparableEmbeddingBaseTower

L32 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceSeparableEmbeddingBaseTower
Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations HilbertRamification
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "Kv" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "w" => finitePlaceAbsoluteValueExtension F v
local instance finitePlaceSeparableEmbeddingBaseAlgebra : Algebra F (SeparableClosure Kv) :=
  Algebra.compHom (SeparableClosure Kv) (algebraMap F Kv)
Lean source · statement
instance finitePlaceSeparableEmbeddingBaseTower : IsScalarTower F Kv (SeparableClosure Kv)
instance

finitePlaceSeparableEmbeddingAbsoluteAlgebra

L34 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceSeparableEmbeddingAbsoluteAlgebra
Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations HilbertRamification
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "Kv" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "w" => finitePlaceAbsoluteValueExtension F v
local instance finitePlaceSeparableEmbeddingBaseAlgebra : Algebra F (SeparableClosure Kv) :=
  Algebra.compHom (SeparableClosure Kv) (algebraMap F Kv)
local instance finitePlaceSeparableEmbeddingBaseTower : IsScalarTower F Kv (SeparableClosure Kv) :=
  IsScalarTower.of_algebraMap_eq' rfl
Lean source · statement
instance finitePlaceSeparableEmbeddingAbsoluteAlgebra : Algebra F w.1.Completion
instance

finitePlaceSeparableEmbeddingCompletionAlgebra

L36 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceSeparableEmbeddingCompletionAlgebra
Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations HilbertRamification
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "Kv" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "w" => finitePlaceAbsoluteValueExtension F v
local instance finitePlaceSeparableEmbeddingBaseAlgebra : Algebra F (SeparableClosure Kv) :=
  Algebra.compHom (SeparableClosure Kv) (algebraMap F Kv)
local instance finitePlaceSeparableEmbeddingBaseTower : IsScalarTower F Kv (SeparableClosure Kv) :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance finitePlaceSeparableEmbeddingAbsoluteAlgebra : Algebra F w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := F) w.1
Lean source · statement
instance finitePlaceSeparableEmbeddingCompletionAlgebra : Algebra Kv w.1.Completion
def

finitePlaceSeparableEmbedding

L40 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceSeparableEmbedding
Documentation

The selected global algebraic closure inside the local separable closure.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations HilbertRamification
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "Kv" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "w" => finitePlaceAbsoluteValueExtension F v
local instance finitePlaceSeparableEmbeddingBaseAlgebra : Algebra F (SeparableClosure Kv) :=
  Algebra.compHom (SeparableClosure Kv) (algebraMap F Kv)
local instance finitePlaceSeparableEmbeddingBaseTower : IsScalarTower F Kv (SeparableClosure Kv) :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance finitePlaceSeparableEmbeddingAbsoluteAlgebra : Algebra F w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := F) w.1
local instance finitePlaceSeparableEmbeddingCompletionAlgebra : Algebra Kv w.1.Completion :=
  AbsoluteValue.completionAlgebra (HeightOneSpectrum.adicAbv F v) w.1 w.2
Lean source · full declaration
def finitePlaceSeparableEmbedding : AlgebraicClosure F →ₐ[F] SeparableClosure Kv where
  toRingHom := (finitePlaceAlgebraicLocalizationAlgEquivSeparableClosure F v).toRingHom.comp
    (AbsoluteValue.toAlgebraicLocalization (HeightOneSpectrum.adicAbv F v) w.1 w.2)
  commutes' x := by
    change (finitePlaceAlgebraicLocalizationAlgEquivSeparableClosure F v)
      (AbsoluteValue.toAlgebraicLocalization (HeightOneSpectrum.adicAbv F v) w.1 w.2
        (algebraMap F (AlgebraicClosure F) x)) = _
    rw [AbsoluteValue.toAlgebraicLocalization_algebraMap]
    exact (finitePlaceAlgebraicLocalizationAlgEquivSeparableClosure F v).commutes
      (algebraMap F Kv x)
theorem

finitePlaceSeparableEmbedding_equivariant

L52 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceSeparableEmbedding_equivariant
Documentation

Pointwise compatibility with the actual decomposition-group comparison.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations HilbertRamification
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "Kv" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "w" => finitePlaceAbsoluteValueExtension F v
local instance finitePlaceSeparableEmbeddingBaseAlgebra : Algebra F (SeparableClosure Kv) :=
  Algebra.compHom (SeparableClosure Kv) (algebraMap F Kv)
local instance finitePlaceSeparableEmbeddingBaseTower : IsScalarTower F Kv (SeparableClosure Kv) :=
  IsScalarTower.of_algebraMap_eq' rfl
local instance finitePlaceSeparableEmbeddingAbsoluteAlgebra : Algebra F w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := F) w.1
local instance finitePlaceSeparableEmbeddingCompletionAlgebra : Algebra Kv w.1.Completion :=
  AbsoluteValue.completionAlgebra (HeightOneSpectrum.adicAbv F v) w.1 w.2
Lean source · statement
theorem finitePlaceSeparableEmbedding_equivariant
    (sigma : finitePlaceAbsoluteDecompositionGroup F v) (x : AlgebraicClosure F) :
    finitePlaceDecompositionGroupContinuousMulEquivSeparableAbsoluteGaloisGroup F v sigma
        (finitePlaceSeparableEmbedding F v x) =
      finitePlaceSeparableEmbedding F v (sigma.1 x)

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