The quotient of a locally ringed space by an ideal sheaf

Hironaka's local analytic K-space is (S(𝓘), (𝒜_G/𝓘)|_{S(𝓘)}) [Hir64, Ch. 0, §1]: the support S(𝓘) = supp (𝒜_G/𝓘) of the quotient sheaf, with the restriction of the quotient sheaf to it ("restriction to a closed subset" meaning the inverse-image sheaf). Bierstone and Milman use the same construction for every closed subspace [BM97, §3]: a closed subspace Y of X is given by a sheaf of ideals 𝓘_Y of finite type in 𝒪_X, with |Y| = supp 𝒪_X/𝓘_Y and 𝒪_Y the restriction of 𝒪_X/𝓘_Y to |Y|. This file carries out the construction for an arbitrary locally ringed space X and an ideal sheaf 𝒥 on it.

The construction

The structure sheaf of the quotient is built directly as the sheaf of compatible germ families over Z := supp (𝒪_X/𝒥) = {z | 𝒥_z ≠ 𝒪_{X,z}}: a section over an open V ⊆ Z is a family (s_z)_{z ∈ V} with s_z ∈ 𝒪_{X,z}/𝒥_z which is locally the family of classes of one ambient section. This is Mathlib's TopCat.LocalPredicate (the sheafification of the prelocal predicate "the family of classes of one section over an open W of X") and TopCat.subsheafToTypes, lifted to CommRingCat pointwise as smoothSheafCommRing lifts smoothSheaf. Its stalk at z is 𝒪_{X,z}/𝒥_z: the evaluation evalHom of a germ at z is a ring homomorphism, surjective (every class is realized by a family near z) and injective (two families agreeing at z agree near z: the difference of the ambient representatives has germ in 𝒥_z, hence is the germ of a section of 𝒥, hence lies in 𝒥_y for y near z). So the stalks are local rings (quotients of the local rings 𝒪_{X,z} by proper ideals), quotientSpace X 𝒥 is a locally ringed space, and the canonical morphism ι : quotientSpace X 𝒥 ⟶ X has the quotient maps as stalk maps (stalkMap_comp_evalHom, stalkMap_surjective), which are local.

Main definitions

In the namespace QuotientSpace: support, fiber, localPred, presheafCommRing, sheafCommRing, quotientSpace, evalHom with stalkEquiv (the identification 𝒪_{Z,z} ≅ 𝒪_{X,z}/𝒥_z) and ι; then KLocallyRingedSpace.quotient with quotientι, the same with the induced K-structure. The local models (localModel) are the quotients of (G, 𝒜_G) by (f₁, …, f_k), and the closed subspaces of an analytic space (closedSubspace) are the quotients by its finite-type ideal sheaves.

@[reducible, inline]

abbrev AnalyticSpace.QuotientSpace.stalkIdeal (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (z : ↑X.toTopCat) : Ideal ↑(X.presheaf.stalk z)

The stalk ideal 𝒥_z, as an ideal of the local ring 𝒪_{X,z} (the same ideal as J.stalkIdeal z, typed over X.presheaf.stalk z).

Equations

• AnalyticSpace.QuotientSpace.stalkIdeal X J z = J.stalkIdeal z

theorem AnalyticSpace.QuotientSpace.mem_stalkIdeal_iff (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) {z : ↑X.toTopCat} {s : ↑(X.presheaf.stalk z)} : s ∈ stalkIdeal X J z ↔ ∃ (V : TopologicalSpace.Opens ↑X.toTopCat) (hz : z ∈ V), ∃ g ∈ J.carrier V, (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ V z hz)) g = s

The stalk ideal 𝒥_z consists of the germs at z of sections of 𝒥. Restates IdealSheaf.mem_stalkIdeal_iff (Hironaka/Manifold/IdealSheaf/Basic.lean) for the abbreviation stalkIdeal X J z.

@[implicit_reducible]

def AnalyticSpace.QuotientSpace.support (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) : TopCat

