CategoryTheory.Limits.imageSubobject_iso_comp
theorem CategoryTheory.Limits.imageSubobject_iso_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasEqualizers C]
{X' : C} (h : X' ⟶ X) [inst_2 : CategoryTheory.IsIso h] (f : X ⟶ Y) [inst_3 : CategoryTheory.Limits.HasImage f],
CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f) =
CategoryTheory.Limits.imageSubobject f
This theorem, `CategoryTheory.Limits.imageSubobject_iso_comp`, states that for any category `C` that has equalizers, and any objects `X`, `Y`, `X'` in `C`, if we have an isomorphism `h` from `X'` to `X`, and a morphism `f` from `X` to `Y` such that `f` has an image, then the image subobject of the composition of `h` and `f` (denoted as `h ≫ f`) is the same as the image subobject of `f`. In other words, precomposing by an isomorphism does not change the image subobject.
More concisely: For any category with equalizers, if `h` is an isomorphism from `X'` to `X` and `f` is a morphism from `X` to `Y` with an image subobject, then the image subobject of `h ≫ f` equals the image subobject of `f`.
|
CategoryTheory.Limits.kernelSubobjectMap_arrow
theorem CategoryTheory.Limits.kernelSubobjectMap_arrow :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f]
{X' Y' : C} {f' : X' ⟶ Y'} [inst_3 : CategoryTheory.Limits.HasKernel f']
(sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f'),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap sq)
(CategoryTheory.Limits.kernelSubobject f').arrow =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject f).arrow sq.left
This theorem is about the composition of morphisms in the context of category theory. Specifically, for any category `C`, objects `X`, `Y`, `X'`, and `Y'` in `C`, and morphisms `f : X ⟶ Y`, `f' : X' ⟶ Y'`, where `f` and `f'` have kernels, then for any morphism `sq` from the arrow object made from `f` to the arrow object made from `f'`, the composition of the kernel subobject map of `sq` and the arrow from the kernel subobject of `f'` is equal to the composition of the arrow from the kernel subobject of `f` and the left part of `sq`. In mathematical terms, this theorem states that `(kernelSubobjectMap sq) ∘ (arrow (kernelSubobject f')) = (arrow (kernelSubobject f)) ∘ sq.left`, where `∘` denotes the composition of morphisms.
More concisely: Given any categories `C`, objects `X`, `Y`, `X'`, `Y'`, morphisms `f : X ⟶ Y`, `f' : X' ⟶ Y'` with kernels, and arrow object morphism `sq : (f ⟶ f')`, the composition of the kernel subobject maps factors through `sq` as `(kernelSubobjectMap sq) ∘ (arrow (kernelSubobject f')) = (arrow (kernelSubobject f)) ∘ sq.left`.
|
CategoryTheory.Limits.kernelSubobject_arrow_comp
theorem CategoryTheory.Limits.kernelSubobject_arrow_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject f).arrow f = 0
The theorem `CategoryTheory.Limits.kernelSubobject_arrow_comp` states that, for any category `C` with zero morphisms, and for any morphisms `f` from object `X` to object `Y` in `C` which possess a kernel, the composition of the arrow of the kernel subobject of `f` and `f` itself equals to the zero morphism. In mathematical terms, if `f : X ⟶ Y` and `g` is the arrow of the kernel subobject of `f`, then `g ≫ f = 0` in the category `C`.
More concisely: Given a category with zero morphisms `C`, if `f : X ⟶ Y` in `C` has a kernel and `g` is its arrow, then `g ∘ f = 0`.
|
CategoryTheory.Limits.kernelSubobject_arrow_comp_assoc
theorem CategoryTheory.Limits.kernelSubobject_arrow_comp_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f]
{Z : C} (h : Y ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject f).arrow
(CategoryTheory.CategoryStruct.comp f h) =
CategoryTheory.CategoryStruct.comp 0 h
This theorem states that in a category `C` with zero morphisms, given morphisms `f : X ⟶ Y` and `h : Y ⟶ Z` where `f` has a kernel, the composition of the arrow from the kernel subobject of `f` to `f`, followed by the composition of `f` and `h`, is equal to the composition of the zero morphism and `h`. This is a statement about the behavior of kernel subobjects in a category.
More concisely: In a category with zero morphisms, given a morphism `f` with kernel `k` and another morphism `h`, the composition of `k` with `f` and `h` is equal to the composition of the zero morphism and `h`.
|
CategoryTheory.Limits.imageSubobject_arrow'
theorem CategoryTheory.Limits.imageSubobject_arrow' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
[inst_1 : CategoryTheory.Limits.HasImage f],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).inv
(CategoryTheory.Limits.imageSubobject f).arrow =
CategoryTheory.Limits.image.ι f
The theorem `CategoryTheory.Limits.imageSubobject_arrow'` states that for any category `C` and morphism `f` from `X` to `Y`, if `f` has an image, then the composition of the inverse of the isomorphism between the image subobject of `f` and the image of `f`, and the arrow from the image subobject of `f` to `Y`, is equivalent to the inclusion of the image of `f` into `Y`. In other words, we have this equality of morphisms: `(imageSubobjectIso f).inv ≫ Subobject.arrow (imageSubobject f) = image.ι f` where `≫` signifies the composition of morphisms.
More concisely: For any morphism `f` in a category `C` with an image subobject, the composition of the inverse of the isomorphism between the image subobject and the image of `f`, and the inclusion of the image of `f` into `Y`, is equal to the morphism `image.ι f`.
|
CategoryTheory.Limits.le_kernelSubobject
theorem CategoryTheory.Limits.le_kernelSubobject :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f]
(A : CategoryTheory.Subobject X),
CategoryTheory.CategoryStruct.comp A.arrow f = 0 → A ≤ CategoryTheory.Limits.kernelSubobject f
In the context of category theory, this theorem states that for any category `C` with zero morphisms, given a morphism `f` from object `X` to `Y` that has a kernel, and a subobject `A` of `X`, if the composition of the arrow of `A` and `f` is a zero morphism, then `A` is less than or equal to the kernel subobject of `f`. Here, "less than or equal to" is meant in the sense of the ordering of subobjects.
More concisely: If `C` is a category with zero morphisms, given a morphism `f` from object `X` to `Y` with kernel `k`, and a subobject `A` of `X` such that `A ∘ f = 0`, then `A ≤ k`.
|
CategoryTheory.Limits.imageSubobject_arrow_comp
theorem CategoryTheory.Limits.imageSubobject_arrow_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
[inst_1 : CategoryTheory.Limits.HasImage f],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImageSubobject f)
(CategoryTheory.Limits.imageSubobject f).arrow =
f
This theorem states that in any category `C`, for any objects `X` and `Y`, and any morphism `f` from `X` to `Y` that has an image, the composition of the factorisation of `f` through the image subobject of `f` and the arrow from the underlying object of the image subobject of `f` to the ambient object is equal to `f`. Thus, it captures the property that the image subobject of a morphism in category theory is a canonical factorization of that morphism.
More concisely: In any category, for any morphism with an image, the factorization through the image subobject and the arrow from the image to the ambient object equals the morphism itself.
|
CategoryTheory.Limits.imageSubobject_comp_le
theorem CategoryTheory.Limits.imageSubobject_comp_le :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y X' : C} (h : X' ⟶ X) (f : X ⟶ Y)
[inst_1 : CategoryTheory.Limits.HasImage f]
[inst_2 : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp h f)],
CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f) ≤
CategoryTheory.Limits.imageSubobject f
This theorem states that within a category `C`, for any objects `X`, `Y`, and `X'`, and morphisms `h` from `X'` to `X` and `f` from `X` to `Y`, if the morphism `f` has an image and the composition of `h` and `f` (`h ≫ f`) also has an image, then the image of the composition (`h ≫ f`) is always a subobject of, or equal to, the image of `f`. This implies that the image of `f` contains all the information about the image of the composition `h ≫ f`.
More concisely: If `h: X' -> X` and `f: X -> Y` are morphisms in a category `C` with images, then the image of `h ≫ f` is a subobject of, or equal to, the image of `f`.
|
CategoryTheory.Limits.kernelSubobject_arrow
theorem CategoryTheory.Limits.kernelSubobject_arrow :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).hom
(CategoryTheory.Limits.kernel.ι f) =
(CategoryTheory.Limits.kernelSubobject f).arrow
The theorem `CategoryTheory.Limits.kernelSubobject_arrow` states that for any category `C` with zero morphisms, given a morphism `f` from object `X` to object `Y` in `C` that has a kernel, the composition of the isomorphism from the kernel subobject of `f` to `f` and the kernel inclusion morphism `f` is equal to the morphism from the kernel subobject of `f` to `X`. In mathematical terms, given a morphism `f : X ⟶ Y`, it asserts that `(kernelSubobjectIso f).hom ≫ kernel.ι f = Subobject.arrow (kernelSubobject f)`.
More concisely: Given a morphism `f : X ➝ Y` in a category with zero morphisms and a kernel `kernel f : Subobject (Set X)`, the composition of the kernel isomorphism `kernelSubobjectIso f` with the kernel inclusion morphism `kernel.ι f` equals the subobject arrow of the kernel `Subobject.arrow (kernelSubobject f)`.
|
CategoryTheory.Limits.imageSubobject_arrow
theorem CategoryTheory.Limits.imageSubobject_arrow :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
[inst_1 : CategoryTheory.Limits.HasImage f],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).hom
(CategoryTheory.Limits.image.ι f) =
(CategoryTheory.Limits.imageSubobject f).arrow
This theorem states that, in any category `C` where we have a morphism `f` from `X` to `Y` and the image of `f` exists, the composition of the homomorphism associated with the isomorphism between the underlying object of the image subobject of `f` and the image of `f`, and the inclusion of the image of `f` into `Y`, is equal to the morphism from the arbitrarily chosen underlying object of the image subobject of `f` to `Y`. In other words, this theorem is asserting the commutativity of a certain diagram in the category `C`, providing a relationship between the concepts of image subobject, image, and the arrow of a subobject.
More concisely: In any category with subobjects, the composition of the homomorphism from the image subobject of a morphism to its image, and the inclusion of the image into the codomain, is equal to the morphism from the image subobject to the codomain.
|
CategoryTheory.Limits.imageSubobjectMap_arrow
theorem CategoryTheory.Limits.imageSubobjectMap_arrow :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X}
[inst_1 : CategoryTheory.Limits.HasImage f] {g : Y ⟶ Z} [inst_2 : CategoryTheory.Limits.HasImage g]
(sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) [inst_3 : CategoryTheory.Limits.HasImageMap sq],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectMap sq)
(CategoryTheory.Limits.imageSubobject g).arrow =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow sq.right
The theorem `CategoryTheory.Limits.imageSubobjectMap_arrow` states that, in any category `C` with morphisms `f: W ⟶ X` and `g: Y ⟶ Z` that have images, and a commutative square `sq` from the arrow of `f` to the arrow of `g`, the composition of the imageSubobjectMap of `sq` with the arrow of the image subobject of `g` is equal to the composition of the arrow of the image subobject of `f` with the right object of `sq`. This theorem is a fundamental result in category theory pertaining to the interaction between morphisms, their images, and subobjects, and it illustrates the alignment of structures preserved under the processes of image formation and morphism composition.
More concisely: In any category with commutative squares and morphisms with images, the image of the subobject of the composite morphism under the left morphism is equal to the composition of the image of the subobject of the left morphism and the right object of the square.
|
CategoryTheory.Limits.kernelSubobject_arrow'
theorem CategoryTheory.Limits.kernelSubobject_arrow' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).inv
(CategoryTheory.Limits.kernelSubobject f).arrow =
CategoryTheory.Limits.kernel.ι f
The theorem `CategoryTheory.Limits.kernelSubobject_arrow'` states that in any category `C` with zero-morphisms, given a morphism `f` from `X` to `Y` which has a kernel, the composition of the inverse of the isomorphism from the kernel of `f` to a subobject of `X` with the morphism from this subobject to `X` equals the morphism from the kernel of `f` to `X`.
In other words, it expresses a property of the kernel of a morphism in category theory: that it can be identified with a subobject such that a particular composed map is equivalent to the map from the kernel to the source of the original morphism. This is a common way of viewing the kernel in terms of subobjects in category theory.
More concisely: Given a morphism with a kernel in a category with zero-morphisms, the subobject isomorphism from the kernel to a subobject of the domain makes the following diagram commute:
```
Kernel(f) ───────≃─────── Subobject of X
│ │
│ ↓
│ maps to
│
↓
X
─────── f ─────── Y
```
|
CategoryTheory.Limits.kernelSubobject_comp_le
theorem CategoryTheory.Limits.kernelSubobject_comp_le :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f]
{Z : C} (h : Y ⟶ Z) [inst_3 : CategoryTheory.Limits.HasKernel (CategoryTheory.CategoryStruct.comp f h)],
CategoryTheory.Limits.kernelSubobject f ≤
CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f h)
This theorem states that in any category `C` equipped with zero morphisms, for any morphisms `f : X ⟶ Y` and `h : Y ⟶ Z` such that `f` and `f ≫ h` both have kernels, the kernel subobject of `f` is always a subobject of (or equal to) the kernel subobject of the composition `f ≫ h`. In other words, the kernel of `f` is always contained in the kernel of `f ≫ h`.
More concisely: In any category with zero morphisms, if morphisms `f` from `X` to `Y` and `h` from `Y` to `Z` have kernels and `f` is a subobject of `f ≫ h`, then the kernel of `f` is contained in the kernel of `f ≫ h`.
|
CategoryTheory.Limits.kernelSubobject_comp_mono
theorem CategoryTheory.Limits.kernelSubobject_comp_mono :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f]
{Z : C} (h : Y ⟶ Z) [inst_3 : CategoryTheory.Mono h],
CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp f h) =
CategoryTheory.Limits.kernelSubobject f
The theorem `CategoryTheory.Limits.kernelSubobject_comp_mono` states that in any category `C` that has zero morphisms, for any morphisms `f` from `X` to `Y`, and `h` from `Y` to `Z`, where `f` has a kernel and `h` is a monomorphism, the kernel subobject of the composition of `f` and `h` (denoted `f ≫ h`) is the same as the kernel subobject of `f`. In other words, post-composing by a monomorphism doesn't change the kernel subobject.
More concisely: In a zero-object category with kernel subobjects, the kernel of a composition of a morphism with a monomorphism is equal to the kernel of the morphism.
|
CategoryTheory.Limits.kernelSubobject_factors
theorem CategoryTheory.Limits.kernelSubobject_factors :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f]
{W : C} (h : W ⟶ X),
CategoryTheory.CategoryStruct.comp h f = 0 → (CategoryTheory.Limits.kernelSubobject f).Factors h
The theorem `CategoryTheory.Limits.kernelSubobject_factors` states that in any category `C` with zero morphisms, given a morphism `f` from object `X` to `Y` that has a kernel, and another morphism `h` from an object `W` to `X`, if the composition of `h` and `f` (i.e., `h ≫ f`) is a zero morphism (essentially meaning that the morphism `h` maps into the kernel of `f`), then `h` factors through the kernel subobject of `f`. In other words, there exists a factorisation of `h` through the kernel of `f`. This is a general property in category theory that encapsulates one of the defining properties of the kernel of a morphism.
More concisely: In a category with zero morphisms, if a morphism has a kernel and another morphism into the domain of the first one makes their composition a zero morphism, then the second morphism factors through the kernel of the first one.
|
CategoryTheory.Limits.imageSubobject_zero_arrow
theorem CategoryTheory.Limits.imageSubobject_zero_arrow :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.Limits.HasZeroObject C],
(CategoryTheory.Limits.imageSubobject 0).arrow = 0
The theorem `CategoryTheory.Limits.imageSubobject_zero_arrow` states that in any category `C` with zero morphisms and zero object, the morphism from the underlying object of the image subobject of the zero morphism to the ambient object `Y` is the zero morphism. This theorem illustrates the fact that the image of the zero morphism in a category with zero morphisms and a zero object is essentially trivial.
More concisely: In a category with zero morphisms and a zero object, the image of the zero morphism under any object's subobject is the zero morphism.
|