NYLL
Module

AmbientNormResidue.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FixedFieldIntrinsicReciprocity.AmbientNormResidue
9 declarations indexed from sourceView source ↗

Module documentation

Ambient embedded norm-residue values

This module defines the ambient fixed-field norm-residue value attached to a unit of the intrinsically presented base field, both before and after identifying the abelianization of an abelian Galois group with the group itself.

Imports3
Imported by3

Declarations

abbrev

ambientEmbeddedSeparableClosureEquiv

L33 ↗
LocalClassFieldTheory.ambientEmbeddedSeparableClosureEquiv
Documentation

The separable-closure equivalence used to compare the intrinsic extension over F with its realization inside the ambient separable closure of K.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
open scoped IsMulCommutative
Lean source · statement
abbrev ambientEmbeddedSeparableClosureEquiv
    (K F E : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field F] [ValuativeRel F] [TopologicalSpace F]
    [IsNonarchimedeanLocalField F]
    [Field E] [Algebra K F] [Algebra F E] [Algebra K E]
    [IsScalarTower K F E]
    [FiniteDimensional K F] [Algebra.IsSeparable K F]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation F)]
    [FiniteDimensional F E] [IsGalois F E]
    (j : E →ₐ[K] SeparableClosure K)
structure

AmbientEmbeddedFixedFieldPresentation

L57 ↗
LocalClassFieldTheory.AmbientEmbeddedFixedFieldPresentation
Documentation

A finite fixed-field presentation of an embedded finite Galois extension.

The object records the actual ambient fixed-field quotient, its realization of the embedded base field, and the quotient map to the original Galois group. It is the common interface for calculations that use the ambient norm-residue value without unfolding the construction of that presentation.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
open scoped IsMulCommutative
Lean source · full declaration
structure AmbientEmbeddedFixedFieldPresentation
    (K F E : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field F] [ValuativeRel F] [TopologicalSpace F]
    [IsNonarchimedeanLocalField F]
    [Field E] [Algebra K F] [Algebra F E] [Algebra K E]
    [IsScalarTower K F E]
    [FiniteDimensional K F] [Algebra.IsSeparable K F]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation F)]
    [FiniteDimensional F E] [IsGalois F E]
    (j : E →ₐ[K] SeparableClosure K) where
  /-- The given base field embedded in the ambient separable closure. -/
  baseEmbedding : F →ₐ[K] SeparableClosure K
  /-- The finite ambient fixed field representing the embedded base field. -/
  base : FiniteAbstractField Gal(SeparableClosure K / K)
  /-- The finite Galois ambient fixed-field extension representing `E / F`. -/
  extension : FiniteGaloisSubextension base.field
  /-- The base embedding is induced by the embedding of the top field. -/
  baseEmbedding_eq :
    baseEmbedding = j.comp (IsScalarTower.toAlgHom K F E)
  /-- The ambient base subgroup fixes precisely the range of the base embedding. -/
  base_field_eq :
    base.field =
      closedFixingSubgroup K (SeparableClosure K)
        (AlgHom.fieldRange baseEmbedding)
  /-- The ambient top subgroup fixes precisely the range of the top embedding. -/
  extension_field_eq :
    extension.field =
      closedFixingSubgroup K (SeparableClosure K)
        (AlgHom.fieldRange j)
  /-- The actual equivalence from the given base field to its ambient fixed field. -/
  baseEquiv :
    F ≃ₐ[K] abstractFixedField K (SeparableClosure K) base.field
  /-- The base-field equivalence realizes the chosen ambient embedding. -/
  baseEquiv_apply (x : F) :
    ((baseEquiv x :
      abstractFixedField K (SeparableClosure K) base.field) :
        SeparableClosure K) =
      baseEmbedding x
  /-- The actual quotient equivalence to the original Galois group. -/
  quotientEquiv : extension.extensionQuotient ≃* Gal(E / F)
  /-- The quotient equivalence acts through the supplied ambient embedding. -/
  quotientEquiv_mk_apply
      (sigma : base.field.toSubgroup) (x : E) :
    j (quotientEquiv (extension.extensionQuotientMk sigma) x) =
      sigma.1 (j x)
def

fixedFieldQuotientEquiv

