Module

RootCharacters.lean

Nyll.GaloisCohomology.Kummer.Concrete.RootCharacters

36 declarations indexed from sourceView source ↗

Module documentation

Root characters for Kummer theory

Support API for root-quotient constructions in concrete Kummer extensions.

Imports1

Nyll.GaloisCohomology.Kummer.Concrete.GaloisCohomology

Imported by9

theorem

div_pow_eq_one_of_pow_eq_pow

L26 ↗

KummerTheory.div_pow_eq_one_of_pow_eq_pow

Documentation

Two unit roots with the same n-th power differ by an n-th root of unity.

Source context 4 commands

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

namespace KummerTheory
open groupCohomology
section RootQuotientPrelim
variable {L : Type*} [Field L]

Lean source · statement

theorem div_pow_eq_one_of_pow_eq_pow
    {n : ℕ} {u v : Lˣ} (h : u ^ n = v ^ n) :
    (u / v) ^ n = 1

def

nthRootsSubgroup

L39 ↗

KummerTheory.nthRootsSubgroup

Documentation

The subgroup of units whose n-th power is 1.

Source context 4 commands

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

namespace KummerTheory
open groupCohomology
section TorsionSubgroups
variable (L : Type*) [Field L]

Lean source · full declaration

def nthRootsSubgroup (n : ℕ) : Subgroup Lˣ where
  carrier := {u | u ^ n = 1}
  one_mem' := by
    simp
  mul_mem' := by
    intro u v hu hv
    change (u * v) ^ n = 1
    rw [mul_pow, hu, hv, one_mul]
  inv_mem' := by
    intro u hu
    change u⁻¹ ^ n = 1
    rw [inv_pow, hu, inv_one]

theorem

mem_nthRootsSubgroup_iff

L53 ↗

KummerTheory.mem_nthRootsSubgroup_iff

Documentation

Membership in the roots subgroup is equivalent to satisfying the nth-root equation.

Source context 4 commands

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

namespace KummerTheory
open groupCohomology
section TorsionSubgroups
variable (L : Type*) [Field L]

Lean source · statement

theorem mem_nthRootsSubgroup_iff {n : ℕ} {u : Lˣ} :
    u ∈ nthRootsSubgroup L n ↔ u ^ n = 1

theorem

div_mem_nthRootsSubgroup_of_pow_eq_pow

L58 ↗

KummerTheory.div_mem_nthRootsSubgroup_of_pow_eq_pow

Documentation

If two units have the same n-th power, then their quotient lies in μₙ(L).

Source context 4 commands

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

namespace KummerTheory
open groupCohomology
section TorsionSubgroups
variable (L : Type*) [Field L]

Lean source · statement

theorem div_mem_nthRootsSubgroup_of_pow_eq_pow
    {n : ℕ} {u v : Lˣ} (h : u ^ n = v ^ n) :
    u / v ∈ nthRootsSubgroup L n

theorem

smul_mem_nthRootsSubgroup

L65 ↗

KummerTheory.smul_mem_nthRootsSubgroup

Documentation

Galois automorphisms preserve the subgroup of n-torsion units.

Source context 4 commands

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

namespace KummerTheory
open groupCohomology
section TorsionSubgroups
variable (L : Type*) [Field L]

Lean source · statement

theorem smul_mem_nthRootsSubgroup
    {K : Type*} [Field K] [Algebra K L]
    (n : ℕ) (σ : Gal(L/K)) {u : Lˣ}
    (hu : u ∈ nthRootsSubgroup L n) :
    σ • u ∈ nthRootsSubgroup L n

def

rootQuotient

L83 ↗

KummerTheory.rootQuotient

Documentation

The basic root-quotient attached to a unit β and a Galois automorphism σ.

Source context 4 commands

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

namespace KummerTheory
open groupCohomology
section RootQuotients
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

def rootQuotient (β : Lˣ) (σ : Gal(L/K)) : Lˣ

theorem

rootQuotient_one

L87 ↗

KummerTheory.rootQuotient_one

Documentation

