AlgebraicGeometry.PresheafedSpace.Hom.ext
theorem AlgebraicGeometry.PresheafedSpace.Hom.ext :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C}
(α β : X.Hom Y) (w : α.base = β.base),
CategoryTheory.CategoryStruct.comp α.c (CategoryTheory.whiskerRight (CategoryTheory.eqToHom ⋯) X.presheaf) = β.c →
α = β
This theorem states that for any category `C`, and any two objects `X` and `Y` in the category of algebraic geometry presheafed spaces over `C`, if we have two morphisms `α` and `β` from `X` to `Y`, and if the base maps of `α` and `β` are equal, then if the composition of `α.c` and the whisker right of the equality morphism (derived from the equality of base maps) with `X.presheaf` is equal to `β.c`, then `α` and `β` are equal.
In simple terms, this theorem is about the equality of two morphisms in the category of algebraic geometry presheafed spaces. It states that if these two morphisms have the same base map, and if a certain composite morphism involving one of the morphisms and the identity morphism (that comes from the equality of the base maps) is equal to the other morphism, then the two original morphisms are indeed the same.
More concisely: If two morphisms in the category of algebraic geometry presheafed spaces over a category `C` have equal base maps and their compositions with the identity morphism from the equality of base maps yield equal morphisms when precomposed with the presheaf of one object, then the two morphisms are equal.
|
AlgebraicGeometry.PresheafedSpace.restrict.proof_1
theorem AlgebraicGeometry.PresheafedSpace.restrict.proof_1 :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} C] {U : TopCat}
(X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X}, OpenEmbedding ⇑f → IsOpenMap ⇑f
This theorem states that for any category `C`, topological space `U`, and presheafed space `X` over `C`, if the morphism `f` from `U` to the underlying topological space of `X` is an open embedding, then `f` is an open map. In other words, if a morphism between topological spaces is an open embedding (i.e., it is a continuous, injective map with its image being an open set), then the image of any open set through this morphism is also an open set.
More concisely: If `f : U -> X` is an open embedding of a morphism from a topological space `U` to a presheafed space `X` over a category `C`, then `f` is an open map, i.e., the image of any open set in `U` is an open set in `X`.
|
AlgebraicGeometry.PresheafedSpace.comp_c_app
theorem AlgebraicGeometry.PresheafedSpace.comp_c_app :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C}
(α : X ⟶ Y) (β : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑↑Z)ᵒᵖ),
(CategoryTheory.CategoryStruct.comp α β).c.app U =
CategoryTheory.CategoryStruct.comp (β.c.app U)
(α.c.app (Opposite.op ((TopologicalSpace.Opens.map β.base).obj U.unop)))
The theorem `AlgebraicGeometry.PresheafedSpace.comp_c_app` states that for any category `C`, and any presheafed spaces `X`, `Y`, and `Z` in `C`, given morphisms `α: X ⟶ Y` and `β: Y ⟶ Z`, and an open set `U` in the double opposite of the opens of `Z`, the application of the composite morphism `(α β).c.app` to `U` equals the composite of the application of `β.c.app` to `U` and the application of `α.c.app` to the open set obtained by applying `Opposite.op` to the object in the opens of `Z` mapped from `U.unop` under `β.base`. This theorem is useful when rewriting with `comp_c_app` fails due to dependent type issues, and in such cases, the helper lemma `comp_c_app_assoc` might be used to make progress. The lemma `comp_c_app_assoc` is also more suitable for rewrites in the opposite direction.
More concisely: For any presheafed spaces X, Y, Z in a category C and morphisms α: X ⟶ Y, β: Y ⟶ Z, the application of the composite presheaf morphism αβ to an open set U in Z equals the composition of β's application to U and α's application to the open set obtained by applying the opposite of β's base to U.
|
AlgebraicGeometry.PresheafedSpace.isIso_of_components
theorem AlgebraicGeometry.PresheafedSpace.isIso_of_components :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C}
(f : X ⟶ Y) [inst_1 : CategoryTheory.IsIso f.base] [inst_2 : CategoryTheory.IsIso f.c], CategoryTheory.IsIso f
This theorem states that for any category 'C', and presheaved spaces 'X' and 'Y' over that category, if 'f' is a morphism from 'X' to 'Y', and both the base of 'f' and the presheaf homomorphism of 'f' are isomorphisms, then 'f' itself is an isomorphism in the category of presheaved spaces over 'C'. This theorem can be used in conjunction with `CategoryTheory.NatIso.isIso_of_isIso_app`.
More concisely: If a morphism between presheaves over a category, along with its base and homomorphism parts, is a pair of isomorphisms, then the morphism itself is an isomorphism.
|
AlgebraicGeometry.PresheafedSpace.id_c_app
theorem AlgebraicGeometry.PresheafedSpace.id_c_app :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C)
(U : (TopologicalSpace.Opens ↑↑X)ᵒᵖ),
(CategoryTheory.CategoryStruct.id X).c.app U = X.presheaf.map (CategoryTheory.CategoryStruct.id U)
This theorem states that for any category `C` and any pre-sheafed space `X` over `C`, and for any open set `U` in the topological space underlying `X`, the morphism corresponding to the identity on `X` (when applied to `U`) is equal to the map induced by the presheaf on `X` when applied to the identity on `U`. In other words, the identity morphism on the pre-sheafed space behaves as expected when acting on elements of the category.
More concisely: For any pre-sheafed space X over a category C and open set U in X, the identity morphism on X induced by the identity on U is equal to the morphism induced by the presheaf on X when applied to the identity on U.
|