Restriction of pre-adic spaces to open subspaces #
For a pre-adic space X and an open embedding f : U ⟶ X of topological spaces, the
restriction X.restrict h is the pre-adic space on U whose presheaf is the restriction of
the presheaf of X. Its stalk at x is the stalk of X at f x, and its valuation at x is
the valuation of X at f x, transported along this identification. The canonical morphism
X.ofRestrict h : X.restrict h ⟶ X is a morphism of pre-adic spaces.
Restrictions are the infrastructure for the locally affinoid condition, which is not defined
here: an adic space will be a pre-adic space admitting an open cover whose members, with the
restricted structure, are isomorphic in 𝒱^pre to affinoid pre-adic spaces. A general
PreAdicSpace carries no such cover. The canonical morphism is a monomorphism whose stalk maps
are isomorphisms, and the restriction of X to the whole space is isomorphic to X, because
the forgetful functor to presheafed spaces reflects isomorphisms. An isomorphism X ≅ Y carries
the restriction of X to an open U isomorphically onto the restriction of Y to the image of
U: the two open immersions into Y have the same range, so Mathlib's
PresheafedSpace.IsOpenImmersion.isoOfRangeEq identifies the underlying presheafed spaces, and the
identification is a morphism of pre-adic spaces because it factors one through the other.
Main definitions #
TauCeti.PreAdicSpace.restrict: the restriction of a pre-adic space along an open embedding.TauCeti.PreAdicSpace.ofRestrict: the canonical morphism from the restriction.TauCeti.PreAdicSpace.restrictStalkIso: the stalk of the restriction atxis the stalk ofXatf x.TauCeti.PreAdicSpace.restrictTopIso: the restriction to the whole space is isomorphic toX.TauCeti.PreAdicSpace.restrictIso: the transport of a restriction along an isomorphism.TauCeti.PreAdicSpace.restrictIsoOfRangeEq: restrictions along two open embeddings with the same range are isomorphic.
The design follows AlgebraicGeometry.LocallyRingedSpace.restrict.
References #
- T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, §8.1.
Pulling a valuation on a stalk of P back along the stalk map of P.ofRestrict h and then
along the stalk identification of the restriction returns the valuation.
The restriction of a pre-adic space along an open embedding f : U ⟶ X. The presheaf is
the restriction of the presheaf of X; the stalk at x is identified with the stalk of X at
f x, and the valuation at x is the valuation of X at f x transported along this
identification.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The presheaf of rings of the restriction is the restriction of the presheaf of rings.
The stalk of the restriction at x is the stalk of X at f x.
Equations
- X.restrictStalkIso h x = X.toRingPresheafedSpace.restrictStalkIso h x
Instances For
The stalk identification is Mathlib's, for the underlying presheafed spaces of rings.
The valuation of the restriction at x is the valuation of X at f x, pulled back along
the residue-field map of the stalk identification.
The stalk valuation of the restriction at x is the stalk valuation of X at f x,
pulled back along the stalk identification.
The canonical morphism from the restriction of a pre-adic space along an open embedding.
Equations
- X.ofRestrict h = { toHom := X.toPresheafedSpace.ofRestrict h, stalkValuation_eq := ⋯ }
Instances For
The inverse of the stalk identification is the stalk map of X.ofRestrict h.
The stalk maps of X.ofRestrict h are isomorphisms.
The canonical morphism from a restriction is a monomorphism, as its underlying morphism of presheafed spaces is.
The restriction of a pre-adic space to the whole space is isomorphic to the space.
Equations
Instances For
An isomorphism e : X ≅ Y of pre-adic spaces restricts to an isomorphism from the
restriction of X to an open U onto the restriction of Y to the image of U. It is the
unique morphism compatible with the canonical morphisms from the restrictions
(restrictIso_hom_ofRestrict).
Equations
Instances For
The transported restriction composed with the canonical morphism from the restriction of
Y is the canonical morphism from the restriction of X followed by e.
The transported restriction composed with the canonical morphism from the restriction of
Y is the canonical morphism from the restriction of X followed by e.
The inverse of the transported restriction composed with the canonical morphism from the
restriction of X is the canonical morphism from the restriction of Y followed by e⁻¹.
The inverse of the transported restriction composed with the canonical morphism from the
restriction of X is the canonical morphism from the restriction of Y followed by e⁻¹.
The restrictions of a pre-adic space X along two open embeddings with the same range are
isomorphic. The isomorphism is the unique morphism compatible with the canonical morphisms to
X (restrictIsoOfRangeEq_hom_ofRestrict).
Equations
- X.restrictIsoOfRangeEq hf hg e = CategoryTheory.asIso (TauCeti.PreAdicSpace.restrictHomOfRangeEq✝ X hf hg e)
Instances For
The isomorphism of restrictions with the same range commutes with the canonical morphisms
to X.
The isomorphism of restrictions with the same range commutes with the canonical morphisms
to X.