CategoryTheory.GradedObject.ι_mapMap
theorem CategoryTheory.GradedObject.ι_mapMap :
∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{u_5, u_4} C]
{X Y : CategoryTheory.GradedObject I C} (φ : X ⟶ Y) (p : I → J) [inst_1 : X.HasMap p] [inst_2 : Y.HasMap p]
(i : I) (j : J) (hij : p i = j),
CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) (CategoryTheory.GradedObject.mapMap φ p j) =
CategoryTheory.CategoryStruct.comp (φ i) (Y.ιMapObj p i j hij)
The theorem `CategoryTheory.GradedObject.ι_mapMap` is about the composition of morphisms in a categorical context. Specifically, for any types `I`, `J`, and `C`, with `C` behaving as a category, and for any `I`-graded objects `X` and `Y` in `C`, a morphism `φ` from `X` to `Y`, a function `p` from `I` to `J`, and for all `i` in `I` and `j` in `J` such that `p` maps `i` to `j`, if both `X` and `Y` have the property `HasMap` with respect to `p` (meaning that for each `j`, the coproduct of all objects `X i` or `Y i` for which `p i = j` exists), then the composition of the morphism that maps `X i` to the coproduct for `j` in `X` and the morphism that maps this coproduct to `Y j` is equal to the composition of the morphism `φ i` and the morphism that maps `Y i` to the coproduct for `j` in `Y`. This theorem highlights a specific property of these compositions in the context of category theory.
More concisely: Given categories `C` with types `I`, `J`, `C`-graded objects `X` and `Y`, morphism `φ: X ⟶ Y`, function `p: I ⟶ J`, and `HasMap` instance for both `X` and `Y` with respect to `p`, the morphism composition `φ ∘ (∑ i, p = j, X i ⟶ ∑ j, Y j)` is equal to `∑ i, p = j, φ i ∘ (X i ⟶ Y j)`.
|
CategoryTheory.GradedObject.ι_mapMap_assoc
theorem CategoryTheory.GradedObject.ι_mapMap_assoc :
∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{u_5, u_4} C]
{X Y : CategoryTheory.GradedObject I C} (φ : X ⟶ Y) (p : I → J) [inst_1 : X.HasMap p] [inst_2 : Y.HasMap p]
(i : I) (j : J) (hij : p i = j) {Z : C} (h : Y.mapObj p j ⟶ Z),
CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap φ p j) h) =
CategoryTheory.CategoryStruct.comp (φ i) (CategoryTheory.CategoryStruct.comp (Y.ιMapObj p i j hij) h)
This theorem, named `CategoryTheory.GradedObject.ι_mapMap_assoc`, states that in a category `C`, given two `I`-graded objects `X` and `Y` and a morphism `φ` from `X` to `Y`, as well as a map `p` from `I` to another type `J` (where both `X` and `Y` have a corresponding `p`-map), for any `i` from `I` and `j` from `J` such that `p(i) = j`, and any morphism `h` from the `j`-object of the `p`-map of `Y` to another object `Z` in `C`, the composition of the `i`-object of the `p`-map of `X` with the composition of the `j`-object of the `p`-map of `φ` and `h` is equal to the composition of `φ(i)` with the composition of the `i`-object of the `p`-map of `Y` and `h`.
In more straightforward terms, this theorem expresses a certain associativity property in the context of graded objects in a category, involving the interaction of morphisms, grading maps and the coproduct structure of the graded objects.
More concisely: For any category `C`, given graded objects `X` and `Y` and a morphism `φ:` `X` → `Y`, and maps `p:` `I` → `J` for their grading, for all `i` in `I` and `j` in `J` with `p(i) = j`, and for any morphism `h:` the `j`-object of `Y` → `Z` in `C`, we have `(ι_X i) ∘ (φ i ∘ h) = (φ i) ∘ (ι_Y i)`.
|
CategoryTheory.GradedObject.mapMap_id
theorem CategoryTheory.GradedObject.mapMap_id :
∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{u_5, u_4} C]
(X : CategoryTheory.GradedObject I C) (p : I → J) [inst_1 : X.HasMap p],
CategoryTheory.GradedObject.mapMap (CategoryTheory.CategoryStruct.id X) p =
CategoryTheory.CategoryStruct.id (X.mapObj p)
The theorem `CategoryTheory.GradedObject.mapMap_id` states that for any types `I`, `J`, and `C` with `C` being a category, any graded object `X` of type `I` in category `C`, and any function `p: I → J`, if `X` has a map associated with function `p`, then applying the identity morphism of `X` and then mapping with `p` is the same as applying the identity morphism of the mapped object (i.e., the object obtained by mapping the graded object `X` using the function `p`). In other words, this is essentially a statement of the identity law in the context of graded objects in a category.
More concisely: For any category `C`, any graded object `X` over `C` of type `I`, and any function `p: I → J`, if `X` has a map `f: X ➝ Ob C`, then `id X �circ f = f (id I)`.
|
CategoryTheory.GradedObject.mapObj_ext
theorem CategoryTheory.GradedObject.mapObj_ext :
∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{u_5, u_4} C]
(X : CategoryTheory.GradedObject I C) (p : I → J) [inst_1 : X.HasMap p] {A : C} {j : J} (f g : X.mapObj p j ⟶ A),
(∀ (i : I) (hij : p i = j),
CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) f =
CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) g) →
f = g
This theorem, `CategoryTheory.GradedObject.mapObj_ext`, states that for any `I`, `J` and `C` such that `C` is a category, any `X` being a graded object in `C` indexed by `I`, and any function `p: I → J`, if we have that the coproduct of all `X i` such that `p i = j` exists for all `j: J` and any object `A` in `C` and `j` in `J`, then for any two morphisms `f` and `g` from `CategoryTheory.GradedObject.mapObj X p j` to `A`, if for all `i: I` such that `p i = j`, the composition of `CategoryTheory.GradedObject.ιMapObj X p i j hij` and `f` is equal to the composition of `CategoryTheory.GradedObject.ιMapObj X p i j hij` and `g`, then `f` and `g` must be equal. This theorem encapsulates the idea of uniqueness in the context of category theory, stating that if two morphisms make the same commutative diagrams, they must be the same morphism.
More concisely: Given any category `C`, a graded object `X` indexed by `I` in `C`, a function `p: I → J`, and objects `A` and morphisms `f` and `g` in `C`, if for all `j: J` the coproduct of `X i` with `p i = j` exists and for all `i: I` such that `p i = j` the diagrams commute: `ιMapObj X p i j (hij ∘ f) = ιMapObj X p i j (hij ∘ g)`, then `f = g`.
|
CategoryTheory.GradedObject.ι_descMapObj
theorem CategoryTheory.GradedObject.ι_descMapObj :
∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{u_5, u_4} C]
(X : CategoryTheory.GradedObject I C) (p : I → J) [inst_1 : X.HasMap p] {A : C} {j : J}
(φ : (i : I) → p i = j → (X i ⟶ A)) (i : I) (hi : p i = j),
CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hi) (X.descMapObj p φ) = φ i hi
The theorem `CategoryTheory.GradedObject.ι_descMapObj` states that for any types `I`, `J`, and `C` where `C` is a category, any graded object `X` of type `I` in category `C`, any function `p` from `I` to `J`, and given that `X` has a map `p`, for any object `A` in `C` and any `j` in `J`, if we have a family of morphisms `φ` from each `i` in `I` (where `p i` equals `j`) to `A`, then the composition of the morphism from `X i` to the coproduct of all `X i` such that `p i = j` and the morphism from this coproduct to `A` (which is constructed using the family `φ`), is equal to `φ i`, for any `i` in `I` where `p i = j`. In other words, this theorem captures a property of commuting diagrams in the category, where the direct morphism from one object to another is the same as the composite of two morphisms via an intermediary object.
More concisely: For any graded object X in a category C, function p from I to J, and object A in C, if for all i in I with p(i) = j, there are morphisms φi from X i to A, then the composition of the morphism from the coproduct of {X i | p(i) = j} to A constructed from φi and the morphism from X i to this coproduct is equal to φi for all i.
|
CategoryTheory.GradedObject.hom_ext
theorem CategoryTheory.GradedObject.hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type u_1} {X Y : CategoryTheory.GradedObject β C}
(f g : X ⟶ Y), (∀ (x : β), f x = g x) → f = g
The theorem `CategoryTheory.GradedObject.hom_ext` states that for any category `C`, for any type `β`, and for any two `β`-graded objects `X` and `Y` in `C`, if for any element `x` of type `β`, the morphisms `f` and `g` from `X` to `Y` behave in such a way that `f(x) = g(x)`, then we can conclude that `f` is equal to `g`. In other words, if two morphisms between the same pair of `β`-graded objects in a category coincide on each grading, they are equal.
More concisely: Given any category `C`, if for every `β`-graded object `X` and `Y` in `C` and every element `x` of type `β`, the morphisms `f` and `g` from `X` to `Y` satisfy `f(x) = g(x)`, then `f = g` as morphisms from `X` to `Y`.
|