Module

InfiniteCharacterEquiv.lean

Nyll.GaloisCohomology.Kummer.Concrete.InfiniteCharacterEquiv

8 declarations indexed from sourceView source ↗

Module documentation

Infinite Kummer character equivalence

Continuous characters of an infinite Galois group factor through finite Galois stages. Finite Kummer surjectivity at such a stage then supplies a radical representative in the ambient extension.

Imports3

Imported by3

theorem

primitiveRoots_intermediate_nonempty

L25 ↗

KummerTheory.primitiveRoots_intermediate_nonempty

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem primitiveRoots_intermediate_nonempty
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (E : IntermediateField K Ω) :
    (primitiveRoots (n : ℕ) E).Nonempty

def

intermediateNthRootsEquiv

L34 ↗

KummerTheory.intermediateNthRootsEquiv

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

def intermediateNthRootsEquiv
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (E : IntermediateField K Ω) :
    nthRootsSubgroup E (n : ℕ) ≃* nthRootsSubgroup Ω (n : ℕ)

theorem

intermediateNthRootsEquiv_apply_val

L41 ↗

KummerTheory.intermediateNthRootsEquiv_apply_val

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem intermediateNthRootsEquiv_apply_val
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (E : IntermediateField K Ω) (u : nthRootsSubgroup E (n : ℕ)) :
    ((intermediateNthRootsEquiv n hmu E u : nthRootsSubgroup Ω (n : ℕ)) : Ωˣ) =
      Units.map (algebraMap E Ω).toMonoidHom (u : Eˣ)

theorem

rootQuotient_map_intermediate

L50 ↗

KummerTheory.rootQuotient_map_intermediate

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem rootQuotient_map_intermediate
    (E : IntermediateField K Ω) [Normal K E]
    (β : Eˣ) (σ : Gal(Ω/K)) :
    rootQuotient (K := K) (L := Ω)
        (Units.map (algebraMap E Ω).toMonoidHom β) σ =
      Units.map (algebraMap E Ω).toMonoidHom
        (rootQuotient (K := K) (L := E) β
          (AlgEquiv.restrictNormalHom E σ))

def

finiteRadicalToAmbient

L67 ↗

KummerTheory.finiteRadicalToAmbient

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

def finiteRadicalToAmbient
    (n : ℕ+) (E : IntermediateField K Ω)
    (a : (chosenFiniteKummerRadicalDatum (K := K) (L := E) n).carrier) :
    (chosenFiniteKummerRadicalDatum (K := K) (L := Ω) n).carrier

theorem

finiteRadicalToAmbient_mapped_root_pow

L78 ↗

KummerTheory.finiteRadicalToAmbient_mapped_root_pow

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem finiteRadicalToAmbient_mapped_root_pow
    (n : ℕ+) (E : IntermediateField K Ω)
    (a : (chosenFiniteKummerRadicalDatum (K := K) (L := E) n).carrier) :
    (Units.map (algebraMap E Ω).toMonoidHom
        ((chosenFiniteKummerRadicalDatum (K := K) (L := E) n).root a)) ^ (n : ℕ) =
      Units.map (algebraMap K Ω).toMonoidHom
        (finiteRadicalToAmbient n E a).1

theorem

infiniteKummerContinuousQuotientCharacter_surjective_of_primitiveRoots

L94 ↗

KummerTheory.infiniteKummerContinuousQuotientCharacter_surjective_of_primitiveRoots

Documentation

Every continuous μₙ(Ω)-valued character is represented by a radical class when a primitive n-th root of unity lies in the base field.

Source context 4 commands

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

noncomputable section
namespace KummerTheory
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
variable [IsGalois K Ω]

Lean source · statement

theorem infiniteKummerContinuousQuotientCharacter_surjective_of_primitiveRoots
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    Function.Surjective
      (infiniteKummerContinuousQuotientCharacter n
        (nthRootsOfUnityInBase_of_primitiveRoots (K := K) (L := Ω) n hmu))

def

infiniteKummerContinuousCharacterEquivOfPrimitiveRoots

L155 ↗

KummerTheory.infiniteKummerContinuousCharacterEquivOfPrimitiveRoots

Documentation

Continuous Kummer characters of an infinite Galois extension are multiplicatively equivalent to its radical quotient.

Source context 4 commands

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

noncomputable section
namespace KummerTheory
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
variable [IsGalois K Ω]

Lean source · statement

def infiniteKummerContinuousCharacterEquivOfPrimitiveRoots
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    (chosenFiniteKummerRadicalDatum (K := K) (L := Ω) n).RadicalQuotient ≃*
      (Gal(Ω/K) →ₜ* DiscreteNthRootsSubgroup Ω (n : ℕ))

Module documentation

Infinite Kummer character equivalence

Declarations