Module

RootFieldPowerClasses.lean

Nyll.AnabelianGeometry.KummerTheory.RootFieldPowerClasses

6 declarations indexed from sourceView source ↗

Module documentation

Power classes recovered from a root field

Over a field containing the relevant roots of unity, the full root field of a unit determines its cyclic subgroup modulo powers. The statement retains the roots-of-unity hypothesis; it does not assert descent through an arbitrary cyclotomic extension.

Imports2

Imported by3

def

cyclicPowerSubgroup

L28 ↗

AnabelianGeometry.KummerTheory.cyclicPowerSubgroup

Documentation

The cyclic subgroup generated by a unit, enlarged by all ambient powers.

Source context 4 commands

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

noncomputable section
namespace AnabelianGeometry.KummerTheory
open _root_.KummerTheory
variable {K L : Type*} [Field K] [Field L] [Algebra K L] [IsSepClosure K L]

Lean source · statement

def cyclicPowerSubgroup (n : ℕ+) (a : Kˣ) : KummerSubgroup K n

theorem

rootField_eq_cyclicPowerRadical

L33 ↗

AnabelianGeometry.KummerTheory.rootField_eq_cyclicPowerRadical

Documentation

The full root field is the radical extension associated with the cyclic power subgroup.

Source context 4 commands

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

noncomputable section
namespace AnabelianGeometry.KummerTheory
open _root_.KummerTheory
variable {K L : Type*} [Field K] [Field L] [Algebra K L] [IsSepClosure K L]

Lean source · statement

theorem rootField_eq_cyclicPowerRadical
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ) :
    rootField (L := L) n (a : K) =
      kummerRadicalExtension (K := K) (Omega := L) n (cyclicPowerSubgroup n a).val

theorem

rootField_radicalSubgroup

L76 ↗

AnabelianGeometry.KummerTheory.rootField_radicalSubgroup

Documentation

The radical subgroup of the root field is exactly the cyclic subgroup modulo ambient powers, rather than an unspecified larger subgroup.

Source context 4 commands

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

noncomputable section
namespace AnabelianGeometry.KummerTheory
open _root_.KummerTheory
variable {K L : Type*} [Field K] [Field L] [Algebra K L] [IsSepClosure K L]

Lean source · statement

theorem rootField_radicalSubgroup
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ) :
    finiteKummerRadicalSubgroup (K := K) (L := rootField (L := L) n (a : K)) n =
      (cyclicPowerSubgroup n a).val

theorem

rootField_eq_iff_cyclicPowerSubgroup_eq

L87 ↗

AnabelianGeometry.KummerTheory.rootField_eq_iff_cyclicPowerSubgroup_eq

Documentation

Equality of root fields is equivalent to equality of cyclic power subgroups when the roots of unity belong to the base field.

Source context 4 commands

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

noncomputable section
namespace AnabelianGeometry.KummerTheory
open _root_.KummerTheory
variable {K L : Type*} [Field K] [Field L] [Algebra K L] [IsSepClosure K L]

Lean source · statement

theorem rootField_eq_iff_cyclicPowerSubgroup_eq
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b : Kˣ) :
    rootField (L := L) n (a : K) = rootField (L := L) n (b : K) ↔
      cyclicPowerSubgroup n a = cyclicPowerSubgroup n b

theorem

exists_zpow_mul_power_of_rootField_eq

L103 ↗

AnabelianGeometry.KummerTheory.exists_zpow_mul_power_of_rootField_eq

Documentation

Equal full root fields give an explicit multiplicative relation modulo n-th powers when the base contains the n-th roots of unity.

Source context 4 commands

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

noncomputable section
namespace AnabelianGeometry.KummerTheory
open _root_.KummerTheory
variable {K L : Type*} [Field K] [Field L] [Algebra K L] [IsSepClosure K L]

Lean source · statement

theorem exists_zpow_mul_power_of_rootField_eq
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b : Kˣ)
    (h : rootField (L := L) n (a : K) = rootField (L := L) n (b : K)) :
    ∃ k : ℤ, ∃ c : Kˣ, b = a ^ k * c ^ (n : ℕ)

theorem

cyclicPowerSubgroup_baseChange_eq_of_rootField_eq

L122 ↗

AnabelianGeometry.KummerTheory.cyclicPowerSubgroup_baseChange_eq_of_rootField_eq

Documentation

After adjoining the relevant roots of unity, equal root fields over the original base give equal cyclic power subgroups over the extended base. No descent of the resulting power relation is asserted here.

Source context 5 commands

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

noncomputable section
namespace AnabelianGeometry.KummerTheory
open _root_.KummerTheory
variable {K L : Type*} [Field K] [Field L] [Algebra K L] [IsSepClosure K L]
omit [IsSepClosure K L] in

Lean source · statement

theorem cyclicPowerSubgroup_baseChange_eq_of_rootField_eq
    (C : IntermediateField K L) [IsSepClosure C L]
    (n : ℕ+) (hn : ((n : ℕ) : C) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) C).Nonempty) (a b : Kˣ)
    (h : rootField (L := L) n (a : K) = rootField (L := L) n (b : K)) :
    cyclicPowerSubgroup n (Units.map (algebraMap K C).toMonoidHom a) =
      cyclicPowerSubgroup n (Units.map (algebraMap K C).toMonoidHom b)

Module documentation

Power classes recovered from a root field

Declarations

cyclicPowerSubgroup

rootField_eq_cyclicPowerRadical

rootField_radicalSubgroup

rootField_eq_iff_cyclicPowerSubgroup_eq

exists_zpow_mul_power_of_rootField_eq

cyclicPowerSubgroup_baseChange_eq_of_rootField_eq