Module

SeparablyClosedFractionHenselian.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.SeparablyClosedFractionHenselian

5 declarations indexed from sourceView source ↗

Module documentation

Normal local domains with separably closed fraction field

A simple residue root of a monic polynomial belongs to a monic irreducible factor. Its derivative cannot vanish, so Gauss's lemma and separable closedness force that factor to be linear. This gives the Hensel lift.

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

Imports6

Nyll.EtaleFundamentalGroups.StrictHenselian.SeparablyClosedFractionResidue
Mathlib.Algebra.Polynomial.Eval.Irreducible
Mathlib.Algebra.Polynomial.Lifts
Mathlib.Algebra.Polynomial.Monic
Mathlib.FieldTheory.IsSepClosed
Mathlib.RingTheory.Henselian

Imported by2

theorem

isUnit_derivative_of_factor_root

L30 ↗

EtaleFundamentalGroups.StrictHenselian.isUnit_derivative_of_factor_root

Source context 3 commands

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

namespace EtaleFundamentalGroups.StrictHenselian
open Polynomial
universe u v

Lean source · statement

theorem isUnit_derivative_of_factor_root
    {R : Type u} [CommRing R] [IsLocalRing R]
    (g h : R[X]) (a : R)
    (hg : g.eval a ∈ IsLocalRing.maximalIdeal R)
    (hd : IsUnit ((g * h).derivative.eval a)) : IsUnit (g.derivative.eval a)

theorem

exists_root_lift_of_isSepClosed_fractionRing

L50 ↗

EtaleFundamentalGroups.StrictHenselian.exists_root_lift_of_isSepClosed_fractionRing

Documentation

Every simple residue root lifts in a normal local domain with separably closed fraction field.

Source context 3 commands

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

namespace EtaleFundamentalGroups.StrictHenselian
open Polynomial
universe u v

Lean source · statement

theorem exists_root_lift_of_isSepClosed_fractionRing
    (R : Type u) [CommRing R] [IsDomain R] [IsLocalRing R] [IsIntegrallyClosed R]
    (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsSepClosed K]
    (f : R[X]) (hf : f.Monic) (a₀ : R)
    (ha₀ : f.eval a₀ ∈ IsLocalRing.maximalIdeal R)
    (hd₀ : IsUnit (f.derivative.eval a₀)) :
    ∃ a : R, f.IsRoot a ∧ a - a₀ ∈ IsLocalRing.maximalIdeal R

theorem

henselianLocalRing_of_isSepClosed_fractionRing

L117 ↗

EtaleFundamentalGroups.StrictHenselian.henselianLocalRing_of_isSepClosed_fractionRing

Documentation

A normal local domain with separably closed fraction field is henselian.

Source context 3 commands

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

namespace EtaleFundamentalGroups.StrictHenselian
open Polynomial
universe u v

Lean source · full declaration

theorem henselianLocalRing_of_isSepClosed_fractionRing
    (R : Type u) [CommRing R] [IsDomain R] [IsLocalRing R] [IsIntegrallyClosed R]
    (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsSepClosed K] :
    HenselianLocalRing R where
  is_henselian f hf a₀ ha₀ hd₀ :=
    exists_root_lift_of_isSepClosed_fractionRing R K f hf a₀ ha₀ hd₀

theorem

isSepClosed_residueField_of_isSepClosed_fractionRing

L126 ↗

EtaleFundamentalGroups.StrictHenselian.isSepClosed_residueField_of_isSepClosed_fractionRing

Documentation

The residue field of a normal local domain with separably closed fraction field is separably closed, including when the local ring is a field.

Source context 3 commands

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

namespace EtaleFundamentalGroups.StrictHenselian
open Polynomial
universe u v

Lean source · statement

theorem isSepClosed_residueField_of_isSepClosed_fractionRing
    (R : Type u) [CommRing R] [IsDomain R] [IsLocalRing R] [IsIntegrallyClosed R]
    (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsSepClosed K] :
    IsSepClosed (IsLocalRing.ResidueField R)

theorem

henselianLocalRing_and_isSepClosed_residueField_of_isSepClosed_fractionRing

L150 ↗

EtaleFundamentalGroups.StrictHenselian.henselianLocalRing_and_isSepClosed_residueField_of_isSepClosed_fractionRing

Documentation

Stacks Project, Tag 0BSQ: a normal local domain with separably closed fraction field is henselian and has separably closed residue field.

Source context 3 commands

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

namespace EtaleFundamentalGroups.StrictHenselian
open Polynomial
universe u v

Lean source · statement

theorem henselianLocalRing_and_isSepClosed_residueField_of_isSepClosed_fractionRing
    (R : Type u) [CommRing R] [IsDomain R] [IsLocalRing R] [IsIntegrallyClosed R]
    (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsSepClosed K] :
    HenselianLocalRing R ∧ IsSepClosed (IsLocalRing.ResidueField R)

Module documentation

Normal local domains with separably closed fraction field

Declarations

isUnit_derivative_of_factor_root

exists_root_lift_of_isSepClosed_fractionRing

henselianLocalRing_of_isSepClosed_fractionRing

isSepClosed_residueField_of_isSepClosed_fractionRing

henselianLocalRing_and_isSepClosed_residueField_of_isSepClosed_fractionRing