CategoryTheory.BundledHom.hom_ext
theorem CategoryTheory.BundledHom.hom_ext :
∀ {c : Type u → Type u} {hom : ⦃α β : Type u⦄ → c α → c β → Type u} (self : CategoryTheory.BundledHom hom)
{α β : Type u} (Iα : c α) (Iβ : c β), Function.Injective (self.toFun Iα Iβ)
The theorem `CategoryTheory.BundledHom.hom_ext` states that for any category `c` with objects of type `Type u` and morphisms `hom` between these objects, given an instance of the category `self` and objects `Iα` and `Iβ` of this category, the function `toFun` mapping from `Iα` to `Iβ` is injective. In other words, if we have two objects in a category and a function acting on these objects, then this function is such that if it maps two distinct objects to the same object, then those initial objects must have been the same - meaning the function does not 'collapse' distinct objects into the same one.
More concisely: In any category, the morphism induced by a map between objects is an injection.
|
CategoryTheory.BundledHom.comp_toFun
theorem CategoryTheory.BundledHom.comp_toFun :
∀ {c : Type u → Type u} {hom : ⦃α β : Type u⦄ → c α → c β → Type u} (self : CategoryTheory.BundledHom hom)
{α β γ : Type u} (Iα : c α) (Iβ : c β) (Iγ : c γ) (f : hom Iα Iβ) (g : hom Iβ Iγ),
self.toFun Iα Iγ (self.comp Iα Iβ Iγ g f) = self.toFun Iβ Iγ g ∘ self.toFun Iα Iβ f
This theorem states that in the context of category theory, the composition of two morphisms (which are mappings between objects in a category) is compatible with the function "toFun". In more detail, given a bundled homomorphism "self" and three objects α, β, and γ in a certain category c, along with two morphisms f (from α to β) and g (from β to γ), the result of applying "toFun" to the composition of g and f (in that order) is the same as composing the results of applying "toFun" to g and f separately.
More concisely: In category theory, for objects α, β, γ and morphisms f: α → β and g: β → γ in a given category, the application of the "toFun" function to the composition g ∘ f is equal to the composition of the applications of "toFun" to g and f. In other words, toFun (g ∘ f) = toFun (g) ∘ toFun (f).
|
CategoryTheory.BundledHom.id_toFun
theorem CategoryTheory.BundledHom.id_toFun :
∀ {c : Type u → Type u} {hom : ⦃α β : Type u⦄ → c α → c β → Type u} (self : CategoryTheory.BundledHom hom)
{α : Type u} (I : c α), self.toFun I I (self.id I) = id
This theorem, `CategoryTheory.BundledHom.id_toFun`, states that for any category of types `c` and morphisms `hom`, and any object `I` of the category, applying the `toFun` function of a `BundledHom` instance to the identity morphism of `I` is equal to the identity function. In other words, it asserts the compatibility of the functor represented by a `BundledHom` instance with identity morphisms in the category, one of the basic requirements for a category in category theory.
More concisely: For any category `c` and `BundledHom` instance over it, the application of `toFun` to the identity morphism of an object `I` is equal to the identity function on `I`.
|