The root-quotient attached to the identity automorphism is trivial.

Source context 4 commands

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

namespace KummerTheory
open groupCohomology
section RootQuotients
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem rootQuotient_one (β : Lˣ) :
    rootQuotient (K := K) (L := L) β 1 = 1

theorem

rootQuotient_mul_right

L92 ↗

KummerTheory.rootQuotient_mul_right

Documentation

Multiplying the root-quotient by the chosen root recovers its Galois transform.

Source context 4 commands

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

namespace KummerTheory
open groupCohomology
section RootQuotients
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem rootQuotient_mul_right (β : Lˣ) (σ : Gal(L/K)) :
    rootQuotient (K := K) (L := L) β σ * β = σ • β

theorem

rootQuotient_algebraMap_unit

L97 ↗

KummerTheory.rootQuotient_algebraMap_unit

Documentation

Base-field units have trivial root-quotient.

Source context 4 commands

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

namespace KummerTheory
open groupCohomology
section RootQuotients
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem rootQuotient_algebraMap_unit (u : Kˣ) (σ : Gal(L/K)) :
    rootQuotient (K := K) (L := L) (Units.map (algebraMap K L).toMonoidHom u) σ = 1

theorem

rootQuotient_mul_root

L104 ↗

KummerTheory.rootQuotient_mul_root

Documentation

The root-quotient attached to a product is the product of the root-quotients.

Source context 4 commands

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

namespace KummerTheory
open groupCohomology
section RootQuotients
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem rootQuotient_mul_root (u v : Lˣ) (σ : Gal(L/K)) :
    rootQuotient (K := K) (L := L) (u * v) σ =
      rootQuotient (K := K) (L := L) u σ *
        rootQuotient (K := K) (L := L) v σ

theorem

rootQuotient_eq_one_iff

L111 ↗

KummerTheory.rootQuotient_eq_one_iff

Documentation

The root-quotient is trivial exactly when the chosen root is fixed by σ.

Source context 4 commands

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

namespace KummerTheory
open groupCohomology
section RootQuotients
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem rootQuotient_eq_one_iff (β : Lˣ) (σ : Gal(L/K)) :
    rootQuotient (K := K) (L := L) β σ = 1 ↔ σ • β = β

theorem

rootQuotient_mul

L117 ↗

KummerTheory.rootQuotient_mul

Documentation

The root-quotient construction satisfies the multiplicative cocycle identity.

Source context 4 commands

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

namespace KummerTheory
open groupCohomology
section RootQuotients
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem rootQuotient_mul (β : Lˣ) (σ τ : Gal(L/K)) :
    rootQuotient (K := K) (L := L) β (σ * τ) =
      σ • rootQuotient (K := K) (L := L) β τ *
        rootQuotient (K := K) (L := L) β σ

theorem

isMulCocycle₁_rootQuotient

L126 ↗

KummerTheory.isMulCocycle₁_rootQuotient

Documentation

Reformulation: σ ↦ σ(β) / β is a multiplicative 1-cocycle.

Source context 4 commands

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

namespace KummerTheory
open groupCohomology
section RootQuotients
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem isMulCocycle₁_rootQuotient (β : Lˣ) :
    IsMulCocycle₁ (rootQuotient (K := K) (L := L) β)

theorem

rootQuotient_inv

L132 ↗

KummerTheory.rootQuotient_inv

Documentation

The root-quotient at σ⁻¹ is determined by the value at σ.

Source context 4 commands

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

namespace KummerTheory
open groupCohomology
section RootQuotients
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem rootQuotient_inv (β : Lˣ) (σ : Gal(L/K)) :
    σ • rootQuotient (K := K) (L := L) β σ⁻¹ =
      (rootQuotient (K := K) (L := L) β σ)⁻¹

theorem

rootQuotient_div

L139 ↗

KummerTheory.rootQuotient_div

Documentation

The root-quotient of a quotient is the quotient of the root-quotients.

Source context 4 commands

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

