CategoryTheory.map_hom_inv_app_assoc
theorem CategoryTheory.map_hom_inv_app_assoc :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {X Y : C} (e : X ≅ Y) (Z : D) {Z_1 : E}
(h : (F.obj X).obj Z ⟶ Z_1),
CategoryTheory.CategoryStruct.comp ((F.map e.hom).app Z)
(CategoryTheory.CategoryStruct.comp ((F.map e.inv).app Z) h) =
h
This theorem, `CategoryTheory.map_hom_inv_app_assoc`, states that for any categories `C`, `D`, and `E`, given a functor `F` from `C` to the category of functors from `D` to `E`, any two objects `X` and `Y` in `C` related by an isomorphism `e`, an object `Z` of `D` and a morphism `h` from the functor object `(F.obj X).obj Z` to an object `Z_1` in `E`, the composition of the application of the homomorphism part `e.hom` of the isomorphism `e` followed by the composition of the application of the inverse part `e.inv` of the isomorphism `e` and the morphism `h` is equal to `h`. This can be interpreted as a kind of cancellation law for morphisms in a category, showing that the inverse of a morphism behaves as expected under composition.
More concisely: Given functors F from category C to Functor(D, E), isomorphisms e : X ≅ Y in C, objects Z in D, and morphisms h : (F.obj X).obj Z → Z'\_, the composition of e.hom ∘ (e.inv ∘ h) equals h.
|
CategoryTheory.NatTrans.mono_of_mono_app
theorem CategoryTheory.NatTrans.mono_of_mono_app :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G)
[inst_2 : ∀ (X : C), CategoryTheory.Mono (α.app X)], CategoryTheory.Mono α
This theorem states that in the context of category theory, given two categories C and D and two functors F and G from C to D, a natural transformation α from F to G is a monomorphism if each component of α, denoted as α.app X for each object X in C, is a monomorphism.
More concisely: A natural transformation between functors is a monomorphism if each of its components is a monomorphism in the corresponding categories.
|
CategoryTheory.NatTrans.ext'
theorem CategoryTheory.NatTrans.ext' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} {α β : F ⟶ G},
α.app = β.app → α = β
The theorem `CategoryTheory.NatTrans.ext'` states that for any two categories `C` and `D` (of types `u₁` and `u₂`, and with category structures `inst` and `inst_1`, respectively) and any two functors `F` and `G` from `C` to `D`, and for natural transformations `α` and `β` from `F` to `G`, if the application of `α` and `β` are equal, then `α` is equal to `β`. This is a result in category theory that says that natural transformations are completely determined by their action on objects.
More concisely: Given categories `C` and `D` with functors `F` and `G` from `C` to `D`, and natural transformations `α` and `β` from `F` to `G`, if `α.app (x) = β.app (x)` for all objects `x` in `C`, then `α = β`.
|
CategoryTheory.NatTrans.epi_of_epi_app
theorem CategoryTheory.NatTrans.epi_of_epi_app :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G)
[inst_2 : ∀ (X : C), CategoryTheory.Epi (α.app X)], CategoryTheory.Epi α
This theorem states that in the context of category theory, a natural transformation is an epimorphism if each component of the natural transformation is an epimorphism. More specifically, for any categories `C` and `D`, and any functors `F` and `G` between them, if the application of a natural transformation `α` from `F` to `G` to any object `X` in `C` is an epimorphism, then `α` itself is an epimorphism.
More concisely: A natural transformation between functors is an epimorphism if each of its components is an epimorphism in the source category.
|
CategoryTheory.NatTrans.id_app
theorem CategoryTheory.NatTrans.id_app :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C),
(CategoryTheory.CategoryStruct.id F).app X = CategoryTheory.CategoryStruct.id (F.obj X)
The theorem `CategoryTheory.NatTrans.id_app` states that for any objects `C` and `D` in the categories `u₁` and `u₂` respectively, and any functor `F` from `C` to `D` and object `X` in `C`, the application of the identity natural transformation on `F` at `X` is equal to the identity morphism on the object `F.obj X` in `D`. In other words, applying the identity natural transformation to a functor and then applying the result to an object is the same as first applying the functor to the object and then applying the identity morphism.
More concisely: For any functors F : C -> D between categories C and D, and object X in C, the identity natural transformation on F at X equals the identity morphism on F(X) in D.
|
CategoryTheory.NatTrans.comp_app
theorem CategoryTheory.NatTrans.comp_app :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H)
(X : C),
(CategoryTheory.CategoryStruct.comp α β).app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app X)
The theorem `CategoryTheory.NatTrans.comp_app` states that for any categories `C` and `D`, and any functors `F`, `G`, and `H` from `C` to `D`, and for all natural transformations `α` from `F` to `G` and `β` from `G` to `H`, and any object `X` in `C`, the application of the composite of `α` and `β` to `X` is equal to the composition of the applications of `α` and `β` to `X`. This is essentially asserting the functoriality of natural transformations in the category of functors from `C` to `D`.
More concisely: Given categories C and D, functors F, G, and H from C to D, and natural transformations α: F ➝ G and β: G ➝ H, the composition of α and β, β ∘ α, is equal to the composition of their applications to any object X in C, (β ∘ α)(X) = β(G(α(X))).
|
CategoryTheory.NatTrans.congr_app
theorem CategoryTheory.NatTrans.congr_app :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} {α β : F ⟶ G},
α = β → ∀ (X : C), α.app X = β.app X
This theorem states that in the context of category theory, for any two categories `C` and `D`, and any two functors `F` and `G` from `C` to `D`, if two natural transformations `α` and `β` from `F` to `G` are equal, then their applications to any object `X` in `C` are also equal. In other words, if two natural transformations are the same, they behave the same way when applied to any object in the source category.
More concisely: For any categories C, D, functors F and G from C to D, and natural transformations α and β from F to G, if α = β, then for all objects X in C, α(X) = β(X).
|