Module

InfiniteContinuity.lean

Nyll.GaloisCohomology.Kummer.Concrete.InfiniteContinuity

14 declarations indexed from sourceView source ↗

Module documentation

continuity of Kummer characters for infinite extensions

For an infinite Galois extension Ω/K, a Kummer character attached to a chosen root β is already determined on the finite Galois normal closure of K(β). Equivalently, its kernel contains the fixing subgroup of that finite Galois intermediate field. This makes the kernel open in the Krull topology and proves continuity into the discrete group of n-th roots of unity.

The final construction descends these continuous characters through the ambient-power quotient Δ / (Δ ∩ Kˣⁿ). No surjectivity or lattice correspondence is asserted here.

Imports2

Mathlib.Topology.Algebra.ContinuousMonoidHom
Nyll.GaloisCohomology.Kummer.Concrete.FiniteCharacterEquiv

Imported by3

def

DiscreteNthRootsSubgroup

L35 ↗

KummerTheory.DiscreteNthRootsSubgroup

Documentation

The group μₙ(L) equipped explicitly with the discrete topology used for continuous characters in the infinite form of the finite Kummer character equivalence.

Source context 4 commands

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

noncomputable section
namespace KummerTheory
open scoped Topology
open Filter

Lean source · statement

def DiscreteNthRootsSubgroup (L : Type*) [Field L] (n : ℕ)

instance

(anonymous instance)

L43 ↗

Documentation

The discrete copy of the roots-of-unity subgroup retains its commutative group structure.

Source context 6 commands

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

noncomputable section
namespace KummerTheory
open scoped Topology
open Filter
namespace DiscreteNthRootsSubgroup
variable (L : Type*) [Field L] (n : ℕ)

Lean source · statement

instance : CommGroup (DiscreteNthRootsSubgroup L n)

instance

(anonymous instance)

L47 ↗

Documentation

The discrete roots-of-unity copy is equipped with the bottom topology.

Source context 6 commands

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

noncomputable section
namespace KummerTheory
open scoped Topology
open Filter
namespace DiscreteNthRootsSubgroup
variable (L : Type*) [Field L] (n : ℕ)

Lean source · statement

instance : TopologicalSpace (DiscreteNthRootsSubgroup L n)

instance

(anonymous instance)

L50 ↗

Documentation

The bottom topology makes the roots-of-unity copy discrete.

Source context 6 commands

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

noncomputable section
namespace KummerTheory
open scoped Topology
open Filter
namespace DiscreteNthRootsSubgroup
variable (L : Type*) [Field L] (n : ℕ)

Lean source · statement

instance : DiscreteTopology (DiscreteNthRootsSubgroup L n)

def

infiniteKummerRootCharacter

L61 ↗

KummerTheory.infiniteKummerRootCharacter

Documentation

The Kummer root character with codomain given its intended discrete topology.

Source context 6 commands

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

noncomputable section
namespace KummerTheory
open scoped Topology
open Filter
section InfiniteKummerContinuity
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

def infiniteKummerRootCharacter
    (n : ℕ+) (hmu : NthRootsOfUnityInBase (K := K) (L := Ω) n)
    (a : (chosenFiniteKummerRadicalDatum (K := K) (L := Ω) n).carrier) :
    Gal(Ω/K) →* DiscreteNthRootsSubgroup Ω (n : ℕ)

theorem

infiniteKummerRootCharacter_apply

L69 ↗

KummerTheory.infiniteKummerRootCharacter_apply

Documentation

The infinite Kummer root character evaluates by the usual Galois ratio.

Source context 6 commands

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

noncomputable section
namespace KummerTheory
open scoped Topology
open Filter
section InfiniteKummerContinuity
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem infiniteKummerRootCharacter_apply
    (n : ℕ+) (hmu : NthRootsOfUnityInBase (K := K) (L := Ω) n)
    (a : (chosenFiniteKummerRadicalDatum (K := K) (L := Ω) n).carrier)
    (σ : Gal(Ω/K)) :
    infiniteKummerRootCharacter n hmu a σ =
      (chosenFiniteKummerRadicalDatum (K := K) (L := Ω) n).rootCharacterToMuWithoutSection
        a (nthRootsOfUnity_fixed (K := K) (L := Ω) n hmu) σ

