AlgebraicGeometry.morphismRestrict_base_coe
theorem AlgebraicGeometry.morphismRestrict_base_coe :
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace)
(x : (CategoryTheory.forget TopCat).obj ↑(X ∣_ᵤ f⁻¹ᵁ U).toPresheafedSpace),
Coe.coe ((f ∣_ U).val.base x) = f.val.base ↑x
This theorem, `AlgebraicGeometry.morphismRestrict_base_coe`, states that for any two algebraic geometry schemes `X` and `Y`, a morphism `f` from `X` to `Y`, an open subset `U` of the topological space associated with `Y`, and a point `x` in the presheafed space associated with the restriction of `X` by the preimage of `U` under `f`, the image of `x` under the base of the restricted morphism `f ∣_ U` cast to the codomain type of `f` is equal to the image of `x` cast to the codomain type of `f` under the base of `f`.
In simpler terms, it states that the restriction of the morphism `f` to the preimage of `U` under `f` behaves the same as `f` itself when acting on `x`, in the sense that the image of `x` remains the same in the codomain type of `f`.
More concisely: For any morphism `f` between algebraic geometry schemes `X` and `Y`, open subset `U` of `Y`, and point `x` in the presheafed space of `X` restricted to `U` by `f`, the base of the restriction `f ∣_ U` maps `x` to the same image as `f` mapping `x` to the codomain of `f`.
|
AlgebraicGeometry.Scheme.ιOpens.proof_1
theorem AlgebraicGeometry.Scheme.ιOpens.proof_1 :
∀ {X : AlgebraicGeometry.Scheme} (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace), OpenEmbedding ⇑U.inclusion
The theorem `AlgebraicGeometry.Scheme.ιOpens.proof_1` states that for any Algebraic Geometry Scheme `X` and any open subset `U` of the underlying topological space of `X`, the inclusion map that embeds `U` into the whole space `X` is an open embedding. An open embedding is a continuous function between topological spaces that, intuitively, 'preserves' open sets in the sense that the image of any open set is open. Thus, this theorem asserts that the inclusion map preserves the openness of any set in the defined algebraic geometry scheme.
More concisely: The inclusion map of an open subset into an Algebraic Geometry Scheme is an open embedding.
|