CategoryTheory.Comonad.Coalgebra.counit
theorem CategoryTheory.Comonad.Coalgebra.counit :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (self : G.Coalgebra),
CategoryTheory.CategoryStruct.comp self.a (G.ε.app self.A) = CategoryTheory.CategoryStruct.id self.A
The theorem `CategoryTheory.Comonad.Coalgebra.counit` is a statement about category theory. It describes the counit axiom associated with a coalgebra in a category. For any category `C` and any comonad `G` on `C`, and for any coalgebra `self` of type `G.Coalgebra`, the composition of the morphism `self.a` and the application of the counit natural transformation `G.ε.app` to `self.A` is equivalent to the identity morphism on `self.A`. This is a fundamental principle in the theory of comonads and coalgebras, where the counit gives a way to "extract" an element from the comonad.
More concisely: For any comonad `G` and its coalgebra `self` in a category `C`, the composition of `self.a` and `G.ε.app` on `self.A` is equal to the identity morphism on `self.A`.
|
CategoryTheory.Comonad.Coalgebra.Hom.h_assoc
theorem CategoryTheory.Comonad.Coalgebra.Hom.h_assoc :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A B : G.Coalgebra}
(self : A.Hom B) {Z : C} (h : G.obj B.A ⟶ Z),
CategoryTheory.CategoryStruct.comp A.a (CategoryTheory.CategoryStruct.comp (G.map self.f) h) =
CategoryTheory.CategoryStruct.comp self.f (CategoryTheory.CategoryStruct.comp B.a h)
The theorem `CategoryTheory.Comonad.Coalgebra.Hom.h_assoc` in Lean 4 states that for any category `C` and comonad `G` on `C`, any morphism `self` from a coalgebra `A` to a coalgebra `B` of the comonad `G`, and any morphism `h` from the object of `B` under the comonad `G` to another object `Z` in `C`, the composition of morphisms in the category follows the associative law. More explicitly, composing the morphism from `A` to `B` with the composition of the morphism induced by `self` under the functor `G` and `h` is the same as composing `self` with the composition of the morphism from `B` to `Z` and `h`. This theorem is a statement about the associativity of morphism composition in a category with a comonad.
More concisely: For any comonad `G` on a category `C` and coalgebras `A`, `B`, and `Z` with morphisms `self : A --> B`, `h : B --> Z`, the association isomorphism holds: `self * (G h * h) = (G (self * h)) * h`.
|
CategoryTheory.Monad.algebra_iso_of_iso
theorem CategoryTheory.Monad.algebra_iso_of_iso :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) {A B : T.Algebra}
(f : A ⟶ B) [inst_1 : CategoryTheory.IsIso f.f], CategoryTheory.IsIso f
The theorem `CategoryTheory.Monad.algebra_iso_of_iso` states that given a category `C` and a monad `T` on `C`, for any two algebras `A` and `B` of `T`, if there is a morphism `f` from `A` to `B` such that the carrier part of `f` is an isomorphism, then `f` itself is an isomorphism in the category of `T`-algebras.
More concisely: If `f` is an isomorphism on the carrier part of two `T`-algebras `A` and `B` in a category `C`, then `f` is an isomorphism in the category of `T`-algebras.
|
CategoryTheory.Comonad.coalgebra_iso_of_iso
theorem CategoryTheory.Comonad.coalgebra_iso_of_iso :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) {A B : G.Coalgebra}
(f : A ⟶ B) [inst_1 : CategoryTheory.IsIso f.f], CategoryTheory.IsIso f
The theorem `CategoryTheory.Comonad.coalgebra_iso_of_iso` asserts that, for any category `C` and comonad `G` on `C`, and for any morphism `f` of G-coalgebras from `A` to `B`, if the carrier part of `f` is an isomorphism, then `f` itself is an isomorphism. This ties together the concepts of isomorphism in the category of G-coalgebras and isomorphism in the underlying category `C`.
More concisely: If `f` is an isomorphism on carrier morphisms of `G-`coalgebras in a category `C` with comonad `G`, then `f` is an isomorphism as a morphism of `G-`coalgebras.
|
CategoryTheory.Comonad.Coalgebra.Hom.h
theorem CategoryTheory.Comonad.Coalgebra.Hom.h :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A B : G.Coalgebra}
(self : A.Hom B),
CategoryTheory.CategoryStruct.comp A.a (G.map self.f) = CategoryTheory.CategoryStruct.comp self.f B.a
The theorem `CategoryTheory.Comonad.Coalgebra.Hom.h` states that, for any category `C`, any comonad `G` on `C`, and any two `G`-coalgebras `A` and `B`, if there exists a morphism from `A` to `B`, denoted as `self`, then composing the structure morphism of `A` with the `G`-map of `self` is equivalent to composing `self` with the structure morphism of `B`. Here, the `G`-map is a functor associated with the comonad `G`, and the structure morphisms of `A` and `B` are morphisms in the category `C` associated with the coalgebras `A` and `B`, respectively. This theorem essentially asserts the compatibility of a morphism of coalgebras with structure morphism.
More concisely: For any comonad `G` on a category `C` and `G`-coalgebras `A` and `B` with a morphism `self` from `A` to `B`, the following diagram commutes:
structure morphism of `A` ─┐
│ composing with `G-map` of `self`
│
structure morphism of `B` ─┘
|
CategoryTheory.Comonad.algebra_mono_of_mono
theorem CategoryTheory.Comonad.algebra_mono_of_mono :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) {X Y : G.Coalgebra}
(f : X ⟶ Y) [h : CategoryTheory.Mono f.f], CategoryTheory.Mono f
This theorem states that in the context of category theory, given a coalgebra morphism whose carrier part is a monomorphism, we can derive an algebra monomorphism. Specifically, for any type `C`, which is a category, and any comonad `G` on `C`, if `X` and `Y` are coalgebras for `G` and there exists a morphism `f` from `X` to `Y` such that `f.f` is a monomorphism, then `f` itself is a monomorphism. Basically, the monomorphism property is preserved when moving from the carrier part of the coalgebra morphism to the morphism itself.
More concisely: If `f` is a coalgebra morphism between `G`-coalgebras `X` and `Y` in a category `C` with monic carrier part `f.f`, then `f` is a monomorphism.
|
CategoryTheory.Monad.Algebra.unit
theorem CategoryTheory.Monad.Algebra.unit :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (self : T.Algebra),
CategoryTheory.CategoryStruct.comp (T.η.app self.A) self.a = CategoryTheory.CategoryStruct.id self.A
This theorem is the unit axiom related to an algebra in category theory. It states that for any category 'C', and any monad 'T' on 'C', for every algebra 'self' of the monad 'T', the composition of the natural transformation η (unit of the monad) applied to the object of the algebra with the structure map of the algebra is equal to the identity morphism on the object of the algebra. This can be expressed mathematically as `T.η.app self.A ≫ self.a = id self.A`.
More concisely: For any monad T on a category C and algebra self of T, the unit η of T satisfies self.a ∘ T.η.app self.A = id self.A.
|
CategoryTheory.Monad.Algebra.assoc
theorem CategoryTheory.Monad.Algebra.assoc :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (self : T.Algebra),
CategoryTheory.CategoryStruct.comp (T.μ.app self.A) self.a =
CategoryTheory.CategoryStruct.comp (T.map self.a) self.a
The theorem `CategoryTheory.Monad.Algebra.assoc` establishes the associativity axiom for a monad in category theory. For any category `C` and any monad `T` over `C`, the theorem states that for every algebra structure `self` over `T`, the composition of morphisms (denoted by `CategoryTheory.CategoryStruct.comp`) of `T.μ.app self.A` with `self.a` is equal to the composition of `T.map self.a` with `self.a`. This means that the order in which the morphisms are composed does not affect the result, which is a central concept in category theory and an essential property of a monad.
More concisely: For any category `C`, monad `T` over `C`, and algebra structure `self` over `T`, the compositions `T.μ.app self.A . self.a` and `T.map self.a . self.a` are equal.
|
CategoryTheory.Comonad.Coalgebra.coassoc
theorem CategoryTheory.Comonad.Coalgebra.coassoc :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (self : G.Coalgebra),
CategoryTheory.CategoryStruct.comp self.a (G.δ.app self.A) =
CategoryTheory.CategoryStruct.comp self.a (G.map self.a)
This theorem states the coassociativity axiom for a coalgebra in category theory. Given any category `C` and a comonad `G` on `C`, for any coalgebra `self` under this comonad, the composition of the structure map of the coalgebra `self.a` with the comultiplication at the carrier `self.A` of the coalgebra is equal to the composition of `self.a` with the image of `self.a` under the functor part of the comonad. This is a key property in the theory of comonads and coalgebras, ensuring that the algebraic operations interact in a consistent manner.
More concisely: For any comonad `G` and coalgebra `self` in a category `C`, the diagram commutes: `self.a ∘ self.A = G.map (self.a) ∘ self.A`.
|
CategoryTheory.Monad.Algebra.Hom.h
theorem CategoryTheory.Monad.Algebra.Hom.h :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A B : T.Algebra}
(self : A.Hom B),
CategoryTheory.CategoryStruct.comp (T.map self.f) B.a = CategoryTheory.CategoryStruct.comp A.a self.f
This theorem, referred to as "Compatibility with the structure morphism, for a morphism of algebras", establishes that for any category `C` under certain conditions, given a monad `T` over `C` and a morphism `self` between two algebras `A` and `B` of `T`, the composition of the morphism `self.f` under the functor `T.map` and the structure morphism `B.a` is the same as the composition of the structure morphism `A.a` and `self.f`. In other words, it asserts that `(T.map self.f) ≫ B.a = A.a ≫ self.f`, thus showing a commutativity property crucial for the algebraic structure.
More concisely: For any monad `T` over a category `C` and morphisms `self : A -> B` between two `T`-algebras `A` and `B`, the diagram commutes: `(T.map self.f) ≫ B.a = A.a ≫ self.f`.
|
CategoryTheory.Comonad.algebra_epi_of_epi
theorem CategoryTheory.Comonad.algebra_epi_of_epi :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) {X Y : G.Coalgebra}
(f : X ⟶ Y) [h : CategoryTheory.Epi f.f], CategoryTheory.Epi f
This theorem, `CategoryTheory.Comonad.algebra_epi_of_epi`, states that in the category theory context, if we have a coalgebra morphism whose carrier part is an epimorphism, then we obtain an algebra epimorphism. More specifically, for any category `C` and any comonad `G` on `C`, and for any two G-coalgebras `X` and `Y`, if a morphism `f` from `X` to `Y` is such that its 'f-function' is an epimorphism, then `f` itself is an epimorphism.
More concisely: If `f : X → Y` is a coalgebra morphism in a category `C` for a comonad `G`, and the 'f-function' `G.map f : G X → G Y` is an epimorphism, then `f` is an epimorphism.
|
CategoryTheory.Comonad.Coalgebra.Hom.ext'
theorem CategoryTheory.Comonad.Coalgebra.Hom.ext' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (X Y : G.Coalgebra)
(f g : X ⟶ Y), f.f = g.f → f = g
This theorem states that for any given category `C`, and any comonad `G` on `C`, if we have two coalgebras `X` and `Y` of `G`, and two morphisms `f` and `g` from `X` to `Y`, then if the underlying functions of `f` and `g` are equal (i.e., `f.f = g.f`), then the morphisms themselves are equal, i.e., `f = g`. In mathematical terms, this asserts the uniqueness of morphisms in the category of coalgebras for a given comonad, based solely on their underlying function.
More concisely: If `C` is a category, `G` is a comonad on `C`, `X` and `Y` are coalgebras of `G`, and `f` and `g` are morphisms from `X` to `Y` with equal underlying functions, then `f = g`.
|
CategoryTheory.Monad.algebra_epi_of_epi
theorem CategoryTheory.Monad.algebra_epi_of_epi :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) {X Y : T.Algebra}
(f : X ⟶ Y) [h : CategoryTheory.Epi f.f], CategoryTheory.Epi f
The theorem `CategoryTheory.Monad.algebra_epi_of_epi` states that for any category `C`, given a monad `T` and two objects `X` and `Y` in the category of `T`-algebras, if we have a morphism `f` from `X` to `Y` whose carrier part is an epimorphism (which means that for every pair of morphisms, if their composition with `f` are equal then the morphisms themselves are equal), then `f` itself is an epimorphism in the category of `T`-algebras.
More concisely: If `f` is a morphism between `T-`algebras in a category `C` with carrier part an epimorphism, then `f` is an epimorphism in the category of `T-`algebras.
|
CategoryTheory.Monad.Algebra.Hom.ext'
theorem CategoryTheory.Monad.Algebra.Hom.ext' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X Y : T.Algebra)
(f g : X ⟶ Y), f.f = g.f → f = g
This theorem states that in the category theory, for a given category `C` and a monad `T` on `C`, if we have two morphisms `f` and `g` from a monad algebra `X` to another monad algebra `Y`, and if the underlying functions of `f` and `g` (denoted by `f.f` and `g.f`) are identical, then the morphisms `f` and `g` themselves are identical. This is a statement about the uniqueness of morphisms in the category of monad algebras.
More concisely: In the category of monad algebras, if two morphisms have identical underlying functions, then they are equal.
|
CategoryTheory.Monad.algebra_mono_of_mono
theorem CategoryTheory.Monad.algebra_mono_of_mono :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) {X Y : T.Algebra}
(f : X ⟶ Y) [h : CategoryTheory.Mono f.f], CategoryTheory.Mono f
The theorem `CategoryTheory.Monad.algebra_mono_of_mono` states that for any category `C` and a monad `T` on `C`, if we have an algebra morphism `f` from `X` to `Y` (where `X` and `Y` are both algebras of the monad `T`), and if the carrier part of this morphism is a monomorphism, then the morphism `f` itself is a monomorphism. In category theory, a monomorphism is a morphism (or arrow) that, roughly speaking, is "injective" in a categorical sense.
More concisely: If `f` is an algebra morphism between `T`-algebras `X` and `Y` in a category `C` with monad `T`, and the carrier part of `f` is a monomorphism, then `f` is a monomorphism.
|