theorem

fixingSubgroup_adjoin_root_le_infiniteKummerRootCharacter_ker

L82 ↗

KummerTheory.fixingSubgroup_adjoin_root_le_infiniteKummerRootCharacter_ker

Documentation

The fixing subgroup of the finite Galois normal closure of the chosen root lies in the kernel of its Kummer character.

Source context 7 commands

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

noncomputable section
namespace KummerTheory
open scoped Topology
open Filter
section InfiniteKummerContinuity
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
variable [IsGalois K Ω]

Lean source · statement

theorem fixingSubgroup_adjoin_root_le_infiniteKummerRootCharacter_ker
    (n : ℕ+) (hmu : NthRootsOfUnityInBase (K := K) (L := Ω) n)
    (a : (chosenFiniteKummerRadicalDatum (K := K) (L := Ω) n).carrier) :
    (FiniteGaloisIntermediateField.adjoin K
      {((chosenFiniteKummerRadicalDatum (K := K) (L := Ω) n).root a : Ω)}).fixingSubgroup ≤
        MonoidHom.ker (infiniteKummerRootCharacter n hmu a)

theorem

infiniteKummerRootCharacter_isOpen_ker

L105 ↗

KummerTheory.infiniteKummerRootCharacter_isOpen_ker

Documentation

The kernel of an infinite Kummer root character is open in the Krull topology.

Source context 7 commands

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

noncomputable section
namespace KummerTheory
open scoped Topology
open Filter
section InfiniteKummerContinuity
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
variable [IsGalois K Ω]

Lean source · statement

theorem infiniteKummerRootCharacter_isOpen_ker
    (n : ℕ+) (hmu : NthRootsOfUnityInBase (K := K) (L := Ω) n)
    (a : (chosenFiniteKummerRadicalDatum (K := K) (L := Ω) n).carrier) :
    IsOpen (MonoidHom.ker (infiniteKummerRootCharacter n hmu a) :
      Set Gal(Ω/K))

theorem

infiniteKummerRootCharacter_continuous

L118 ↗

KummerTheory.infiniteKummerRootCharacter_continuous

Documentation

Every Kummer root character for an infinite actual-field Galois extension is continuous into the discrete group μₙ(Ω).

Source context 7 commands

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

noncomputable section
namespace KummerTheory
open scoped Topology
open Filter
section InfiniteKummerContinuity
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
variable [IsGalois K Ω]

Lean source · statement

theorem infiniteKummerRootCharacter_continuous
    (n : ℕ+) (hmu : NthRootsOfUnityInBase (K := K) (L := Ω) n)
    (a : (chosenFiniteKummerRadicalDatum (K := K) (L := Ω) n).carrier) :
    Continuous (infiniteKummerRootCharacter n hmu a)

def

infiniteKummerContinuousRootCharacter

L130 ↗

KummerTheory.infiniteKummerContinuousRootCharacter

Documentation

The continuous Kummer character attached to one radical element.

Source context 7 commands

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

noncomputable section
namespace KummerTheory
open scoped Topology
open Filter
section InfiniteKummerContinuity
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
variable [IsGalois K Ω]

Lean source · statement

def infiniteKummerContinuousRootCharacter
    (n : ℕ+) (hmu : NthRootsOfUnityInBase (K := K) (L := Ω) n)
    (a : (chosenFiniteKummerRadicalDatum (K := K) (L := Ω) n).carrier) :
    Gal(Ω/K) →ₜ* DiscreteNthRootsSubgroup Ω (n : ℕ)

def

infiniteKummerContinuousCharacter

L138 ↗

KummerTheory.infiniteKummerContinuousCharacter

Documentation

Radical elements map multiplicatively to continuous Kummer characters.

Source context 7 commands

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

noncomputable section
namespace KummerTheory
open scoped Topology
open Filter
section InfiniteKummerContinuity
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
variable [IsGalois K Ω]

Lean source · full declaration

