Module

SemilinearNaturality.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.SemilinearNaturality

9 declarations indexed from sourceView source ↗

Module documentation

Semilinear naturality of finite local reciprocity

The actual finite local Artin map is natural when both the base local field and the finite abelian extension are replaced by compatible field equivalences. The proof realizes the base equivalence as a degree-one vertical extension and applies the genuine norm--restriction theorem.

Imports1

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FixedFieldIntrinsicReciprocity.NormRestriction

Imported by8

def

SemilinearValuationCompatible

L31 ↗

LocalClassFieldTheory.SemilinearValuationCompatible

Documentation

A base-field equivalence preserves the chosen valuations. Keeping the transported Algebra structure behind this opaque predicate prevents every consumer of semilinear Artin naturality from storing a dependent letI in its public theorem type.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open scoped ValuativeRel

Lean source · statement

def SemilinearValuationCompatible
    (K K' : Type)
    [Field K] [ValuativeRel K]
    [Field K'] [ValuativeRel K']
    (eK : K ≃+* K') : Prop

structure

SemilinearBaseCompatible

L43 ↗

LocalClassFieldTheory.SemilinearBaseCompatible

Documentation

A certificate that an extension-field equivalence restricts to the specified base-field equivalence. Its generic head is cheap to expose in public APIs even when the concrete algebra towers are large.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open scoped ValuativeRel

Lean source · full declaration

structure SemilinearBaseCompatible
    (K K' L L' : Type)
    [Field K] [Field K'] [Field L] [Field L']
    [Algebra K L] [Algebra K' L']
    (eK : K ≃+* K') (eL : L ≃+* L') : Prop where
  /-- The extension equivalence agrees with the base equivalence. -/
  commutes : ∀ x : K,
    eL (algebraMap K L x) =
      algebraMap K' L' (eK x)

def

semilinearGaloisGroupCongr

L56 ↗

LocalClassFieldTheory.semilinearGaloisGroupCongr

Documentation

Conjugation of relative Galois groups by compatible equivalences of the base and extension fields. Compatibility is semilinear: eL restricts to eK on the base field.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open scoped ValuativeRel

Lean source · statement

def semilinearGaloisGroupCongr
    (K K' L L' : Type)
    [Field K] [Field K'] [Field L] [Field L']
    [Algebra K L] [Algebra K' L']
    (eK : K ≃+* K') (eL : L ≃+* L')
    (hcomm : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x)) :
    Gal(L / K) ≃* Gal(L' / K')

theorem

semilinearGaloisGroupCongr_apply_equiv

L111 ↗

LocalClassFieldTheory.semilinearGaloisGroupCongr_apply_equiv

Documentation

Semilinear conjugation intertwines the two actions through the target field equivalence.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open scoped ValuativeRel

Lean source · statement

theorem semilinearGaloisGroupCongr_apply_equiv
    (K K' L L' : Type)
    [Field K] [Field K'] [Field L] [Field L']
    [Algebra K L] [Algebra K' L']
    (eK : K ≃+* K') (eL : L ≃+* L')
    (hcomm : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x))
    (σ : Gal(L / K)) (x : L) :
    semilinearGaloisGroupCongr K K' L L' eK eL hcomm σ (eL x) =
      eL (σ x)

theorem

conjugation_apply

L127 ↗

LocalClassFieldTheory.SemilinearBaseCompatible.conjugation_apply

Documentation

Evaluate certified semilinear conjugation on an element of the extension field.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open scoped ValuativeRel

Lean source · statement

theorem SemilinearBaseCompatible.conjugation_apply
    {K K' L L' : Type}
    [Field K] [Field K'] [Field L] [Field L']
    [Algebra K L] [Algebra K' L']
    {eK : K ≃+* K'} {eL : L ≃+* L'}
    (h : SemilinearBaseCompatible K K' L L' eK eL)
    (sigma : Gal(L/K)) (x : L) :
    semilinearGaloisGroupCongr
        K K' L L' eK eL h.commutes sigma (eL x) =
      eL (sigma x)

theorem

abelianLocalArtinMonoidHom_semilinear_conjugation

L147 ↗

LocalClassFieldTheory.abelianLocalArtinMonoidHom_semilinear_conjugation

Documentation

The actual finite abelian local Artin map commutes with simultaneous semilinear equivalences of the base local field and the target extension.

The valuation-extension condition says that the local-field valuation on K', pulled back through eK, is the valuation on K. It is the genuine valued-field compatibility needed by norm--restriction, rather than an assumption of the desired Artin equality.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open scoped ValuativeRel

Lean source · statement

