Module

SeparablyClosedFractionResidue.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.SeparablyClosedFractionResidue

3 declarations indexed from sourceView source ↗

Module documentation

Residue fields of normal domains with separably closed fraction field

An irreducible residue polynomial lifts to a monic polynomial over the normal domain. Gauss's lemma transports irreducibility to its fraction field. A nonzero derivative forces degree one there. Otherwise, adding a nonzero element of the maximal ideal times X preserves the residue polynomial and makes the derivative nonzero.

Reference: Stacks Project, Tag 0BSP. https://stacks.math.columbia.edu/tag/0BSP

Imports7

Mathlib.Algebra.Polynomial.Eval.Irreducible
Mathlib.Algebra.Polynomial.Lifts
Mathlib.FieldTheory.IsSepClosed
Mathlib.RingTheory.LocalRing.ResidueField.Basic
Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Mathlib.RingTheory.Localization.LocalizationLocalization
Mathlib.RingTheory.Polynomial.GaussLemma

Imported by3

theorem

natDegree_eq_one_of_monic_irreducible_derivative_ne_zero

L37 ↗

EtaleFundamentalGroups.StrictHenselian.natDegree_eq_one_of_monic_irreducible_derivative_ne_zero

Documentation

A monic irreducible polynomial over a normal domain with separably closed fraction field is linear if its derivative is nonzero.

Source context 4 commands

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

namespace EtaleFundamentalGroups.StrictHenselian
open Polynomial
open scoped nonZeroDivisors
universe u v

Lean source · statement

theorem natDegree_eq_one_of_monic_irreducible_derivative_ne_zero
    {R : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsSepClosed K]
    (f : R[X]) (hf : f.Monic) (hirr : Irreducible f) (hder : f.derivative ≠ 0) :
    f.natDegree = 1

theorem

isAlgClosed_residueField_of_isSepClosed_fractionRing

L58 ↗

EtaleFundamentalGroups.StrictHenselian.isAlgClosed_residueField_of_isSepClosed_fractionRing

Documentation

A normal local domain with separably closed fraction field and a nonzero maximal ideal has an algebraically closed residue field.

Source context 4 commands

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

namespace EtaleFundamentalGroups.StrictHenselian
open Polynomial
open scoped nonZeroDivisors
universe u v

Lean source · statement

theorem isAlgClosed_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]
    (hm : IsLocalRing.maximalIdeal R ≠ ⊥) :
    IsAlgClosed (IsLocalRing.ResidueField R)

theorem

isAlgClosed_primeResidueField_of_isSepClosed_fractionRing

L109 ↗

EtaleFundamentalGroups.StrictHenselian.isAlgClosed_primeResidueField_of_isSepClosed_fractionRing

Documentation

Stacks Project, Tag 0BSP: the residue field at any nonzero prime of a normal domain with separably closed fraction field is algebraically closed.

Source context 4 commands

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

namespace EtaleFundamentalGroups.StrictHenselian
open Polynomial
open scoped nonZeroDivisors
universe u v

Lean source · statement

theorem isAlgClosed_primeResidueField_of_isSepClosed_fractionRing
    (R : Type u) [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] [IsSepClosed K]
    (p : Ideal R) [p.IsPrime] (hp : p ≠ ⊥) :
    IsAlgClosed p.ResidueField

Module documentation

Residue fields of normal domains with separably closed fraction field

Declarations

natDegree_eq_one_of_monic_irreducible_derivative_ne_zero

isAlgClosed_residueField_of_isSepClosed_fractionRing

isAlgClosed_primeResidueField_of_isSepClosed_fractionRing