Module

ResidueFieldPushout.lean

Nyll.SchemeTheory.Etale.ResidueFieldPushout

1 declaration indexed from sourceView source ↗

Module documentation

The residue-field pushout of a local ring map

When the extended maximal ideal is the maximal ideal of the target, the actual square of the ring map and the two residue maps is a pushout. The universal factorization is the quotient lift of the given map from the target ring; its kernel containment follows from the supplied cocone.

Imports5

Mathlib.Algebra.Category.Ring.Basic
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.LocalRing.ResidueField.Basic

Imported by2

lemma

isPushout_residue_of_maximalIdeal_map_eq

L32 ↗

CommRingCat.isPushout_residue_of_maximalIdeal_map_eq

Documentation

Extending the maximal ideal to the target maximal ideal identifies the closed-fibre base change with the target residue field, as an actual pushout.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace CommRingCat
universe u

Lean source · statement

lemma isPushout_residue_of_maximalIdeal_map_eq
    (A B : Type u) [CommRing A] [CommRing B] [Algebra A B]
    [IsLocalRing A] [IsLocalRing B] [IsLocalHom (algebraMap A B)]
    (hMaximal : (IsLocalRing.maximalIdeal A).map (algebraMap A B) =
      IsLocalRing.maximalIdeal B) :
    IsPushout (ofHom (IsLocalRing.residue A)) (ofHom (algebraMap A B))
      (ofHom (IsLocalRing.ResidueField.map (algebraMap A B)))
      (ofHom (IsLocalRing.residue B))

Module documentation

The residue-field pushout of a local ring map

Declarations

isPushout_residue_of_maximalIdeal_map_eq