namespace KummerTheory
open groupCohomology
section RootQuotients
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem rootQuotient_div (u v : Lˣ) (σ : Gal(L/K)) :
    rootQuotient (K := K) (L := L) (u / v) σ =
      rootQuotient (K := K) (L := L) u σ /
        rootQuotient (K := K) (L := L) v σ

theorem

rootQuotient_changeRoot

L146 ↗

KummerTheory.rootQuotient_changeRoot

Documentation

Changing the chosen root changes the corresponding quotient cocycle by a coboundary.

Source context 4 commands

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

namespace KummerTheory
open groupCohomology
section RootQuotients
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem rootQuotient_changeRoot (u v : Lˣ) (σ : Gal(L/K)) :
    rootQuotient (K := K) (L := L) u σ /
        rootQuotient (K := K) (L := L) v σ =
      rootQuotient (K := K) (L := L) (u / v) σ

theorem

rootQuotient_pow_eq_one_of_pow_fixed

L153 ↗

KummerTheory.rootQuotient_pow_eq_one_of_pow_fixed

Documentation

If β ^ n is fixed by Galois, then σ(β) / β is n-torsion.

Source context 4 commands

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

namespace KummerTheory
open groupCohomology
section RootQuotients
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem rootQuotient_pow_eq_one_of_pow_fixed
    {n : ℕ} {β : Lˣ} (hβ : ∀ σ : Gal(L/K), σ • (β ^ n) = β ^ n)
    (σ : Gal(L/K)) :
    rootQuotient (K := K) (L := L) β σ ^ n = 1

theorem

rootQuotient_mem_nthRootsSubgroup_of_pow_fixed

L162 ↗

KummerTheory.rootQuotient_mem_nthRootsSubgroup_of_pow_fixed

Documentation

If β ^ n is fixed by Galois, then the root-quotient lands in μₙ(L).

Source context 4 commands

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

namespace KummerTheory
open groupCohomology
section RootQuotients
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem rootQuotient_mem_nthRootsSubgroup_of_pow_fixed
    {n : ℕ} {β : Lˣ} (hβ : ∀ σ : Gal(L/K), σ • (β ^ n) = β ^ n)
    (σ : Gal(L/K)) :
    rootQuotient (K := K) (L := L) β σ ∈ nthRootsSubgroup L n

structure

RadicalDatum

L179 ↗

KummerTheory.RadicalDatum

Documentation

A radical datum of exponent n consists of a subgroup of Kˣ together with a chosen n-th root in Lˣ for each of its elements.

Source context 4 commands

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

namespace KummerTheory
open groupCohomology
section RadicalData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · full declaration

structure RadicalDatum (n : ℕ+) where
  /-- The subgroup of base-field units for which roots are chosen. -/
  carrier : Subgroup Kˣ
  /-- A chosen `n`-th root in `Lˣ` for each unit in `carrier`. -/
  root : carrier → Lˣ
  /-- Each chosen root has `n`-th power equal to the image of its base-field unit in `Lˣ`. -/
  root_pow_eq : ∀ a : carrier,
    root a ^ (n : ℕ) = Units.map (algebraMap K L).toMonoidHom a.1

theorem

root_pow_eq_map

L193 ↗

KummerTheory.RadicalDatum.root_pow_eq_map

Documentation

The chosen root witness has the prescribed n-th power.

Source context 6 commands

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

namespace KummerTheory
open groupCohomology
section RadicalData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
namespace RadicalDatum
variable {n : ℕ+} (D : RadicalDatum (K := K) (L := L) n)

Lean source · statement

theorem root_pow_eq_map (a : D.carrier) :
    D.root a ^ (n : ℕ) = Units.map (algebraMap K L).toMonoidHom a.1

theorem

div_pow_eq_one_of_same_image

L198 ↗

KummerTheory.RadicalDatum.div_pow_eq_one_of_same_image

Documentation

Two n-th roots of the same radical element differ by an n-th root of unity.

Source context 6 commands

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

namespace KummerTheory
open groupCohomology
section RadicalData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
namespace RadicalDatum
variable {n : ℕ+} (D : RadicalDatum (K := K) (L := L) n)

