The quotient of a locally ringed space by an ideal sheaf: basic properties

The canonical morphism ι : quotientSpace X 𝒥 ⟶ X of the quotient by an ideal sheaf has surjective stalk maps: through the identification 𝒪_{Z,z} ≅ 𝒪_{X,z}/𝒥_z they are the quotient maps 𝒪_{X,z} → 𝒪_{X,z}/𝒥_z (stalkMap_surjective).

theorem AnalyticSpace.QuotientSpace.stalkMap_surjective (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (z : ↑(support X J)) : Function.Surjective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (ιHom X J) z))

The stalk map of the canonical morphism is the quotient map 𝒪_{X,z} → 𝒪_{X,z}/𝒥_z, hence surjective.