Module

ResidueFieldExtension.lean

Nyll.SchemeTheory.Etale.ResidueFieldExtension

2 declarations indexed from sourceView source ↗

Module documentation

Realizing separable residue-field extensions in étale neighborhoods

A common denominator rescales a primitive element so that its minimal polynomial lifts to a monic polynomial over the original ring. Inverting its derivative gives a standard étale algebra. The kernel of evaluation at the primitive element defines the required prime, and its residue field maps isomorphically to the prescribed extension.

Imports9

Mathlib.Algebra.Polynomial.Lifts
Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Mathlib.FieldTheory.PrimitiveElement
Mathlib.RingTheory.Etale.StandardEtale
Mathlib.RingTheory.Ideal.Over
Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Mathlib.RingTheory.Localization.Integral
Mathlib.RingTheory.Polynomial.Tower

Imported by3

theorem

exists_monic_primitive_residue_polynomial

L38 ↗

Algebra.Etale.exists_monic_primitive_residue_polynomial

Source context 5 commands

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

@[expose] public section
open Polynomial
open scoped nonZeroDivisors
universe u v
namespace Algebra.Etale

Lean source · statement

theorem exists_monic_primitive_residue_polynomial
    {R : Type u} [CommRing R] (p : Ideal R) [p.IsPrime]
    (L : Type v) [Field L] [Algebra p.ResidueField L]
    [FiniteDimensional p.ResidueField L] [Algebra.IsSeparable p.ResidueField L] :
    ∃ β : L, Algebra.adjoin p.ResidueField {β} = ⊤ ∧
      ∃ f : R[X], f.Monic ∧
        f.map (algebraMap R p.ResidueField) = minpoly p.ResidueField β

theorem

exists_residueField_extension

L83 ↗

Algebra.Etale.exists_residueField_extension

Documentation

Every finite separable extension of a residue field is the residue field of a point in an actual étale neighborhood. The displayed equality makes the isomorphism compatible with the canonical map from the original residue field.