CategoryTheory.Under.mono_of_mono_right
theorem CategoryTheory.Under.mono_of_mono_right :
∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (k : f ⟶ g)
[hk : CategoryTheory.Mono k.right], CategoryTheory.Mono k
This theorem states that given a category `T` and an object `X` in `T`, if there's a morphism `k` from an object `f` to an object `g` in the under category of `X` (which consists of arrows with domain `X`), and if the morphism `k.right` is a monomorphism (an injective morphism), then `k` is also a monomorphism. Essentially, the `Under.forget X` functor, which forgets the structure of the under category and just considers the underlying category `T`, reflects monomorphisms. However, the reverse implication doesn't hold true without further assumptions on the category `T`, as explained in `CategoryTheory.Under.mono_right_of_mono`.
More concisely: In a category, if the right component of a morphism is a monomorphism, then the morphism itself is a monomorphism when regarded as an arrow in the under category of an object. (This statement holds without loss of monomorphisms under the underlying forgetful functor, but the converse does not generally hold.)
|
CategoryTheory.Over.mono_of_mono_left
theorem CategoryTheory.Over.mono_of_mono_left :
∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (k : f ⟶ g)
[hk : CategoryTheory.Mono k.left], CategoryTheory.Mono k
The theorem `CategoryTheory.Over.mono_of_mono_left` states that given a category `T` and an object `X` in `T`, if `k` is a morphism from `f` to `g` in the over category of `X` (i.e., `f` and `g` are arrows in `T` with codomain `X`), and if the underlying morphism of `k` in `T` (denoted by `k.left`) is a monomorphism (an injective morphism), then `k` itself is a monomorphism in the over category. This theorem essentially says that the functor that forgets the extra structure of the over category and returns to `T` reflects monomorphisms. Note that this is the converse of `CategoryTheory.Over.mono_left_of_mono`.
More concisely: If `k` is a morphism in the over category of object `X` in category `T`, with its underlying morphism in `T` being a monomorphism, then `k` is a monomorphism in the over category.
|
CategoryTheory.Over.OverMorphism.ext
theorem CategoryTheory.Over.OverMorphism.ext :
∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X} {f g : U ⟶ V},
f.left = g.left → f = g
The theorem `CategoryTheory.Over.OverMorphism.ext` states that for any category `T` and any object `X` in `T`, given two objects `U` and `V` in the over category over `X`, and two morphisms `f` and `g` from `U` to `V` in this over category, if the underlying morphisms of `f` and `g` in the original category `T` are equal, then `f` and `g` themselves are equal. This essentially tells us that in the over category, the morphisms are determined by their underlying morphisms in the base category.
More concisely: In the over category of an object X in a category T, two morphisms from U to V have the same underlying morphism in T imply they are equal as morphisms.
|
CategoryTheory.Under.w
theorem CategoryTheory.Under.w :
∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {A B : CategoryTheory.Under X} (f : A ⟶ B),
CategoryTheory.CategoryStruct.comp A.hom f.right = B.hom
This theorem is in the context of category theory and it states that for any category `T` with an object `X`, and any two objects `A` and `B` in the under category of `X` (meaning that the objects are arrows with domain `X`), any morphism `f` from `A` to `B` satisfies the property that the composition of `A.hom` and `f.right` is equal to `B.hom`. In other words, if we have a morphism from `A` to `B` in this under category, then the composition of the homomorphism of `A` and the right component of `f` will give us the homomorphism of `B`. This expresses a condition of commutativity in the under category.
More concisely: For any category T with an object X and morphisms f from A to B in the under category of X, the composition of A.hom and f.right equals B.hom.
|
CategoryTheory.Under.UnderMorphism.ext
theorem CategoryTheory.Under.UnderMorphism.ext :
∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Under X} {f g : U ⟶ V},
f.right = g.right → f = g
This theorem in the Category Theory is stating that for any type `T` which forms a category, for any object `X` of the category `T` and for any two objects `U` and `V` in the under category of `X`, if we have two morphisms `f` and `g` from `U` to `V` and if the right component of the morphisms `f` and `g` are equal, then the morphisms `f` and `g` are themselves equal. Here, the under category is defined as a category where objects are arrows with domain `X` and morphisms are commutative triangles.
More concisely: In the under category of an object `X` in a category `T`, if two morphisms from an object `U` to `V` have equal right components, then they are equal.
|
CategoryTheory.Over.w
theorem CategoryTheory.Over.w :
∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {A B : CategoryTheory.Over X} (f : A ⟶ B),
CategoryTheory.CategoryStruct.comp f.left B.hom = A.hom
This theorem states that for any category `T` and any object `X` in `T`, if `A` and `B` are objects in the over category of `X` and `f` is a morphism from `A` to `B` in this over category, then the composition of the morphism `f` with the homomorphism of `B` is the same as the homomorphism of `A`. In other words, if we consider `A` and `B` as arrows in `T` with codomain `X`, this theorem guarantees that composing `f` with the arrow of `B` gives us the arrow of `A`. This description captures the commutativity of the triangle formed by `A`, `B`, and `X` in the over category of `X`.
More concisely: Given a category T and an object X, for any objects A and B in the over category of X, and a morphism f from A to B in this over category, the composition of f with the structure morphism of B is equal to the structure morphism of A.
|
CategoryTheory.Over.epi_of_epi_left
theorem CategoryTheory.Over.epi_of_epi_left :
∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (k : f ⟶ g)
[hk : CategoryTheory.Epi k.left], CategoryTheory.Epi k
This theorem states that if `k.left` is an epimorphism in a category theory context, then `k` is also an epimorphism. In other words, the `Over.forget X` operation, which discards extra structure and retrieves the underlying category, reflects epimorphisms. However, the converse of this statement doesn't hold true without additional assumptions on the underlying category, as pointed out in `CategoryTheory.Over.epi_left_of_epi`. Here, `T` is a type that forms a category, `X` is an object in `T`, and `f` and `g` are objects in the over category over `X`. The morphism `k` is a morphism from `f` to `g` in the over category.
More concisely: If `k` is an epimorphism in the over category with underlying category `T` and object `X`, then `k.left` is an epimorphism in `T`.
|
CategoryTheory.Under.epi_of_epi_right
theorem CategoryTheory.Under.epi_of_epi_right :
∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (k : f ⟶ g)
[hk : CategoryTheory.Epi k.right], CategoryTheory.Epi k
This theorem states that, for any category `T` and any object `X` of `T`, if we deal with the "Under" category (which is the category of arrows with `X` as their domain), then if we have two objects `f` and `g` in this Under category and a morphism `k` from `f` to `g`, if `k.right` (which corresponds to a morphism in the original category `T`) is an epimorphism (a right-cancellable morphism), then `k` itself is also an epimorphism in the Under category. This means that the `Under.forget` functor, which forgets the structure of the Under category and sees only the original category, reflects epimorphisms. The theorem is the converse of `CategoryTheory.Under.epi_right_of_epi`. Note that this theorem is not marked as an instance, to avoid potential loops in type class inference.
More concisely: In any category T, if a morphism in the Under category with domain X is right-cancelled (has right-cancellable right component in T) as a morphism in T, then it is an epimorphism in the Under category.
|