Module

LocalAbsoluteData.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Existence.LocalAbsoluteData

6 declarations indexed from sourceView source ↗

Module documentation

Absolute data for finite local existence

This file isolates the common abstract Galois-theoretic realization of the absolute Galois group, its unit representation, and the ground-field fixing subgroup. Both the characteristic-zero and equal-characteristic existence arguments use these definitions.

Imports3

Imported by4

structure

OpenFiniteIndexSubgroup

L34 ↗

LocalClassFieldTheory.OpenFiniteIndexSubgroup

Documentation

An open finite-index subgroup of the ordinary topological group Kˣ.

This is a genuine public object rather than a transparent subtype alias: its topological and finite-index contracts remain available without exposing a particular nested-pair representation.

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 LocalClassFieldTheory

Lean source · full declaration

structure OpenFiniteIndexSubgroup
    (K : Type) [Field K] [TopologicalSpace K] where
  /-- The underlying subgroup of field units. -/
  subgroup : Subgroup Kˣ
  /-- The underlying subgroup is open in the unit-group topology. -/
  isOpen : IsOpen (subgroup : Set Kˣ)
  /-- The underlying subgroup has finite index. -/
  finiteIndex : subgroup.FiniteIndex

instance

(anonymous instance)

L48 ↗

Documentation

Provides this instance.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
namespace OpenFiniteIndexSubgroup
variable {K : Type} [Field K] [TopologicalSpace K]

Lean source · statement

instance : Coe (OpenFiniteIndexSubgroup K) (Subgroup Kˣ)

theorem

ext

L53 ↗

LocalClassFieldTheory.OpenFiniteIndexSubgroup.ext

Documentation

States the theorem ext.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
namespace OpenFiniteIndexSubgroup
variable {K : Type} [Field K] [TopologicalSpace K]

Lean source · statement

theorem ext {H H' : OpenFiniteIndexSubgroup K}
    (h : H.subgroup = H'.subgroup) : H = H'

instance

(anonymous instance)

L61 ↗

Documentation

Provides this instance.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
namespace OpenFiniteIndexSubgroup
variable {K : Type} [Field K] [TopologicalSpace K]

Lean source · statement

instance : PartialOrder (OpenFiniteIndexSubgroup K)

theorem

abstractFixedField_isGalois_of_base_normal

L69 ↗

LocalClassFieldTheory.abstractFixedField_isGalois_of_base_normal

Documentation

Normality over the abstract base fixing group makes the represented fixed field Galois over the concrete 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 LocalClassFieldTheory

Lean source · statement

theorem abstractFixedField_isGalois_of_base_normal
    (K : Type) [Field K]
    (H : ClosedSubgroup (Gal(SeparableClosure K/K)))
    (hnormal :
      (extensionSubgroup
        (baseField (Gal(SeparableClosure K/K))) H
        (le_baseField H)).Normal) :
    IsGalois K (abstractFixedField K (SeparableClosure K) H)

instance

intrinsicAbstractBase_index_finite

L109 ↗

LocalClassFieldTheory.intrinsicAbstractBase_index_finite

Documentation

The closed fixing group of the ground field is absolutely finite in the abstract Galois-theoretic sense (indeed, it is the full absolute Galois group).

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 LocalClassFieldTheory
variable (K : Type) [Field K]

Lean source · statement

instance intrinsicAbstractBase_index_finite :
    Finite ((baseField (intrinsicAbsoluteGalois K)).toSubgroup ⧸
      extensionSubgroup (baseField (intrinsicAbsoluteGalois K))
        (intrinsicAbstractBase K) (le_baseField (intrinsicAbstractBase K)))

Module documentation

Absolute data for finite local existence

Declarations

OpenFiniteIndexSubgroup

(anonymous instance)

ext

(anonymous instance)

abstractFixedField_isGalois_of_base_normal

intrinsicAbstractBase_index_finite