NYLL
Module

AmbientPrimeComparison.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FixedFieldIntrinsicReciprocity.AmbientPrimeComparison
3 declarations indexed from sourceView source ↗

Module documentation

Ambient prime comparison

The local Artin map and the ambient embedded norm-residue construction agree on norm classes and therefore agree pointwise.

Imports3
Imported by4

Declarations

theorem

exists_localArtin_ambientEmbedded_prime

L31 ↗
LocalClassFieldTheory.exists_localArtin_ambientEmbedded_prime
Documentation

Every abelianized Galois element is simultaneously represented by the local Artin map and by the ambient embedded norm-residue construction.

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
theorem
    exists_localArtin_ambientEmbedded_prime
    (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)) :
    ∃ x : Fˣ,
      localArtinMonoidHom F E x = z ∧
        ambientEmbeddedNormResidueAbelianElement K F E j e x = z
theorem

ambientEmbeddedNormResidueAbelianElement_eq_of_normClass_eq

L57 ↗
LocalClassFieldTheory.ambientEmbeddedNormResidueAbelianElement_eq_of_normClass_eq
Documentation

The ambient embedded norm-residue element depends only on the unit's norm class modulo norms from E.

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
theorem
    ambientEmbeddedNormResidueAbelianElement_eq_of_normClass_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)
    (a x : Fˣ)
    (h : normClass F E a = normClass F E x) :
    ambientEmbeddedNormResidueAbelianElement K F E j e a =
      ambientEmbeddedNormResidueAbelianElement K F E j e x
theorem

abelianLocalArtin_eq_ambientEmbeddedNormResidueSymbol_of_equiv

L194 ↗
LocalClassFieldTheory.abelianLocalArtin_eq_ambientEmbeddedNormResidueSymbol_of_equiv
Documentation

For an embedded finite abelian local extension, the abelian local Artin map agrees pointwise with the ambient norm-residue element transported through a separable-closure equivalence.

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
theorem
    abelianLocalArtin_eq_ambientEmbeddedNormResidueSymbol_of_equiv
    (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ˣ) :
    abelianLocalArtinMonoidHom F E a =
      ambientEmbeddedNormResidueElement K F E j e a

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