Residue fields of valuation rings
TheoremMonic polynomials have roots in valuation subrings of closed fields#✓fully proved
A monic polynomial over a valuation subring of an algebraically closed field, of nonzero degree, has a root in the subring: take a root in the field, it is integral over the subring, and valuation subrings are integrally closed.
theorem ValuationSubring.exists_root_mem_of_monic {K : Type*} [Field K] [IsAlgClosed K]
(A : ValuationSubring K) (f : Polynomial A) (hf : f.Monic) (hd : f.natDegree ≠ 0) :
∃ x : A, Polynomial.aeval (x : K) f = 0TheoremResidue field of a valuation subring of a closed field is closed#✓fully proved
The residue field of a valuation subring of an algebraically closed field is algebraically closed: lift a monic irreducible polynomial to the valuation subring, take a root there, and reduce it back.
theorem ValuationSubring.isAlgClosed_residueField {L : Type*} [Field L] [IsAlgClosed L]
(A : ValuationSubring L) : IsAlgClosed (IsLocalRing.ResidueField ↥A)TheoremResidue fields in algebraic extensions of \(\mathbb{Q}\) are algebraic#✓fully proved
The residue field of a valuation subring of an algebraic extension of
ℚ is algebraic over 𝔽_p.
theorem ValuationSubring.algebra_isAlgebraic_zmod_residueField_of_isAlgebraic_rat
(K : Type*) [Field K] [Algebra ℚ K] [Algebra.IsAlgebraic ℚ K]
(A : ValuationSubring K) (p : ℕ) [Fact p.Prime]
[Algebra (ZMod p) (IsLocalRing.ResidueField ↥A)] :
Algebra.IsAlgebraic (ZMod p) (IsLocalRing.ResidueField ↥A)TheoremRoots of unity under the residue map of a valuation subring#✓fully proved
The residue map is injective on m-th roots of unity, and every m-th
root of unity in the residue field lifts, when m is nonzero in the
residue field.
theorem ValuationSubring.residue_injOn_pow_eq_one_and_exists_residue_eq_of_isAlgClosed
(K : Type*) [Field K] [IsAlgClosed K] (A : ValuationSubring K)
(m : ℕ) (hm : (m : ResidueField ↥A) ≠ 0) :
(∀ ζ₁ ζ₂ : ↥A, ζ₁ ^ m = 1 → ζ₂ ^ m = 1 → residue ↥A ζ₁ = residue ↥A ζ₂ → ζ₁ = ζ₂) ∧
(∀ u : ResidueField ↥A, u ^ m = 1 → ∃ ζ : ↥A, ζ ^ m = 1 ∧ residue ↥A ζ = u)Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.