NYLL
Module

RadicalQuotient.lean

Nyll.GaloisCohomology.Kummer.Concrete.RadicalQuotient
24 declarations indexed from sourceView source ↗

Module documentation

Ambient radical quotients

Source lemmas for the quotient on the radical side of the Kummer pairing in Concrete Kummer radical quotients. Unlike MultiplicativeRadicalDatum, this construction starts with an arbitrary choice of roots. The hypothesis that μₙ(L) is fixed by Galois makes the resulting root characters independent of that choice.

The denominator is the subgroup of elements of D.carrier which are n-th powers in the ambient group Kˣ, in the ambient group, rather than the generally smaller subgroup of n-th powers of elements of D.carrier.

Imports2
Imported by2

Declarations

theorem

rootCharacter_mul_withoutSection

L36 ↗
KummerTheory.RadicalDatum.rootCharacter_mul_withoutSection
Documentation

Multiplicativity of root characters does not require a multiplicative choice of roots.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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_mul_withoutSection
    (hfixed : ∀ σ : Gal(L/K), ∀ u : Lˣ, u ^ (n : ℕ) = 1 → σ • u = u)
    (a b : D.carrier) :
    D.rootCharacter (a * b) hfixed =
      D.rootCharacter a hfixed * D.rootCharacter b hfixed
theorem

rootCharacter_one_withoutSection

L50 ↗
KummerTheory.RadicalDatum.rootCharacter_one_withoutSection
Documentation

The root character of 1 is trivial, without choosing roots multiplicatively.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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_one_withoutSection
    (hfixed : ∀ σ : Gal(L/K), ∀ u : Lˣ, u ^ (n : ℕ) = 1 → σ • u = u) :
    D.rootCharacter 1 hfixed = 1
def

rootCharacterToMuWithoutSection

L62 ↗
KummerTheory.RadicalDatum.rootCharacterToMuWithoutSection
Documentation

The root character, bundled with its codomain restricted to μₙ(L).

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 rootCharacterToMuWithoutSection (a : D.carrier)
    (hfixed : ∀ σ : Gal(L/K), ∀ u : Lˣ, u ^ (n : ℕ) = 1 → σ • u = u) :
    Gal(L/K) →* nthRootsSubgroup L (n : ℕ) where
  toFun := fun σ =>
    ⟨D.rootCharacter a hfixed σ, D.rootCharacter_mem_nthRootsSubgroup a hfixed σ⟩
  map_one' := by
    apply Subtype.ext
    exact map_one (D.rootCharacter a hfixed)
  map_mul' := by
    intro σ τ
    apply Subtype.ext
    exact map_mul (D.rootCharacter a hfixed) σ τ
theorem

rootCharacterToMuWithoutSection_apply

L77 ↗
KummerTheory.RadicalDatum.rootCharacterToMuWithoutSection_apply
Documentation

The section-free root character evaluates as the quotient of the transported root by the root itself.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 rootCharacterToMuWithoutSection_apply (a : D.carrier)
    (hfixed : ∀ σ : Gal(L/K), ∀ u : Lˣ, u ^ (n : ℕ) = 1 → σ • u = u)
    (σ : Gal(L/K)) :
    D.rootCharacterToMuWithoutSection a hfixed σ =
      ⟨D.rootCharacter a hfixed σ, D.rootCharacter_mem_nthRootsSubgroup a hfixed σ⟩
def

kummerCharacterWithoutSection

L85 ↗
KummerTheory.RadicalDatum.kummerCharacterWithoutSection
Documentation

The root-character construction is a homomorphism on the radical subgroup.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 kummerCharacterWithoutSection
    (hfixed : ∀ σ : Gal(L/K), ∀ u : Lˣ, u ^ (n : ℕ) = 1 → σ • u = u) :
    D.carrier →* (Gal(L/K) →* nthRootsSubgroup L (n : ℕ)) where
  toFun := fun a => D.rootCharacterToMuWithoutSection a hfixed
  map_one' := by
    apply MonoidHom.ext
    intro σ
    apply Subtype.ext
    exact congrArg (fun χ : Gal(L/K) →* Lˣ => χ σ)
      (D.rootCharacter_one_withoutSection hfixed)
  map_mul' := by
    intro a b
    apply MonoidHom.ext
    intro σ
    apply Subtype.ext
    exact congrArg (fun χ : Gal(L/K) →* Lˣ => χ σ)
      (D.rootCharacter_mul_withoutSection hfixed a b)
