NYLL
Module

FiniteGaloisRealizationFinitePlace.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.FiniteGaloisRealizationFinitePlace
3 declarations indexed from sourceView source ↗

Module documentation

Finite places in the compatible Galois realization

This module extends a chosen finite place of L to the common rational separable closure and compares its decomposition data with the corresponding places and completions in the original number-field tower.

Imports1
Imported by2

Declarations

def

numberFieldTowerFinitePlaceExtensionToSeparableClosure

L45 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePlaceExtensionToSeparableClosure
Documentation

Extend a specified finite place of the compatible top number field to the common rational separable closure.

Its restriction to L is definitionally the supplied exact extension, so the resulting decomposition-group restriction lands at the specified place rather than at an unrelated conjugate.

Source context 12 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open AlgebraicNumberTheory
open AlgebraicNumberTheory.Valuations
open IsDedekindDomain
open LocalClassFieldTheory
open RamificationTheory
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · full declaration
def
    numberFieldTowerFinitePlaceExtensionToSeparableClosure
    (v : HeightOneSpectrum (𝓞 K))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L) :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v)
      (SeparableClosure ℚ) := by
  letI : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  letI : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  letI : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  letI : IsScalarTower ℚ L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopScalarTower L
  letI : Algebra.IsAlgebraic L (SeparableClosure ℚ) :=
    Algebra.IsAlgebraic.tower_top (K := ℚ) L
  exact
    w.extendToAlgebraicallyClosed
      (NumberField.HeightOneSpectrum.adicAbv K v)
      (RayClass.adicAbv_isNontrivial v)
theorem

numberFieldTowerFinitePlaceExtensionToSeparableClosure_algebraMap

L78 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePlaceExtensionToSeparableClosure_algebraMap
Documentation

The compatible separable-closure extension restricts to the specified finite-place extension on L.

Source context 13 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open AlgebraicNumberTheory
open AlgebraicNumberTheory.Valuations
open IsDedekindDomain
open LocalClassFieldTheory
open RamificationTheory
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · full declaration
theorem
    numberFieldTowerFinitePlaceExtensionToSeparableClosure_algebraMap
    (v : HeightOneSpectrum (𝓞 K))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L)
    (x : L) :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    (numberFieldTowerFinitePlaceExtensionToSeparableClosure
      K L v w).1
        (algebraMap L (SeparableClosure ℚ) x) =
      w.1 x := by
  let : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  let : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  let : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  let : IsScalarTower ℚ L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopScalarTower L
  let : Algebra.IsAlgebraic L (SeparableClosure ℚ) :=
    Algebra.IsAlgebraic.tower_top (K := ℚ) L
  exact
    AbsoluteValueExtension.extendToAlgebraicallyClosed_algebraMap
      (NumberField.HeightOneSpectrum.adicAbv K v)
      (RayClass.adicAbv_isNontrivial v) w x
theorem

numberFieldTowerFinitePlaceExtensionToSeparableClosure_restrict

L112 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePlaceExtensionToSeparableClosure_restrict
Documentation

Restricting the compatible separable-closure absolute value along the chosen top-field embedding recovers the supplied exact extension.

Source context 13 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open AlgebraicNumberTheory
open AlgebraicNumberTheory.Valuations
open IsDedekindDomain
open LocalClassFieldTheory
open RamificationTheory
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · full declaration
theorem
    numberFieldTowerFinitePlaceExtensionToSeparableClosure_restrict
    (v : HeightOneSpectrum (𝓞 K))
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v) L) :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    (numberFieldTowerFinitePlaceExtensionToSeparableClosure
        K L v w).1.comp
        (f := algebraMap L (SeparableClosure ℚ))
        (algebraMap L (SeparableClosure ℚ)).injective =
      w.1 := by
  let : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  let : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  let : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  ext x
  exact
    numberFieldTowerFinitePlaceExtensionToSeparableClosure_algebraMap
      K L v w x

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