Module

MathlibInterface.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.MathlibInterface

9 declarations indexed from sourceView source ↗

Module documentation

Mathlib-facing finite local class field theory

This is the implementation layer for the reader-facing local CFT module. It collects the existing finite, absolute, naturality, normalization, and existence results without renaming them or wrapping them in an existence structure.

Imports10

Imported by9

instance

localNormQuotientTopologicalSpace

L35 ↗

ClassFieldTheory.LocalCFT.localNormQuotientTopologicalSpace

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory.LocalCFT
open ClassFormation

Lean source · statement

instance localNormQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (LocalFieldTheory.NormQuotient K L)

instance

fieldNormQuotientTopologicalSpace

L42 ↗

ClassFieldTheory.LocalCFT.fieldNormQuotientTopologicalSpace

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory.LocalCFT
open ClassFormation
noncomputable local instance localNormQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (LocalFieldTheory.NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ LocalFieldTheory.localNormSubgroup K L)
  infer_instance

Lean source · statement

instance fieldNormQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [TopologicalSpace K] :
    TopologicalSpace (FieldNormQuotient K L)

theorem

finiteAbelianLocalExistence

L51 ↗

ClassFieldTheory.LocalCFT.finiteAbelianLocalExistence

Documentation

Finite abelian local extensions are classified, contravariantly, by open finite-index subgroups of Kˣ.

Source context 5 commands

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

noncomputable section
namespace ClassFieldTheory.LocalCFT
open ClassFormation
noncomputable local instance localNormQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (LocalFieldTheory.NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ LocalFieldTheory.localNormSubgroup K L)
  infer_instance
noncomputable local instance fieldNormQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [TopologicalSpace K] :
    TopologicalSpace (FieldNormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ fieldNormSubgroup K L)
  infer_instance

Lean source · statement

theorem finiteAbelianLocalExistence
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    ∀ H : LocalClassFieldTheory.OpenFiniteIndexSubgroup K,
      ∃ L : FiniteAbelianSubextension
          (LocalClassFieldTheory.intrinsicAbstractBase K),
        LocalClassFieldTheory.finiteAbelianNormSubgroupMap K L = H

theorem

finiteAbelianLocalExistence_orderIso

L61 ↗

ClassFieldTheory.LocalCFT.finiteAbelianLocalExistence_orderIso

Documentation

Order-isomorphism form of the finite abelian local existence theorem.

Source context 5 commands

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

noncomputable section
namespace ClassFieldTheory.LocalCFT
open ClassFormation
noncomputable local instance localNormQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (LocalFieldTheory.NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ LocalFieldTheory.localNormSubgroup K L)
  infer_instance
noncomputable local instance fieldNormQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [TopologicalSpace K] :
    TopologicalSpace (FieldNormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ fieldNormSubgroup K L)
  infer_instance

Lean source · statement

theorem finiteAbelianLocalExistence_orderIso
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    Nonempty
      (FiniteAbelianSubextension
          (LocalClassFieldTheory.intrinsicAbstractBase K) ≃o
        (LocalClassFieldTheory.OpenFiniteIndexSubgroup K)ᵒᵈ)

theorem

finiteAbelianLocalReciprocity

L72 ↗

ClassFieldTheory.LocalCFT.finiteAbelianLocalReciprocity

Documentation

Construction of the Artin map in the finite abelian local reciprocity theorem, expressed only through its mathematical universal properties.

Source context 5 commands

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

noncomputable section
namespace ClassFieldTheory.LocalCFT
open ClassFormation
noncomputable local instance localNormQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (LocalFieldTheory.NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ LocalFieldTheory.localNormSubgroup K L)
  infer_instance
noncomputable local instance fieldNormQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [TopologicalSpace K] :
    TopologicalSpace (FieldNormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ fieldNormSubgroup K L)
  infer_instance

Lean source · statement

theorem finiteAbelianLocalReciprocity
    (K L : Type)
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    ∃ artin : Kˣ →ₜ* (L ≃ₐ[K] L),
      Function.Surjective artin ∧
      ∀ x : Kˣ, artin x = 1 ↔ IsFieldNorm K L x

theorem

finiteAbelianLocalReciprocity_quotient

L90 ↗

ClassFieldTheory.LocalCFT.finiteAbelianLocalReciprocity_quotient

Documentation

The quotient form of finite abelian local reciprocity.

Source context 5 commands

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

noncomputable section
namespace ClassFieldTheory.LocalCFT
open ClassFormation
noncomputable local instance localNormQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (LocalFieldTheory.NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ LocalFieldTheory.localNormSubgroup K L)
  infer_instance
noncomputable local instance fieldNormQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [TopologicalSpace K] :
    TopologicalSpace (FieldNormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ fieldNormSubgroup K L)
  infer_instance

Lean source · statement

theorem finiteAbelianLocalReciprocity_quotient
    (K L : Type)
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    Nonempty
      (FieldNormQuotient K L ≃ₜ* (L ≃ₐ[K] L))

theorem

isOpen_fieldNormSubgroup

L102 ↗

ClassFieldTheory.LocalCFT.isOpen_fieldNormSubgroup

Documentation

The field-norm subgroup is open in the native topology on Kˣ.

Source context 5 commands

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

noncomputable section
namespace ClassFieldTheory.LocalCFT
open ClassFormation
noncomputable local instance localNormQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (LocalFieldTheory.NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ LocalFieldTheory.localNormSubgroup K L)
  infer_instance
noncomputable local instance fieldNormQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [TopologicalSpace K] :
    TopologicalSpace (FieldNormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ fieldNormSubgroup K L)
  infer_instance

Lean source · statement

theorem isOpen_fieldNormSubgroup
    (K L : Type)
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    IsOpen (fieldNormSubgroup K L : Set Kˣ)

theorem

fieldNormSubgroup_finiteIndex

L113 ↗

ClassFieldTheory.LocalCFT.fieldNormSubgroup_finiteIndex

Documentation

The field-norm subgroup has finite index, by finite local reciprocity.

Source context 5 commands

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

noncomputable section
namespace ClassFieldTheory.LocalCFT
open ClassFormation
noncomputable local instance localNormQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (LocalFieldTheory.NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ LocalFieldTheory.localNormSubgroup K L)
  infer_instance
noncomputable local instance fieldNormQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [TopologicalSpace K] :
    TopologicalSpace (FieldNormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ fieldNormSubgroup K L)
  infer_instance

Lean source · statement

theorem fieldNormSubgroup_finiteIndex
    (K L : Type)
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    (fieldNormSubgroup K L).FiniteIndex

theorem

fieldNormSubgroup_index_eq_finrank

L130 ↗

ClassFieldTheory.LocalCFT.fieldNormSubgroup_index_eq_finrank

Documentation

The norm-subgroup index equals the degree of the abelian extension.

Source context 5 commands

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

noncomputable section
namespace ClassFieldTheory.LocalCFT
open ClassFormation
noncomputable local instance localNormQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [TopologicalSpace K] :
    TopologicalSpace (LocalFieldTheory.NormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ LocalFieldTheory.localNormSubgroup K L)
  infer_instance
noncomputable local instance fieldNormQuotientTopologicalSpace
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [TopologicalSpace K] :
    TopologicalSpace (FieldNormQuotient K L) := by
  change TopologicalSpace (Kˣ ⧸ fieldNormSubgroup K L)
  infer_instance

Lean source · statement

theorem fieldNormSubgroup_index_eq_finrank
    (K L : Type)
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    (fieldNormSubgroup K L).index = Module.finrank K L

Module documentation

Mathlib-facing finite local class field theory

Declarations