def

ambientNthPowersSubgroup

L104 ↗
KummerTheory.RadicalDatum.ambientNthPowersSubgroup
Documentation

Elements of the radical subgroup which are n-th powers in the ambient Kˣ.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 ambientNthPowersSubgroup : Subgroup D.carrier
theorem

mem_ambientNthPowersSubgroup_iff

L108 ↗
KummerTheory.RadicalDatum.mem_ambientNthPowersSubgroup_iff
Documentation

An element belongs to the ambient power subgroup exactly when it is an nth power.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 mem_ambientNthPowersSubgroup_iff {a : D.carrier} :
    a ∈ D.ambientNthPowersSubgroup ↔ ∃ b : Kˣ, b ^ (n : ℕ) = a.1
theorem

rootCharacter_eq_one_of_mem_ambientNthPowers

L113 ↗
KummerTheory.RadicalDatum.rootCharacter_eq_one_of_mem_ambientNthPowers
Documentation

A root character is trivial on an ambient n-th power.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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_one_of_mem_ambientNthPowers
    (hfixed : ∀ σ : Gal(L/K), ∀ u : Lˣ, u ^ (n : ℕ) = 1 → σ • u = u)
    {a : D.carrier} (ha : a ∈ D.ambientNthPowersSubgroup) :
    D.rootCharacter a hfixed = 1
theorem

ambientNthPowersSubgroup_le_ker

L127 ↗
KummerTheory.RadicalDatum.ambientNthPowersSubgroup_le_ker
Documentation

The ambient n-th-power subgroup lies in the kernel of the Kummer character.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 ambientNthPowersSubgroup_le_ker
    (hfixed : ∀ σ : Gal(L/K), ∀ u : Lˣ, u ^ (n : ℕ) = 1 → σ • u = u) :
    D.ambientNthPowersSubgroup ≤ MonoidHom.ker (D.kummerCharacterWithoutSection hfixed)
theorem

ker_kummerCharacterWithoutSection_eq_ambientNthPowers

L141 ↗
KummerTheory.RadicalDatum.ker_kummerCharacterWithoutSection_eq_ambientNthPowers
Documentation

For a Galois extension, triviality of the Kummer character forces the chosen root to come from the base field. Consequently the kernel is exactly the subgroup of ambient n-th powers, not merely a subgroup containing it.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 ker_kummerCharacterWithoutSection_eq_ambientNthPowers
    [IsGalois K L]
    (hfixed : ∀ σ : Gal(L/K), ∀ u : Lˣ, u ^ (n : ℕ) = 1 → σ • u = u) :
    MonoidHom.ker (D.kummerCharacterWithoutSection hfixed) =
      D.ambientNthPowersSubgroup
def

RadicalQuotient

L180 ↗
KummerTheory.RadicalDatum.RadicalQuotient
Documentation

The ambient radical quotient Δ / (Δ ∩ Kˣⁿ).

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 RadicalQuotient : Type _
instance

radicalQuotient_commGroupInstance

L185 ↗
KummerTheory.RadicalDatum.radicalQuotient_commGroupInstance
Documentation

The commutative group structure transported to the named ambient radical quotient.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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
instance radicalQuotient_commGroupInstance : CommGroup D.RadicalQuotient
def

radicalQuotientMulEquiv

L191 ↗
KummerTheory.RadicalDatum.radicalQuotientMulEquiv
Documentation

Comparison with the group-library presentation of the ambient radical quotient.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 radicalQuotientMulEquiv :
    D.RadicalQuotient ≃* (D.carrier ⧸ D.ambientNthPowersSubgroup)
def

radicalQuotientMk

L196 ↗
KummerTheory.RadicalDatum.radicalQuotientMk
Documentation

The canonical projection to the named ambient radical quotient.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 radicalQuotientMk : D.carrier →* D.RadicalQuotient
theorem

radicalQuotientMk_apply

L201 ↗
KummerTheory.RadicalDatum.radicalQuotientMk_apply
Documentation

The named radical quotient projection agrees with the underlying quotient map.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 radicalQuotientMk_apply (a : D.carrier) :
    D.radicalQuotientMulEquiv (D.radicalQuotientMk a) =
      (QuotientGroup.mk a : D.carrier ⧸ D.ambientNthPowersSubgroup)
