Module

SeparableClosureRootsOfUnity.lean

Nyll.EtaleFundamentalGroups.Inertia.SeparableClosureRootsOfUnity

5 declarations indexed from sourceView source ↗

Module documentation

Prime-to-characteristic roots of unity in the separable closure

The canonical inclusion from the relative separable closure induces an isomorphism on roots of unity of order invertible in the base field. This is the change of residue field needed in Stacks Project, Tag 0BUB.

Reference: https://stacks.math.columbia.edu/tag/0BUB

Imports2

Mathlib.FieldTheory.SeparableClosure
Mathlib.RingTheory.RootsOfUnity.Basic

Imported by2

theorem

rootOfUnity_mem_separableClosure

L30 ↗

EtaleFundamentalGroups.Inertia.rootOfUnity_mem_separableClosure

Documentation

Every root of unity of order nonzero in the base field is separable over that field, by the separability of X ^ n - 1.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open Polynomial
universe u v

Lean source · statement

theorem rootOfUnity_mem_separableClosure
    (k : Type u) (E : Type v) [Field k] [Field E] [Algebra k E]
    (n : ℕ) (hn : (n : k) ≠ 0) (ζ : rootsOfUnity n E) :
    ((ζ : Eˣ) : E) ∈ separableClosure k E

theorem

separableClosure_rootsOfUnity_bijective

L43 ↗

EtaleFundamentalGroups.Inertia.separableClosure_rootsOfUnity_bijective

Documentation

The literal inclusion of the relative separable closure is bijective on the prime-to-characteristic roots of unity.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open Polynomial
universe u v

Lean source · statement

theorem separableClosure_rootsOfUnity_bijective
    (k : Type u) (E : Type v) [Field k] [Field E] [Algebra k E]
    (n : ℕ) (hn : (n : k) ≠ 0) :
    Function.Bijective (restrictRootsOfUnity (algebraMap (separableClosure k E) E) n)

def

separableClosureRootsOfUnityEquiv

L67 ↗

EtaleFundamentalGroups.Inertia.separableClosureRootsOfUnityEquiv

Documentation

Canonical identification of the two roots-of-unity groups, with no chosen primitive root.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open Polynomial
universe u v

Lean source · statement

def separableClosureRootsOfUnityEquiv
    (k : Type u) (E : Type v) [Field k] [Field E] [Algebra k E]
    (n : ℕ) (hn : (n : k) ≠ 0) :
    rootsOfUnity n (separableClosure k E) ≃* rootsOfUnity n E

def

separableClosureRootsCoefficient

L76 ↗

EtaleFundamentalGroups.Inertia.separableClosureRootsCoefficient

Documentation

Literal subtype inclusion, closed as a coefficient homomorphism before limit construction.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open Polynomial
universe u v

Lean source · full declaration

def separableClosureRootsCoefficient
    (k : Type u) (E : Type v) [Field k] [Field E] [Algebra k E] :
    (separableClosure k E) →* E where
  toFun := Subtype.val
  map_one' := rfl
  map_mul' := fun _ _ => rfl

theorem

separableClosureRootsCoefficient_bijective

L84 ↗

EtaleFundamentalGroups.Inertia.separableClosureRootsCoefficient_bijective

Documentation

The explicit subtype coefficient map has the proved bijective root restrictions.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open Polynomial
universe u v

Lean source · statement

theorem separableClosureRootsCoefficient_bijective
    (k : Type u) (E : Type v) [Field k] [Field E] [Algebra k E]
    (n : ℕ) (hn : (n : k) ≠ 0) :
    Function.Bijective (restrictRootsOfUnity (separableClosureRootsCoefficient k E) n).toFun

Module documentation

Prime-to-characteristic roots of unity in the separable closure

Declarations

rootOfUnity_mem_separableClosure

separableClosure_rootsOfUnity_bijective

separableClosureRootsOfUnityEquiv

separableClosureRootsCoefficient

separableClosureRootsCoefficient_bijective