NYLL
Module

ConjugationNaturality.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.ConjugationNaturality
7 declarations indexed from sourceView source ↗

Module documentation

Conjugation naturality of finite local reciprocity

Two realizations of a finite Galois extension inside the fixed separable closure are related by conjugation. This module transports that conjugation to the actual Galois group, records the algebraic norm-residue square, and bundles the resulting map on the topological abelianization continuously.

Imports2
Imported by3

Declarations

def

abelianizedGaloisConjugationOfEmbeddings

L33 ↗
LocalClassFieldTheory.abelianizedGaloisConjugationOfEmbeddings
Documentation

Conjugation between two separable-closure realizations, transported to the abelianization of the actual relative Galois group.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def abelianizedGaloisConjugationOfEmbeddings
    (i j : L →ₐ[K] SeparableClosure K) :
    Abelianization (Gal(L / K)) ≃* Abelianization (Gal(L / K))
theorem

abelianizedGaloisConjugationOfEmbeddings_eq_refl

L42 ↗
LocalClassFieldTheory.abelianizedGaloisConjugationOfEmbeddings_eq_refl
Documentation

After both realizations are identified with the actual extension, the transported conjugation is the identity on the abelianization.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem abelianizedGaloisConjugationOfEmbeddings_eq_refl
    (i j : L →ₐ[K] SeparableClosure K) :
    abelianizedGaloisConjugationOfEmbeddings K L i j =
      MulEquiv.refl (Abelianization (Gal(L / K)))
theorem

concreteNormResidueSymbolOfEmbedding_conjugation

L64 ↗
LocalClassFieldTheory.concreteNormResidueSymbolOfEmbedding_conjugation
Documentation

Algebraic conjugation naturality for the norm-residue symbols computed from two explicit realizations of the same finite Galois extension.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem concreteNormResidueSymbolOfEmbedding_conjugation
    (i j : L →ₐ[K] SeparableClosure K)
    (D : ClassFormation.DegreeData (Gal(SeparableClosure K/K)))
    (v : ClassFormation.ValuationData D
      (galoisAmbientUnitsRep K (SeparableClosure K)))
    (hcf : ClassFormation.SatisfiesClassFieldAxiom
      (galoisAmbientUnitsRep K (SeparableClosure K))) :
    (abelianizedGaloisConjugationOfEmbeddings K L i j).toMonoidHom.comp
        (concreteNormResidueSymbolOfEmbedding K L i D v hcf) =
      concreteNormResidueSymbolOfEmbedding K L j D v hcf
theorem

localArtinMonoidHom_conjugation

L87 ↗
LocalClassFieldTheory.localArtinMonoidHom_conjugation
Documentation

Field-facing algebraic form of the second naturality diagram for the canonical local class formation.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
section LocalAlgebraic
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem localArtinMonoidHom_conjugation
    (i j : L →ₐ[K] SeparableClosure K) :
    (abelianizedGaloisConjugationOfEmbeddings K L i j).toMonoidHom.comp
        (concreteNormResidueSymbolOfEmbedding K L i
          (localResidueDatum K) (localHenselianValuation K)
          (separableClosureUnits_isClassFormation K)) =
      concreteNormResidueSymbolOfEmbedding K L j
        (localResidueDatum K) (localHenselianValuation K)
        (separableClosureUnits_isClassFormation K)
def

topologicalAbelianizationConjugationOfEmbeddings

L104 ↗
LocalClassFieldTheory.topologicalAbelianizationConjugationOfEmbeddings
Documentation

The conjugation of two realizations, bundled continuously on the topological abelianization of the finite Krull Galois group.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def topologicalAbelianizationConjugationOfEmbeddings
    (i j : L →ₐ[K] SeparableClosure K) :
    TopologicalAbelianization (Gal(L / K)) ≃ₜ*
      TopologicalAbelianization (Gal(L / K))
theorem

topologicalAbelianizationConjugationOfEmbeddings_toMonoidHom

L122 ↗
LocalClassFieldTheory.topologicalAbelianizationConjugationOfEmbeddings_toMonoidHom
Documentation

Forgetting topology identifies the bundled conjugation with the algebraic conjugation through the finite abelianization comparison.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem topologicalAbelianizationConjugationOfEmbeddings_toMonoidHom
    (i j : L →ₐ[K] SeparableClosure K) :
    (topologicalAbelianization_finite_equiv K L).symm.toMonoidHom.comp
        (topologicalAbelianizationConjugationOfEmbeddings K L i j).toMonoidHom =
      (abelianizedGaloisConjugationOfEmbeddings K L i j).toMonoidHom.comp
        (topologicalAbelianization_finite_equiv K L).symm.toMonoidHom
theorem

localArtinMap_conjugation

L138 ↗
LocalClassFieldTheory.localArtinMap_conjugation
Documentation

The continuous local Artin map is equivariant for conjugation between two realizations of the finite Galois extension.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
section LocalContinuous
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem localArtinMap_conjugation
    (i j : L →ₐ[K] SeparableClosure K) :
    (ContinuousMonoidHom.toContinuousMonoidHom
        (topologicalAbelianizationConjugationOfEmbeddings K L i j)).comp
        (localArtinMap K L) =
      localArtinMap K L

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