L110 ↗
LocalClassFieldTheory.AmbientEmbeddedFixedFieldPresentation.fixedFieldQuotientEquiv
Documentation

The canonical quotient equivalence from an ambient finite fixed-field extension to the Galois group of its relative fixed field.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
open scoped IsMulCommutative
namespace AmbientEmbeddedFixedFieldPresentation
Lean source · statement
def fixedFieldQuotientEquiv
    {K F E : Type}
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field F] [ValuativeRel F] [TopologicalSpace F]
    [IsNonarchimedeanLocalField F]
    [Field E] [Algebra K F] [Algebra F E] [Algebra K E]
    [IsScalarTower K F E]
    [FiniteDimensional K F] [Algebra.IsSeparable K F]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation F)]
    [FiniteDimensional F E] [IsGalois F E]
    {j : E →ₐ[K] SeparableClosure K}
    (P : AmbientEmbeddedFixedFieldPresentation K F E j) :
    P.extension.extensionQuotient ≃*
      Gal(abstractRelativeFixedField K (SeparableClosure K)
        P.extension.below /
        abstractFixedField K (SeparableClosure K) P.base.field)
def

abelianizedTransport

L136 ↗
LocalClassFieldTheory.AmbientEmbeddedFixedFieldPresentation.abelianizedTransport
Documentation

The actual additive equivalence obtained by transporting abelianized relative fixed-field Galois elements through an ambient fixed-field presentation.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
open scoped IsMulCommutative
namespace AmbientEmbeddedFixedFieldPresentation
Lean source · statement
def abelianizedTransport
    {K F E : Type}
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field F] [ValuativeRel F] [TopologicalSpace F]
    [IsNonarchimedeanLocalField F]
    [Field E] [Algebra K F] [Algebra F E] [Algebra K E]
    [IsScalarTower K F E]
    [FiniteDimensional K F] [Algebra.IsSeparable K F]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation F)]
    [FiniteDimensional F E] [IsGalois F E]
    {j : E →ₐ[K] SeparableClosure K}
    (P : AmbientEmbeddedFixedFieldPresentation K F E j) :
    Additive
      (Abelianization
        Gal(abstractRelativeFixedField K (SeparableClosure K)
          P.extension.below /
          abstractFixedField K (SeparableClosure K) P.base.field)) ≃+
      Additive (Abelianization Gal(E / F))
def

normResidueAbelianElement

L161 ↗
LocalClassFieldTheory.AmbientEmbeddedFixedFieldPresentation.normResidueAbelianElement
Documentation

Evaluate the ambient fixed-field norm-residue construction using this presentation's actual finite quotient and base-field realization.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
open scoped IsMulCommutative
namespace AmbientEmbeddedFixedFieldPresentation
Lean source · statement
def normResidueAbelianElement
    {K F E : Type}
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field F] [ValuativeRel F] [TopologicalSpace F]
    [IsNonarchimedeanLocalField F]
    [Field E] [Algebra K F] [Algebra F E] [Algebra K E]
    [IsScalarTower K F E]
    [FiniteDimensional K F] [Algebra.IsSeparable K F]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation F)]
    [FiniteDimensional F E] [IsGalois F E]
    {j : E →ₐ[K] SeparableClosure K}
    (P : AmbientEmbeddedFixedFieldPresentation K F E j)
    (a : Fˣ) : Abelianization Gal(E / F)
theorem

normResidueAbelianElement_apply

L206 ↗
LocalClassFieldTheory.AmbientEmbeddedFixedFieldPresentation.normResidueAbelianElement_apply
Documentation

