The quotient by the zero ideal sheaf

The canonical morphism QuotientSpace.ι : (S(𝒥), 𝒪_X/𝒥) ⟶ X of the quotient is an isomorphism when every stalk ideal of 𝒥 is zero: the support is the whole space, so the base map is a homeomorphism (the inclusion of univ), and the stalk maps are the quotient maps 𝒪_{X,z} → 𝒪_{X,z}/0, bijective; a morphism of sheaves whose stalk maps are isomorphisms is an isomorphism (Mathlib's TopCat.Presheaf.isIso_of_stalkFunctor_map_iso, through the pushforward along the homeomorphism, whose stalks are those of the quotient sheaf: stalkPushforward_iso_of_isInducing). Hence X.quotient 𝒥 ≅ X as K-local-ringed spaces (quotientBotIso), and in particular the local analytic K-space with no equations, localModel K n G ![], is K-isomorphic to (G, 𝒜_G) — a theorem, not a definitional identity. This is how the chart domain of an analytic manifold is exhibited as a local model when the space of a manifold is shown to be an analytic K-space. Not in the sources; routine.

theorem AnalyticSpace.QuotientSpace.cosupport_eq_univ_of_stalkIdeal_eq_bot (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (hJ : ∀ (x : ↑X.toTopCat), J.stalkIdeal x = ⊥) : J.support = Set.univ

If every stalk ideal of 𝒥 is zero, its cosupport is the whole space.

noncomputable def AnalyticSpace.QuotientSpace.supportHomeomorph (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (hJ : ∀ (x : ↑X.toTopCat), J.stalkIdeal x = ⊥) : ↑(support X J) ≃ₜ ↑X.toTopCat

The homeomorphism S(𝒥) ≃ₜ X when every stalk ideal of 𝒥 is zero.

Equations

• AnalyticSpace.QuotientSpace.supportHomeomorph X J hJ = (Homeomorph.setCongr ⋯).trans (Homeomorph.Set.univ ↑X.toTopCat)

theorem AnalyticSpace.QuotientSpace.isIso_ιTop_of_stalkIdeal_eq_bot (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (hJ : ∀ (x : ↑X.toTopCat), J.stalkIdeal x = ⊥) : CategoryTheory.IsIso (ιTop X J)

theorem AnalyticSpace.QuotientSpace.stalkMap_injective_of_stalkIdeal_eq_bot (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (z : ↑(support X J)) (hz : J.stalkIdeal ↑z = ⊥) : Function.Injective ⇑(CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (ιHom X J) z))

The stalk map of the canonical morphism is injective when the stalk ideal is zero.

theorem AnalyticSpace.QuotientSpace.isIso_stalkMap_of_stalkIdeal_eq_bot (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (z : ↑(support X J)) (hz : J.stalkIdeal ↑z = ⊥) : CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (ιHom X J) z)

theorem AnalyticSpace.QuotientSpace.isIso_ιHom_c_of_stalkIdeal_eq_bot (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (hJ : ∀ (x : ↑X.toTopCat), J.stalkIdeal x = ⊥) : CategoryTheory.IsIso (ιHom X J).c

The sheaf map of the canonical morphism is an isomorphism when every stalk ideal is zero.

theorem AnalyticSpace.QuotientSpace.isIso_ιHom_of_stalkIdeal_eq_bot (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (hJ : ∀ (x : ↑X.toTopCat), J.stalkIdeal x = ⊥) : CategoryTheory.IsIso (ιHom X J)

The canonical morphism of presheafed spaces (S(𝒥), 𝒪_X/𝒥) ⟶ X is an isomorphism when every stalk ideal of 𝒥 is zero.

theorem AnalyticSpace.QuotientSpace.isIso_ι_of_stalkIdeal_eq_bot (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (hJ : ∀ (x : ↑X.toTopCat), J.stalkIdeal x = ⊥) : CategoryTheory.IsIso (ι X J)

The canonical morphism of locally ringed spaces (S(𝒥), 𝒪_X/𝒥) ⟶ X is an isomorphism when every stalk ideal of 𝒥 is zero.

theorem AnalyticSpace.KLocallyRingedSpace.isIso_quotientι_of_stalkIdeal_eq_bot {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (J : Manifold.IdealSheaf X.𝒪) (hJ : ∀ (x : ↑↑X.toPresheafedSpace), J.stalkIdeal x = ⊥) : CategoryTheory.IsIso (X.quotientι J)

The canonical K-morphism of the quotient by an ideal sheaf with zero stalks is an isomorphism.

noncomputable def AnalyticSpace.KLocallyRingedSpace.quotientBotIso {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (J : Manifold.IdealSheaf X.𝒪) (hJ : ∀ (x : ↑↑X.toPresheafedSpace), J.stalkIdeal x = ⊥) : (X.quotient J).KIso X

The quotient of a K-local-ringed space by an ideal sheaf with zero stalks is K-isomorphic to the space.

Equations

• X.quotientBotIso J hJ = CategoryTheory.asIso (X.quotientι J)