Module

UnitRoot.lean

Nyll.EtaleFundamentalGroups.Kummer.Henselian.UnitRoot

1 declaration indexed from sourceView source ↗

Module documentation

Roots of units over a Henselian local ring

If the residue field is separably closed and the exponent is a unit in that field, every unit of a Henselian local ring has a root of that exponent. This is the characteristic-zero-compatible unit-absorption step for tame Kummer presentations.

Imports2

Mathlib.FieldTheory.IsSepClosed
Mathlib.RingTheory.Henselian

Imported by2

theorem

exists_pow_eq_of_isUnit_of_isSepClosed_residue

L27 ↗

EtaleFundamentalGroups.Kummer.exists_pow_eq_of_isUnit_of_isSepClosed_residue

Documentation

A unit over a Henselian local ring has an n-th root when the residue field is separably closed and n is invertible there.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u

Lean source · statement

theorem exists_pow_eq_of_isUnit_of_isSepClosed_residue
    {R : Type u} [CommRing R] [IsLocalRing R]
    [HenselianRing R (IsLocalRing.maximalIdeal R)]
    [IsSepClosed (IsLocalRing.ResidueField R)]
    {n : ℕ} (hn : IsUnit (n : IsLocalRing.ResidueField R))
    (u : R) (hu : IsUnit u) :
    ∃ z : R, z ^ n = u

Module documentation

Roots of units over a Henselian local ring

Declarations

exists_pow_eq_of_isUnit_of_isSepClosed_residue