Module

RootsOfUnityFieldEmbedding.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RootsOfUnityFieldEmbedding

4 declarations indexed from sourceView source ↗

Module documentation

Roots of unity under field embeddings

Proves that a field embedding induces a bijection on n-th roots of unity for nonzero n when the source contains a primitive n-th root. It also bundles root groups and their maps induced by coefficient homomorphisms.

Imports3

Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
Mathlib.SetTheory.Cardinal.Finite
Mathlib.Algebra.Category.Grp.Basic

Imported by13

theorem

restrictRootsOfUnity_bijective_of_primitiveRoot

L27 ↗

RamificationTheory.HilbertRamification.restrictRootsOfUnity_bijective_of_primitiveRoot

Documentation

If the lower field has a primitive n-th root, its full n-th root group maps bijectively to the full n-th root group in every field extension.

Source context 3 commands

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

namespace RamificationTheory.HilbertRamification
open CategoryTheory
universe u v

Lean source · statement

theorem restrictRootsOfUnity_bijective_of_primitiveRoot
    {k : Type u} {l : Type v} [Field k] [Field l] (f : k →+* l)
    (n : ℕ) [NeZero n] (hroot : ∃ ζ : k, IsPrimitiveRoot ζ n) :
    Function.Bijective (restrictRootsOfUnity f n)

def

rootsGroupObject

L44 ↗

RamificationTheory.HilbertRamification.rootsGroupObject

Documentation

A full root group as its native group object.

Source context 3 commands

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

namespace RamificationTheory.HilbertRamification
open CategoryTheory
universe u v

Lean source · statement

def rootsGroupObject (k : Type u) [CommRing k] (n : ℕ) : GrpCat.{u}

def

rootsGroupMap

L48 ↗

RamificationTheory.HilbertRamification.rootsGroupMap

Documentation

The actual root-group map induced by a coefficient ring map.

Source context 3 commands

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

namespace RamificationTheory.HilbertRamification
open CategoryTheory
universe u v

Lean source · full declaration

def rootsGroupMap {k l : Type u} [CommRing k] [CommRing l] (f : k →+* l) (n : ℕ) :
    GrpCat.Hom (rootsGroupObject k n) (rootsGroupObject l n) where
  hom' := restrictRootsOfUnity f n

theorem

rootsGroupMap_surjective_of_primitiveRoot

L54 ↗

RamificationTheory.HilbertRamification.rootsGroupMap_surjective_of_primitiveRoot

Documentation

The native root-group morphism is onto whenever its source field already contains a primitive root of the nonzero degree.

Source context 3 commands

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

namespace RamificationTheory.HilbertRamification
open CategoryTheory
universe u v

Lean source · statement

theorem rootsGroupMap_surjective_of_primitiveRoot
    {k l : Type u} [Field k] [Field l] (f : k →+* l)
    (n : ℕ) [NeZero n] (hroot : ∃ ζ : k, IsPrimitiveRoot ζ n) :
    Function.Surjective (rootsGroupMap f n).hom'.toFun

Module documentation

Roots of unity under field embeddings

Declarations

restrictRootsOfUnity_bijective_of_primitiveRoot

rootsGroupObject

rootsGroupMap

rootsGroupMap_surjective_of_primitiveRoot