CategoryTheory.mono_iff_injective
theorem CategoryTheory.mono_iff_injective :
∀ {X Y : Type u} (f : X ⟶ Y), CategoryTheory.Mono f ↔ Function.Injective f
The theorem `CategoryTheory.mono_iff_injective` states that for every morphism `f` from type `X` to type `Y`, `f` is a monomorphism in the category of types if and only if `f` is an injective function. This means that a morphism (a function between types) preserves the distinctness of elements from the domain (`X`) to the codomain (`Y`), i.e., if `f(a) = f(b)`, then `a` must equal `b`. The theorem links the concept of an injective function in set theory and a monomorphism in category theory.
More concisely: A morphism in a category is a monomorphism if and only if it is an injective function between sets.
|
CategoryTheory.FunctorToTypes.map_comp_apply
theorem CategoryTheory.FunctorToTypes.map_comp_apply :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X Y Z : C}
(f : X ⟶ Y) (g : Y ⟶ Z) (a : F.obj X), F.map (CategoryTheory.CategoryStruct.comp f g) a = F.map g (F.map f a)
The theorem `CategoryTheory.FunctorToTypes.map_comp_apply` states that for any category `C`, functor `F` from `C` to the category of types, and morphisms `f` and `g` in `C`, the action of the functor on the composition of `f` and `g` when applied to an object `a` of `F.obj X` is the same as first applying the functor to `f` and `g` separately on `a` and then composing the results. This is a version of the functoriality condition that applies specifically to the category of types.
More concisely: For any functor F from a category C to the category of types, and objects X, Y in C and morphisms f : X → Y and g : Y → Z in C, we have F(g ∘ f) a = F(g) (F(f) a) for all objects a of F X.
|
CategoryTheory.epi_iff_surjective
theorem CategoryTheory.epi_iff_surjective :
∀ {X Y : Type u} (f : X ⟶ Y), CategoryTheory.Epi f ↔ Function.Surjective f
This theorem establishes the equivalence between two properties for a morphism `f` between two types `X` and `Y`. Specifically, it states that `f` is an epimorphism in the category of types if and only if `f` is a surjective function. In other words, a function from `X` to `Y` is considered an epimorphism (i.e., every parallel pair of morphisms from `Y` to some object that `f` coequalizes is already coequalized by `f`) if and only if every element of `Y` is the image of some element of `X` under `f`. For a more detailed explanation, you can refer to the link provided in the comment above the theorem.
More concisely: A function between types `X` and `Y` in Lean 4 is an epimorphism if and only if it is surjective.
|
CategoryTheory.isIso_iff_bijective
theorem CategoryTheory.isIso_iff_bijective :
∀ {X Y : Type u} (f : X ⟶ Y), CategoryTheory.IsIso f ↔ Function.Bijective f
The theorem states that, for any two types 'X' and 'Y' in the same universe 'u', a morphism 'f' from 'X' to 'Y' is an isomorphism if and only if it is bijective. In other words, in the category of types, a morphism (which is simply a function in this context) is an isomorphism (an invertible morphism) exactly when it is a bijective function, i.e., a function that is both injective (no two different inputs have the same output) and surjective (every element in the codomain is an output for at least one input).
More concisely: A morphism between types is an isomorphism if and only if it is a bijective function.
|
CategoryTheory.types_comp_apply
theorem CategoryTheory.types_comp_apply :
∀ {X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X), CategoryTheory.CategoryStruct.comp f g x = g (f x)
The theorem `CategoryTheory.types_comp_apply` states that for any three types `X`, `Y`, and `Z` in the same universe `u`, and for any two functions `f` from `X` to `Y` and `g` from `Y` to `Z`, and for any object `x` of type `X`, the composition of `f` and `g`, when applied to `x`, is the same as first applying `f` to `x` and then applying `g` to the result. This is a formal statement of the fundamental concept of function composition in category theory.
More concisely: For any types X, Y, Z in the same universe u, and functions f : X -> Y and g : Y -> Z, the composition g o f is equal to the function g applied to the result of applying f. In other words, g (f(x)) = (g o f)(x) for all x in X.
|
CategoryTheory.Functor.sections_property
theorem CategoryTheory.Functor.sections_property :
∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w)} (s : ↑F.sections)
{j j' : J} (f : j ⟶ j'), F.map f (↑s j) = ↑s j'
This theorem states that for any category `J` and any functor `F` from `J` to the category of Types, if `s` is a section of the functor `F`, then for every morphism `f` from `j` to `j'` in `J`, the image of `f` under the functor `F`, applied to `s(j)`, equals `s(j')`. In simpler terms, this theorem establishes that the sections of a functor `F` have the property that they map morphisms in `J` to morphisms in the category of Types in a way that is consistent with the action of the functor `F`.
More concisely: Given a category J and a functor F from J to Types, if s is a section of F, then for all morphisms f from j to j' in J, F(f)(s(j)) = s(j').
|
CategoryTheory.FunctorToTypes.naturality
theorem CategoryTheory.FunctorToTypes.naturality :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) {X Y : C}
(σ : F ⟶ G) (f : X ⟶ Y) (x : F.obj X), σ.app Y (F.map f x) = G.map f (σ.app X x)
This theorem states the naturality condition for functors between categories and types in the context of category theory. More specifically, given any two functors `F` and `G` from a category `C` to the category of types, any natural transformation `σ` from `F` to `G`, any morphism `f` from object `X` to object `Y` in `C`, and any element `x` in the type `F.obj X`, applying `σ` at `Y` to the result of mapping `f` across `x` with `F` is equal to the result of mapping `f` across the result of applying `σ` at `X` to `x` with `G`. This captures the core principle of naturality in category theory, which asserts that the behavior of morphisms and transformations should be consistent across the entire category.
More concisely: Given any functors F and G from a category C to types, any natural transformation σ from F to G, and any morphism f in C and object x in F.X, we have F.map (σ\_Y (F.map f x)) = G.map f (σ\_X x).
|
CategoryTheory.FunctorToTypes.map_id_apply
theorem CategoryTheory.FunctorToTypes.map_id_apply :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X : C}
(a : F.obj X), F.map (CategoryTheory.CategoryStruct.id X) a = a
This theorem is stating that for any category `C`, and any functor `F` from that category into the category of types, for any object `X` in the category `C` and any object `a` in the image of `X` under the functor `F`, the image of `a` under the mapping induced by the identity morphism on `X` is equal to `a` itself. In other words, it states that the functor `F` preserves the identity morphisms of the category `C`, a key property of functors in category theory.
More concisely: For any functor F from a category C to Type, and for any object X in C and its image a under F, the image of the identity morphism on X maps a to itself. (Alternatively: Identity morphisms are preserved under functor F.)
|
CategoryTheory.types_ext
theorem CategoryTheory.types_ext : ∀ {α β : Type u} (f g : α ⟶ β), (∀ (a : α), f a = g a) → f = g
This theorem states that in the category of types, for any two types `α` and `β`, if two morphisms (functions) `f` and `g` from `α` to `β` produce the same result for every element of `α`, then `f` and `g` are the same function. In other words, two functions are identical if they map every element of the domain to the same element in the codomain.
More concisely: In the category of types and functions, two functions between types are equal if and only if they map every element of their domain to the same image in the codomain.
|