CategoryTheory.Endofunctor.Algebra.mono_of_mono
theorem CategoryTheory.Endofunctor.Algebra.mono_of_mono :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
{X Y : CategoryTheory.Endofunctor.Algebra F} (f : X ⟶ Y) [h : CategoryTheory.Mono f.f], CategoryTheory.Mono f
This theorem states that within a category `C`, if we have an algebra morphism `f` between two objects (or algebras) `X` and `Y` in the endofunctor of `C`, and `f.f` is a monomorphism (a morphism that is left-cancellable), then `f` itself is also a monomorphism. In other words, an algebra morphism that carries a monomorphism in the underlying category `C` is itself a monomorphism in the category of algebras.
More concisely: If `f : X --> Y` is an algebra morphism in a category `C` and `f.f` is a monomorphism, then `f` is a monomorphism.
|
CategoryTheory.Endofunctor.Coalgebra.Hom.ext
theorem CategoryTheory.Endofunctor.Coalgebra.Hom.ext :
∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C C}
{V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} (x y : V₀.Hom V₁), x.f = y.f → x = y
This theorem states that in a given category `C` with an endofunctor `F`, for any two coalgebras `V₀` and `V₁` of this functor, any two morphisms `x` and `y` from `V₀` to `V₁` are identical if their underlying functions `x.f` and `y.f` are identical. In other words, in the context of endofunctor coalgebras, the morphism between two coalgebras is entirely determined by its underlying function.
More concisely: In the category of endofunctor coalgebras, morphisms are determined by their underlying functions.
|
CategoryTheory.Endofunctor.Algebra.Initial.str_isIso
theorem CategoryTheory.Endofunctor.Algebra.Initial.str_isIso :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
{A : CategoryTheory.Endofunctor.Algebra F}, CategoryTheory.Limits.IsInitial A → CategoryTheory.IsIso A.str
The theorem `CategoryTheory.Endofunctor.Algebra.Initial.str_isIso` states that for any category `C`, any endofunctor `F` on `C`, and any initial `F`-algebra `A` in `C`, the structure map of the initial algebra `A` is an isomorphism. Therefore, endofunctors preserve their initial algebras.
More concisely: The structure map of the initial algebra of an endofunctor on a category is an isomorphism.
|
CategoryTheory.Endofunctor.Coalgebra.epi_of_epi
theorem CategoryTheory.Endofunctor.Coalgebra.epi_of_epi :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
{X Y : CategoryTheory.Endofunctor.Coalgebra F} (f : X ⟶ Y) [h : CategoryTheory.Epi f.f], CategoryTheory.Epi f
This theorem states that, for any category `C`, any endofunctor `F` on `C`, and any morphism `f` from one coalgebra `X` to another coalgebra `Y` under `F`, if the underlying homomorphism of `f` in `C` is an epimorphism (surjective), then `f` itself is an algebra epimorphism. In other words, surjectivity is preserved under the structure of coalgebras and endofunctors in category theory.
More concisely: If `f : X → Y` is a coalgebra homomorphism in a category `C` with endofunctor `F`, and the underlying homomorphism is an epimorphism, then `f` is a coalgebra epimorphism.
|
CategoryTheory.Endofunctor.Algebra.Hom.ext
theorem CategoryTheory.Endofunctor.Algebra.Hom.ext :
∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C C}
{A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} (x y : A₀.Hom A₁), x.f = y.f → x = y
This theorem states that in the context of category theory, given a category `C` and a functor `F` from `C` to itself, for any two 'algebras' `A₀` and `A₁` over this endofunctor `F`, any two morphisms `x` and `y` from `A₀` to `A₁` are equal if and only if their underlying functions `x.f` and `y.f` are equal. This theorem is essentially expressing that the morphism in a category of this specific type of algebra (endofunctor algebra) is fully determined by its function part.
More concisely: In the category of endofunctor algebras, two morphisms between algebras are equal if and only if their underlying functions are equal.
|
CategoryTheory.Endofunctor.Algebra.Hom.h
theorem CategoryTheory.Endofunctor.Algebra.Hom.h :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
{A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} (self : A₀.Hom A₁),
CategoryTheory.CategoryStruct.comp (F.map self.f) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str self.f
The theorem `CategoryTheory.Endofunctor.Algebra.Hom.h` states a compatibility condition for the category theory concept of Endofunctor. Specifically, for any category `C`, and an endofunctor `F` from this category to itself, and for any two algebras `A₀` and `A₁` over this endofunctor, any morphism (`self`) from `A₀` to `A₁` must satisfy the condition that the composition of the functor's map applied to `self.f` and `A₁.str` is equal to the composition of `A₀.str` and `self.f`. This condition essentially ensures the morphism (`self`) is compatible with the structure (`str`) of the algebras and the map of the endofunctor.
More concisely: For any endofunctor `F` on a category `C` and algebra morphisms `f: A₀ → A₁` between algebras `A₀` and `A₁` over `F`, the composition `F(f).f * A₁.str = A₀.str * f` holds.
|
CategoryTheory.Endofunctor.Algebra.iso_of_iso
theorem CategoryTheory.Endofunctor.Algebra.iso_of_iso :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
{A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} (f : A₀ ⟶ A₁) [inst_1 : CategoryTheory.IsIso f.f],
CategoryTheory.IsIso f
This theorem in the field of category theory states that for any category `C` and endofunctor `F` in `C`, and for any two algebras `A₀` and `A₁` over the endofunctor `F`, if there is an algebra morphism `f` from `A₀` to `A₁` such that the underlying morphism `f.f` in `C` is an isomorphism, then `f` itself is an isomorphism. In other words, an algebra morphism with an underlying isomorphism in the category `C` will be an algebra isomorphism.
More concisely: In any category, if an algebra morphism over an endofunctor with underlying morphism being an isomorphism is given, then the algebra morphism itself is an isomorphism.
|
CategoryTheory.Endofunctor.Coalgebra.iso_of_iso
theorem CategoryTheory.Endofunctor.Coalgebra.iso_of_iso :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
{V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} (f : V₀ ⟶ V₁) [inst_1 : CategoryTheory.IsIso f.f],
CategoryTheory.IsIso f
This theorem states that for any category `C` and functor `F` on `C`, if we have a coalgebra morphism `f` between two coalgebras `V₀` and `V₁` of `F`, and the underlying morphism `f.f` in `C` is an isomorphism, then `f` itself is a coalgebra isomorphism. In other words, a coalgebra morphism with an underlying isomorphism in the category `C` is a coalgebra isomorphism.
More concisely: If `f` is a coalgebra morphism of a functor `F` on category `C` with underlying isomorphism in `C`, then `f` is a coalgebra isomorphism.
|
CategoryTheory.Endofunctor.Coalgebra.mono_of_mono
theorem CategoryTheory.Endofunctor.Coalgebra.mono_of_mono :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
{X Y : CategoryTheory.Endofunctor.Coalgebra F} (f : X ⟶ Y) [h : CategoryTheory.Mono f.f], CategoryTheory.Mono f
This theorem states that in any category `C`, and for any functor `F` from `C` to `C`, if there's a morphism `f` between two coalgebras `X` and `Y` of the endofunctor of `F`, and the underlying morphism of `f` is a monomorphism, then `f` itself is a monomorphism. In other words, an algebra morphism which corresponds to a monomorphism in the category `C` is also a monomorphism in the category of coalgebras of the endofunctor of `F`.
More concisely: In any category with finite limits, if a morphism between coalgebras of an endofunctor is underlined by a monomorphism and is itself a coalgebra morphism, then it is a monomorphic coalgebra morphism.
|
CategoryTheory.Endofunctor.Algebra.epi_of_epi
theorem CategoryTheory.Endofunctor.Algebra.epi_of_epi :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
{X Y : CategoryTheory.Endofunctor.Algebra F} (f : X ⟶ Y) [h : CategoryTheory.Epi f.f], CategoryTheory.Epi f
This theorem states that given a category `C` and a functor `F` from `C` to itself, if there is an algebra morphism `f` between two algebras `X` and `Y` over the endofunctor `F` in the category, and the underlying morphism `f.f` in `C` is an epimorphism (surjective morphism), then `f` itself is an algebra epimorphism. In simpler terms, it says that if the underlying structure of an algebra morphism is "surjective", then the algebra morphism is also "surjective" in the sense of category theory.
More concisely: If `f` is an algebra morphism between `F`-algebras `X` and `Y` in a category `C` and the underlying morphism `f.f` is an epimorphism in `C`, then `f` is an algebra epimorphism.
|
CategoryTheory.Endofunctor.Algebra.ext
theorem CategoryTheory.Endofunctor.Algebra.ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
{A B : CategoryTheory.Endofunctor.Algebra F} {f g : A ⟶ B}, autoParam (f.f = g.f) _auto✝ → f = g
The theorem `CategoryTheory.Endofunctor.Algebra.ext` states that if `C` is a type and a category, `F` is a functor from `C` to `C`, `A` and `B` are algebras of the endofunctor `F`, and `f` and `g` are morphisms from `A` to `B`, then if the underlying functions of `f` and `g` (denoted `f.f` and `g.f`) are equal (a condition which is automatically checked by the `autoParam` gadget), then `f` and `g` are equal as morphisms in the category.
More concisely: If `C` is a category, `F` is a functor from `C` to `C`, `A` and `B` are algebras of the endofunctor `F`, `f` and `g` are morphisms from `A` to `B` with equal underlying functions, then `f` and `g` are equal as morphisms in `C`.
|
CategoryTheory.Endofunctor.Coalgebra.ext
theorem CategoryTheory.Endofunctor.Coalgebra.ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
{A B : CategoryTheory.Endofunctor.Coalgebra F} {f g : A ⟶ B}, autoParam (f.f = g.f) _auto✝ → f = g
The theorem `CategoryTheory.Endofunctor.Coalgebra.ext` states that, in any category `C` with a given endofunctor `F`, for any two coalgebras `A` and `B` of that endofunctor, if two morphisms `f` and `g` from `A` to `B` have the same underlying function (i.e., `f.f = g.f`), then `f` and `g` are indeed the same morphism. This equality condition is provided as an `autoParam`, which means it is typically inferred automatically by Lean.
More concisely: In any category with an endofunctor, two coalgebras' morphisms with equal underlying functions are equal as morphisms.
|
CategoryTheory.Endofunctor.Coalgebra.Hom.h
theorem CategoryTheory.Endofunctor.Coalgebra.Hom.h :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
{V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} (self : V₀.Hom V₁),
CategoryTheory.CategoryStruct.comp V₀.str (F.map self.f) = CategoryTheory.CategoryStruct.comp self.f V₁.str
The theorem `CategoryTheory.Endofunctor.Coalgebra.Hom.h` states a compatibility condition for endofunctors in category theory. Specifically, it says that for any category `C`, any endofunctor `F` on `C`, and any two coalgebras `V₀` and `V₁` for this endofunctor, for any morphism `self` from `V₀` to `V₁`, the composition of the structure map of `V₀` and the functor applied to `self.f` is the same as the composition of `self.f` and the structure map of `V₁`. In mathematical terms, it says that `V₀.str ≫ F.map self.f = self.f ≫ V₁.str`, where `≫` denotes composition of morphisms.
More concisely: For any category C, endofunctor F, coalgebras V₀ and V₁, and morphism self from V₀ to V₁ in C, the structure map of V₀ composed with F's action on self's morphism is equal to self's morphism composed with the structure map of V₁: V₀.str ≫ F.map self.f = self.f ≫ V₁.str.
|