AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem

{X Y : AlgebraicGeometry.Scheme} →
  (f : X.PartialMap Y) → {x : ↥X} → x ∈ f.domain → (AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ Y)

If x is in the domain of a partial map f, then f restricts to a map from Spec 𝒪_x.

Defined in: Mathlib.AlgebraicGeometry.Birational.RationalMap
Cited by: 5 results in Mathlib
Foundations: Depth 148 from the axioms · uses propext, Classical.choice, Quot.sound

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Quiver.Homstatement · cited by 32,603
CategoryTheory.CategoryStruct.compproof · cited by 17,999
TopCat.carrierstatement and proof · cited by 3,184
AlgebraicGeometry.Schemestatement and proof · cited by 2,540
CommRingCatstatement · cited by 2,333
AlgebraicGeometry.PresheafedSpace.carrierstatement and proof · cited by 2,020
AlgebraicGeometry.SheafedSpace.toPresheafedSpacestatement and proof · cited by 1,988
AlgebraicGeometry.LocallyRingedSpace.toSheafedSpacestatement and proof · cited by 1,892
AlgebraicGeometry.Scheme.toLocallyRingedSpacestatement and proof · cited by 1,734
AlgebraicGeometry.Scheme.Opensstatement · cited by 1,149
AlgebraicGeometry.PresheafedSpace.presheafstatement · cited by 1,104
AlgebraicGeometry.Specstatement · cited by 626

Results whose statement or proof uses this declaration.