AlgebraicGeometry.IsOpenImmersion.lift_fac
theorem AlgebraicGeometry.IsOpenImmersion.lift_fac :
∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f]
(H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base),
CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.lift f g H') f = g
The theorem `AlgebraicGeometry.IsOpenImmersion.lift_fac` states that for any three algebraic geometrical schemes `X`, `Y`, and `Z`, and morphisms `f : X ⟶ Z` and `g : Y ⟶ Z`, if `f` is an open immersion and the range of `g` is a subset of the range of `f`, then the composition of the lift of `f` and `g` (under these conditions) followed by `f` is equal to `g`. In other words, this theorem is about the commutativity of a certain diagram in the category of algebraic geometric schemes, where the morphisms involved are open immersions.
More concisely: If `f : X ⟶ Z` is an open immersion and `g : Y ⟶ Z` has image contained in that of `f`, then `(g ∘ f^(-1)) ∘ f = g`.
|
AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq
theorem AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq :
∀ {X Y U : AlgebraicGeometry.Scheme} (f : Y ⟶ U) (g : U ⟶ X) (fg : Y ⟶ X)
(H : fg = CategoryTheory.CategoryStruct.comp f g) [h : AlgebraicGeometry.IsOpenImmersion g]
(V : TopologicalSpace.Opens ↑↑U.toPresheafedSpace),
f.val.c.app (Opposite.op V) =
CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.invApp g V)
(CategoryTheory.CategoryStruct.comp
(fg.val.c.app (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor g).obj V)))
(Y.presheaf.map (CategoryTheory.eqToHom ⋯).op))
This theorem in Algebraic Geometry is about the composition of morphisms in a category of schemes. Given three schemes X, Y, and U, and three morphisms f: Y ⟶ U, g: U ⟶ X, and fg: Y ⟶ X, assuming that the composition of f and g equals fg (i.e., fg = f ∘ g), and that g is an open immersion, then for any open subset V of the underlying topological space of U, the application of f to the opposite of V is equal to the composition of three operations: firstly, the application of the inverse of the isomorphism induced by the open immersion g to V; secondly, the application of fg to the opposite of the image of V under the functor associated with the open immersion g; lastly, the map induced by the presheaf of Y under the equivalence given by some equality. The purpose of the fg argument is to avoid issues with dependent types.
More concisely: Given schemes X, Y, U, morphisms f: Y ⟶ U, g: U ⟶ X with g an open immersion and fg = f ∘ g, for any open subset V of U, we have f(V^c) = (g^(-1))(fg(V)^c) ∘ i^*, where i: g(V) ⟶ Y is the inclusion morphism.
|
AlgebraicGeometry.Scheme.OpenCover.IsOpen
theorem AlgebraicGeometry.Scheme.OpenCover.IsOpen :
∀ {X : AlgebraicGeometry.Scheme} (self : X.OpenCover) (x : self.J),
AlgebraicGeometry.IsOpenImmersion (self.map x)
This theorem states that for any scheme `X` and any open cover `self` of `X`, the map from the index set `self.J` to `X` associated with each element `x` of `self.J` is an open immersion. In other words, the embedding of each subscheme in the open cover into the scheme `X` is an open immersion. An open immersion in algebraic geometry is a morphism that is also an open immersion in the category of locally ringed spaces.
More concisely: For any scheme X and open cover self, the embedding of each subscheme in the cover into X is an open immersion.
|
AlgebraicGeometry.Scheme.OpenCover.Covers
theorem AlgebraicGeometry.Scheme.OpenCover.Covers :
∀ {X : AlgebraicGeometry.Scheme} (self : X.OpenCover) (x : ↑↑X.toPresheafedSpace),
x ∈ Set.range ⇑(self.map (self.f x)).val.base
This theorem states that for any given scheme `X` in algebraic geometry, and any open cover `self` of the scheme `X`, every point `x` in the underlying topological space of `X` is contained in the range of the base map of the morphism corresponding to the open subset of `X` that contains `x`. In other words, this means that the open cover indeed covers the entire scheme `X`, with each point in `X` mapping to a point in some subset in the open cover.
More concisely: For any scheme X and open cover self, every point in X is contained in the domain of some open subset in self.
|