Lean source · statement

theorem div_pow_eq_one_of_same_image
    {u v : Lˣ} (a : D.carrier)
    (hu : u ^ (n : ℕ) = Units.map (algebraMap K L).toMonoidHom a.1)
    (hv : v ^ (n : ℕ) = Units.map (algebraMap K L).toMonoidHom a.1) :
    (u / v) ^ (n : ℕ) = 1

def

rootCocycle

L206 ↗

KummerTheory.RadicalDatum.rootCocycle

Documentation

The root-quotient map σ ↦ σ(β) / β attached to the chosen root witness of a.

Source context 6 commands

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

namespace KummerTheory
open groupCohomology
section RadicalData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
namespace RadicalDatum
variable {n : ℕ+} (D : RadicalDatum (K := K) (L := L) n)

Lean source · statement

def rootCocycle (a : D.carrier) (σ : Gal(L/K)) : Lˣ

theorem

rootCocycle_one

L210 ↗

KummerTheory.RadicalDatum.rootCocycle_one

Documentation

The chosen root-quotient is trivial at the identity automorphism.

Source context 6 commands

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

namespace KummerTheory
open groupCohomology
section RadicalData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
namespace RadicalDatum
variable {n : ℕ+} (D : RadicalDatum (K := K) (L := L) n)

Lean source · statement

theorem rootCocycle_one (a : D.carrier) :
    D.rootCocycle a 1 = 1

theorem

rootCocycle_mul

L215 ↗

KummerTheory.RadicalDatum.rootCocycle_mul

Documentation

The chosen root-quotient satisfies the multiplicative cocycle identity.

Source context 6 commands

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

namespace KummerTheory
open groupCohomology
section RadicalData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
namespace RadicalDatum
variable {n : ℕ+} (D : RadicalDatum (K := K) (L := L) n)

Lean source · statement

theorem rootCocycle_mul (a : D.carrier) (σ τ : Gal(L/K)) :
    D.rootCocycle a (σ * τ) =
      σ • D.rootCocycle a τ * D.rootCocycle a σ

theorem

isMulCocycle₁_rootCocycle

L221 ↗

KummerTheory.RadicalDatum.isMulCocycle₁_rootCocycle

Documentation

Reformulation: the chosen root-quotient is a multiplicative 1-cocycle.

Source context 6 commands

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

namespace KummerTheory
open groupCohomology
section RadicalData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
namespace RadicalDatum
variable {n : ℕ+} (D : RadicalDatum (K := K) (L := L) n)

Lean source · statement

theorem isMulCocycle₁_rootCocycle (a : D.carrier) :
    IsMulCocycle₁ (D.rootCocycle a)

theorem

smul_algebraMap_unit

L226 ↗

KummerTheory.RadicalDatum.smul_algebraMap_unit

Documentation

Galois automorphisms fix units coming from the base field.

Source context 6 commands

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

namespace KummerTheory
open groupCohomology
section RadicalData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
namespace RadicalDatum
variable {n : ℕ+} (D : RadicalDatum (K := K) (L := L) n)

Lean source · statement

theorem smul_algebraMap_unit (σ : Gal(L/K)) (u : Kˣ) :
    σ • Units.map (algebraMap K L).toMonoidHom u =
      Units.map (algebraMap K L).toMonoidHom u

theorem

rootCocycle_pow_eq_one

L233 ↗

KummerTheory.RadicalDatum.rootCocycle_pow_eq_one

Documentation

The chosen root-quotient of a lands in the n-torsion subgroup of Lˣ.

Source context 6 commands

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

namespace KummerTheory
open groupCohomology
section RadicalData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
namespace RadicalDatum
variable {n : ℕ+} (D : RadicalDatum (K := K) (L := L) n)

Lean source · statement

theorem rootCocycle_pow_eq_one (a : D.carrier) (σ : Gal(L/K)) :
    D.rootCocycle a σ ^ (n : ℕ) = 1

theorem

