Module

FiniteConstants.lean

Nyll.GaloisCohomology.FieldTheory.FiniteConstants

4 declarations indexed from sourceView source ↗

Module documentation

Finite algebraic constant fields

A finite relative algebraic closure contains all roots of unity. It also supplies an element outside the image of every map x ↦ x ^ n - x, for n > 1.

Imports4

Mathlib.FieldTheory.AlgebraicClosure
Mathlib.GroupTheory.Torsion
Mathlib.Algebra.Polynomial.Monic
Mathlib.Data.Fintype.Card

Imported by2

theorem

torsionUnit_mem_algebraicClosure

L24 ↗

FieldTheory.torsionUnit_mem_algebraicClosure

Documentation

Every root of unity lies in the relative algebraic closure.

Source context 3 commands

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

namespace FieldTheory
universe u v
variable (F : Type u) (K : Type v) [Field F] [Field K] [Algebra F K]

Lean source · statement

theorem torsionUnit_mem_algebraicClosure (z : Kˣ) (hz : IsOfFinOrder z) :
    (z : K) ∈ algebraicClosure F K

theorem

finite_torsion_units_of_finite_algebraicClosure

L34 ↗

FieldTheory.finite_torsion_units_of_finite_algebraicClosure

Documentation

A finite field of constants makes the full torsion subgroup of units finite.

Source context 3 commands

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

namespace FieldTheory
universe u v
variable (F : Type u) (K : Type v) [Field F] [Field K] [Algebra F K]

Lean source · statement

theorem finite_torsion_units_of_finite_algebraicClosure
    [Finite (algebraicClosure F K)] : Finite (CommGroup.torsion Kˣ)

theorem

finite_primaryComponent_of_finite_algebraicClosure

L44 ↗

FieldTheory.finite_primaryComponent_of_finite_algebraicClosure

Documentation

In particular, every prime-primary root group is finite.

Source context 3 commands

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

namespace FieldTheory
universe u v
variable (F : Type u) (K : Type v) [Field F] [Field K] [Algebra F K]

Lean source · statement

theorem finite_primaryComponent_of_finite_algebraicClosure
    [Finite (algebraicClosure F K)] (p : ℕ) [Fact p.Prime] :
    Finite (CommGroup.primaryComponent Kˣ p)

theorem

exists_not_pow_sub_of_finite_algebraicClosure

L57 ↗

FieldTheory.exists_not_pow_sub_of_finite_algebraicClosure

Documentation

If the algebraic constant field is finite, x ↦ x ^ n - x is not onto for any exponent greater than one. This includes the Artin--Schreier map.

Source context 3 commands

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

namespace FieldTheory
universe u v
variable (F : Type u) (K : Type v) [Field F] [Field K] [Algebra F K]

Lean source · statement

theorem exists_not_pow_sub_of_finite_algebraicClosure
    [Finite (algebraicClosure F K)] (n : ℕ) (hn : 1 < n) :
    ∃ a : K, ∀ x : K, x ^ n - x ≠ a

Module documentation

Finite algebraic constant fields

Declarations

torsionUnit_mem_algebraicClosure

finite_torsion_units_of_finite_algebraicClosure

finite_primaryComponent_of_finite_algebraicClosure

exists_not_pow_sub_of_finite_algebraicClosure