Functoriality of the quotient by an ideal sheaf #

The closed subspace (S(𝒥), (𝒪_X/𝒥)|_{S(𝒥)}) (QuotientSpace.quotientSpace) is a construction on a locally ringed space X and an ideal sheaf 𝒥. This file makes it functorial and draws two consequences: restriction to an open subset commutes with the quotient (Hironaka's (S(𝓘), (𝒜_G/𝓘)|_{S(𝓘)}) restricted to an open G' ⊆ G is the local model of G' [Hir64, Ch. 0, §1]), and the quotient is transported along a K-isomorphism of the ambient spaces. Both are what one expects, and both are theorems about the germ-family construction rather than definitions, which is why they live here.

The morphism. Let φ : X' ⟶ X be a morphism of locally ringed spaces and 𝒥', 𝒥 ideal sheaves on X', X such that every stalk map φ_{z'}^♯ : 𝒪_{X,φ z'} → 𝒪_{X',z'} carries 𝒥_{φ z'} into 𝒥'_{z'} (Compat). Then φ restricts to the supports (mapBase; a point where 𝒥_{φ z'} is the unit ideal has 𝒥'_{z'} the unit ideal), induces ring homomorphisms of the fibres 𝒪_{X,φ z'}/𝒥_{φ z'} → 𝒪_{X',z'}/𝒥'_{z'} (fiberMap, Mathlib's Ideal.quotientMap), and carries a compatible germ family over an open V of S(𝒥) to a compatible germ family over the preimage of V (mapFamily): if the family is locally the classes of one ambient section a over W ⊆ X, the image is locally the classes of φ^♯ a over φ⁻¹ W, because stalk maps carry the germ of a to the germ of φ^♯ a (Mathlib's stalkMap_germ_apply). This is a morphism of presheafed spaces (mapHom) whose stalk maps are the fibre maps up to the identification 𝒪_{Z,z} ≅ 𝒪_{X,z}/𝒥_z (evalHom_mapHom_stalkMap); the fibre maps are local, so map is a morphism of locally ringed spaces, and it commutes with the canonical morphisms to X' and X (map_comp_ι). For K-morphisms the same square gives a K-morphism of the K-quotients (KLocallyRingedSpace.quotientMap).

Pull-back of an ideal sheaf. For any φ, the family z' ↦ φ_{z'}^♯(𝒥_{φ z'}) has local generators (the pull-backs of local generators of 𝒥), so it is an ideal sheaf comap φ 𝒥 on X', compatible with 𝒥 by construction; its support is the preimage of the support (a local homomorphism carries the unit ideal only to the unit ideal). When the stalk maps of φ are isomorphisms the fibre maps are bijective, hence the stalk maps of map are isomorphisms; when moreover φ is an open embedding on points, so is the map of supports, and Mathlib's IsOpenImmersion.of_stalk_iso makes map an open immersion (isOpenImmersion_map_comap).

The consequences. For an open U ⊆ X the open immersion X|U ⟶ X has isomorphic stalks, so (X|U)/(𝒥|U) ⟶ X/𝒥 is an open immersion with image the part of S(𝒥) over U; two open immersions with the same image are isomorphic (isoOfRangeEq), which is restrictOpen_quotient_iso. A K-isomorphism e : X' ≅ X is an open immersion with isomorphic stalks and every point of S(𝒥) is hit, so X'/e⁻¹𝒥 ≅ X/𝒥 (quotient_kIso). The last section prepares a third consequence, that the quotient of X/𝒥 by an ideal sheaf 𝒥' is the quotient of X by the lifted ideal sheaf (the preimage of 𝒥' under the canonical stalk maps): the lifted stalk family and the kernel of the canonical stalk map are defined here, and the isomorphism is proved in Hironaka/AnalyticSpace/QuotientLift.lean.