rootCocycle_mem_nthRootsSubgroup

L242 ↗

KummerTheory.RadicalDatum.rootCocycle_mem_nthRootsSubgroup

Documentation

The chosen root-quotient of a belongs to μₙ(L).

Source context 6 commands

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

namespace KummerTheory
open groupCohomology
section RadicalData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
namespace RadicalDatum
variable {n : ℕ+} (D : RadicalDatum (K := K) (L := L) n)

Lean source · statement

theorem rootCocycle_mem_nthRootsSubgroup (a : D.carrier) (σ : Gal(L/K)) :
    D.rootCocycle a σ ∈ nthRootsSubgroup L (n : ℕ)

theorem

changeRoot_rootQuotient_pow_eq_one

L248 ↗

KummerTheory.RadicalDatum.changeRoot_rootQuotient_pow_eq_one

Documentation

If two root choices are used for the same radical element, their quotient is n-torsion.

Source context 6 commands

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

namespace KummerTheory
open groupCohomology
section RadicalData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
namespace RadicalDatum
variable {n : ℕ+} (D : RadicalDatum (K := K) (L := L) n)

Lean source · statement

theorem changeRoot_rootQuotient_pow_eq_one
    {u v : Lˣ} (a : D.carrier)
    (hu : u ^ (n : ℕ) = Units.map (algebraMap K L).toMonoidHom a.1)
    (hv : v ^ (n : ℕ) = Units.map (algebraMap K L).toMonoidHom a.1)
    (σ : Gal(L/K)) :
    (rootQuotient (K := K) (L := L) u σ /
        rootQuotient (K := K) (L := L) v σ) ^ (n : ℕ) = 1

theorem

changeRoot_rootQuotient_mem_nthRootsSubgroup

L265 ↗

KummerTheory.RadicalDatum.changeRoot_rootQuotient_mem_nthRootsSubgroup

Documentation

Change-of-root quotient cocycles land in μₙ(L).

Source context 6 commands

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

namespace KummerTheory
open groupCohomology
section RadicalData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
namespace RadicalDatum
variable {n : ℕ+} (D : RadicalDatum (K := K) (L := L) n)

Lean source · statement

theorem changeRoot_rootQuotient_mem_nthRootsSubgroup
    {u v : Lˣ} (a : D.carrier)
    (hu : u ^ (n : ℕ) = Units.map (algebraMap K L).toMonoidHom a.1)
    (hv : v ^ (n : ℕ) = Units.map (algebraMap K L).toMonoidHom a.1)
    (σ : Gal(L/K)) :
    rootQuotient (K := K) (L := L) u σ /
        rootQuotient (K := K) (L := L) v σ ∈ nthRootsSubgroup L (n : ℕ)

theorem

rootQuotient_eq_rootCocycle_of_same_pow

L276 ↗

KummerTheory.RadicalDatum.rootQuotient_eq_rootCocycle_of_same_pow

Documentation

If μₙ(L) is fixed by Galois, root-quotients for the same radical element agree.

Source context 6 commands

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

namespace KummerTheory
open groupCohomology
section RadicalData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
namespace RadicalDatum
variable {n : ℕ+} (D : RadicalDatum (K := K) (L := L) n)

Lean source · statement

theorem rootQuotient_eq_rootCocycle_of_same_pow
    (hfixed : ∀ σ : Gal(L/K), ∀ u : Lˣ, u ^ (n : ℕ) = 1 → σ • u = u)
    {u : Lˣ} (a : D.carrier)
    (hu : u ^ (n : ℕ) = Units.map (algebraMap K L).toMonoidHom a.1)
    (σ : Gal(L/K)) :
    rootQuotient (K := K) (L := L) u σ = D.rootCocycle a σ

def

rootCharacter

L294 ↗

KummerTheory.RadicalDatum.rootCharacter

Documentation

If μₙ(L) is fixed by Galois, the chosen root-quotient is a character.

Source context 6 commands

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

namespace KummerTheory
open groupCohomology
section RadicalData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
namespace RadicalDatum
variable {n : ℕ+} (D : RadicalDatum (K := K) (L := L) n)

