CategoryTheory.ConcreteCategory.mono_of_injective
theorem CategoryTheory.ConcreteCategory.mono_of_injective :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.ConcreteCategory C] {X Y : C}
(f : X ⟶ Y), Function.Injective ⇑f → CategoryTheory.Mono f
In the context of category theory, this theorem states that for any concrete category `C`, if there is an injective morphism `f` from object `X` to object `Y`, then `f` is a monomorphism. In essence, if a function `f` (viewed as a morphism in the category) has the property that equal outputs imply equal inputs (i.e., it's injective), then `f` is a monomorphism, which in category theory means that it "preserves" the operation of "pre-composition".
More concisely: In category theory, if `f` is an injective morphism in a concrete category `C` from object `X` to object `Y`, then `f` is a monomorphism.
|
CategoryTheory.ConcreteCategory.forget_faithful
theorem CategoryTheory.ConcreteCategory.forget_faithful :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.ConcreteCategory C],
CategoryTheory.ConcreteCategory.forget.Faithful
This theorem states that for any type 'C' which is a category and a concrete category, the functor that forgets the category structure and treats 'C' just as a type is faithful. In category theory, a functor is said to be faithful if the mapping it induces between hom-sets (sets of morphisms between objects) is one-to-one, i.e., it never maps distinct morphisms to the same morphism. Here, the 'forget' functor is always faithful, meaning it preserves the distinctness of morphisms when we forget about the category structure.
More concisely: For any type 'C' that is both a category and a concrete category, the forgetful functor from 'C' to Set is faithful.
|
CategoryTheory.comp_apply
theorem CategoryTheory.comp_apply :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.ConcreteCategory C] {X Y Z : C}
(f : X ⟶ Y) (g : Y ⟶ Z) (x : (CategoryTheory.forget C).obj X),
(CategoryTheory.CategoryStruct.comp f g) x = g (f x)
This theorem, "CategoryTheory.comp_apply", states that for any category `C` that is also a concrete category, and for objects `X`, `Y`, and `Z` of this category, if we have morphisms `f` from `X` to `Y` and `g` from `Y` to `Z`, and an object `x` in the image of `X` under the forgetful functor from `C` to `Type w`, then applying the composition of `f` and `g` to `x` is the same as first applying `f` to `x` and then applying `g` to the result. In other words, the composition operation in the category matches function composition in the underlying type.
More concisely: For any concrete category $C$, given objects $X$, $Y$, $Z$, morphisms $f : X \to Y$ and $g : Y \to Z$, and an object $x : X$ in the image of $X$ under the forgetful functor, we have $g \circ f(x) = g(f(x))$.
|
CategoryTheory.ConcreteCategory.epi_of_surjective
theorem CategoryTheory.ConcreteCategory.epi_of_surjective :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.ConcreteCategory C] {X Y : C}
(f : X ⟶ Y), Function.Surjective ⇑f → CategoryTheory.Epi f
In the context of any concrete category, the theorem states that if a morphism `f` from object `X` to object `Y` is surjective, then this morphism is an epimorphism. Here, surjective implies that for every element in the codomain `Y`, there exists at least one element in the domain `X` such that the function `f` maps this element from `X` to that particular element in `Y`. An epimorphism, in category theory, is a morphism which has the property that any two morphisms from its codomain to any other object that are equal after composition with the epimorphism are already equal.
More concisely: In any concrete category, a surjective morphism is an epimorphism.
|
CategoryTheory.forget_map_eq_coe
theorem CategoryTheory.forget_map_eq_coe :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.ConcreteCategory C] {X Y : C}
(f : X ⟶ Y), (CategoryTheory.forget C).map f = ⇑f
This theorem states that for any categories `C` and `C'` of type `u`, with `C` being a concrete category, and for any objects `X` and `Y` in `C`, the action of the forgetful functor `CategoryTheory.forget C` on a morphism `f : X ⟶ Y` in `C` is just the same as the action of the morphism `f` itself. In other words, the forgetful functor essentially "forgets" the categorical structure and treats the morphism purely as a function.
More concisely: For any concrete category `C`, the forgetful functor from `C` to Set preserves morphisms, i.e., for any objects `X` and `Y` in `C` and a morphism `f : X ⟶ Y` in `C`, we have `CategoryTheory.forget C f = f : X → Y`.
|
CategoryTheory.congr_hom
theorem CategoryTheory.congr_hom :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.ConcreteCategory C] {X Y : C}
{f g : X ⟶ Y}, f = g → ∀ (x : (CategoryTheory.forget C).obj X), f x = g x
This theorem, `CategoryTheory.congr_hom`, is an analogue of the function congruence principle `congr_fun h x`, when `h : f = g` is an equality between morphisms in a concrete category. Given a category `C` with category structure `inst` and concrete category structure `inst_1`, along with objects `X`, `Y` of `C` and morphisms `f, g : X ⟶ Y`, if `f` is equal to `g`, then for any `x` in the underlying type of `X` (obtained by applying the forgetful functor to `X`), the result of applying `f` and `g` to `x` are equal. In more familiar terms, if two morphisms are equal in the category, they are also equal as functions on the underlying types.
More concisely: If `f` and `g` are equal morphisms in a category `C`, then for all objects `X` and `x` in `X`, `f x = g x`.
|
CategoryTheory.HasForget₂.forget_comp
theorem CategoryTheory.HasForget₂.forget_comp :
∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.ConcreteCategory C]
[inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.ConcreteCategory D]
[self : CategoryTheory.HasForget₂ C D],
CategoryTheory.HasForget₂.forget₂.comp (CategoryTheory.forget D) = CategoryTheory.forget C
The theorem named `CategoryTheory.HasForget₂.forget_comp` states that for any two types `C` and `D`, where `C` and `D` are both categories and concrete categories, and if there exists a functor (given by `CategoryTheory.HasForget₂`) from `C` to `D`, then the composition of the forgetful functor from `C` to `D` and the forgetful functor from `D` to `Type` is the same as the forgetful functor from `C` to `Type`.
In simpler terms, this theorem encapsulates the property that forgetting the structure in two steps (from a category `C` to `D` and then from `D` to `Type`) is the same as forgetting the structure in one step (directly from `C` to `Type`).
More concisely: For any concrete categories C and D with a forgetful functor from C to D, the composition of the forgetful functors from C to D and from D to Type equals the forgetful functor from C to Type.
|
CategoryTheory.id_apply
theorem CategoryTheory.id_apply :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.ConcreteCategory C] {X : C}
(x : (CategoryTheory.forget C).obj X), (CategoryTheory.CategoryStruct.id X) x = x
This theorem states that for any category `C` which is also a concrete category, and for any object `X` in `C`, the identity morphism applied to an object `x` (which is an object of the "forgotten" version of `X` in the category `C`) results in the same object `x`. In simpler terms, if we "forget" about the category structure of an object by using the forgetful functor and then apply the identity function, we get the original object back. This is an embodiment of the identity law in category theory, which states that the identity morphism for an object leaves the object unchanged.
More concisely: In any concrete category, the identity morphism of an object, when applied using the forgetful functor, equals the identity of that object.
|
CategoryTheory.ConcreteCategory.congr_hom
theorem CategoryTheory.ConcreteCategory.congr_hom :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.ConcreteCategory C] {X Y : C}
{f g : X ⟶ Y}, f = g → ∀ (x : (CategoryTheory.forget C).obj X), f x = g x
This theorem states that for any category `C`, which is also a concrete category, and any two objects `X` and `Y` in this category, if we have two morphisms `f` and `g` from `X` to `Y` that are equal, then for any element `x` of `X` considered as an object in the category of types (i.e., `x` is an element of the underlying set of `X` under `CategoryTheory.forget C`), the application of `f` to `x` is equal to the application of `g` to `x`. In other words, the equality of two morphisms in a concrete category is witnessed by their equality on each element of the domain.
More concisely: In a concrete category `C`, the equality of morphisms `f` and `g` from object `X` to object `Y` implies `f x = g x` for all elements `x` of `X` viewed as objects in the underlying category of types.
|
CategoryTheory.coe_comp
theorem CategoryTheory.coe_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.ConcreteCategory C] {X Y Z : C}
(f : X ⟶ Y) (g : Y ⟶ Z), ⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑g ∘ ⇑f
This theorem, `CategoryTheory.coe_comp`, states that in any category `C` that is also a concrete category, for any three objects `X`, `Y`, and `Z` in `C`, and any two morphisms `f` from `X` to `Y` and `g` from `Y` to `Z`, the action of the composition of `f` and `g` (denoted as `CategoryTheory.CategoryStruct.comp f g`) on any element is the same as first applying `f` and then `g`. This is the categorical analogue of the statement that function composition in set theory is associative, i.e., `(g ∘ f)(x) = g(f(x))` for all `x` in the domain of `f`.
More concisely: In any concrete category, the composition of morphisms is associative with respect to the underlying functions, i.e., `f ∘ g(x) = g(f(x))` for all objects `x` in the domain of `f`.
|
CategoryTheory.ConcreteCategory.hom_ext
theorem CategoryTheory.ConcreteCategory.hom_ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.ConcreteCategory C] {X Y : C}
(f g : X ⟶ Y), (∀ (x : (CategoryTheory.forget C).obj X), f x = g x) → f = g
This theorem states that in any concrete category, we can compare the equality of morphisms by evaluating them pointwise. Specifically, given a concrete category `C` and two morphisms `f` and `g` from object `X` to object `Y` in `C`, if for every element `x` in the underlying set of `X`, the application of `f` and `g` to `x` yields the same result, then the morphisms `f` and `g` are equal in `C`. In essence, this is a formal way of saying that if two functions behave the same way on all inputs, they are indeed the same function.
More concisely: In a concrete category, two morphisms from an object to another are equal if and only if they map every object element to the same image.
|