CategoryTheory.Arrow.hom_ext
theorem CategoryTheory.Arrow.hom_ext :
∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y : CategoryTheory.Arrow T} (f g : X ⟶ Y),
f.left = g.left → f.right = g.right → f = g
The theorem `CategoryTheory.Arrow.hom_ext` states that for any category `T`, and any two objects `X` and `Y` in the arrow category of `T`, if we have two morphisms `f` and `g` from `X` to `Y`, then `f` equals `g` if and only if the `left` component of `f` equals the `left` component of `g` and the `right` component of `f` equals the `right` component of `g`. In other words, two morphisms in the arrow category are considered identical if their corresponding parts are identical.
More concisely: In the arrow category of a category T, two morphisms from object X to object Y are equal if and only if their source and target components are equal.
|
CategoryTheory.Arrow.comp_left
theorem CategoryTheory.Arrow.comp_left :
∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y Z : CategoryTheory.Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z),
(CategoryTheory.CategoryStruct.comp f g).left = CategoryTheory.CategoryStruct.comp f.left g.left
This theorem, named `CategoryTheory.Arrow.comp_left`, establishes a property about the composition of morphisms in the arrow category of a given category `T`. Specifically, for any three objects `X`, `Y`, `Z` in the arrow category of `T`, and given two morphisms `f` and `g` such that `f` goes from `X` to `Y` and `g` goes from `Y` to `Z`, the left component of the composition of `f` and `g` (denoted as `(CategoryTheory.CategoryStruct.comp f g).left`) is equal to the composition of the left components of `f` and `g` (denoted as `CategoryTheory.CategoryStruct.comp f.left g.left`). In essence, this theorem demonstrates that the composition operation in the arrow category behaves correctly with respect to the left components of its morphisms.
More concisely: In the arrow category of a given category, the left component of the composition of two morphisms is equal to the composition of their left components.
|
CategoryTheory.Arrow.square_to_iso_invert
theorem CategoryTheory.Arrow.square_to_iso_invert :
∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] (i : CategoryTheory.Arrow T) {X Y : T} (p : X ≅ Y)
(sq : i ⟶ CategoryTheory.Arrow.mk p.hom),
CategoryTheory.CategoryStruct.comp i.hom (CategoryTheory.CategoryStruct.comp sq.right p.inv) = sq.left
This theorem, named `CategoryTheory.Arrow.square_to_iso_invert`, states that for any category `T` and any arrow `i` in this category, if we have a commutative square `sq` that connects `i` to an isomorphism `p` between objects `X` and `Y`, then the left side of this square (`sq.left`) is equivalent to the composition of `i.hom` and the composition of `sq.right` and the inverse of `p` (`p.inv`). In other words, the source part of the square can be expressed through the composition of the morphism associated with the arrow and the composition of the right part of the square and the inverse of the isomorphism. This theorem formalizes one of the fundamental properties of commutative squares in category theory.
More concisely: For any arrow `i` in a category `T` and commutative square `sq` connecting `i` to an isomorphism `p`, the source of `sq` is equivalent to the composition of `i` and the right square followed by the inverse of `p`.
|
CategoryTheory.Arrow.w_assoc
theorem CategoryTheory.Arrow.w_assoc :
∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g) {Z : T}
(h : g.right ⟶ Z),
CategoryTheory.CategoryStruct.comp sq.left (CategoryTheory.CategoryStruct.comp g.hom h) =
CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp sq.right h)
This theorem states that for any category `T`, and any two objects `f` and `g` in the arrow category of `T` with a morphism `sq` from `f` to `g`, and any object `Z` in `T` with a morphism `h` from `g.right` to `Z`, the composition of the morphism `sq.left` with the composition of `g.hom` and `h` is equal to the composition of `f.hom` with the composition of `sq.right` and `h`. In other words, the theorem is stating a property of commutative squares in the arrow category, where the paths around the square via different routes yield the same result, a fundamental property in category theory.
More concisely: For any commutative square in a category, the composition of the morphisms along the two parallel paths is equal.
|
CategoryTheory.Arrow.comp_right
theorem CategoryTheory.Arrow.comp_right :
∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y Z : CategoryTheory.Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z),
(CategoryTheory.CategoryStruct.comp f g).right = CategoryTheory.CategoryStruct.comp f.right g.right
This theorem states that for any category `T` and for any three objects `X`, `Y`, `Z` in the arrow category of `T`, given two morphisms `f` from `X` to `Y` and `g` from `Y` to `Z`, the right component (which is a morphism in the original category `T`) of the composite morphism `f ≫ g` in the arrow category of `T` is equal to the composite of the right components of `f` and `g` in the original category `T`. In other words, in the arrow category, composition of morphisms on the right is consistent with the composition operation in the original category.
More concisely: In the arrow category of a given category, the right component of the composite morphism is equal to the composition of the right components in the original category.
|
CategoryTheory.Arrow.w
theorem CategoryTheory.Arrow.w :
∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g),
CategoryTheory.CategoryStruct.comp sq.left g.hom = CategoryTheory.CategoryStruct.comp f.hom sq.right
The theorem `CategoryTheory.Arrow.w` states that for any category `T` and any two objects `f` and `g` in the arrow category of `T`, if there exists a morphism `sq` from `f` to `g`, then the composition of `sq.left` and `g.hom` is equal to the composition of `f.hom` and `sq.right`. Here, `CategoryTheory.CategoryStruct.comp` represents the composition of morphisms in the category. In more mathematical terms, this is saying that for any commutative square in a category, the composition of arrows across one diagonal of the square is equal to the composition of arrows across the other diagonal.
More concisely: For any commutative square in a category, the composition of morphisms along the diagonal from the lower-left to the upper-right is equal to the composition of morphisms along the diagonal from the upper-left to the lower-right.
|
CategoryTheory.Arrow.id_left
theorem CategoryTheory.Arrow.id_left :
∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] (f : CategoryTheory.Arrow T),
(CategoryTheory.CategoryStruct.id f).left = CategoryTheory.CategoryStruct.id f.left
This theorem states that for any category `T` and any arrow `f` in that category, the left component of the identity morphism on `f` is equal to the identity morphism on the left component of `f`. In other words, when we apply the identity morphism to an arrow in the arrow category, it behaves just like applying the identity morphism to the original object in the category `T`.
More concisely: For any category T and arrow f, the left identity morphism of f is equal to the identity morphism on the domain of f.
|
CategoryTheory.Arrow.iso_w'
theorem CategoryTheory.Arrow.iso_w' :
∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {W X Y Z : T} {f : W ⟶ X} {g : Y ⟶ Z}
(e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g),
g = CategoryTheory.CategoryStruct.comp e.inv.left (CategoryTheory.CategoryStruct.comp f e.hom.right)
This theorem, `CategoryTheory.Arrow.iso_w'`, in category theory states that for any category `T` and any four objects `W, X, Y, Z` in `T` with morphisms `f: W ⟶ X` and `g: Y ⟶ Z`, if we have an isomorphism `e` between the arrows (which are simply morphisms in `T`) created by `f` and `g`, then `g` can be obtained by first applying the inverse of the left morphism of `e` and then applying the right morphism of `e` to `f`. In other words, `g` is the composition of `e.inv.left` and the composition of `f` and `e.hom.right`.
More concisely: If `f: W ⟶ X`, `g: Y ⟶ Z` are morphisms in a category `T` and `e: f ≅ g` is an isomorphism, then `g = e.inv.left ∘ (f ∘ e.hom.right)`.
|
CategoryTheory.Arrow.w_mk_right
theorem CategoryTheory.Arrow.w_mk_right :
∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f : CategoryTheory.Arrow T} {X Y : T} {g : X ⟶ Y}
(sq : f ⟶ CategoryTheory.Arrow.mk g),
CategoryTheory.CategoryStruct.comp sq.left g = CategoryTheory.CategoryStruct.comp f.hom sq.right
This theorem, CategoryTheory.Arrow.w_mk_right, states that for any category `T`, any object `f` in the arrow category of `T`, any objects `X` and `Y` in `T`, and any morphism `g` from `X` to `Y`, if there exists a commutative square `sq` in `T` from `f` to the object in the arrow category of `T` represented by `g`, then the composition of the morphism represented by `sq.left` with `g` is equal to the composition of the morphism represented by `f.hom` and `sq.right`. In simpler terms, this theorem ensures the commutativity of a certain square in the arrow category.
More concisely: For any category T, given an arrow f in T's arrow category, objects X and Y in T, and a commutative square from f to the arrow represented by a morphism g from X to Y in T, the composition of g with sq.left is equal to the composition of f.hom with sq.right.
|
CategoryTheory.Arrow.id_right
theorem CategoryTheory.Arrow.id_right :
∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] (f : CategoryTheory.Arrow T),
(CategoryTheory.CategoryStruct.id f).right = CategoryTheory.CategoryStruct.id f.right
This theorem states that for any category `T` and any object `f` in the arrow category of `T`, the "right" component of the identity morphism on `f` is equal to the identity morphism on the "right" component of `f`. In terms of category theory, this means that the identity morphism in the arrow category behaves as expected with respect to the underlying category `T`.
More concisely: For any category T and any arrow f in T, the right identity morphism of the identity morphism of f is equal to the identity morphism of the right component of f.
|
CategoryTheory.Arrow.square_from_iso_invert
theorem CategoryTheory.Arrow.square_from_iso_invert :
∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y : T} (i : X ≅ Y) (p : CategoryTheory.Arrow T)
(sq : CategoryTheory.Arrow.mk i.hom ⟶ p),
CategoryTheory.CategoryStruct.comp i.inv (CategoryTheory.CategoryStruct.comp sq.left p.hom) = sq.right
This theorem states that for any given category `T`, with objects `X` and `Y`, and an isomorphism `i` between `X` and `Y`, and any arrow `p` in the category, if there's a commutative square `sq` from the arrow made by `i.hom` to `p`, then the composition of `i.inv` and the composition of `sq.left` and `p.hom` is equal to `sq.right`. In simpler terms, it expresses the target part of the commutative square in terms of the inverse of the isomorphism.
More concisely: Given any category `T`, isomorphism `i : X ≅ Y`, and arrow `p : X �o Y`, if there's a commutative square `sq` from `i` to `p`, then `i.inv ∘ sq.left ∘ p.hom = sq.right`.
|