CategoryTheory.Limits.pullback.diagonal.proof_1
theorem CategoryTheory.Limits.pullback.diagonal.proof_1 :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y : C} (f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f =
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f
This theorem states that in any category `C`, for any objects `X` and `Y` in `C` and for any morphism `f` from `X` to `Y`, the composition of the identity morphism on `X` with `f` is equal to the composition of the identity morphism on `X` with `f`. In simpler terms, it says that composing `f` with the identity on `X` doesn't change `f`, a fundamental property in category theory.
More concisely: In any category, the composition of an identity morphism with any morphism is equal to the morphism itself.
|
CategoryTheory.Limits.pullback.diagonal_isKernelPair
theorem CategoryTheory.Limits.pullback.diagonal_isKernelPair :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y)
[inst_1 : CategoryTheory.Limits.HasPullback f f],
CategoryTheory.IsKernelPair f CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd
The theorem `CategoryTheory.Limits.pullback.diagonal_isKernelPair` states that in any category `C`, for any objects `X` and `Y` and a morphism `f` from `X` to `Y`, if the pullback of `f` and `f` exists, then the two projections from the pullback to `X` form a kernel pair for `f`. This means that the diagram formed by the two projections and `f` is a pullback square, and the compositions of the projections with `f` are equal. This theorem is significant in the theory of limits in category theory.
More concisely: In any category, given objects X, Y and a morphism f from X to Y with a pullback, the pullback projections form a kernel pair for f. (That is, the diagram of the two projections and f is a pullback square, and their compositions with f are equal.)
|