The quotient of a quotient #
A closed subspace of a closed subspace is a closed subspace: for an ideal sheaf 𝒥 on a locally
ringed space X and an ideal sheaf 𝒥' on the quotient Z = (S(𝒥), (𝒪_X/𝒥)|_{S(𝒥)}), the
quotient of Z by 𝒥' is the quotient of X by the lifted ideal sheaf 𝒥̃ whose stalk at
a point x of S(𝒥) is the preimage of 𝒥'_x under the canonical stalk map
𝒪_{X,x} → 𝒪_{Z,x} = 𝒪_{X,x}/𝒥_x (and the unit ideal off S(𝒥)). This is what makes the local
models of a closed subspace of an analytic K-space the zero sets V(f₁, …, f_k, g₁, …, g_l):
the f_i cut out the ambient model, the g_j are ambient lifts of local generators of 𝒥'; it
is how a closed subspace of an analytic K-space is shown to be an analytic K-space.
The lifted ideal sheaf. The stalk family liftStalk (Hironaka/AnalyticSpace/QuotientMap.lean)
has local generators (hasLocalGenerators_liftStalk): near a point a ∈ S(𝒥), local generators
g_j of 𝒥' on an open of S(𝒥) are compatible germ families, each of which is, near a, the
class family of an ambient section b_j over an open W_j ⊆ X; on the common open U of X the
germs of the b_j together with local generators f_i of 𝒥 generate the preimage — the
canonical stalk map is surjective with kernel 𝒥_x (ker_stalkMap_ι), and the preimage of an
ideal generated by the images of the b_j is the ideal they generate plus the kernel (Mathlib's
Ideal.comap_map_of_surjective); near a point off S(𝒥) the closed set S(𝒥) is avoided and
1 generates. The germ of g_j at a point is the image of the germ of b_j
(germ_eq_stalkMap_ι_germ, by germ_ext on the open where the two families agree).
The isomorphism. The canonical morphism ι : Z ⟶ X is compatible with 𝒥' and 𝒥̃
(compat_liftIdeal), so the functorial map gives Z/𝒥' ⟶ X/𝒥̃. Its fibre maps
𝒪_{X,x}/𝒥̃_x → 𝒪_{Z,x}/𝒥'_x are bijective (fiberMap_lift_bijective: surjective because the
stalk map is, injective because 𝒥̃_x is exactly the preimage), so the stalk maps are
isomorphisms; the base map identifies S(𝒥') with S(𝒥̃) — the support of 𝒥̃ is the image of
that of 𝒥' (cosupport_eq_preimage_cosupport_liftIdeal, mapBase_lift_surjective), and the
map is an embedding as the restriction of the subtype inclusion (isOpenEmbedding_mapBase_lift).
Mathlib's IsOpenImmersion.of_stalk_iso makes map an open immersion onto everything, hence an
isomorphism (isoOfRangeEq against the identity): KLocallyRingedSpace.quotient_quotient_iso.
A compatible germ family that is, on the trace of an open O ∋ z, the class family of an
ambient section b has at z the germ ι^♯_z (germ b).
The lifted stalk family has local generators: near a point of the support, the generators of 𝒥
together with ambient lifts of local generators of 𝒥'; off the support, 1.
The lifted ideal sheaf on X: the preimage of 𝒥' under the canonical stalk maps at the
points of the support, the unit ideal elsewhere.
Equations
Instances For
The support of 𝒥' is the part of the support of 𝒥 lying over the support of the lifted
ideal sheaf.
The lifted ideal sheaf of 𝒥' on X / 𝒥, as an ideal sheaf on X: an alias of
QuotientSpace.liftIdeal for the K-local-ringed space X.
Equations
- X.liftIdeal J J' = AnalyticSpace.QuotientSpace.liftIdeal X.toLocallyRingedSpace J J'
Instances For
The quotient of a quotient is the quotient by the lifted ideal sheaf:
(X / 𝒥) / 𝒥' ≅ X / 𝒥̃.
Equations
- One or more equations did not get rendered due to their size.