Morphisms of presheafed spaces determined by sections #
Two morphisms α β : X ⟶ Y of presheafed spaces with the same underlying continuous map agree
once their maps on sections Γ(Y, U) ⟶ Γ(X, α⁻¹ U) and Γ(Y, U) ⟶ Γ(X, β⁻¹ U) agree up to the
identification α⁻¹ U = β⁻¹ U. This is the presheafed-space form of Mathlib's
AlgebraicGeometry.Scheme.Hom.ext, and is convenient when a morphism of presheafed spaces is
built by hand before its locality on stalks is known, so that it is not yet a morphism of
locally ringed spaces or of schemes.
A morphism f : X ⟶ Y of presheafed spaces which is surjective on points and whose maps on sections
Γ(Y, U) ⟶ Γ(X, f⁻¹ U) are all monomorphisms is an epimorphism: two morphisms out of Y which
agree after composing with f agree on points because f is surjective, and then on sections
because the maps on sections of f can be cancelled. This is the sectionwise analogue of
Mathlib's AlgebraicGeometry.SheafedSpace.epi_of_base_surjective_of_stalk_mono, and applies when
𝒪_Y ⟶ f_* 𝒪_X is an isomorphism.
Main results #
AlgebraicGeometry.PresheafedSpace.ext_of_app: morphisms of presheafed spaces agreeing on the underlying map and on sections over every open are equal.AlgebraicGeometry.PresheafedSpace.epi_of_base_surjective_of_c_app_mono: a morphism which is surjective on points and a monomorphism on sections over every open is an epimorphism.
Two morphisms of presheafed spaces are equal if they have the same underlying continuous map and the same maps on sections over every open subset, up to the induced identification of preimages.
A morphism of presheafed spaces which is surjective on points and a monomorphism on sections is an epimorphism.