CategoryTheory.IsKernelPair.cancel_right
theorem CategoryTheory.IsKernelPair.cancel_right :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y Z : C} {a b : R ⟶ X} {f₁ : X ⟶ Y} {f₂ : Y ⟶ Z},
CategoryTheory.CategoryStruct.comp a f₁ = CategoryTheory.CategoryStruct.comp b f₁ →
CategoryTheory.IsKernelPair (CategoryTheory.CategoryStruct.comp f₁ f₂) a b →
CategoryTheory.IsKernelPair f₁ a b
The theorem `CategoryTheory.IsKernelPair.cancel_right` states that in a category `C`, for any objects `R`, `X`, `Y`, and `Z`, and morphisms `a`, `b` from `R` to `X` and `f₁` from `X` to `Y`, and `f₂` from `Y` to `Z`, if `(a,b)` forms a kernel pair for the composition of `f₁` and `f₂`, and the composition of `a` with `f₁` is equal to the composition of `b` with `f₁`, then `(a,b)` is also a kernel pair for `f₁` alone. In other words, to show that `(a,b)` is a kernel pair for `f₁`, it suffices to show the square commutes for `f₁ ≫ f₂`, rather than showing it is a pullback for `f₁` separately.
More concisely: Given objects R, X, Y, Z in a category C, morphisms a, b from R to X, and f₁ from X to Y, f₂ from Y to Z such that (a, b) is a kernel pair for the composition f₁ ∘ f₂ and a ∘ f₁ = b ∘ f₁, then (a, b) is also a kernel pair for f₁.
|
CategoryTheory.IsKernelPair.mono_of_isIso_fst
theorem CategoryTheory.IsKernelPair.mono_of_isIso_fst :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X},
CategoryTheory.IsKernelPair f a b → ∀ [inst_1 : CategoryTheory.IsIso a], CategoryTheory.Mono f
The theorem `CategoryTheory.IsKernelPair.mono_of_isIso_fst` states that for any objects R, X, Y, and morphisms f, a, b in some category C, if `(a, b)` forms a kernel pair for `f` (i.e., both `a` and `b` are morphisms from `R` to `X` such that `a` composed with `f` equals `b` composed with `f` and the square formed by `R` to `X`, `R` to `X`, `X` to `Y`, and `X` to `Y` is a pullback square), and `a` is an isomorphism (i.e., it has an inverse under composition in the category), then `f` is a monomorphism (i.e., `f` is left-cancellable: for any morphisms `g` and `h`, if `f` composed with `g` equals `f` composed with `h`, then `g` equals `h`).
More concisely: If in a category, a morphism `f` has an isomorphism `a` as its kernel pair, then `f` is a monomorphism.
|
CategoryTheory.IsKernelPair.comp_of_mono
theorem CategoryTheory.IsKernelPair.comp_of_mono :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y Z : C} {a b : R ⟶ X} {f₁ : X ⟶ Y} {f₂ : Y ⟶ Z}
[inst_1 : CategoryTheory.Mono f₂],
CategoryTheory.IsKernelPair f₁ a b → CategoryTheory.IsKernelPair (CategoryTheory.CategoryStruct.comp f₁ f₂) a b
This theorem states that in a category theory context, if `(a, b)` is a kernel pair for a morphism `f₁` and `f₂` is a monomorphism (i.e., a morphism that is left-cancellable), then `(a, b)` is also a kernel pair for the composition of `f₁` and `f₂` (written as `f₁ ≫ f₂`). This is the converse of the `cancel_right_of_mono` property, which says that if `(a, b)` is a kernel pair for `f₁ ≫ f₂` and `f₂` is mono, then `(a, b)` is a kernel pair for `f₁`.
In other words, the property of being a kernel pair is preserved under composition with a monomorphism on the right.
More concisely: If `(a, b)` is a kernel pair for a morphism `f₁` and `f₂` is a monomorphism, then `(a, b)` is a kernel pair for the composition `f₁ ≫ f₂`.
|
CategoryTheory.IsKernelPair.cancel_right_of_mono
theorem CategoryTheory.IsKernelPair.cancel_right_of_mono :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y Z : C} {a b : R ⟶ X} {f₁ : X ⟶ Y} {f₂ : Y ⟶ Z}
[inst_1 : CategoryTheory.Mono f₂],
CategoryTheory.IsKernelPair (CategoryTheory.CategoryStruct.comp f₁ f₂) a b → CategoryTheory.IsKernelPair f₁ a b
The theorem `CategoryTheory.IsKernelPair.cancel_right_of_mono` states that in a category `C`, if `(a, b)` is a kernel pair for the composition of two morphisms `f₁` and `f₂` (expressed as `f₁ ≫ f₂`) and `f₂` is a monomorphism (injective), then `(a, b)` is also a kernel pair for `f₁` alone. This theorem is essentially the converse of `comp_of_mono`, asserting the ability to cancel the right morphism in a kernel pair under the assumption of it being a monomorphism.
More concisely: If `(a, b)` is a kernel pair for the composition of morphisms `f₁ ≫ f₂` in a category `C` and `f₂` is a monomorphism, then `(a, b)` is a kernel pair for `f₁`.
|
CategoryTheory.IsKernelPair.pullback
theorem CategoryTheory.IsKernelPair.pullback :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z A : C} {g : Y ⟶ Z} {a₁ a₂ : A ⟶ Y}
(h : CategoryTheory.IsKernelPair g a₁ a₂) (f : X ⟶ Z) [inst_1 : CategoryTheory.Limits.HasPullback f g]
[inst_2 : CategoryTheory.Limits.HasPullback f (CategoryTheory.CategoryStruct.comp a₁ g)],
CategoryTheory.IsKernelPair CategoryTheory.Limits.pullback.fst
(CategoryTheory.Limits.pullback.map f (CategoryTheory.CategoryStruct.comp a₁ g) f g
(CategoryTheory.CategoryStruct.id X) a₁ (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)
(CategoryTheory.Limits.pullback.map f (CategoryTheory.CategoryStruct.comp a₁ g) f g
(CategoryTheory.CategoryStruct.id X) a₂ (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)
This theorem states that if a pair of morphisms `a₁, a₂ : A ⟶ Y` form a kernel pair for another morphism `g : Y ⟶ Z` in some category `C`, then the pullback pair (i.e., `a₁ ×[Z] X` and `a₂ ×[Z] X`) forms a kernel pair for the morphism `Y ×[Z] X ⟶ X`. This result holds given the existence of pullbacks for `f : X ⟶ Z` and `g`, and for the composition `a₁` followed by `g`. The pullback pair is formed via the `CategoryTheory.Limits.pullback.map` function which constructs a new morphism from the pullback of the original pair of morphisms.
More concisely: If `a₁` and `a₂` form a kernel pair for `g` in a category with pullbacks, then their pullback pair forms a kernel pair for the product morphism `Y ×[Z] X ⟶ X`.
|
CategoryTheory.IsKernelPair.id_of_mono
theorem CategoryTheory.IsKernelPair.id_of_mono :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
CategoryTheory.IsKernelPair f (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X)
The theorem `CategoryTheory.IsKernelPair.id_of_mono` states that if a morphism `f` in a category `C` is a monomorphism (i.e., it has the left cancellation property), then the pair of identity morphisms on the domain object `X` of `f` forms a kernel pair for `f`. In other words, the pair `(𝟙 _, 𝟙 _)` satisfies the property that their compositions with `f` are equal and the square, whose corners are the domain of `f`, the codomain of `f`, and the domain of the identity morphisms, is a pullback square.
More concisely: If `f` is a monomorphism in a category `C`, then the pair of identity morphisms on the domain of `f` forms a kernel pair for `f`, meaning their compositions with `f` are equal and the square they form with `f` as the diagonal morphism is a pullback square.
|