Module

LocalResidueFieldExtension.lean

Nyll.SchemeTheory.Etale.LocalResidueFieldExtension

1 declaration indexed from sourceView source ↗

Module documentation

Local Noetherian base change realizing a residue extension

A finite separable extension of the residue field of a Noetherian local ring is realized by localizing an actual etale neighborhood at its supplied prime. The resulting ring is Noetherian and faithfully flat over the original local ring. The residue-field equivalence is compatible with the canonical map of local residue fields. The maximal ideal of the original ring generates the new maximal ideal, so the closed-fibre base change is exactly the new residue field.

The localization need not itself be finitely presented over the original ring; its flatness and the displayed residue compatibility are the facts needed for the proper-section base-change argument.

Imports12

Nyll.SchemeTheory.Etale.ResidueFieldExtension
Mathlib.RingTheory.FiniteType
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Mathlib.RingTheory.Flat.Localization
Mathlib.RingTheory.LocalRing.ResidueField.Basic
Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Mathlib.RingTheory.LocalRing.RingHom.Basic
Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.Localization.Submodule
Mathlib.RingTheory.Smooth.Flat
Mathlib.RingTheory.Unramified.LocalRing

Imported by2

theorem

exists_faithfullyFlat_local_residueField_extension

L44 ↗

Algebra.Etale.exists_faithfullyFlat_local_residueField_extension

Documentation

A finite separable extension of a local residue field comes from an actual Noetherian faithfully flat local base change, with its canonical residue map.

Source context 3 commands

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

noncomputable section
namespace Algebra.Etale
universe u v

Lean source · statement

theorem exists_faithfullyFlat_local_residueField_extension
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (L : Type v) [Field L] [Algebra (IsLocalRing.ResidueField A) L]
    [FiniteDimensional (IsLocalRing.ResidueField A) L]
    [Algebra.IsSeparable (IsLocalRing.ResidueField A) L] :
    ∃ (B : Type u) (_ : CommRing B) (_ : Algebra A B) (_ : IsLocalRing B)
      (_ : IsNoetherianRing B) (_ : Module.FaithfullyFlat A B)
      (_ : IsLocalHom (algebraMap A B)),
      ∃ e : IsLocalRing.ResidueField B ≃+* L,
        e.toRingHom.comp (IsLocalRing.ResidueField.map (algebraMap A B)) =
          algebraMap (IsLocalRing.ResidueField A) L ∧
        (IsLocalRing.maximalIdeal A).map (algebraMap A B) =
          IsLocalRing.maximalIdeal B

Module documentation

Local Noetherian base change realizing a residue extension

Declarations

exists_faithfullyFlat_local_residueField_extension