NYLL
Module

AmbientPrimeWitnessComparison.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FixedFieldIntrinsicReciprocity.AmbientPrimeWitnessComparison
5 declarations indexed from sourceView source ↗

Module documentation

Local and ambient comparison for prime witnesses

The chosen ambient prime witness represents the prescribed abelianized Galois element both under the concrete local Artin map and under the ambient fixed-field norm-residue construction.

Imports4
Imported by3

Declarations

theorem

ambientEmbeddedPrimeWitness_local

L32 ↗
LocalClassFieldTheory.ambientEmbeddedPrimeWitness_local
Documentation

The chosen ambient prime witness maps to the prescribed abelianized Galois element under the concrete local Artin map.

Source context 5 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
Lean source · statement
theorem
    ambientEmbeddedPrimeWitness_local
    (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)
    (z : Abelianization Gal(E/F)) :
    localArtinMonoidHom F E
        (ambientEmbeddedPrimeWitness K F E j e z) =
      z
theorem

ambientEmbeddedPrimeWitness_symbol

L327 ↗
LocalClassFieldTheory.ambientEmbeddedPrimeWitness_symbol
Documentation

The chosen prime witness satisfies the ambient fixed-field norm-residue symbol formula.

Source context 5 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
Lean source · statement
theorem
    ambientEmbeddedPrimeWitness_symbol
    (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)
    (z : Abelianization Gal(E/F)) :
    ambientEmbeddedPrimeSymbolProperty K F E j e z
theorem

ambientEmbeddedPrimeTransportValue_eq_target

L639 ↗
LocalClassFieldTheory.ambientEmbeddedPrimeTransportValue_eq_target
Documentation

The transported ambient symbol of the chosen prime witness equals its ambient Frobenius target.

Source context 5 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
Lean source · statement
theorem
    ambientEmbeddedPrimeTransportValue_eq_target
    (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)
    (z : Abelianization Gal(E/F)) :
    ambientEmbeddedPrimeTransportValue K F E j e z =
      ambientEmbeddedPrimeTarget K F E j e z
theorem

ambientEmbeddedPrimeTarget_eq

L666 ↗
LocalClassFieldTheory.ambientEmbeddedPrimeTarget_eq
Documentation

The ambient Frobenius target recovers the original abelianized Galois element.

Source context 5 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
Lean source · statement
theorem
    ambientEmbeddedPrimeTarget_eq
    (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)
    (z : Abelianization Gal(E/F)) :
    ambientEmbeddedPrimeTarget K F E j e z = z
theorem

ambientEmbeddedPrimeWitness_ambient

L808 ↗
LocalClassFieldTheory.ambientEmbeddedPrimeWitness_ambient
Documentation

The ambient norm-residue value of the chosen prime witness is the prescribed abelianized Galois element.

Source context 5 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
Lean source · statement
theorem
    ambientEmbeddedPrimeWitness_ambient
    (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)
    (z : Abelianization Gal(E/F)) :
    ambientEmbeddedNormResidueAbelianElement K F E j e
        (ambientEmbeddedPrimeWitness K F E j e z) =
      z

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