theorem abelianLocalArtinMonoidHom_semilinear_conjugation
    (K K' L L' : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field K'] [ValuativeRel K'] [TopologicalSpace K']
    [IsNonarchimedeanLocalField K']
    [Field L] [Field L']
    [Algebra K L] [Algebra K' L']
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [FiniteDimensional K' L'] [IsAbelianGalois K' L']
    (eK : K ≃+* K') (eL : L ≃+* L')
    (hcomm : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x))
    (hExt : SemilinearValuationCompatible K K' eK) :
    (semilinearGaloisGroupCongr K K' L L' eK eL hcomm).toMonoidHom.comp
        (abelianLocalArtinMonoidHom K L) =
      (abelianLocalArtinMonoidHom K' L').comp
        (Units.map eK.toMonoidHom)

theorem

abelianLocalArtinMonoidHom_semilinear_conjugation_apply

L260 ↗

LocalClassFieldTheory.abelianLocalArtinMonoidHom_semilinear_conjugation_apply

Documentation

Pointwise Galois-automorphism form of semilinear naturality for the abelian local Artin map. Concrete consumers should use this opaque generic boundary instead of specializing DFunLike.congr_fun to a large dependent local-field instance tower.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open scoped ValuativeRel

Lean source · statement

theorem abelianLocalArtinMonoidHom_semilinear_conjugation_apply
    (K K' L L' : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field K'] [ValuativeRel K'] [TopologicalSpace K']
    [IsNonarchimedeanLocalField K']
    [Field L] [Field L']
    [Algebra K L] [Algebra K' L']
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [FiniteDimensional K' L'] [IsAbelianGalois K' L']
    (eK : K ≃+* K') (eL : L ≃+* L')
    (hcomm : ∀ x : K,
      eL (algebraMap K L x) = algebraMap K' L' (eK x))
    (hExt : SemilinearValuationCompatible K K' eK)
    (u : Kˣ) :
    semilinearGaloisGroupCongr K K' L L' eK eL hcomm
        (abelianLocalArtinMonoidHom K L u) =
      abelianLocalArtinMonoidHom K' L'
        (Units.map eK.toMonoidHom u)

theorem

abelianLocalArtinMonoidHom_eq_one_of_semilinear

L286 ↗

LocalClassFieldTheory.abelianLocalArtinMonoidHom_eq_one_of_semilinear

Documentation

Triviality transports backwards through a semilinear equivalence of local Artin data. Keeping the injectivity calculation generic prevents concrete finite-place instance towers from entering consumer proof terms.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open scoped ValuativeRel

Lean source · statement

theorem abelianLocalArtinMonoidHom_eq_one_of_semilinear
    (K K' L L' : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field K'] [ValuativeRel K'] [TopologicalSpace K']
    [IsNonarchimedeanLocalField K']
    [Field L] [Field L']
    [Algebra K L] [Algebra K' L']
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [FiniteDimensional K' L'] [IsAbelianGalois K' L']
    (eK : K ≃+* K') (eL : L ≃+* L')
    (hcomm : ∀ x : K,
      eL (algebraMap K L x) = algebraMap K' L' (eK x))
    (hExt : SemilinearValuationCompatible K K' eK)
    (u : Kˣ)
    (htrivial :
      abelianLocalArtinMonoidHom K' L'
          (Units.map eK.toMonoidHom u) = 1) :
    abelianLocalArtinMonoidHom K L u = 1

theorem

abelianLocalArtinMonoidHom_semilinear_action

L323 ↗

LocalClassFieldTheory.abelianLocalArtinMonoidHom_semilinear_action

Documentation

Pointwise form of semilinear naturality for the abelian local Artin map.

This theorem keeps the equality of Galois automorphisms and its dependent instance tower behind an opaque generic boundary. Concrete consumers can transport the action on one element without specializing and then reducing the full monoid-hom equality.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory
open scoped ValuativeRel

Lean source · statement

theorem abelianLocalArtinMonoidHom_semilinear_action
    (K K' L L' : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field K'] [ValuativeRel K'] [TopologicalSpace K']
    [IsNonarchimedeanLocalField K']
    [Field L] [Field L']
    [Algebra K L] [Algebra K' L']
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [FiniteDimensional K' L'] [IsAbelianGalois K' L']
    (eK : K ≃+* K') (eL : L ≃+* L')
    (hcomm : ∀ x : K,
      eL (algebraMap K L x) =
        algebraMap K' L' (eK x))
    (hExt : SemilinearValuationCompatible K K' eK)
    (u : Kˣ) (z : L) :
    eL (abelianLocalArtinMonoidHom K L u z) =
      abelianLocalArtinMonoidHom K' L'
        (Units.map eK.toMonoidHom u) (eL z)

Module documentation

Semilinear naturality of finite local reciprocity

Declarations