NYLL
Module

FiniteSupport.lean

Nyll.GaloisCohomology.Kummer.Concrete.FiniteSupport
29 declarations indexed from sourceView source ↗

Module documentation

finite radical support

Membership in K(√[n]{Δ}) uses only finitely many of the adjoined roots. For such a finite root set this file chooses the corresponding coefficients in Δ, records them in a finite subset of Kˣ, and forms the subgroup they generate. The resulting subgroup lies in Δ, and every selected root has its n-th power in that finitely generated subgroup.

These are the concrete finite-support data needed for the later reduction to finite Kummer theory; no finite Kummer endpoint is assumed here.

Imports2
Imported by2

Declarations

theorem

exists_finset_kummerRootSet_of_mem_kummerRadicalExtension

L33 ↗
KummerTheory.exists_finset_kummerRootSet_of_mem_kummerRadicalExtension
Documentation

An element of a radical extension belongs to the field generated by a finite subset of the full Kummer root set.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem exists_finset_kummerRootSet_of_mem_kummerRadicalExtension
    (n : ℕ+) (Delta : Subgroup Kˣ) {beta : Omega}
    (hbeta : beta ∈ kummerRadicalExtension (K := K) (Omega := Omega) n Delta) :
    ∃ T : Finset Omega,
      (T : Set Omega) ⊆ kummerRootSet (K := K) (Omega := Omega) n Delta ∧
      beta ∈ IntermediateField.adjoin K (T : Set Omega)
def

chosenFiniteSupportCoefficient

L43 ↗
KummerTheory.chosenFiniteSupportCoefficient
Documentation

For each member of a finite Kummer root set, choose its coefficient in Delta. This choice is made only after the finite root set is known.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
def chosenFiniteSupportCoefficient
    (n : ℕ+) (Delta : Subgroup Kˣ) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆ kummerRootSet (K := K) (Omega := Omega) n Delta)
    (beta : T) : Delta
theorem

chosenFiniteSupportCoefficient_pow

L50 ↗
KummerTheory.chosenFiniteSupportCoefficient_pow
Documentation

The chosen coefficient really is the n-th power of its root.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem chosenFiniteSupportCoefficient_pow
    (n : ℕ+) (Delta : Subgroup Kˣ) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆ kummerRootSet (K := K) (Omega := Omega) n Delta)
    (beta : T) :
    (beta.1 : Omega) ^ (n : ℕ) =
      algebraMap K Omega ((chosenFiniteSupportCoefficient n Delta T hT beta).1 : K)
def

chosenFiniteSupportCoefficientSet

L59 ↗
KummerTheory.chosenFiniteSupportCoefficientSet
Documentation

The finite set of base-field coefficients used by the selected roots.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
def chosenFiniteSupportCoefficientSet
    (n : ℕ+) (Delta : Subgroup Kˣ) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆ kummerRootSet (K := K) (Omega := Omega) n Delta) :
    Finset Kˣ
def

chosenFiniteSupportCoefficientSubgroup

L68 ↗
KummerTheory.chosenFiniteSupportCoefficientSubgroup
Documentation

The subgroup Delta₀ generated by the finitely many selected coefficients.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
def chosenFiniteSupportCoefficientSubgroup
    (n : ℕ+) (Delta : Subgroup Kˣ) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆ kummerRootSet (K := K) (Omega := Omega) n Delta) :
    Subgroup Kˣ
theorem

chosenFiniteSupportCoefficient_mem_set

L76 ↗
KummerTheory.chosenFiniteSupportCoefficient_mem_set
Documentation

The selected nonzero coefficient belongs to the finite support set.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem chosenFiniteSupportCoefficient_mem_set
    (n : ℕ+) (Delta : Subgroup Kˣ) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆ kummerRootSet (K := K) (Omega := Omega) n Delta)
    (beta : T) :
    (chosenFiniteSupportCoefficient n Delta T hT beta).1 ∈
      chosenFiniteSupportCoefficientSet (K := K) (Omega := Omega) n Delta T hT
theorem

chosenFiniteSupportCoefficientSubgroup_le

L89 ↗
KummerTheory.chosenFiniteSupportCoefficientSubgroup_le
Documentation

The finitely generated coefficient subgroup is a subgroup of the original radical subgroup Delta.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem chosenFiniteSupportCoefficientSubgroup_le
    (n : ℕ+) (Delta : Subgroup Kˣ) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆ kummerRootSet (K := K) (Omega := Omega) n Delta) :
    chosenFiniteSupportCoefficientSubgroup (K := K) (Omega := Omega) n Delta T hT ≤ Delta
theorem

chosenFiniteSupportCoefficient_mem_subgroup