The support S(𝒥) = supp (𝒪_X/𝒥) = {z | 𝒥_z ≠ 𝒪_{X,z}} of the quotient sheaf Hir64, Ch. 0, §1 (the cosupport of the ideal sheaf), as a topological space.

Equations

• AnalyticSpace.QuotientSpace.support X J = ↧↑J.support

@[implicit_reducible]

def AnalyticSpace.QuotientSpace.ιTop (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) : support X J ⟶ X.toTopCat

The inclusion of the support into X.

Equations

• AnalyticSpace.QuotientSpace.ιTop X J = TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ }

@[reducible, inline]

abbrev AnalyticSpace.QuotientSpace.preimage (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (W : TopologicalSpace.Opens ↑X.toTopCat) : TopologicalSpace.Opens ↑(support X J)

The preimage in the support of an open subset of X.

Equations

• AnalyticSpace.QuotientSpace.preimage X J W = (TopologicalSpace.Opens.map (AnalyticSpace.QuotientSpace.ιTop X J)).obj W

@[simp]

theorem AnalyticSpace.QuotientSpace.mem_preimage (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) {W : TopologicalSpace.Opens ↑X.toTopCat} {z : ↑(support X J)} : z ∈ preimage X J W ↔ ↑z ∈ W

Membership in the trace W ∩ S(𝒥) of an open W ⊆ X on the support.

@[reducible, inline]

abbrev AnalyticSpace.QuotientSpace.fiber (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (z : ↑(support X J)) : Type u

The fibre 𝒪_{X,z}/𝒥_z of the quotient at a point z of the support.

Equations

• AnalyticSpace.QuotientSpace.fiber X J z = (↑(X.presheaf.stalk ↑z) ⧸ AnalyticSpace.QuotientSpace.stalkIdeal X J ↑z)

instance AnalyticSpace.QuotientSpace.instNontrivialFiber (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (z : ↑(support X J)) : Nontrivial (fiber X J z)

instance AnalyticSpace.QuotientSpace.instIsLocalRingFiber (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (z : ↑(support X J)) : IsLocalRing (fiber X J z)

@[reducible, inline]

abbrev AnalyticSpace.QuotientSpace.prelocalPred (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) : TopCat.PrelocalPredicate (fiber X J)

The prelocal predicate on families (s_z)_{z ∈ V} of classes: "s is the family of the classes [a_z] of one ambient section a ∈ 𝒪_X(W)".

Equations

• One or more equations did not get rendered due to their size.

def AnalyticSpace.QuotientSpace.localPred (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) : TopCat.LocalPredicate (fiber X J)

The local predicate "compatible germ family": locally the family of classes of one ambient section — the sheafification of prelocalPred.

Equations

• AnalyticSpace.QuotientSpace.localPred X J = (AnalyticSpace.QuotientSpace.prelocalPred X J).sheafify

def AnalyticSpace.QuotientSpace.sheafTypes (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) : TopCat.Sheaf (Type u) (support X J)

The sheaf of sets of compatible germ families (TopCat.subsheafToTypes).

Equations

• AnalyticSpace.QuotientSpace.sheafTypes X J = TopCat.subsheafToTypes (AnalyticSpace.QuotientSpace.localPred X J)

def AnalyticSpace.QuotientSpace.sectionsSubring (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (V : TopologicalSpace.Opens ↑(support X J)) : Subring ((z : ↥V) → fiber X J ↑z)

The compatible germ families over V form a subring of the product of the fibres.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance AnalyticSpace.QuotientSpace.instCommRingObjOppositeOpensCarrierSupportPresheafSheafTypes (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (V : (TopologicalSpace.Opens ↑(support X J))ᵒᵖ) : CommRing ((sheafTypes X J).presheaf.obj V)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AnalyticSpace.QuotientSpace.presheafCommRing (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) : TopCat.Presheaf CommRingCat (support X J)

The presheaf of commutative rings of compatible germ families (pointwise operations).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AnalyticSpace.QuotientSpace.sheafCommRing (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) : TopCat.Sheaf CommRingCat (support X J)

The sheaf of commutative rings (𝒪_X/𝒥)|_{S(𝒥)} of compatible germ families, a sheaf because its sheaf of sets is one.

Equations

• AnalyticSpace.QuotientSpace.sheafCommRing X J = { obj := AnalyticSpace.QuotientSpace.presheafCommRing X J, property := ⋯ }

noncomputable def AnalyticSpace.QuotientSpace.evalAt (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (z : ↑(support X J)) (U : TopologicalSpace.OpenNhds z) : (presheafCommRing X J).obj (Opposite.op ↑U) ⟶ ↧(fiber X J z)

Evaluation at z of a section over an open neighbourhood of z.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AnalyticSpace.QuotientSpace.evalHom (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (z : ↑(support X J)) : (presheafCommRing X J).stalk z ⟶ ↧(fiber X J z)

The evaluation of germs at z, 𝒪_{Z,z} → 𝒪_{X,z}/𝒥_z (Mathlib's stalkToFiber lifted to rings, as smoothSheafCommRing.evalHom).

Equations

• One or more equations did not get rendered due to their size.

theorem AnalyticSpace.QuotientSpace.ι_evalHom (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (z : ↑(support X J)) (U : (TopologicalSpace.OpenNhds z)ᵒᵖ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion z).op.comp (presheafCommRing X J)) U) (evalHom X J z) = evalAt X J z (Opposite.unop U)

The stalk evaluation evalHom after the colimit leg at U ∋ z is the evaluation evalAt of germ families at z.

theorem AnalyticSpace.QuotientSpace.germ_comp_evalHom (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (U : TopologicalSpace.Opens ↑(support X J)) (z : ↑(support X J)) (hz : z ∈ U) : CategoryTheory.CategoryStruct.comp ((presheafCommRing X J).germ U z hz) (evalHom X J z) = evalAt X J z ⟨U, hz⟩

evalHom after the germ map at z is the evaluation of germ families at z.

theorem AnalyticSpace.QuotientSpace.evalHom_germ (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (U : TopologicalSpace.Opens ↑(support X J)) (z : ↑(support X J)) (hz : z ∈ U) (s : ↑((presheafCommRing X J).obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (evalHom X J z)) ((CategoryTheory.ConcreteCategory.hom ((presheafCommRing X J).germ U z hz)) s) = ↑s ⟨z, hz⟩

evalHom of the germ at z of a germ family s is its value s z ∈ 𝒪_{X,z}/𝒥_z.

noncomputable def AnalyticSpace.QuotientSpace.classFamily (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (W : TopologicalSpace.Opens ↑X.toTopCat) (a : ↑(X.presheaf.obj (Opposite.op W))) : ↑((presheafCommRing X J).obj (Opposite.op (preimage X J W)))

The family of the classes [a_z] of an ambient section a ∈ 𝒪_X(W), a section of the quotient sheaf over the preimage of W.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AnalyticSpace.QuotientSpace.classHom (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (W : TopologicalSpace.Opens ↑X.toTopCat) : X.presheaf.obj (Opposite.op W) ⟶ (presheafCommRing X J).obj (Opposite.op (preimage X J W))

a ↦ ([a_z])_z as a morphism of rings 𝒪_X(W) ⟶ 𝒪_Z(ι⁻¹ W).

Equations

• AnalyticSpace.QuotientSpace.classHom X J W = CommRingCat.ofHom { toFun := AnalyticSpace.QuotientSpace.classFamily X J W, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem AnalyticSpace.QuotientSpace.evalHom_surjective (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (z : ↑(support X J)) : Function.Surjective ⇑(CommRingCat.Hom.hom (evalHom X J z))

Every class is the germ of a family: evalHom is surjective (as Mathlib's stalkToFiber_surjective).

theorem AnalyticSpace.QuotientSpace.evalHom_injective (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (z : ↑(support X J)) : Function.Injective ⇑(CommRingCat.Hom.hom (evalHom X J z))

Two families with the same class at z agree near z, because the difference of their ambient representatives has germ in 𝒥_z, hence is the germ of a section of 𝒥, which lies in 𝒥_y for every y near z: evalHom is injective (as Mathlib's stalkToFiber_injective).

noncomputable def AnalyticSpace.QuotientSpace.stalkEquiv (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (z : ↑(support X J)) : ↑((presheafCommRing X J).stalk z) ≃+* fiber X J z

The stalk of the quotient sheaf at z is 𝒪_{X,z}/𝒥_z.

Equations

• AnalyticSpace.QuotientSpace.stalkEquiv X J z = RingEquiv.ofBijective (CommRingCat.Hom.hom (AnalyticSpace.QuotientSpace.evalHom X J z)) ⋯

instance AnalyticSpace.QuotientSpace.instIsLocalRingCarrierStalkCommRingCatPresheafCommRing (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (z : ↑(support X J)) : IsLocalRing ↑((presheafCommRing X J).stalk z)

@[implicit_reducible]

noncomputable def AnalyticSpace.QuotientSpace.quotientSpace (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) : AlgebraicGeometry.LocallyRingedSpace

The locally ringed space (S(𝒥), (𝒪_X/𝒥)|_{S(𝒥)}) [Hir64, Ch. 0, §1], [BM97, §3].

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable def AnalyticSpace.QuotientSpace.ιHom (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) : (quotientSpace X J).toPresheafedSpace ⟶ X.toPresheafedSpace

The canonical morphism of presheafed spaces (S(𝒥), 𝒪_X/𝒥) ⟶ X: the inclusion of the support with a ↦ ([a_z])_z on sections.

Equations

• One or more equations did not get rendered due to their size.

theorem AnalyticSpace.QuotientSpace.stalkMap_comp_evalHom (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (z : ↑(support X J)) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (ιHom X J) z) (evalHom X J z) = CommRingCat.ofHom (Ideal.Quotient.mk (stalkIdeal X J ↑z))

The stalk map of the canonical morphism, followed by the identification of the stalk with 𝒪_{X,z}/𝒥_z, is the quotient map.

theorem AnalyticSpace.QuotientSpace.evalHom_stalkMap (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (z : ↑(support X J)) (σ : ↑(X.presheaf.stalk ↑z)) : (CategoryTheory.ConcreteCategory.hom (evalHom X J z)) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (ιHom X J) z)) σ) = (Ideal.Quotient.mk (stalkIdeal X J ↑z)) σ

The stalk map at z of ι : (𝒪_X/𝒥)|_{S(𝒥)} → X, read through evalHom, is the quotient map 𝒪_{X,z} → 𝒪_{X,z}/𝒥_z.

instance AnalyticSpace.QuotientSpace.isLocalHom_stalkMap (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) (z : ↑(support X J)) : IsLocalHom (CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (ιHom X J) z))

@[implicit_reducible]

noncomputable def AnalyticSpace.QuotientSpace.ι (X : AlgebraicGeometry.LocallyRingedSpace) (J : Manifold.IdealSheaf X.𝒪) : quotientSpace X J ⟶ X

The canonical morphism of locally ringed spaces (S(𝒥), 𝒪_X/𝒥) ⟶ X, the closed embedding of the subspace; its stalk maps are the quotient maps.

Equations

• AnalyticSpace.QuotientSpace.ι X J = { toHom := AnalyticSpace.QuotientSpace.ιHom X J, prop := ⋯ }

noncomputable def AnalyticSpace.KLocallyRingedSpace.quotient {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (J : Manifold.IdealSheaf X.𝒪) : KLocallyRingedSpace K

The quotient of a K-local-ringed space by an ideal sheaf, with the K-structure induced along the canonical morphism. The closed subspaces of an analytic K-space are these (closedSubspace).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AnalyticSpace.KLocallyRingedSpace.quotientι {K : Type} [RCLike K] (X : KLocallyRingedSpace K) (J : Manifold.IdealSheaf X.𝒪) : X.quotient J ⟶ X

The canonical morphism of the quotient as a K-morphism.

Equations

• X.quotientι J = ⟨AnalyticSpace.QuotientSpace.ι X.toLocallyRingedSpace J, ⋯⟩