Open immersions of pre-adic spaces #
A morphism f : X ā¶ Y of pre-adic spaces is an open immersion when its underlying morphism of
presheafed spaces of complete separated topological rings is one: its continuous map is an open
embedding and, over every open of the image, the comparison map of structure presheaves is an
isomorphism. Since f is a morphism of š±^pre, its stalk maps are then isomorphisms compatible
with the stalk valuations, so f identifies X with the restriction of Y to the open image
f(X) as an object of š±^pre (isoRestrict): open immersions are the morphisms inducing an
isomorphism onto an open subspace.
The canonical morphism from a restriction is an open immersion, open immersions compose, and
isomorphisms are open immersions. An open immersion f : X ā¶ Z has the universal property of
the open subspace it defines: every morphism g : Y ā¶ Z whose image lies in the image of f
factors uniquely through f (lift), so two open immersions with the same image have
isomorphic sources (isoOfRangeEq). The lifts are those of the underlying presheafed spaces,
promoted to š±^pre by TauCeti.PreAdicSpace.Hom.ofFac.
Main definitions #
TauCeti.PreAdicSpace.IsOpenImmersion: open immersions of pre-adic spaces.TauCeti.PreAdicSpace.IsOpenImmersion.lift: the factorisation of a morphism with image inside the image of an open immersion.TauCeti.PreAdicSpace.IsOpenImmersion.isoOfRangeEq: two open immersions with the same image have isomorphic sources.TauCeti.PreAdicSpace.IsOpenImmersion.isoRestrict: an open immersion identifies its source with the restriction of its target to its image.
The design follows AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.
References #
- T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Ā§8.2.
A morphism of pre-adic spaces is an open immersion when its underlying morphism of presheafed spaces of complete separated topological rings is an open immersion: an open embedding of the underlying spaces along which the structure presheaf of the target restricts to that of the source.
Equations
Instances For
The underlying continuous map of an open immersion is an open embedding.
The canonical morphism from a restriction is an open immersion.
The composite of two open immersions is an open immersion.
An isomorphism of pre-adic spaces is an open immersion.
An open immersion is a monomorphism, as its underlying morphism of presheafed spaces is.
Forgetting the topology on sections, the underlying morphism of presheafed spaces of rings of an open immersion is an open immersion.
The stalk maps of an open immersion are isomorphisms.
For an open immersion f : X ā¶ Z and a morphism g : Y ā¶ Z whose image is contained in the
image of f, the morphism Y ā¶ X through which g factors. It is the lift of the underlying
morphisms of presheafed spaces, and is unique (lift_uniq).
Equations
Instances For
Two open immersions into Z with the same image have isomorphic sources. The isomorphism is
the unique morphism compatible with the two immersions (isoOfRangeEq_hom_comp).
Equations
- One or more equations did not get rendered due to their size.
Instances For
An open immersion f : X ā¶ Y identifies X with the restriction of Y to the open image
of f: open immersions are the morphisms of š±^pre inducing an isomorphism onto an open
subspace.