Module

OrderReversal.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Existence.OrderReversal

5 declarations indexed from sourceView source ↗

Module documentation

Field-facing order reversal for finite abelian extensions

This module realizes a finite abelian extension inside a fixed separable closure and packages it as an abstract finite abelian subextension. It then transports the abstract order reversal for norm subgroups back to ordinary field norms. The final lemmas record the standard open subgroups contained in the norm subgroup of a finite abelian extension.

Imports6

Imported by8

def

finiteAbelianAbstractExtensionOfEmbedding

L35 ↗

LocalClassFieldTheory.finiteAbelianAbstractExtensionOfEmbedding

Documentation

A finite abelian extension, realized by an explicit embedding in the fixed separable closure, as an abstract finite abelian subextension.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation

Lean source · full declaration

def finiteAbelianAbstractExtensionOfEmbedding
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (i : L →ₐ[K] SeparableClosure K) :
    FiniteAbelianSubextension (intrinsicAbstractBase K) where
  toFiniteGaloisExtension :=
    finiteGaloisAbstractExtensionOfEmbedding K L i
  commutative := by
    change IsMulCommutative
      ((closedFixingSubgroup K (SeparableClosure K)
          (⊥ : IntermediateField K (SeparableClosure K))).toSubgroup ⧸
        extensionSubgroup
          (closedFixingSubgroup K (SeparableClosure K)
            (⊥ : IntermediateField K (SeparableClosure K)))
          (finiteGaloisClosedFixingSubgroupOfEmbedding K L i)
          (fixingSubgroupLeBase K (SeparableClosure K)
            (finiteGaloisFieldRangeOfEmbedding K L i)))
    let e := finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding K L i
    exact
      { is_comm.comm := fun x y => by
          apply e.injective
          simp only [map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm (e x) (e y) }

theorem

map_finiteAbelianAbstractExtension_normSubgroup_eq

L64 ↗

LocalClassFieldTheory.map_finiteAbelianAbstractExtension_normSubgroup_eq

Documentation

Under the canonical identification of the abstract base fixed units with Kˣ, the abstract norm subgroup of an embedded finite abelian extension is its ordinary field-norm subgroup.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation

Lean source · statement

theorem map_finiteAbelianAbstractExtension_normSubgroup_eq
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (i : L →ₐ[K] SeparableClosure K) :
    ((finiteAbelianAbstractExtensionOfEmbedding K L i).normSubgroup
        (intrinsicAbsoluteUnits K)).map
      (baseUnitsEquivGaloisAmbientFixed K (SeparableClosure K)).symm.toAddMonoidHom =
      additiveNormSubgroup K L

theorem

nonempty_algHom_of_normSubgroup_le

L85 ↗

LocalClassFieldTheory.nonempty_algHom_of_normSubgroup_le

Documentation

Reverse inclusion of ordinary norm subgroups produces an embedding of finite abelian extensions over the common local base field.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation

Lean source · statement

theorem nonempty_algHom_of_normSubgroup_le
    (K L M : Type) [Field K] [Field L] [Field M]
    [Algebra K L] [Algebra K M]
    [FiniteDimensional K L] [FiniteDimensional K M]
    [IsAbelianGalois K L] [IsAbelianGalois K M]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (h : localNormSubgroup K M ≤ localNormSubgroup K L) :
    Nonempty (L →ₐ[K] M)

theorem

exists_uniformizerPrincipalSubgroup_le_normSubgroup

L132 ↗

LocalClassFieldTheory.exists_uniformizerPrincipalSubgroup_le_normSubgroup

Documentation

For a prescribed prime element, the norm subgroup of a finite abelian extension contains a standard subgroup ⟨ϖᵈ⟩ Uⁿ for some positive integers d and n.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation

Lean source · statement

theorem exists_uniformizerPrincipalSubgroup_le_normSubgroup
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (ϖ : Kˣ) :
    ∃ d n : ℕ, 0 < d ∧ 1 ≤ n ∧
      LocalFieldTheory.uniformizerPrincipalSubgroup K ϖ d n ≤
        localNormSubgroup K L

theorem

exists_uniformizerPrincipalSubgroup_one_le_normSubgroup

L168 ↗

LocalClassFieldTheory.exists_uniformizerPrincipalSubgroup_one_le_normSubgroup

Documentation

If the prescribed prime element is itself a norm, the norm subgroup contains a standard subgroup with uniformizer exponent one.

Source context 4 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation

Lean source · statement

theorem exists_uniformizerPrincipalSubgroup_one_le_normSubgroup
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (ϖ : Kˣ) (hϖ : ϖ ∈ localNormSubgroup K L) :
    ∃ n : ℕ, 1 ≤ n ∧
      LocalFieldTheory.uniformizerPrincipalSubgroup K ϖ 1 n ≤
        localNormSubgroup K L

Module documentation

Field-facing order reversal for finite abelian extensions

Declarations

finiteAbelianAbstractExtensionOfEmbedding

map_finiteAbelianAbstractExtension_normSubgroup_eq

nonempty_algHom_of_normSubgroup_le

exists_uniformizerPrincipalSubgroup_le_normSubgroup

exists_uniformizerPrincipalSubgroup_one_le_normSubgroup