L102 ↗
KummerTheory.chosenFiniteSupportCoefficient_mem_subgroup
Documentation

Each chosen coefficient belongs to the generated subgroup Delta₀.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem chosenFiniteSupportCoefficient_mem_subgroup
    (n : ℕ+) (Delta : Subgroup Kˣ) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆ kummerRootSet (K := K) (Omega := Omega) n Delta)
    (beta : T) :
    (chosenFiniteSupportCoefficient n Delta T hT beta).1 ∈
      chosenFiniteSupportCoefficientSubgroup (K := K) (Omega := Omega) n Delta T hT
theorem

finiteSupportRoot_pow_from_coefficientSubgroup

L113 ↗
KummerTheory.finiteSupportRoot_pow_from_coefficientSubgroup
Documentation

Every selected root is an n-th root of an actual element of the finite-support subgroup Delta₀.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem finiteSupportRoot_pow_from_coefficientSubgroup
    (n : ℕ+) (Delta : Subgroup Kˣ) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆ kummerRootSet (K := K) (Omega := Omega) n Delta)
    (beta : T) :
    ∃ a : chosenFiniteSupportCoefficientSubgroup (K := K) (Omega := Omega) n Delta T hT,
      (beta.1 : Omega) ^ (n : ℕ) = algebraMap K Omega (a.1 : K)
theorem

exists_finiteKummerSupport

L129 ↗
KummerTheory.exists_finiteKummerSupport
Documentation

Complete finite-support data extracted from one element of K(√[n]{Delta}): finite roots generating the element, a concrete finite coefficient set, its generated subgroup Delta₀ ≤ Delta, and an n-th-power equation over Delta₀ for every selected root.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem exists_finiteKummerSupport
    (n : ℕ+) (Delta : Subgroup Kˣ) {beta : Omega}
    (hbeta : beta ∈ kummerRadicalExtension (K := K) (Omega := Omega) n Delta) :
    ∃ (T : Finset Omega)
      (hT : (T : Set Omega) ⊆ kummerRootSet (K := K) (Omega := Omega) n Delta),
      beta ∈ IntermediateField.adjoin K (T : Set Omega) ∧
      chosenFiniteSupportCoefficientSubgroup (K := K) (Omega := Omega) n Delta T hT ≤ Delta ∧
      ∀ root : T,
        ∃ a : chosenFiniteSupportCoefficientSubgroup
            (K := K) (Omega := Omega) n Delta T hT,
          (root.1 : Omega) ^ (n : ℕ) = algebraMap K Omega (a.1 : K)
def

admissibleFiniteSupportSubgroup

L148 ↗
KummerTheory.admissibleFiniteSupportSubgroup
Documentation

Add all ambient n-th powers to the finite coefficient subgroup. The result is an admissible subgroup-side object for the Kummer correspondence.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
def admissibleFiniteSupportSubgroup
    (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1) :
    KummerSubgroup K n
theorem

admissibleFiniteSupportSubgroup_le

L159 ↗
KummerTheory.admissibleFiniteSupportSubgroup_le
Documentation

The admissible finite-support subgroup still lies in the original admissible subgroup Delta.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem admissibleFiniteSupportSubgroup_le
    (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1) :
    (admissibleFiniteSupportSubgroup
      (K := K) (Omega := Omega) n Delta T hT).1 ≤ Delta.1
def

finiteSupportNthPowersSubgroup

L169 ↗
KummerTheory.finiteSupportNthPowersSubgroup
Documentation

The copy of Kˣⁿ inside the admissible finite-support subgroup.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
def finiteSupportNthPowersSubgroup
    (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1) :
    Subgroup (admissibleFiniteSupportSubgroup
      (K := K) (Omega := Omega) n Delta T hT).1
def

FiniteSupportKummerQuotient

L180 ↗
KummerTheory.FiniteSupportKummerQuotient
Documentation

The finite-support quotient Delta₀ / Kˣⁿ.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
def FiniteSupportKummerQuotient
    (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1)
instance

finiteSupportKummerQuotient_commGroupInstance

L191 ↗
KummerTheory.finiteSupportKummerQuotient_commGroupInstance
Documentation

The commutative group structure on the named finite-support Kummer quotient.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
instance finiteSupportKummerQuotient_commGroupInstance
    (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1) :
    CommGroup (FiniteSupportKummerQuotient
      (K := K) (Omega := Omega) n Delta T hT)
def

finiteSupportKummerQuotientMulEquiv

L206 ↗
KummerTheory.finiteSupportKummerQuotientMulEquiv
Documentation

