Module

CyclotomicInfiniteImage.lean

Nyll.GaloisCohomology.Kummer.Concrete.CyclotomicInfiniteImage

3 declarations indexed from sourceView source ↗

Module documentation

Infinite image of the cyclotomic character

A finite cyclotomic image would yield a finite fixed field containing all primary roots of unity. The actual primitive roots contradict finiteness.

Imports3

Nyll.GaloisCohomology.Kummer.Concrete.PrimitiveRootCoordinates
Mathlib.FieldTheory.Galois.Infinite
Mathlib.GroupTheory.Torsion

Imported by4

theorem

infinite_primaryComponent_of_primitive_roots

L23 ↗

KummerTheory.infinite_primaryComponent_of_primitive_roots

Documentation

Roots of unbounded prime-power order give an infinite primary group.

Source context 3 commands

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

namespace KummerTheory
universe u v
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem infinite_primaryComponent_of_primitive_roots
    (p : ℕ) [Fact p.Prime] [∀ i : ℕ, HasEnoughRootsOfUnity Ω (p ^ i)] :
    Infinite (CommGroup.primaryComponent Ωˣ p)

theorem

primaryUnit_mem_fixedField_cyclotomic_ker

L41 ↗

KummerTheory.primaryUnit_mem_fixedField_cyclotomic_ker

Documentation

Every primary root is fixed by the kernel of the cyclotomic character.

Source context 3 commands

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

namespace KummerTheory
universe u v
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem primaryUnit_mem_fixedField_cyclotomic_ker
    (p : ℕ) [Fact p.Prime] [∀ i : ℕ, HasEnoughRootsOfUnity Ω (p ^ i)]
    (z : CommGroup.primaryComponent Ωˣ p) :
    (z.val : Ω) ∈ IntermediateField.fixedField
      ((cyclotomicCharacter Ω p).comp (MulSemiringAction.toRingAut Gal(Ω/K) Ω)).ker

theorem

infinite_range_cyclotomicCharacter_of_finite_primary

L59 ↗

KummerTheory.infinite_range_cyclotomicCharacter_of_finite_primary

Documentation

Finiteness of primary roots in finite subextensions forces infinite image.

Source context 3 commands

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

namespace KummerTheory
universe u v
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem infinite_range_cyclotomicCharacter_of_finite_primary
    [IsGalois K Ω]
    (p : ℕ) [Fact p.Prime] [∀ i : ℕ, HasEnoughRootsOfUnity Ω (p ^ i)]
    (hRoots : ∀ E : IntermediateField K Ω, FiniteDimensional K E →
      Finite (CommGroup.primaryComponent Eˣ p)) :
    Set.Infinite (Set.range
      ((cyclotomicCharacter Ω p).comp (MulSemiringAction.toRingAut Gal(Ω/K) Ω)))

Module documentation

Infinite image of the cyclotomic character

Declarations

infinite_primaryComponent_of_primitive_roots

primaryUnit_mem_fixedField_cyclotomic_ker

infinite_range_cyclotomicCharacter_of_finite_primary