AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app
theorem AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
(i j k : D.J) (U : TopologicalSpace.Opens ↑↑(D.V (i, j))),
CategoryTheory.CategoryStruct.comp (⋯.invApp U) ((D.f i k).c.app (Opposite.op (⋯.openFunctor.obj U))) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst.c.app (Opposite.op U))
(CategoryTheory.CategoryStruct.comp
(⋯.invApp
{
unop :=
(TopologicalSpace.Opens.map CategoryTheory.Limits.pullback.fst.base).toPrefunctor.1
(Opposite.op U).unop }.unop)
((D.V (i, k)).presheaf.map (CategoryTheory.eqToHom ⋯)))
The theorem `AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app` states that for any category `C`, and for a given glue data `D` on a presheafed space over `C`, the red and blue arrows in a specific diagram commute. More specifically, for any indices `i, j, k` of `D` and any open set `U` in the space `D.V (i, j)`, the composition of two morphisms - the inverse application of `U` and the application of the structure morphism `D.f i k.c` to the opposite of the object `U` under the functor `D.t'_invApp_openFunctor` - is equal to the composition of three other morphisms: the application of the structure morphism `CategoryTheory.Limits.pullback.fst.c` to the opposite of `U`, the inverse application of a certain object to the set obtained by mapping `CategoryTheory.Limits.pullback.fst.base` to the `unop` of the opposite of `U`, and the mapping of the presheaf of `D.V (i, k)` under a certain homomorphism defined by the equality `CategoryTheory.eqToHom`.
More concisely: For any glue data `D` on a presheafed space over a category `C`, the diagram commutes where the composition of `D.t'_invApp_openFunctor U.op (D.f i k.c).op` and `U.op` is equal to the composition of `CategoryTheory.pullback.fst.c U.op`, `(D.V (i, k)).map (hom equality)`, and `(CategoryTheory.pullback.fst.base U).map unop`.
|
AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π
theorem AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
[inst_1 : CategoryTheory.Limits.HasLimits C] {i : D.J} (U : TopologicalSpace.Opens ↑↑(D.U i)),
∃ (eq :
Opposite.op U =
Opposite.op
((TopologicalSpace.Opens.map
(CategoryTheory.Limits.colimit.ι D.diagram.multispan
(Opposite.op (CategoryTheory.Limits.WalkingMultispan.right i)).unop).base).obj
(⋯.functor.obj U))),
CategoryTheory.CategoryStruct.comp (D.ιInvApp U) (D.diagramOverOpenπ U i) =
(D.U i).presheaf.map (CategoryTheory.eqToHom eq)
The theorem `AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π` states that for any category `C` with limits, any glue data `D` on the presheafed spaces over `C`, and any open set `U` in the topological space underlying the `i`th component of `D`, there exists an equality `eq` such that the `U` as an element of the opposite category equals the preimage (under the base of the colimiting cocone at the `i`th component of the diagram associated with `D`) of the open set associated with the `U`'s object under a specific functor. Furthermore, the composition of `D.ιInvApp` at `U` and `D.diagramOverOpenπ` at `U` and `i` equals the map of the presheaf on the `i`th component of `D` associated to the homomorphism given by this equality `eq`.
More concisely: For any category with limits, given a presheafed space with glue data `D` and an open set `U` in the underlying topological space of the `i`-th component, there exists an equality `eq` such that the image of `U` under the opposite category is equal to the preimage of the open set associated with `U`'s object under the functor `D.diagramOverOpenπ` at `U` and `i`, and the composition of `D.ιInvApp` at `U` and this functor is equal to the presheaf map associated to the homomorphism `eq`.
|
AlgebraicGeometry.PresheafedSpace.GlueData.ι_openEmbedding
theorem AlgebraicGeometry.PresheafedSpace.GlueData.ι_openEmbedding :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
[inst_1 : CategoryTheory.Limits.HasLimits C] (i : D.J), OpenEmbedding ⇑(D.ι i).base
This theorem states that for any category `C` and any glue data `D` of presheafed spaces over `C`, if `C` has all small limits, then the base map of the morphism from `D.U i` to `D.glued` given by `CategoryTheory.GlueData.ι D.toGlueData i`, for any `i` in `D.J`, is an open embedding. In the context of algebraic geometry, this means that the inclusion of each open subset into the glued space is an open embedding, which contributes to the local structure of the glued space.
More concisely: For any category with small limits `C` and glue data `D` of presheafed spaces over `C`, the base map from each open subset `D.Ui` to `D.glued` given by `CategoryTheory.GlueData.ι D.toGlueData i` is an open embedding.
|
AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_eq_id
theorem AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_eq_id :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
[inst_1 : CategoryTheory.Limits.HasLimits C] (i : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)),
CategoryTheory.CategoryStruct.comp (D.diagramOverOpenπ U i)
(CategoryTheory.CategoryStruct.comp (D.ιInvAppπEqMap U) (D.ιInvApp U)) =
CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit (D.diagramOverOpen U))
The theorem `AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_eq_id` states that for any category `C` that has all small limits, and for any glue data `D` on the presheafed spaces over `C`, the composition of the diagram over the open set `U` at index `i`, the inverse application of `D.ι` at `U`, and the equality map of `D.ι` at `U`, is the identity on the limit of the diagram over the open set `U`. This theorem is essentially asserting the property that this composition of morphisms is an identity operation in the context of algebraic geometry and presheafed space.
More concisely: For any category with small limits and a presheafed space with glue data, the inverse application of the glueing map followed by the glueing map is the identity on the limit of the diagram.
|
AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_π
theorem AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_π :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
[inst_1 : CategoryTheory.Limits.HasLimits C] (i j : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)),
CategoryTheory.CategoryStruct.comp (D.diagramOverOpenπ U i)
(CategoryTheory.CategoryStruct.comp (D.ιInvAppπEqMap U)
(CategoryTheory.CategoryStruct.comp (D.ιInvApp U) (D.diagramOverOpenπ U j))) =
D.diagramOverOpenπ U j
The theorem `AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_π` states that for any category `C` with limits, any glue data `D` in the category of presheafed spaces over `C`, and any two objects `i` and `j` from the indexing category `J` of `D`, and any open subset `U` of the underlying topological space of `D.U i`, the composition of morphisms `(D.diagramOverOpenπ U i) ≫ (D.ιInvAppπEqMap U) ≫ (D.ιInvApp U) ≫ (D.diagramOverOpenπ U j)` is equal to the morphism `D.diagramOverOpenπ U j`. Here, `≫` denotes the composition of morphisms. This effectively means that the function `ιInvApp` serves as a right inverse to `D.ι i` on `U`.
More concisely: For any presheafed space `D` over a limit-preserving category `C`, and for any open subsets `U` of `D.U i` and `D.U j`, the composition of `D.diagramOverOpenπ U i`, `D.ιInvAppπEqMap U`, `D.ιInvApp U`, and `D.diagramOverOpenπ U j` equals `D.diagramOverOpenπ U j`. In other words, `D.ιInvApp` is a right inverse to `D.ι` on open subsets.
|
AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app
theorem AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
(i j k : D.J) (U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.pullback (D.f i j) (D.f i k))),
CategoryTheory.CategoryStruct.comp (⋯.invApp U) ((D.t k i).c.app (Opposite.op (⋯.openFunctor.obj U))) =
CategoryTheory.CategoryStruct.comp ((D.t' k i j).c.app (Opposite.op U))
(CategoryTheory.CategoryStruct.comp
(⋯.invApp { unop := { carrier := ⇑(D.t' k i j).base ⁻¹' ↑(Opposite.op U).unop, is_open' := ⋯ } }.unop)
((D.V (k, i)).presheaf.map (CategoryTheory.eqToHom ⋯)))
This theorem states that for any category `C`, a given algebraic geometry presheaf space glue data `D` on `C`, and indices `i`, `j`, and `k` in `D.J`, the 'red' and 'blue' maps in a certain diagram commute. Specifically, the diagram involves the pullback of two morphisms `D.f i j` and `D.f i k` in the category. The morphism created by the composition of the inverse application of `U` and the application of `D.t k i` to the opposite of the object `U` in the `openFunctor` is equal to the morphism created by the composition of the application of `D.t' k i j` to the opposite of `U`, the inverse application of `{ unop := { carrier := the inverse image of `U` under `D.t' k i j`, is_open' := ⋯ } }`, and the map of the presheaf `D.V (k, i)` induced by a certain homomorphism. The commutative property is crucial in many areas of algebra and category theory.
More concisely: For any category `C`, given an algebraic geometry presheaf space `D` on `C`, and indices `i`, `j`, and `k` in `D.J`, the diagram commutes where the morphism obtained from `D.t k i`, the inverse image of `U` under `D.t' k i j`, and the presheaf `D.V (k, i)` induced by a homomorphism, is equal to the morphism obtained from `D.t' k i j`, the inverse image of `U` under the opposite of `D.t k i`, and the map of the presheaf `D` induced by the opposite of `U`. (The morphisms `D.f i j` and `D.f i k` are pullbacks in the category.)
|
AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app'
theorem AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
(i j k : D.J) (U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.pullback (D.f i j) (D.f i k))),
∃ (eq :
(TopologicalSpace.Opens.map (D.t k i).base).op.obj (Opposite.op (⋯.openFunctor.obj U)) =
Opposite.op
(⋯.openFunctor.obj
{ unop := { carrier := ⇑(D.t' k i j).base ⁻¹' ↑(Opposite.op U).unop, is_open' := ⋯ } }.unop)),
CategoryTheory.CategoryStruct.comp (⋯.invApp U)
(CategoryTheory.CategoryStruct.comp ((D.t k i).c.app (Opposite.op (⋯.openFunctor.obj U)))
((D.V (k, i)).presheaf.map (CategoryTheory.eqToHom eq))) =
CategoryTheory.CategoryStruct.comp ((D.t' k i j).c.app (Opposite.op U))
(⋯.invApp { unop := { carrier := ⇑(D.t' k i j).base ⁻¹' ↑(Opposite.op U).unop, is_open' := ⋯ } }.unop)
The theorem `AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app'` states that for any category `C`, any glue data `D` on the category of presheaved spaces over `C`, and any three objects `i`, `j`, and `k` in the indexing category of `D`, there exists an equality between two functor objects operating on an open set `U` in the pullback of morphisms `D.f i j` and `D.f i k`. Furthermore, under this equality, the composition of morphisms involving the inverse application on `U`, the application of another morphism, and the mapping of the presheaf via the equality is equal to the composition of morphisms involving the application of a different morphism and the inverse application on a newly defined open set.
More concisely: For any category C, glue data D on the category of presheaved spaces over C, and objects i, j, k of D's indexing category, the functor applications of open sets U in the pullback of i j and i k via D's f are equal, and their respective inverse applications, morphisms, and presheaf mappings compose equivalently.
|
AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app
theorem AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
[inst_1 : CategoryTheory.Limits.HasLimits C] (i j k : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)),
CategoryTheory.CategoryStruct.comp (D.opensImagePreimageMap i j U)
((D.f j k).c.app (Opposite.op ((TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U)))) =
CategoryTheory.CategoryStruct.comp
((CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).c.app
(Opposite.op U))
(CategoryTheory.CategoryStruct.comp
(⋯.invApp
{
unop :=
(TopologicalSpace.Opens.map
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst
(CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).base).toPrefunctor.1
(Opposite.op U).unop }.unop)
((D.V (j, k)).presheaf.map (CategoryTheory.eqToHom ⋯)))
This theorem states that in the context of category theory, given a category `C` with limits, `D` as an "Algebraic Geometry Presheafed Space Glue Data" over `C`, and `i`, `j`, `k` as elements of `D.J` (which presumably represents some indexing set), the composition of the "opens image preimage map from `i` to `j`", applied to a topological open set `U` in the presheafed space `D.U i`, and the morphism `D.f j k` is equivalent to another complex composition of morphisms involving the first projection of the pullback, "D.t j i", "D.f i j", an inverse application, and finally a map of the presheaf on `D.V (j, k)`. This theorem essentially confirms the commutativity of a certain diagram involving these entities and morphisms.
More concisely: Given a category `C` with limits, for any Algebraic Geometry Presheafed Space `D` over `C`, the composition of the opens image preimage map from `i` to `j` with `D.f j k` is equivalent to the composition of `D.t j i`, `D.f i j`, the inverse of `D.f j i`, and the map of presheaves on `D.V (j, k)`.
|