Comparison with the group-library presentation of the finite-support Kummer quotient.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
def finiteSupportKummerQuotientMulEquiv
    (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1) :
    FiniteSupportKummerQuotient (K := K) (Omega := Omega) n Delta T hT ≃*
      ((admissibleFiniteSupportSubgroup
          (K := K) (Omega := Omega) n Delta T hT).1 ⧸
        finiteSupportNthPowersSubgroup
          (K := K) (Omega := Omega) n Delta T hT)
def

finiteSupportKummerQuotientMk

L218 ↗
KummerTheory.finiteSupportKummerQuotientMk
Documentation

The canonical projection to the named finite-support Kummer quotient.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
def finiteSupportKummerQuotientMk
    (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1) :
    (admissibleFiniteSupportSubgroup
        (K := K) (Omega := Omega) n Delta T hT).1 →*
      FiniteSupportKummerQuotient
        (K := K) (Omega := Omega) n Delta T hT
theorem

finiteSupportKummerQuotientMk_eq_one_iff

L233 ↗
KummerTheory.finiteSupportKummerQuotientMk_eq_one_iff
Documentation

A finite-support Kummer class is trivial exactly when its representative lies in the defining subgroup.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem finiteSupportKummerQuotientMk_eq_one_iff
    (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1)
    (a : (admissibleFiniteSupportSubgroup
      (K := K) (Omega := Omega) n Delta T hT).1) :
    finiteSupportKummerQuotientMk
        (K := K) (Omega := Omega) n Delta T hT a = 1 ↔
      a ∈ finiteSupportNthPowersSubgroup
        (K := K) (Omega := Omega) n Delta T hT
theorem

finiteSupportKummerQuotientMk_eq_iff

L252 ↗
KummerTheory.finiteSupportKummerQuotientMk_eq_iff
Documentation

Equality of finite-support Kummer classes is characterized by their quotient lying in the defining subgroup.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem finiteSupportKummerQuotientMk_eq_iff
    (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1)
    (a b : (admissibleFiniteSupportSubgroup
      (K := K) (Omega := Omega) n Delta T hT).1) :
    finiteSupportKummerQuotientMk
        (K := K) (Omega := Omega) n Delta T hT a =
      finiteSupportKummerQuotientMk
        (K := K) (Omega := Omega) n Delta T hT b ↔
      a / b ∈ finiteSupportNthPowersSubgroup
        (K := K) (Omega := Omega) n Delta T hT
theorem

finiteSupportKummerQuotientMk_surjective

L274 ↗
KummerTheory.finiteSupportKummerQuotientMk_surjective
Documentation

Every finite-support Kummer class has a representative.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem finiteSupportKummerQuotientMk_surjective
    (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1) :
    Function.Surjective
      (finiteSupportKummerQuotientMk
        (K := K) (Omega := Omega) n Delta T hT)
theorem

finiteSupportKummerQuotient_inductionOn

L289 ↗
KummerTheory.finiteSupportKummerQuotient_inductionOn
Documentation

Eliminate a finite-support Kummer quotient through canonical representatives.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem finiteSupportKummerQuotient_inductionOn
    (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1)
    {motive : FiniteSupportKummerQuotient
      (K := K) (Omega := Omega) n Delta T hT → Prop}
    (q : FiniteSupportKummerQuotient
      (K := K) (Omega := Omega) n Delta T hT)
    (mk : ∀ a, motive (finiteSupportKummerQuotientMk
      (K := K) (Omega := Omega) n Delta T hT a)) :
    motive q
def

finiteSupportKummerQuotientLift

L303 ↗
KummerTheory.finiteSupportKummerQuotientLift
Documentation

Descend a homomorphism through the named finite-support quotient.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
def finiteSupportKummerQuotientLift {M : Type*} [Group M]
    (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1)
    (f : (admissibleFiniteSupportSubgroup
      (K := K) (Omega := Omega) n Delta T hT).1 →* M)
    (hf : finiteSupportNthPowersSubgroup
      (K := K) (Omega := Omega) n Delta T hT ≤ MonoidHom.ker f) :
    FiniteSupportKummerQuotient
      (K := K) (Omega := Omega) n Delta T hT →* M
theorem

finiteSupportKummerQuotientLift_mk

L321 ↗
KummerTheory.finiteSupportKummerQuotientLift_mk
Documentation