Lean source · full declaration

def rootCharacter (a : D.carrier)
    (hfixed : ∀ σ : Gal(L/K), ∀ u : Lˣ, u ^ (n : ℕ) = 1 → σ • u = u) :
    Gal(L/K) →* Lˣ where
  toFun := D.rootCocycle a
  map_one' := by
    exact D.rootCocycle_one a
  map_mul' := by
    intro σ τ
    rw [D.rootCocycle_mul]
    rw [hfixed σ (D.rootCocycle a τ) (D.rootCocycle_pow_eq_one a τ)]
    exact mul_comm _ _

theorem

rootCharacter_apply

L307 ↗

KummerTheory.RadicalDatum.rootCharacter_apply

Documentation

The Kummer root character evaluates as the Galois translate divided by the chosen root.

Source context 6 commands

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

namespace KummerTheory
open groupCohomology
section RadicalData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
namespace RadicalDatum
variable {n : ℕ+} (D : RadicalDatum (K := K) (L := L) n)

Lean source · statement

theorem rootCharacter_apply (a : D.carrier)
    (hfixed : ∀ σ : Gal(L/K), ∀ u : Lˣ, u ^ (n : ℕ) = 1 → σ • u = u)
    (σ : Gal(L/K)) :
    D.rootCharacter a hfixed σ = D.rootCocycle a σ

theorem

rootCharacter_eq_of_same_pow

L314 ↗

KummerTheory.RadicalDatum.rootCharacter_eq_of_same_pow

Documentation

The canonical character agrees with any root quotient having the same n-th power.

Source context 6 commands

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

namespace KummerTheory
open groupCohomology
section RadicalData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
namespace RadicalDatum
variable {n : ℕ+} (D : RadicalDatum (K := K) (L := L) n)

Lean source · statement

theorem rootCharacter_eq_of_same_pow
    (hfixed : ∀ σ : Gal(L/K), ∀ u : Lˣ, u ^ (n : ℕ) = 1 → σ • u = u)
    {u : Lˣ} (a : D.carrier)
    (hu : u ^ (n : ℕ) = Units.map (algebraMap K L).toMonoidHom a.1)
    (σ : Gal(L/K)) :
    rootQuotient (K := K) (L := L) u σ = D.rootCharacter a hfixed σ

theorem

rootCharacter_pow_eq_one

L324 ↗

KummerTheory.RadicalDatum.rootCharacter_pow_eq_one

Documentation

The character obtained from a chosen root still takes values in μₙ(L).

Source context 6 commands

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

namespace KummerTheory
open groupCohomology
section RadicalData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
namespace RadicalDatum
variable {n : ℕ+} (D : RadicalDatum (K := K) (L := L) n)

Lean source · statement

theorem rootCharacter_pow_eq_one (a : D.carrier)
    (hfixed : ∀ σ : Gal(L/K), ∀ u : Lˣ, u ^ (n : ℕ) = 1 → σ • u = u)
    (σ : Gal(L/K)) :
    D.rootCharacter a hfixed σ ^ (n : ℕ) = 1

theorem

rootCharacter_mem_nthRootsSubgroup

L332 ↗

KummerTheory.RadicalDatum.rootCharacter_mem_nthRootsSubgroup

Documentation

The character obtained from a chosen root lands in μₙ(L).

Source context 6 commands

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

namespace KummerTheory
open groupCohomology
section RadicalData
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
namespace RadicalDatum
variable {n : ℕ+} (D : RadicalDatum (K := K) (L := L) n)

Lean source · statement

theorem rootCharacter_mem_nthRootsSubgroup (a : D.carrier)
    (hfixed : ∀ σ : Gal(L/K), ∀ u : Lˣ, u ^ (n : ℕ) = 1 → σ • u = u)
    (σ : Gal(L/K)) :
    D.rootCharacter a hfixed σ ∈ nthRootsSubgroup L (n : ℕ)

Module documentation

Root characters for Kummer theory

Declarations