CategoryTheory.GlueData.ι_gluedIso_inv
theorem CategoryTheory.GlueData.ι_gluedIso_inv :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂}
[inst_1 : CategoryTheory.Category.{v, u₂} C'] (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
[H : (i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F]
[inst_2 : CategoryTheory.Limits.HasMulticoequalizer D.diagram]
[inst_3 : CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] (i : D.J),
CategoryTheory.CategoryStruct.comp ((D.mapGlueData F).ι i) (D.gluedIso F).inv = F.map (D.ι i)
The theorem `CategoryTheory.GlueData.ι_gluedIso_inv` states that for any category `C` and `C'`, any glue data `D` in `C`, and any functor `F` from `C` to `C'` that preserves the limit of the cospan `(D.f i j) (D.f i k)` for all `i`, `j`, and `k` in the indexing set `D.J`, if `D` has a multi-coequalizer and the functor `F` preserves the colimit of the multi-span of `D`, then the composition of the morphism from `D.U i` to the glued object in the image of `D` under `F`, and the inverse of the isomorphism from the glued object of `D` to the glued object of the image of `D` under `F`, is equal to the image under `F` of the morphism from `D.U i` to the glued object of `D`.
More concisely: If functor `F` preserves limits and colimits of `C` and `C'` respectively, and preserves the multi-coequalizer of glue data `D` in `C` and the colimit of its image under `F`, then for any index `i` in `D.J`, the composition of `D.f i` with the inverse of the isomorphism between the glued objects is equal to the image under `F` of `D.f i`.
|
CategoryTheory.GlueData.ι_jointly_surjective
theorem CategoryTheory.GlueData.ι_jointly_surjective :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C)
[inst_1 : CategoryTheory.Limits.HasMulticoequalizer D.diagram] (F : CategoryTheory.Functor C (Type v))
[inst_2 : CategoryTheory.Limits.PreservesColimit D.diagram.multispan F]
[inst_3 :
(i j k : D.J) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F]
(x : F.obj D.glued), ∃ i y, F.map (D.ι i) y = x
The theorem `CategoryTheory.GlueData.ι_jointly_surjective` states that if there is a forgetful functor from a category `C` into the category of types `Type` that preserves enough colimits, then the family of maps `D.ι`, indexed by elements of `D.J`, from the objects `D.U i` to the glued object `D.glued` in the glueing data `D` will be jointly surjective. In other words, for every element `x` in the functor applied to the glued object, there exists an index `i` in `D.J` and an element `y` in `D.U i` such that `x` is the image of `y` under the functor applied to the map `D.ι i`.
More concisely: If a forgetful functor from a category preserving sufficient colimits maps the glued object to an element, then there exists an object in the domain of the functor and a map to the glued object whose image under the functor is that element.
|
CategoryTheory.GlueData.glue_condition
theorem CategoryTheory.GlueData.glue_condition :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C)
[inst_1 : CategoryTheory.Limits.HasMulticoequalizer D.diagram] (i j : D.J),
CategoryTheory.CategoryStruct.comp (D.t i j) (CategoryTheory.CategoryStruct.comp (D.f j i) (D.ι j)) =
CategoryTheory.CategoryStruct.comp (D.f i j) (D.ι i)
The theorem `CategoryTheory.GlueData.glue_condition` in category theory states that for any category `C` and a glue data `D` over that category, if the associated multispan index of the glue data has a multicoequalizer, then for any two objects `i` and `j` in the indexing set of the glue data, the composition of the morphism `D.t i j` with the composition of the morphism `D.f j i` and the map from `D.U j` to the glued object is equal to the composition of the morphism `D.f i j` and the map from `D.U i` to the glued object. In mathematical notation, this is saying that `(D.t i j) ≫ (D.f j i) ≫ (D.ι j) = (D.f i j) ≫ (D.ι i)`.
More concisely: For any category `C` and glue data `D` over `C`, if the multispan index of `D` has a multicoequalizer, then for all objects `i` and `j` in the indexing set of `D`, we have `(D.t i j) ∘ (D.f j i) ∘ (D.ι j) = (D.f i j) ∘ (D.ι i)` in `C`.
|
CategoryTheory.GlueData.t_inv
theorem CategoryTheory.GlueData.t_inv :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i j : D.J),
CategoryTheory.CategoryStruct.comp (D.t i j) (D.t j i) = CategoryTheory.CategoryStruct.id (D.V (i, j))
This theorem is a property in Category Theory concerning the structure of gluing data. Specifically, it states that for any category `C`, given a gluing data `D` on `C` and any two indices `i` and `j` in the indexing set of `D`, the composition of the transition morphisms `D.t i j` and `D.t j i` (in that order) is equal to the identity morphism on the object `D.V (i, j)`. In other words, the transition morphisms `D.t i j` and `D.t j i` are inverses of each other with respect to composition in the category `C`.
More concisely: For any category `C` and gluing data `D` on `C`, the transition morphisms `D.t i j` and `D.t j i` are mutual inverses in `C`.
|