def infiniteKummerContinuousCharacter
    (n : ℕ+) (hmu : NthRootsOfUnityInBase (K := K) (L := Ω) n) :
    (chosenFiniteKummerRadicalDatum (K := K) (L := Ω) n).carrier →*
      (Gal(Ω/K) →ₜ* DiscreteNthRootsSubgroup Ω (n : ℕ)) where
  toFun := infiniteKummerContinuousRootCharacter n hmu
  map_one' := by
    apply ContinuousMonoidHom.ext
    intro σ
    exact congrArg
      (fun χ : Gal(Ω/K) →* nthRootsSubgroup Ω (n : ℕ) => χ σ)
      (map_one
        ((chosenFiniteKummerRadicalDatum (K := K) (L := Ω) n).kummerCharacterWithoutSection
          (nthRootsOfUnity_fixed (K := K) (L := Ω) n hmu)))
  map_mul' := by
    intro a b
    apply ContinuousMonoidHom.ext
    intro σ
    exact congrArg
      (fun χ : Gal(Ω/K) →* nthRootsSubgroup Ω (n : ℕ) => χ σ)
      (map_mul
        ((chosenFiniteKummerRadicalDatum (K := K) (L := Ω) n).kummerCharacterWithoutSection
          (nthRootsOfUnity_fixed (K := K) (L := Ω) n hmu)) a b)

def

infiniteKummerContinuousQuotientCharacter

L164 ↗

KummerTheory.infiniteKummerContinuousQuotientCharacter

Documentation

The infinite continuous Kummer character map on the ambient-power quotient Δ / (Δ ∩ Kˣⁿ). This is the canonical map; surjectivity is not asserted, and injectivity is proved below from the existing algebraic kernel result.

Source context 7 commands

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

noncomputable section
namespace KummerTheory
open scoped Topology
open Filter
section InfiniteKummerContinuity
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
variable [IsGalois K Ω]

Lean source · statement

def infiniteKummerContinuousQuotientCharacter
    (n : ℕ+) (hmu : NthRootsOfUnityInBase (K := K) (L := Ω) n) :
    (chosenFiniteKummerRadicalDatum (K := K) (L := Ω) n).RadicalQuotient →*
      (Gal(Ω/K) →ₜ* DiscreteNthRootsSubgroup Ω (n : ℕ))

theorem

infiniteKummerContinuousQuotientCharacter_toMonoidHom

L184 ↗

KummerTheory.infiniteKummerContinuousQuotientCharacter_toMonoidHom

Documentation

Forgetting continuity recovers the previously constructed algebraic Kummer character on the same ambient-power quotient.

Source context 7 commands

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

noncomputable section
namespace KummerTheory
open scoped Topology
open Filter
section InfiniteKummerContinuity
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
variable [IsGalois K Ω]

Lean source · statement

theorem infiniteKummerContinuousQuotientCharacter_toMonoidHom
    (n : ℕ+) (hmu : NthRootsOfUnityInBase (K := K) (L := Ω) n)
    (q : (chosenFiniteKummerRadicalDatum (K := K) (L := Ω) n).RadicalQuotient) :
    (infiniteKummerContinuousQuotientCharacter n hmu q).toMonoidHom =
      (chosenFiniteKummerRadicalDatum (K := K) (L := Ω) n).quotientKummerCharacterWithoutSection
        (nthRootsOfUnity_fixed (K := K) (L := Ω) n hmu) q

theorem

infiniteKummerContinuousQuotientCharacter_injective

L199 ↗

KummerTheory.infiniteKummerContinuousQuotientCharacter_injective

Documentation

The continuous character map on the ambient-power quotient is injective. This is the existing algebraic kernel computation with the continuity structure forgotten; it does not use or assert surjectivity.

Source context 7 commands

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

noncomputable section
namespace KummerTheory
open scoped Topology
open Filter
section InfiniteKummerContinuity
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
variable [IsGalois K Ω]

Lean source · statement

theorem infiniteKummerContinuousQuotientCharacter_injective
    (n : ℕ+) (hmu : NthRootsOfUnityInBase (K := K) (L := Ω) n) :
    Function.Injective (infiniteKummerContinuousQuotientCharacter n hmu)

Module documentation

continuity of Kummer characters for infinite extensions

Declarations