theorem

radicalQuotientMk_eq_one_iff

L209 ↗
KummerTheory.RadicalDatum.radicalQuotientMk_eq_one_iff
Documentation

A radical quotient class is trivial exactly when its representative is an ambient nth power.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 radicalQuotientMk_eq_one_iff (a : D.carrier) :
    D.radicalQuotientMk a = 1 ↔ a ∈ D.ambientNthPowersSubgroup
theorem

radicalQuotientMk_eq_iff

L219 ↗
KummerTheory.RadicalDatum.radicalQuotientMk_eq_iff
Documentation

Two radical quotient representatives agree exactly when their ratio is an ambient nth power.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 radicalQuotientMk_eq_iff (a b : D.carrier) :
    D.radicalQuotientMk a = D.radicalQuotientMk b ↔
      a / b ∈ D.ambientNthPowersSubgroup
theorem

radicalQuotientMk_surjective

L229 ↗
KummerTheory.RadicalDatum.radicalQuotientMk_surjective
Documentation

Every ambient radical class has a representative in D.carrier.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 radicalQuotientMk_surjective :
    Function.Surjective D.radicalQuotientMk
theorem

radicalQuotient_inductionOn

L237 ↗
KummerTheory.RadicalDatum.radicalQuotient_inductionOn
Documentation

Eliminate a named ambient radical quotient through its canonical representatives.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 radicalQuotient_inductionOn
    {motive : D.RadicalQuotient → Prop} (q : D.RadicalQuotient)
    (mk : ∀ a : D.carrier, motive (D.radicalQuotientMk a)) :
    motive q
def

radicalQuotientLift

L244 ↗
KummerTheory.RadicalDatum.radicalQuotientLift
Documentation

Descend a homomorphism through the named ambient radical quotient.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 radicalQuotientLift {M : Type*} [Group M]
    (f : D.carrier →* M)
    (hf : D.ambientNthPowersSubgroup ≤ MonoidHom.ker f) :
    D.RadicalQuotient →* M
theorem

radicalQuotientLift_mk

L253 ↗
KummerTheory.RadicalDatum.radicalQuotientLift_mk
Documentation

The radical quotient lift evaluates on a representative by the prescribed lift.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 radicalQuotientLift_mk {M : Type*} [Group M]
    (f : D.carrier →* M)
    (hf : D.ambientNthPowersSubgroup ≤ MonoidHom.ker f)
    (a : D.carrier) :
    D.radicalQuotientLift f hf (D.radicalQuotientMk a) = f a
def

quotientKummerCharacterWithoutSection

L261 ↗
KummerTheory.RadicalDatum.quotientKummerCharacterWithoutSection
Documentation

The Kummer character descended to the correct ambient-power quotient.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 quotientKummerCharacterWithoutSection
    (hfixed : ∀ σ : Gal(L/K), ∀ u : Lˣ, u ^ (n : ℕ) = 1 → σ • u = u) :
    D.RadicalQuotient →* (Gal(L/K) →* nthRootsSubgroup L (n : ℕ))
theorem

quotientKummerCharacterWithoutSection_mk

L268 ↗
KummerTheory.RadicalDatum.quotientKummerCharacterWithoutSection_mk
Documentation

The section-free Kummer character on a quotient class is computed from any representative.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 quotientKummerCharacterWithoutSection_mk (a : D.carrier)
    (hfixed : ∀ σ : Gal(L/K), ∀ u : Lˣ, u ^ (n : ℕ) = 1 → σ • u = u) :
    D.quotientKummerCharacterWithoutSection hfixed
        (D.radicalQuotientMk a) =
      D.kummerCharacterWithoutSection hfixed a
theorem

quotientKummerCharacterWithoutSection_injective

L277 ↗
KummerTheory.RadicalDatum.quotientKummerCharacterWithoutSection_injective
Documentation

The character map on the ambient radical quotient is injective. This is the kernel half of the canonical isomorphism in the finite Kummer character equivalence.

Source context 5 commands

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

namespace KummerTheory
section RadicalQuotient
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 quotientKummerCharacterWithoutSection_injective
    [IsGalois K L]
    (hfixed : ∀ σ : Gal(L/K), ∀ u : Lˣ, u ^ (n : ℕ) = 1 → σ • u = u) :
    Function.Injective (D.quotientKummerCharacterWithoutSection hfixed)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.