CategoryTheory.MonoOver.pullback.proof_1
theorem CategoryTheory.MonoOver.pullback.proof_1 :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasPullbacks C] (f : X ⟶ Y) (g : CategoryTheory.MonoOver Y),
CategoryTheory.Mono CategoryTheory.Limits.pullback.snd
This theorem states that for any category `C` with pullbacks, given any morphisms `f` (from object `X` to object `Y`) and `g` (which is a monomorphism over `Y`), the second projection of the pullback of `f` and `g` is a monomorphism. Here, a monomorphism is a morphism that is left-cancellable, and a pullback is a universal construction that comes with two morphisms such that their composition is equal to the original morphisms. This theorem is a part of the categorical theory and it is instrumental in understanding the properties of categories with certain limits.
More concisely: Given a category with pullbacks, if `f: X → Y` is a morphism and `g: Y' → Y` is a monomorphism, then the second projection of the pullback of `f` and `g` is a monomorphism.
|
CategoryTheory.MonoOver.map.proof_1
theorem CategoryTheory.MonoOver.map.proof_1 :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y : C} (f : X ⟶ Y)
[inst_1 : CategoryTheory.Mono f] (g : CategoryTheory.MonoOver X),
CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp g.arrow f)
This theorem states that in the category theory context, given a category `C`, objects `X` and `Y` in `C`, a morphism `f` from `X` to `Y` which is a monomorphism, and a monomorphism `g` over `X`, the composition of the underlying arrow of `g` and `f` (i.e., `CategoryTheory.MonoOver.arrow g` followed by `f`) is also a monomorphism.
More concisely: In the category theory context, given a monomorphism `g` over `X` and a monomorphism `f` from `X` to `Y`, their composition `g ∘ f` is also a monomorphism.
|
CategoryTheory.MonoOver.w
theorem CategoryTheory.MonoOver.w :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {f g : CategoryTheory.MonoOver X} (k : f ⟶ g),
CategoryTheory.CategoryStruct.comp k.left g.arrow = f.arrow
The theorem `CategoryTheory.MonoOver.w` states that for any category `C`, and any object `X` in `C`, if `f` and `g` are monomorphisms over `X`, and if there exists a morphism `k` from `f` to `g`, then the composition of the left arrow of `k` with the underlying arrow of `g` is equal to the underlying arrow of `f`. This is essentially a commutativity condition in the context of monomorphisms in a category.
More concisely: If `f` and `g` are monomorphisms in a category `C` over an object `X`, and there exists a morphism `k` from `f` to `g`, then the left arrow of `k` composes with the underlying arrow of `g` to equal the underlying arrow of `f`: `left k ∘ g = f`.
|
CategoryTheory.MonoOver.image.proof_1
theorem CategoryTheory.MonoOver.image.proof_1 :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X : C} [inst_1 : CategoryTheory.Limits.HasImages C]
(f : CategoryTheory.Over X), CategoryTheory.Limits.HasImage f.hom
This theorem states that for any category 'C' and object 'X' in 'C', if 'C' has limits and 'f' is an object in the over category of 'X', then the morphism 'f.hom' from 'f' has an image. In category theory, the over category 'CategoryTheory.Over X' is defined as the category whose objects are arrows in 'C' with codomain 'X' and morphisms are commutative triangles. The morphism 'f.hom' from an object 'f' in this over category therefore has a codomain of 'X'. The image of a morphism is a generalization of the concept of image in set theory. This theorem thus asserts the existence of such an image for the morphism 'f.hom' given the stated conditions.
More concisely: For any category 'C' with limits and object 'X', the morphism 'f.hom' in the over category 'CategoryTheory.Over X' of 'X' has an image.
|