Module

ResidueAlgebraicClosedness.lean

Nyll.ValuedFieldTheory.Valuation.ResidueAlgebraicClosedness

1 declaration indexed from sourceView source ↗

Module documentation

Algebraic closedness of a valuation residue field

A valuation subring of an algebraically closed field has algebraically closed residue field. Lift a monic residue polynomial, choose its root in the ambient field, and use integral closedness to realize that same root in the valuation ring before reducing it. No hypothesis on the valuation rank or residue characteristic is needed.

Imports6

Mathlib.Algebra.Polynomial.AlgebraMap
Mathlib.Algebra.Polynomial.Lifts
Mathlib.FieldTheory.IsAlgClosed.Basic
Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.RingTheory.LocalRing.ResidueField.Basic
Mathlib.RingTheory.Valuation.LocalSubring

Imported by2

theorem

isAlgClosed_residueField

L30 ↗

ValuationSubring.isAlgClosed_residueField

Documentation

The residue field of any valuation subring of an algebraically closed field is algebraically closed.

Source context 2 commands

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

namespace ValuationSubring
universe u

Lean source · statement

theorem isAlgClosed_residueField
    {Ω : Type u} [Field Ω] [IsAlgClosed Ω] (A : ValuationSubring Ω) :
    IsAlgClosed (IsLocalRing.ResidueField A)

Module documentation

Algebraic closedness of a valuation residue field

Declarations

isAlgClosed_residueField