CategoryTheory.Limits.MonoFactorisation.ext
theorem CategoryTheory.Limits.MonoFactorisation.ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
{F F' : CategoryTheory.Limits.MonoFactorisation f} (hI : F.I = F'.I),
F.m = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hI) F'.m → F = F'
This theorem states that in the context of a category `C` and for any morphisms `f : X ⟶ Y` in the category, if `F` and `F'` are two monofactorisations of `f` such that `F.I = F'.I`, then the morphism `m` in the factorisation `f = e ≫ m` is uniquely determined by `F.m = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hI) F'.m`, and thus `F` is equal to `F'`. A monofactorisation in category theory is a factorisation through a monomorphism, which is an injective morphism.
More concisely: In a category, given two monofactorizations `F` and `F'` of a morphism `f` with equal initial objects, their morphisms `m` are equal, implying `F` and `F'` are equal.
|
CategoryTheory.Limits.image.fac_assoc
theorem CategoryTheory.Limits.image.fac_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
[inst_1 : CategoryTheory.Limits.HasImage f] {Z : C} (h : Y ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h) =
CategoryTheory.CategoryStruct.comp f h
The theorem `CategoryTheory.Limits.image.fac_assoc` states that in any category `C` with objects `X`, `Y`, and `Z`, given a morphism `f` from `X` to `Y`, and assuming that `f` has an image, for any morphism `h` from `Y` to `Z`, the composition of the morphism `f` with `h` is equal to the composition of the factor through image of `f`, the inclusion of the image of `f` into `Y`, and `h`. In other words, this theorem states the associativity of composition in terms of images in a category, capturing a fundamental characteristic of image factorization in category theory.
More concisely: In any category, given morphisms $f: X \to Y$ with image $I$, and $h: Y \to Z$, the compositions $h \circ f$ and $h \circ \operatorname{im} f \circ i$ are equal, where $\operatorname{im} f$ is the image of $f$ and $i: \operatorname{im} f \to Y$ is the inclusion.
|
CategoryTheory.Limits.StrongEpiMonoFactorisation.e_strong_epi
theorem CategoryTheory.Limits.StrongEpiMonoFactorisation.e_strong_epi :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
(self : CategoryTheory.Limits.StrongEpiMonoFactorisation f), CategoryTheory.StrongEpi self.e
The theorem `CategoryTheory.Limits.StrongEpiMonoFactorisation.e_strong_epi` states that in any category `C`, for any objects `X` and `Y` in `C`, and any morphism `f` from `X` to `Y`, if there exists a strong epi-mono factorisation of `f` (i.e., a decomposition `f = e ≫ m` where `e` is a strong epimorphism and `m` is a monomorphism), then `e` is indeed a strong epimorphism. This theorem is a fundamental property that confirms the validity of the strong epi-mono factorisation structure in category theory.
More concisely: In any category, if a morphism has a strong epi-mono factorisation, then the strong epimorphism in the factorisation is indeed a strong epimorphism.
|
CategoryTheory.Limits.HasImageMap.mk
theorem CategoryTheory.Limits.HasImageMap.mk :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
[inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g},
CategoryTheory.Limits.ImageMap sq → CategoryTheory.Limits.HasImageMap sq
This theorem states that for any category `C`, given two objects `f` and `g` in the arrow category of `C` (which means `f` and `g` are morphisms in `C`), and a morphism `sq` from `f` to `g` (which translates to a commutative square in `C`), if the image of homomorphisms of both `f` and `g` exist and there's an image mapping for `sq`, then the image mapping for `sq` exists. This is a concept in category theory, where the image of a morphism is a sort of "minimal" subobject through which the morphism factors, while an image map captures the idea of morphing one image to another.
More concisely: Given any commutative square in a category with existing image homomorphisms for the morphisms involved, the image mapping for the morphism between the objects exists.
|
CategoryTheory.Limits.image.ext
theorem CategoryTheory.Limits.image.ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
[inst_1 : CategoryTheory.Limits.HasImage f] {W : C} {g h : CategoryTheory.Limits.image f ⟶ W}
[inst_2 : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair g h)],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f) g =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f) h →
g = h
This theorem, `CategoryTheory.Limits.image.ext`, states that in any category `C` with given objects `X`, `Y`, and `W`, and a morphism `f` from `X` to `Y` that has an image, if there exist two morphisms `g` and `h` from the image of `f` to `W`, and if a limit exists for the parallel pair `g` and `h`, then if the composition of the factor through image of `f` with `g` equals the composition of the factor through image of `f` with `h`, it must be the case that `g` equals `h`. Essentially, this theorem asserts the uniqueness of morphisms from the image of `f` under certain conditions.
More concisely: If in a category with an object `X`, morphisms `f: X -> Y`, `g, h: Im(f) -> W`, and a limit for the parallel pair `g` and `h`, then equal composition with `f` implies `g = h`.
|
CategoryTheory.Limits.image.preComp_ι
theorem CategoryTheory.Limits.image.preComp_ι :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z)
[inst_1 : CategoryTheory.Limits.HasImage g]
[inst_2 : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.preComp f g) (CategoryTheory.Limits.image.ι g) =
CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g)
The theorem `CategoryTheory.Limits.image.preComp_ι` states that in any category `C`, for any objects `X, Y, Z` in `C` and morphisms `f : X ⟶ Y` and `g : Y ⟶ Z`, if `g` and the composition `f ≫ g` have images, then the composition of the pre-image morphism of `f` and `g` with the inclusion of the image of `g` into `Z` is equal to the inclusion of the image of the composition `f ≫ g` into `Z`. In more mathematical terms, it says that in the context of category theory, image inclusion respects the composition of morphisms.
More concisely: In any category, given morphisms $f : X \to Y$, $g : Y \to Z$, and objects $I_g$ and $I_{g \circ f}$ denoting the images of $g$ and $g \circ f$ respectively, we have $I_g \circ \text{pre-img}(f) = I_{g \circ f}$.
|
CategoryTheory.Limits.MonoFactorisation.fac
theorem CategoryTheory.Limits.MonoFactorisation.fac :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
(self : CategoryTheory.Limits.MonoFactorisation f), CategoryTheory.CategoryStruct.comp self.e self.m = f
This theorem states that for any category `C`, and any objects `X` and `Y` in `C`, if we have a morphism `f` from `X` to `Y` and a monic factorization of `f`, then the composition of the two morphisms in the factorization (`self.e` and `self.m`) equals `f`. In the context of category theory, a monic factorization is a decomposition of a morphism into a sequence where the second morphism is monic, meaning it has a certain kind of injectivity property.
More concisely: Given any category `C`, morphism `f` from object `X` to object `Y`, and monic factorization `m ∘ e = f` of `f`, then `m ∘ e = f`.
|
CategoryTheory.Limits.image.eq_fac
theorem CategoryTheory.Limits.image.eq_fac :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f f' : X ⟶ Y}
[inst_1 : CategoryTheory.Limits.HasImage f] [inst_2 : CategoryTheory.Limits.HasImage f']
[inst_3 : CategoryTheory.Limits.HasEqualizers C] (h : f = f'),
CategoryTheory.Limits.image.ι f =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.eqToIso h).hom
(CategoryTheory.Limits.image.ι f')
The theorem `CategoryTheory.Limits.image.eq_fac` states that, for a category that has equalizers, the inclusion maps of images (from the image of a morphism to the target) are compatible with isomorphisms between images induced by equality of morphisms. More specifically, for any two morphisms `f` and `f'` from `X` to `Y` in the category `C`, if `f = f'`, then the inclusion map of the image of `f` is equal to the composition of the isomorphism from the image of `f` to the image of `f'` and the inclusion map of the image of `f'`.
More concisely: For any equal morphisms `f` and `f'` in a category with equalizers, the inclusion maps of their images are equal, up to composition with the isomorphism from `image(f)` to `image(f')`.
|
CategoryTheory.Limits.image.fac
theorem CategoryTheory.Limits.image.fac :
∀ {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.factorThruImage f) (CategoryTheory.Limits.image.ι f) =
f
The theorem `CategoryTheory.Limits.image.fac` states that for any category `C` with objects `X` and `Y`, and a morphism `f` from `X` to `Y` (denoted `f : X ⟶ Y`) for which an image exists (formally, `[inst_1 : CategoryTheory.Limits.HasImage f]`), the composition of the morphism from `X` to the image of `f` (denoted `CategoryTheory.Limits.factorThruImage f`) followed by the inclusion of the image of `f` into `Y` (denoted `CategoryTheory.Limits.image.ι f`) is equal to the original morphism `f`. In other words, this theorem confirms the fundamental property of the image of a morphism in category theory that compositing the morphism to the image and the inclusion from the image gives back the original morphism.
More concisely: The theorem asserts that for any morphism `f : X ⟶ Y` in a category `C` with an image, the composition of `f` with the inclusion of the image of `f` is equal to the morphism to the image of `f`.
|
CategoryTheory.Limits.image.preComp_comp
theorem CategoryTheory.Limits.image.preComp_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) {W : C}
(h : Z ⟶ W) [inst_1 : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp g h)]
[inst_2 :
CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))]
[inst_3 : CategoryTheory.Limits.HasImage h]
[inst_4 :
CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)],
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.image.preComp f (CategoryTheory.CategoryStruct.comp g h))
(CategoryTheory.Limits.image.preComp g h) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.eqToHom ⋯)
(CategoryTheory.Limits.image.preComp (CategoryTheory.CategoryStruct.comp f g) h)
This theorem, `CategoryTheory.Limits.image.preComp_comp`, in the context of category theory, states that for any category `C`, and any objects `X`, `Y`, `Z`, `W` in `C`, given morphisms `f : X ⟶ Y`, `g : Y ⟶ Z`, and `h : Z ⟶ W` in `C`, and assuming the existence of images of the morphisms `(g ≫ h)`, `(f ≫ (g ≫ h))` and `((f ≫ g) ≫ h)`, the composition of the two-step comparison map `image (f ≫ (g ≫ h)) ⟶ image (g ≫ h) ⟶ image h` is equal to the composition of the one-step comparison map `image (f ≫ (g ≫ h)) ≅ image ((f ≫ g) ≫ h) ⟶ image h`. This essentially shows the associative property of the composition of morphisms and their images in category theory.
More concisely: Given any morphisms `f : X ⟶ Y`, `g : Y ⟶ Z`, and `h : Z ⟶ W` in a category `C` with the existence of their images, the comparison maps `image (f ≫ (g ≫ h)) ⟶ image (g ≫ h)` and `image (f ≫ (g ≫ h)) ≅ image ((f ≫ g) ≫ h)` are equal.
|
CategoryTheory.Limits.as_factorThruImage
theorem CategoryTheory.Limits.as_factorThruImage :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
[inst_1 : CategoryTheory.Limits.HasImage f],
(CategoryTheory.Limits.Image.monoFactorisation f).e = CategoryTheory.Limits.factorThruImage f
The theorem `CategoryTheory.Limits.as_factorThruImage` states that for any category `C`, and for any morphism `f` from `X` to `Y` in this category, given that `f` has an image, the morphism `e` obtained from some factorisation of `f` through a monomorphism is the same as the morphism obtained by passing `f` through the image. In other words, the morphism from the source to the image of `f` can be obtained by a specific type of factorisation of `f`. This result provides a way to rewrite or represent this morphism, connecting two different approaches or views on the image of a morphism in category theory.
More concisely: For any monic morphism $i : Z \to X$ and any morphism $f : X \to Y$ with image $g : \operatorname{im}(f) \to Y$, the factorization $f = h \circ i$ for some $h : Z \to Y$ implies that $\operatorname{im}(f) \cong \operatorname{im}(g)$, and the unique isomorphism is given by $h$.
|
CategoryTheory.Limits.image.fac_lift_assoc
theorem CategoryTheory.Limits.image.fac_lift_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
[inst_1 : CategoryTheory.Limits.HasImage f] (F' : CategoryTheory.Limits.MonoFactorisation f) {Z : C}
(h : F'.I ⟶ Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.lift F') h) =
CategoryTheory.CategoryStruct.comp F'.e h
This theorem states that in a category `C`, for any objects `X` and `Y` and a morphism `f : X ⟶ Y` with an existing image, given a monomorphism factorisation `F'` of `f`, and any morphism `h : F'.I ⟶ Z`, the composition of the morphism from `X` to the image of `f` with the composition of the lift of `F'` to the image of `f` and `h` is equal to the composition of `F'.e` and `h`. This principle is generally used in the context of category theory and abstract algebra, specifically while dealing with image factorisations and monomorphisms.
More concisely: In a category C, given morphisms f : X ⟶ Y with an image, F' a monomorphism factorization of f, and h : F'.I ⟶ Z, the compositions of f to the image of f, F'.e with h, and the lift of F' to the image of f with h are equal.
|
CategoryTheory.Limits.HasImage.mk
theorem CategoryTheory.Limits.HasImage.mk :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y},
CategoryTheory.Limits.ImageFactorisation f → CategoryTheory.Limits.HasImage f
This theorem states that for any category `C` with objects `X` and `Y`, and for any morphism `f` from `X` to `Y`, if there exists an image factorisation of `f`, then `f` has an image. The 'image' here refers to the category-theoretic concept of an image, which is a kind of optimal factorisation of a morphism.
More concisely: If a morphism in a category has an image factorization, then it has an image.
|
CategoryTheory.Limits.image.lift_fac
theorem CategoryTheory.Limits.image.lift_fac :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
[inst_1 : CategoryTheory.Limits.HasImage f] (F' : CategoryTheory.Limits.MonoFactorisation f),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.lift F') F'.m = CategoryTheory.Limits.image.ι f
The theorem `CategoryTheory.Limits.image.lift_fac` states that for any category `C`, and for any morphism `f` from `X` to `Y` in this category for which an image exists, given any monomorphism factorization `F'` of `f`, the composition of the lift (a special morphism) of the image of `f` through `F'` and the morphism `F'.m` is equal to the inclusion of the image of `f` into `Y`. In other words, this theorem specifies a commutative diagram related to the image and the monomorphism factorization in the category theory.
More concisely: Given a category `C`, a morphism `f : X → Y` with an image, and a monomorphism factorization `F' · m` of `f`, the diagram commutes: image `(f)` ≅ F'.m ∘ lift (image `(f)`) (F').
Alternatively, the lift of the image of `f` through `F'` equals the inclusion of the image of `f` into `Y`. In other words, `lift (image f) (F') = ⊆i (image f)`, where `⊆i` denotes the inclusion morphism.
|
CategoryTheory.Limits.image.map_ι
theorem CategoryTheory.Limits.image.map_ι :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
[inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g)
[inst_3 : CategoryTheory.Limits.HasImageMap sq],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.map sq) (CategoryTheory.Limits.image.ι g.hom) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) sq.right
This theorem states that in an arbitrary category `C`, given two morphisms, `f` and `g`, in the arrow category of `C` (meaning that they are given by pairs of objects and morphisms in `C`), if `f` and `g` both have images, and there is a morphism `sq` between `f` and `g` which also has an image, then the composition of the image map of `sq` and the inclusion of the image of `g` into its target is equal to the composition of the inclusion of the image of `f` into its target and the right part of `sq`. This can be written in mathematical terms as: `(ImageMap sq) ∘ (ImageInclusion g) = (ImageInclusion f) ∘ (sq.right)`.
More concisely: In an arbitrary category, if morphisms `f` and `g` have images and there is an image-preserving morphism `sq` between them, then the inclusion of `g`'s image into its target followed by the image map of `sq` is equal to the inclusion of `f`'s image into its target followed by `sq`'s right component.
|
CategoryTheory.Limits.IsImage.isoExt_inv_m
theorem CategoryTheory.Limits.IsImage.isoExt_inv_m :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
{F F' : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F)
(hF' : CategoryTheory.Limits.IsImage F'), CategoryTheory.CategoryStruct.comp (hF.isoExt hF').inv F.m = F'.m
The theorem `CategoryTheory.Limits.IsImage.isoExt_inv_m` states that for any category `C` and objects `X`, `Y` in `C` with a morphism `f` from `X` to `Y`, and given two monomorphisms `F` and `F'` of `f`, if `F` and `F'` satisfy the universal property of an image (i.e., `F` and `F'` are images), then the composition of the inverse of the isomorphism between `F.I` and `F'.I` (obtained by `CategoryTheory.Limits.IsImage.isoExt`) and the morphism `F.m` equals the morphism `F'.m`. In simpler terms, this theorem states a property about the particular composition of morphisms involving inverse isomorphisms in the context of images in category theory.
More concisely: For any category C, morphisms f : X -> Y, and monomorphisms F, F' of f in C such that F and F' are images, the composition of the inverse of the isomorphism between F.I and F'.I and F.m equals F'.m.
|
CategoryTheory.Limits.HasImages.has_image
theorem CategoryTheory.Limits.HasImages.has_image :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.Limits.HasImages C] {X Y : C}
(f : X ⟶ Y), CategoryTheory.Limits.HasImage f
The theorem `CategoryTheory.Limits.HasImages.has_image` states that for a category `C`, if `C` has the property of `HasImages`, then for any two objects `X` and `Y` in `C`, and any morphism `f` from `X` to `Y`, `f` has an image. In the context of category theory, having an image means there exists an object (the image) and a morphism from `X` to this image, such that any other morphism from `X` to an object `Z` factors through the image.
More concisely: For any category withImages, given objects X and Y and a morphism f from X to Y, there exists an object Z and a morphism g from X to Z such that for all morphisms h from X to any object W, there exists a unique morphism k from Z to W making the diagram commute: h = k ∘ g.
|
CategoryTheory.Limits.HasImage.exists_image
theorem CategoryTheory.Limits.HasImage.exists_image :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
[self : CategoryTheory.Limits.HasImage f], Nonempty (CategoryTheory.Limits.ImageFactorisation f)
The theorem `CategoryTheory.Limits.HasImage.exists_image` states that for any category `C`, and any objects `X` and `Y` in `C` with a morphism `f` from `X` to `Y`, if `f` has an image, then there exists an image factorisation of `f`. This is to say, if `f` can be factored into two morphisms such that the first morphism is epi and the second is mono, then such a factorisation exists. Image factorisations are a common concept in category theory, relating to the structure of morphisms within a category.
More concisely: If a morphism in a category has an image, then it has an image factorisation, i.e., there exist epi and mono morphisms making the given morphism the composite of an epimorphism and a monomorphism.
|
CategoryTheory.Limits.IsImage.fac_lift
theorem CategoryTheory.Limits.IsImage.fac_lift :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
{F : CategoryTheory.Limits.MonoFactorisation f} (hF : CategoryTheory.Limits.IsImage F)
(F' : CategoryTheory.Limits.MonoFactorisation f), CategoryTheory.CategoryStruct.comp F.e (hF.lift F') = F'.e
The theorem `CategoryTheory.Limits.IsImage.fac_lift` states that for any category `C`, any two objects `X` and `Y` in `C`, and any morphism `f` from `X` to `Y`, given a monic factorisation `F` of `f` that is an image, and another monic factorisation `F'` of `f`, the composition of the morphism `F.e` in `F` and the lift of `F'` under `hF` is equal to the morphism `F'.e` in `F'`. In essence, it verifies a key property of images in category theory, namely the existence of a unique morphism from the image to any other factorization of the same morphism.
More concisely: For any category `C`, given morphisms `f: X → Y`, monic factorizations `F: X → I ⊟ X` and `F': X → I' ⊟ Y` of `f` that are images, the lift of `F'` under `hF` followed by `F.e` equals `F'.e`.
|
CategoryTheory.Limits.MonoFactorisation.m_mono
theorem CategoryTheory.Limits.MonoFactorisation.m_mono :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
(self : CategoryTheory.Limits.MonoFactorisation f), CategoryTheory.Mono self.m
This theorem states that in the context of category theory, given a category `C` and morphism `f` from object `X` to `Y` in `C`, if `f` can be factorized as the composition of two morphisms `e` and `m` (i.e., `f = e ≫ m`), then `m` is monic (or a monomorphism, which is a generalization of the concept of an injective function in set theory). In other words, for any `MonoFactorisation` instance of `f`, the second morphism in the factorisation is always a monomorphism.
More concisely: Given a morphism `f` in a category `C` with a factorization `f = e ≫ m`, the morphism `m` is a monomorphism.
|
CategoryTheory.Limits.strongEpi_of_strongEpiMonoFactorisation
theorem CategoryTheory.Limits.strongEpi_of_strongEpiMonoFactorisation :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y},
CategoryTheory.Limits.StrongEpiMonoFactorisation f →
∀ {F' : CategoryTheory.Limits.MonoFactorisation f},
CategoryTheory.Limits.IsImage F' → CategoryTheory.StrongEpi F'.e
This theorem states that in any category `C`, if a morphism `f` from `X` to `Y` has a strong epi-mono factorization, then any image factorization of `f` is also a strong epi-mono factorization. Here, a morphism is a function from one object to another within the category, a factorization of a morphism is a representation of the morphism as a composition of two other morphisms, and a strong epi-mono factorization is a particular kind of factorization where the first morphism is a strong epimorphism and the second is a monomorphism. An image factorization is a factorization where the first morphism is an image of the original morphism.
More concisely: In any category, if a morphism has a strong epi-mono factorization, then any image factorization of it is also a strong epi-mono factorization.
|
CategoryTheory.Limits.IsImage.lift_fac
theorem CategoryTheory.Limits.IsImage.lift_fac :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
{F : CategoryTheory.Limits.MonoFactorisation f} (self : CategoryTheory.Limits.IsImage F)
(F' : CategoryTheory.Limits.MonoFactorisation f), CategoryTheory.CategoryStruct.comp (self.lift F') F'.m = F.m
The theorem `CategoryTheory.Limits.IsImage.lift_fac` states that for any category `C`, any two objects `X` and `Y` in `C`, and a morphism `f` from `X` to `Y`, if we have a monic factorization `F` of `f` and an image object `self` of `F`, then for any other monic factorization `F'` of `f`, the composition of the morphism obtained by lifting `self` along `F'` and the morphism `F'.m` equals the morphism `F.m`. In simpler terms, this theorem is about the uniqueness of factorizations through monomorphisms (injective morphisms) in a category, a fundamental concept in category theory.
More concisely: Given any category `C`, morphism `f` from object `X` to `Y`, monic factorizations `F` and `F'` of `f`, and image objects `self` of `F`, if `self` is also an image object of `F'`, then `F.m` is equal to `F'.m ∘ (self ↦ X)`, where `(self ↦ X)` is the morphism obtained by lifting `self` along `F'`.
|
CategoryTheory.Limits.HasStrongEpiMonoFactorisations.has_fac
theorem CategoryTheory.Limits.HasStrongEpiMonoFactorisations.has_fac :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
[self : CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] {X Y : C} (f : X ⟶ Y),
Nonempty (CategoryTheory.Limits.StrongEpiMonoFactorisation f)
This theorem states that for any category `C` that has strong epi-mono factorisations, and for any objects `X` and `Y` in `C`, every morphism `f` from `X` to `Y` admits a strong epi-mono factorisation. In other words, we can always find a factorisation of the morphism `f` into a strong epimorphism followed by a monomorphism.
More concisely: In any category with strong epimono factorizations, every morphism has a factorisation as a strong epimorphism followed by a monomorphism.
|
CategoryTheory.Limits.image.fac_lift
theorem CategoryTheory.Limits.image.fac_lift :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
[inst_1 : CategoryTheory.Limits.HasImage f] (F' : CategoryTheory.Limits.MonoFactorisation f),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f)
(CategoryTheory.Limits.image.lift F') =
F'.e
The theorem `CategoryTheory.Limits.image.fac_lift` states that in any category `C`, given objects `X` and `Y`, and a morphism `f` from `X` to `Y`, if `f` has an image, then for any monic factorization `F'` of `f`, the composition of the morphism from `X` to the image of `f` with the morphism from the image of `f` to the object of `F'` equals the morphism in `F'`. This essentially asserts the uniqueness part of the universal property of the image of a morphism in category theory.
More concisely: Given any category `C`, morphism `f` from object `X` to object `Y`, monic factorization `F'` of `f`, and if `f` has an image, then the composition of the morphism from the image of `f` to `X` with `f` is equal to the morphism from the image of `f` to the object in `F'`.
|
CategoryTheory.Limits.ImageMap.map_ι
theorem CategoryTheory.Limits.ImageMap.map_ι :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
[inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g}
(self : CategoryTheory.Limits.ImageMap sq),
CategoryTheory.CategoryStruct.comp self.map (CategoryTheory.Limits.image.ι g.hom) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f.hom) sq.right
The theorem `CategoryTheory.Limits.ImageMap.map_ι` states that for any category 'C', given two arrows 'f' and 'g' in 'C' (both having images), and a morphism 'sq' from 'f' to 'g', there exists a map from the image of 'f' to the image of 'g' such that it fits into a commutative square and satisfies commutativity conditions. Specifically, the composition of this map with the inclusion of the image of 'g' into 'g' is equal to the composition of the inclusion of the image of 'f' into 'f' and 'sq'. In mathematical terms, it means the diagram commutes: `self.map ∘ image.ι g = image.ι f ∘ sq.right`.
More concisely: Given any commutative square in a category with images, there exists a unique map making the rectangle commute from the image of the bottom arrow to the image of the right arrow, through the images and the given morphism.
|
CategoryTheory.Limits.HasImageMap.has_image_map
theorem CategoryTheory.Limits.HasImageMap.has_image_map :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
[inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] {sq : f ⟶ g}
[self : CategoryTheory.Limits.HasImageMap sq], Nonempty (CategoryTheory.Limits.ImageMap sq)
The theorem `CategoryTheory.Limits.HasImageMap.has_image_map` states that for any category `C`, and any two morphisms `f` and `g` in the arrow category of `C`, if `f` and `g` both have images and there is a morphism `sq` from `f` to `g` that has an image map, then there exists an `ImageMap` for the morphism `sq`. Here, an `ImageMap` is a specific type of morphism in category theory that describes a relationship between the images of two other morphisms.
More concisely: Given any category C and morphisms f, g with images, if there exists an arrow sq from f to g having an image map, then there exists an image map for sq.
|
CategoryTheory.Limits.MonoFactorisation.fac_assoc
theorem CategoryTheory.Limits.MonoFactorisation.fac_assoc :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
(self : CategoryTheory.Limits.MonoFactorisation f) {Z : C} (h : Y ⟶ Z),
CategoryTheory.CategoryStruct.comp self.e (CategoryTheory.CategoryStruct.comp self.m h) =
CategoryTheory.CategoryStruct.comp f h
This theorem states that in any category `C`, for any objects `X` and `Y`, and a morphism `f` from `X` to `Y`, if we have a monomorphism factorisation `self` of `f`, and a morphism `h` from `Y` to some other object `Z`, then composing the morphism `e` from the factorisation with the composition of the monomorphism `m` from the factorisation and `h`, is the same as composing `f` with `h`. In terms of category theory, this can be written as `e ∘ (m ∘ h) = f ∘ h`. This theorem essentially ensures that the factorisation respects the structure of the category.
More concisely: Given any category `C`, for any morphism `f: X → Y`, monomorphism factorization `m �circ e = 1��ource X ∘ f = 1��ource Y ∘ f ∘ h = m ∘ (h)`, where `m` and `e` are the monomorphism and epimorphism parts of the factorization respectively, and `h: Y → Z` is any morphism, the diagram commutes.
|
CategoryTheory.Limits.IsImage.lift_ι
theorem CategoryTheory.Limits.IsImage.lift_ι :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
[inst_1 : CategoryTheory.Limits.HasImage f] {F : CategoryTheory.Limits.MonoFactorisation f}
(hF : CategoryTheory.Limits.IsImage F),
CategoryTheory.CategoryStruct.comp (hF.lift (CategoryTheory.Limits.Image.monoFactorisation f))
(CategoryTheory.Limits.image.ι f) =
F.m
The theorem `CategoryTheory.Limits.IsImage.lift_ι` states that for any category `C` with objects `X` and `Y`, and a morphism `f` from `X` to `Y` that has an image, and for any monomorphism factorization `F` of `f` that satisfies the conditions of being an image, the composition of the lift of the standard monomorphism factorisation of `f` to `F` and the inclusion of the image of `f` into `Y` is equal to the morphism `m` of the monomorphism factorisation `F`.
In more intuitive terms, it's stating a property of the "lift" function in the context of category theory: If you have a morphism and a particular way to factor it through a monomorphism (i.e., a way to "split" it that preserves its properties), then "lifting" this factorisation and then going through the image of the original morphism gets you back to where you started.
More concisely: For any morphism `f` with image `I` in a category `C`, and any monomorphism factorization `F` of `f`, the diagram commutes: `lift F . inclusion I ∘ image f = F`.
|