The presentation-level evaluation formula for the ambient norm-residue value. It exposes only the actual finite quotient equivalences carried by the presentation.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
open scoped IsMulCommutative
namespace AmbientEmbeddedFixedFieldPresentation
Lean source · full declaration
theorem normResidueAbelianElement_apply
    {K F E : Type}
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field F] [ValuativeRel F] [TopologicalSpace F]
    [IsNonarchimedeanLocalField F]
    [Field E] [Algebra K F] [Algebra F E] [Algebra K E]
    [IsScalarTower K F E]
    [FiniteDimensional K F] [Algebra.IsSeparable K F]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation F)]
    [FiniteDimensional F E] [IsGalois F E]
    {j : E →ₐ[K] SeparableClosure K}
    (P : AmbientEmbeddedFixedFieldPresentation K F E j)
    (a : Fˣ) :
    letI : (extensionSubgroup
        P.base.field P.extension.field P.extension.below).Normal :=
      P.extension.normal
    letI : Finite
        (P.base.field.toSubgroup ⧸
          extensionSubgroup P.base.field P.extension.field
            P.extension.below) :=
      P.extension.finite
    letI : Finite
        ((baseField
          Gal(SeparableClosure K / K)).toSubgroup ⧸
          extensionSubgroup
            (baseField Gal(SeparableClosure K / K))
            P.base.field (le_baseField P.base.field)) :=
      P.base.finite
    P.normResidueAbelianElement a =
      P.quotientEquiv.abelianizationCongr
        (P.fixedFieldQuotientEquiv.abelianizationCongr.symm
          (Additive.toMul
            (abstractFixedFieldNormResidueSymbol
              K (SeparableClosure K)
              (localResidueDatum K)
              (localHenselianValuation K)
              (separableClosureUnits_isClassFormation K)
              P.base.field P.extension.field P.extension.below
              (Additive.ofMul
                (Units.mapEquiv P.baseEquiv.toMulEquiv a))))) :=
  rfl
def

ambientEmbeddedFixedFieldPresentation

L254 ↗
LocalClassFieldTheory.ambientEmbeddedFixedFieldPresentation
Documentation

The canonical ambient fixed-field presentation of an embedded finite Galois local extension.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
open scoped IsMulCommutative
Lean source · statement
def ambientEmbeddedFixedFieldPresentation
    (K F E : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field F] [ValuativeRel F] [TopologicalSpace F]
    [IsNonarchimedeanLocalField F]
    [Field E] [Algebra K F] [Algebra F E] [Algebra K E]
    [IsScalarTower K F E]
    [FiniteDimensional K F] [Algebra.IsSeparable K F]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation F)]
    [FiniteDimensional F E] [IsGalois F E]
    (j : E →ₐ[K] SeparableClosure K)
    (e : ambientEmbeddedSeparableClosureEquiv K F E j) :
    AmbientEmbeddedFixedFieldPresentation K F E j
def

ambientEmbeddedNormResidueAbelianElement

L345 ↗
LocalClassFieldTheory.ambientEmbeddedNormResidueAbelianElement
Documentation

The abelianized ambient fixed-field norm-residue value attached to a unit of the intrinsically presented base field.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
open scoped IsMulCommutative
Lean source · statement
def ambientEmbeddedNormResidueAbelianElement
    (K F E : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field F] [ValuativeRel F] [TopologicalSpace F]
    [IsNonarchimedeanLocalField F]
    [Field E] [Algebra K F] [Algebra F E] [Algebra K E]
    [IsScalarTower K F E]
    [FiniteDimensional K F] [Algebra.IsSeparable K F]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation F)]
    [FiniteDimensional F E] [IsGalois F E]
    (j : E →ₐ[K] SeparableClosure K)
    (e : ambientEmbeddedSeparableClosureEquiv K F E j)
    (a : Fˣ) : Abelianization Gal(E / F)
def

ambientEmbeddedNormResidueElement

L364 ↗
LocalClassFieldTheory.ambientEmbeddedNormResidueElement
Documentation

The ambient fixed-field norm-residue value in Gal(E/F), obtained from its abelianized value using the canonical equivalence for an abelian extension.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
open scoped ValuativeRel
open scoped IsMulCommutative
Lean source · statement
def ambientEmbeddedNormResidueElement
    (K F E : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field F] [ValuativeRel F] [TopologicalSpace F]
    [IsNonarchimedeanLocalField F]
    [Field E] [Algebra K F] [Algebra F E] [Algebra K E]
    [IsScalarTower K F E]
    [FiniteDimensional K F] [Algebra.IsSeparable K F]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation F)]
    [FiniteDimensional F E] [IsAbelianGalois F E]
    (j : E →ₐ[K] SeparableClosure K)
    (e : ambientEmbeddedSeparableClosureEquiv K F E j)
    (a : Fˣ) : Gal(E / F)

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