Module

ResiduePointFixedness.lean

Nyll.SchemeTheory.Morphisms.ResiduePointFixedness

2 declarations indexed from sourceView source ↗

Module documentation

From the literal residue action to a fixed residue-field point

If a scheme endomorphism fixes a point and its induced residue-field map is the canonical identification at that same point, naturality identifies its composite with the actual canonical residue-field point morphism. Conversely, injectivity of residue-field maps proves the point and residue condition at every point in any fixed test morphism's image. No geometric-point comparison is assumed.

Imports1

Mathlib.AlgebraicGeometry.ResidueField

Imported by5

theorem

fixes_fromSpecResidueField_of_residueFieldMap_eq

L31 ↗

AlgebraicGeometry.Scheme.Hom.fixes_fromSpecResidueField_of_residueFieldMap_eq

Documentation

The original point-and-residue inertia condition fixes the actual canonical residue-field point morphism. The equality of residue maps uses the canonical identification supplied by the given equality of points.

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Hom
universe u

Lean source · statement

theorem fixes_fromSpecResidueField_of_residueFieldMap_eq
    {X : Scheme.{u}} (e : X ⟶ X) (x : X) (hx : e x = x)
    (hres : e.residueFieldMap x = (X.residueFieldCongr hx).hom) :
    X.fromSpecResidueField x ≫ e = X.fromSpecResidueField x

theorem

residueFieldMap_eq_of_comp_eq_self

L46 ↗

AlgebraicGeometry.Scheme.Hom.residueFieldMap_eq_of_comp_eq_self