Module

AmbientPrimeWitness.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FixedFieldIntrinsicReciprocity.AmbientPrimeWitness

3 declarations indexed from sourceView source ↗

Module documentation

Ambient prime witnesses

This module constructs the ambient norm-residue value, a valuation-one prime witness for each abelianized Galois element, and the corresponding ambient Frobenius target.

Imports3

Imported by3

theorem

abelianizationCongr_symm_eq_primeTarget

L31 ↗

LocalClassFieldTheory.abelianizationCongr_symm_eq_primeTarget

Documentation

Transporting an identified abelianized prime value back through one quotient equivalence and forward through another preserves its 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 abelianizationCongr_symm_eq_primeTarget
    {Q₀ G₀ G : Type}
    [Group Q₀] [Group G₀] [Group G]
    (q₀ : Q₀ ≃* G₀)
    (qE : Q₀ ≃* G)
    (qAmbient : Q₀)
    (r : Additive (Abelianization G₀))
    (hprime :
      r =
        Additive.ofMul
          (q₀.abelianizationCongr
            (Abelianization.of qAmbient))) :
    qE.abelianizationCongr
        (q₀.abelianizationCongr.symm
          (Additive.toMul r)) =
      qE.abelianizationCongr
        (Abelianization.of qAmbient)

def

ambientEmbeddedPrimeWitness

L70 ↗

LocalClassFieldTheory.ambientEmbeddedPrimeWitness

Documentation

A prime-norm unit in the intrinsic base field chosen from a Frobenius lift of an 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

def ambientEmbeddedPrimeWitness
    (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)) : Fˣ

def

ambientEmbeddedPrimeTarget

L261 ↗

LocalClassFieldTheory.ambientEmbeddedPrimeTarget

Documentation

The ambient abelianized Frobenius target associated with the same chosen intrinsic Frobenius lift as the prime witness.

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

def ambientEmbeddedPrimeTarget
    (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)) :
    Abelianization Gal(E / F)

Module documentation

Ambient prime witnesses

Declarations

abelianizationCongr_symm_eq_primeTarget

ambientEmbeddedPrimeWitness

ambientEmbeddedPrimeTarget