Module

RootCharacter.lean

Nyll.AnabelianGeometry.KummerTheory.RootCharacter

4 declarations indexed from sourceView source ↗

Module documentation

Radical characters and their fixed fields

When the relevant roots of unity belong to the base field, a nonzero radical defines a unit-valued Galois character. Its kernel fixes precisely the field generated by that radical in an arbitrary Galois ambient extension.

Imports2

Nyll.AnabelianGeometry.KummerTheory.RootCocycle
Mathlib.FieldTheory.Galois.Infinite

Imported by2

def

rootCharacter

L25 ↗

AnabelianGeometry.KummerTheory.rootCharacter

Documentation

The Kummer character of a nonzero radical, with values in ambient units.

Source context 3 commands

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

namespace AnabelianGeometry.KummerTheory
universe u v
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · full declaration

def rootCharacter (r : L) (hr : r ≠ 0) {n : ℕ} {a : K}
    (ha : r ^ n = algebraMap K L a)
    (hroots : ∀ ξ : L, ξ ^ n = 1 → ∃ b : K, algebraMap K L b = ξ) :
    (L ≃ₐ[K] L) →* Lˣ where
  toFun σ := Units.mk0 (rootRatio r σ) (rootRatio_ne_zero hr σ)
  map_one' := by
    apply Units.ext
    change r / r = 1
    exact div_self hr
  map_mul' σ τ := by
    apply Units.ext
    exact rootRatio_mul_of_roots_in_base hr ha hroots σ τ

theorem

rootCharacter_ker

L39 ↗

AnabelianGeometry.KummerTheory.rootCharacter_ker

Documentation

The character kernel is exactly the pointwise stabilizer of the radical field.

Source context 3 commands

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

namespace AnabelianGeometry.KummerTheory
universe u v
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

theorem rootCharacter_ker (r : L) (hr : r ≠ 0) {n : ℕ} {a : K}
    (ha : r ^ n = algebraMap K L a)
    (hroots : ∀ ξ : L, ξ ^ n = 1 → ∃ b : K, algebraMap K L b = ξ) :
    (rootCharacter r hr ha hroots).ker =
      (IntermediateField.adjoin K ({r} : Set L)).fixingSubgroup

theorem

fixedField_rootCharacter_ker

L56 ↗

AnabelianGeometry.KummerTheory.fixedField_rootCharacter_ker

Documentation

In an arbitrary Galois ambient extension, the radical field is recovered as the fixed field of the radical character's kernel.

Source context 3 commands

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

namespace AnabelianGeometry.KummerTheory
universe u v
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

theorem fixedField_rootCharacter_ker [IsGalois K L]
    (r : L) (hr : r ≠ 0) {n : ℕ} {a : K}
    (ha : r ^ n = algebraMap K L a)
    (hroots : ∀ ξ : L, ξ ^ n = 1 → ∃ b : K, algebraMap K L b = ξ) :
    IntermediateField.fixedField (rootCharacter r hr ha hroots).ker =
      IntermediateField.adjoin K ({r} : Set L)

theorem

rootCharacter_ker_isOpen

L66 ↗

AnabelianGeometry.KummerTheory.rootCharacter_ker_isOpen

Documentation

A radical character has open kernel in the Krull topology, including when the Galois ambient extension is infinite.

Source context 3 commands

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

namespace AnabelianGeometry.KummerTheory
universe u v
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

theorem rootCharacter_ker_isOpen [IsGalois K L]
    (r : L) (hr : r ≠ 0) {n : ℕ} {a : K}
    (ha : r ^ n = algebraMap K L a)
    (hroots : ∀ ξ : L, ξ ^ n = 1 → ∃ b : K, algebraMap K L b = ξ) :
    IsOpen ((rootCharacter r hr ha hroots).ker : Set (L ≃ₐ[K] L))

Module documentation

Radical characters and their fixed fields

Declarations

rootCharacter

rootCharacter_ker

fixedField_rootCharacter_ker

rootCharacter_ker_isOpen