The finite-support quotient lift evaluates on a representative by the chosen lift.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem finiteSupportKummerQuotientLift_mk {M : Type*} [Group M]
    (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1)
    (f : (admissibleFiniteSupportSubgroup
      (K := K) (Omega := Omega) n Delta T hT).1 →* M)
    (hf : finiteSupportNthPowersSubgroup
      (K := K) (Omega := Omega) n Delta T hT ≤ MonoidHom.ker f)
    (a : (admissibleFiniteSupportSubgroup
      (K := K) (Omega := Omega) n Delta T hT).1) :
    finiteSupportKummerQuotientLift
        (K := K) (Omega := Omega) n Delta T hT f hf
        (finiteSupportKummerQuotientMk
          (K := K) (Omega := Omega) n Delta T hT a) = f a
theorem

finiteSupportRoot_pow_from_admissibleSubgroup

L339 ↗
KummerTheory.finiteSupportRoot_pow_from_admissibleSubgroup
Documentation

A selected root still has its n-th power in the enlarged admissible subgroup Delta₀.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem finiteSupportRoot_pow_from_admissibleSubgroup
    (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1)
    (root : T) :
    ∃ a : (admissibleFiniteSupportSubgroup
        (K := K) (Omega := Omega) n Delta T hT).1,
      (root.1 : Omega) ^ (n : ℕ) = algebraMap K Omega (a.1 : K)
def

chosenFiniteSupportCoefficientToQuotient

L356 ↗
KummerTheory.chosenFiniteSupportCoefficientToQuotient
Documentation

The quotient map restricted to the finitely generated coefficient subgroup.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
def chosenFiniteSupportCoefficientToQuotient
    (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1) :
    chosenFiniteSupportCoefficientSubgroup (K := K) (Omega := Omega) n Delta.1 T hT →*
      FiniteSupportKummerQuotient (K := K) (Omega := Omega) n Delta T hT
theorem

chosenFiniteSupportCoefficientToQuotient_surjective

L367 ↗
KummerTheory.chosenFiniteSupportCoefficientToQuotient_surjective
Documentation

The finite coefficient subgroup generates Delta₀ / Kˣⁿ.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem chosenFiniteSupportCoefficientToQuotient_surjective
    (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1) :
    Function.Surjective
      (chosenFiniteSupportCoefficientToQuotient
        (K := K) (Omega := Omega) n Delta T hT)
theorem

finiteSupportKummerQuotient_pow_eq_one

L394 ↗
KummerTheory.finiteSupportKummerQuotient_pow_eq_one
Documentation

Every element of Delta₀ / Kˣⁿ is killed by n.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem finiteSupportKummerQuotient_pow_eq_one
    (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1)
    (q : FiniteSupportKummerQuotient
      (K := K) (Omega := Omega) n Delta T hT) :
    q ^ (n : ℕ) = 1
theorem

finiteSupportKummerQuotient_finite

L415 ↗
KummerTheory.finiteSupportKummerQuotient_finite
Documentation

The restricted radical quotient Delta₀ / Kˣⁿ is finite: it is a finitely generated commutative group, generated by the selected coefficients, and every element is killed by n.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem finiteSupportKummerQuotient_finite
    (n : ℕ+) (Delta : KummerSubgroup K n) (T : Finset Omega)
    (hT : (T : Set Omega) ⊆
      kummerRootSet (K := K) (Omega := Omega) n Delta.1) :
    Finite (FiniteSupportKummerQuotient
      (K := K) (Omega := Omega) n Delta T hT)
theorem

exists_admissibleFiniteKummerSupport

L444 ↗
KummerTheory.exists_admissibleFiniteKummerSupport
Documentation

Full admissible finite-support package extracted from one element of K(√[n]{Delta}). In addition to the finite root support, it produces the admissible subgroup Delta₀ ≤ Delta, power equations over Delta₀, and the finiteness of Delta₀ / Kˣⁿ.

Source context 3 commands

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

noncomputable section
namespace KummerTheory
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem exists_admissibleFiniteKummerSupport
    (n : ℕ+) (Delta : KummerSubgroup K n) {beta : Omega}
    (hbeta : beta ∈
      kummerRadicalExtension (K := K) (Omega := Omega) n Delta.1) :
    ∃ (T : Finset Omega)
      (hT : (T : Set Omega) ⊆
        kummerRootSet (K := K) (Omega := Omega) n Delta.1),
      beta ∈ IntermediateField.adjoin K (T : Set Omega) ∧
      (admissibleFiniteSupportSubgroup
        (K := K) (Omega := Omega) n Delta T hT).1 ≤ Delta.1 ∧
      (∀ root : T,
        ∃ a : (admissibleFiniteSupportSubgroup
            (K := K) (Omega := Omega) n Delta T hT).1,
          (root.1 : Omega) ^ (n : ℕ) = algebraMap K Omega (a.1 : K)) ∧
      Finite (FiniteSupportKummerQuotient
        (K := K) (Omega := Omega) n Delta T hT)

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