Algebra

📁 Source: Mathlib/CategoryTheory/Endofunctor/Algebra.lean

Statistics

Metric	Count
Definitions `counitIso`, `unitIso`, `toCoalgebraOf`, `toAlgebraOf`, `algebraCoalgebraEquiv`, `Algebra`, `comp`, `f`, `id`, `instInhabited`, `strInv`, `a`, `equivOfNatIso`, `forget`, `functorOfNatTrans`, `functorOfNatTransComp`, `functorOfNatTransEq`, `functorOfNatTransId`, `instCategory`, `instCategoryStruct`, `isoMk`, `str`, `comp`, `f`, `id`, `instInhabited`, `strInv`, `V`, `equivOfNatIso`, `forget`, `functorOfNatTrans`, `functorOfNatTransComp`, `functorOfNatTransEq`, `functorOfNatTransId`, `instCategory`, `instCategoryStruct`, `isoMk`, `str`, `instInhabitedAlgebraId`, `instInhabitedCoalgebraId`	40
Theorems `counitIso_hom_app_f`, `counitIso_inv_app_f`, `unitIso_hom_app_f`, `unitIso_inv_app_f`, `homEquiv_naturality_str`, `toCoalgebraOf_map_f`, `toCoalgebraOf_obj_V`, `toCoalgebraOf_obj_str`, `homEquiv_naturality_str_symm`, `toAlgebraOf_map_f`, `toAlgebraOf_obj_a`, `toAlgebraOf_obj_str`, `algebraCoalgebraEquiv_counitIso_hom_app_f`, `algebraCoalgebraEquiv_counitIso_inv_app_f`, `algebraCoalgebraEquiv_functor_map_f`, `algebraCoalgebraEquiv_functor_obj_V`, `algebraCoalgebraEquiv_functor_obj_str`, `algebraCoalgebraEquiv_inverse_map_f`, `algebraCoalgebraEquiv_inverse_obj_a`, `algebraCoalgebraEquiv_inverse_obj_str`, `algebraCoalgebraEquiv_unitIso_hom_app_f`, `algebraCoalgebraEquiv_unitIso_inv_app_f`, `ext`, `ext_iff`, `h`, `h_assoc`, `left_inv`, `left_inv'`, `right_inv`, `str_isIso`, `comp_eq_comp`, `comp_f`, `epi_of_epi`, `equivOfNatIso_counitIso`, `equivOfNatIso_functor`, `equivOfNatIso_inverse`, `equivOfNatIso_unitIso`, `ext`, `ext_iff`, `forget_faithful`, `forget_map`, `forget_obj`, `forget_reflects_iso`, `functorOfNatTransComp_hom_app_f`, `functorOfNatTransComp_inv_app_f`, `functorOfNatTransEq_hom_app_f`, `functorOfNatTransEq_inv_app_f`, `functorOfNatTransId_hom_app_f`, `functorOfNatTransId_inv_app_f`, `functorOfNatTrans_map_f`, `functorOfNatTrans_obj_a`, `functorOfNatTrans_obj_str`, `id_eq_id`, `id_f`, `isoMk_hom_f`, `isoMk_inv_f`, `iso_of_iso`, `mono_of_mono`, `ext`, `ext_iff`, `h`, `h_assoc`, `left_inv`, `right_inv`, `right_inv'`, `str_isIso`, `comp_eq_comp`, `comp_f`, `epi_of_epi`, `equivOfNatIso_counitIso`, `equivOfNatIso_functor`, `equivOfNatIso_inverse`, `equivOfNatIso_unitIso`, `ext`, `ext_iff`, `forget_faithful`, `forget_map`, `forget_obj`, `forget_reflects_iso`, `functorOfNatTransComp_hom_app_f`, `functorOfNatTransComp_inv_app_f`, `functorOfNatTransEq_hom_app_f`, `functorOfNatTransEq_inv_app_f`, `functorOfNatTransId_hom_app_f`, `functorOfNatTransId_inv_app_f`, `functorOfNatTrans_map_f`, `functorOfNatTrans_obj_V`, `functorOfNatTrans_obj_str`, `id_eq_id`, `id_f`, `isoMk_hom_f`, `isoMk_inv_f`, `iso_of_iso`, `mono_of_mono`	94
Total	134

CategoryTheory.Endofunctor

Definitions

Name	Category	Theorems
`Algebra` 📖	CompData	54 math math: `Algebra.equivOfNatIso_functor`, `Algebra.forget_map`, `Adjunction.algebraCoalgebraEquiv_unitIso_hom_app_f`, `algebraPreadditive_homGroup_neg_f`, `Adjunction.algebraCoalgebraEquiv_inverse_obj_str`, `Algebra.mono_of_mono`, `Algebra.functorOfNatTransId_inv_app_f`, `Algebra.comp_eq_comp`, `Algebra.functorOfNatTransComp_hom_app_f`, `Algebra.forget_reflects_iso`, `Adjunction.algebraCoalgebraEquiv_inverse_obj_a`, `Adjunction.AlgCoalgEquiv.counitIso_inv_app_f`, `Algebra.epi_of_epi`, `algebraPreadditive_homGroup_zsmul_f`, `Adjunction.algebraCoalgebraEquiv_functor_map_f`, `Adjunction.AlgCoalgEquiv.unitIso_inv_app_f`, `Algebra.id_eq_id`, `Adjunction.algebraCoalgebraEquiv_counitIso_inv_app_f`, `Algebra.id_f`, `Algebra.equivOfNatIso_inverse`, `Algebra.isoMk_inv_f`, `Algebra.forget_faithful`, `Algebra.functorOfNatTransEq_inv_app_f`, `Adjunction.algebraCoalgebraEquiv_unitIso_inv_app_f`, `Algebra.functorOfNatTrans_map_f`, `Algebra.functorOfNatTransId_hom_app_f`, `Algebra.equivOfNatIso_counitIso`, `algebraPreadditive_homGroup_sub_f`, `Algebra.comp_f`, `Adjunction.AlgCoalgEquiv.counitIso_hom_app_f`, `CategoryTheory.Algebra.forget_additive`, `Adjunction.algebraCoalgebraEquiv_functor_obj_V`, `Algebra.equivOfNatIso_unitIso`, `Algebra.functorOfNatTransEq_hom_app_f`, `Adjunction.Coalgebra.toAlgebraOf_obj_a`, `Adjunction.algebraCoalgebraEquiv_counitIso_hom_app_f`, `Algebra.iso_of_iso`, `Algebra.functorOfNatTransComp_inv_app_f`, `Algebra.functorOfNatTrans_obj_str`, `algebraPreadditive_homGroup_zero_f`, `Adjunction.Algebra.toCoalgebraOf_obj_V`, `Adjunction.Algebra.toCoalgebraOf_map_f`, `Adjunction.algebraCoalgebraEquiv_functor_obj_str`, `Adjunction.Algebra.toCoalgebraOf_obj_str`, `algebraPreadditive_homGroup_add_f`, `Adjunction.Coalgebra.toAlgebraOf_obj_str`, `algebraPreadditive_homGroup_nsmul_f`, `Adjunction.AlgCoalgEquiv.unitIso_hom_app_f`, `Adjunction.algebraCoalgebraEquiv_inverse_map_f`, `Algebra.Initial.left_inv'`, `Algebra.isoMk_hom_f`, `Adjunction.Coalgebra.toAlgebraOf_map_f`, `Algebra.forget_obj`, `Algebra.functorOfNatTrans_obj_a`
`instInhabitedAlgebraId` 📖	CompOp	—
`instInhabitedCoalgebraId` 📖	CompOp	—

CategoryTheory.Endofunctor.Adjunction

Definitions

Name	Category	Theorems
`algebraCoalgebraEquiv` 📖	CompOp	10 math math: `algebraCoalgebraEquiv_unitIso_hom_app_f`, `algebraCoalgebraEquiv_inverse_obj_str`, `algebraCoalgebraEquiv_inverse_obj_a`, `algebraCoalgebraEquiv_functor_map_f`, `algebraCoalgebraEquiv_counitIso_inv_app_f`, `algebraCoalgebraEquiv_unitIso_inv_app_f`, `algebraCoalgebraEquiv_functor_obj_V`, `algebraCoalgebraEquiv_counitIso_hom_app_f`, `algebraCoalgebraEquiv_functor_obj_str`, `algebraCoalgebraEquiv_inverse_map_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraCoalgebraEquiv_counitIso_hom_app_f` 📖	mathematical	—	`CategoryTheory.Endofunctor.Coalgebra.Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `CategoryTheory.Functor.comp` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `Coalgebra.toAlgebraOf` `Algebra.toCoalgebraOf` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.counitIso` `algebraCoalgebraEquiv` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Endofunctor.Coalgebra.V`	—	—
`algebraCoalgebraEquiv_counitIso_inv_app_f` 📖	mathematical	—	`CategoryTheory.Endofunctor.Coalgebra.Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `Coalgebra.toAlgebraOf` `Algebra.toCoalgebraOf` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.counitIso` `algebraCoalgebraEquiv` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Endofunctor.Coalgebra.V`	—	—
`algebraCoalgebraEquiv_functor_map_f` 📖	mathematical	—	`CategoryTheory.Endofunctor.Coalgebra.Hom.f` `CategoryTheory.Endofunctor.Algebra.a` `Equiv.toFun` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Adjunction.homEquiv` `CategoryTheory.Endofunctor.Algebra.str` `CategoryTheory.Functor.map` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `CategoryTheory.Equivalence.functor` `algebraCoalgebraEquiv` `CategoryTheory.Endofunctor.Algebra.Hom.f`	—	—
`algebraCoalgebraEquiv_functor_obj_V` 📖	mathematical	—	`CategoryTheory.Endofunctor.Coalgebra.V` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `CategoryTheory.Equivalence.functor` `algebraCoalgebraEquiv` `CategoryTheory.Endofunctor.Algebra.a`	—	—
`algebraCoalgebraEquiv_functor_obj_str` 📖	mathematical	—	`CategoryTheory.Endofunctor.Coalgebra.str` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `CategoryTheory.Equivalence.functor` `algebraCoalgebraEquiv` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Endofunctor.Algebra.a` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Adjunction.homEquiv` `CategoryTheory.Endofunctor.Algebra.str`	—	—
`algebraCoalgebraEquiv_inverse_map_f` 📖	mathematical	—	`CategoryTheory.Endofunctor.Algebra.Hom.f` `CategoryTheory.Endofunctor.Coalgebra.V` `Equiv.invFun` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Adjunction.homEquiv` `CategoryTheory.Endofunctor.Coalgebra.str` `CategoryTheory.Functor.map` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `CategoryTheory.Equivalence.inverse` `algebraCoalgebraEquiv` `CategoryTheory.Endofunctor.Coalgebra.Hom.f`	—	—
`algebraCoalgebraEquiv_inverse_obj_a` 📖	mathematical	—	`CategoryTheory.Endofunctor.Algebra.a` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `CategoryTheory.Equivalence.inverse` `algebraCoalgebraEquiv` `CategoryTheory.Endofunctor.Coalgebra.V`	—	—
`algebraCoalgebraEquiv_inverse_obj_str` 📖	mathematical	—	`CategoryTheory.Endofunctor.Algebra.str` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `CategoryTheory.Equivalence.inverse` `algebraCoalgebraEquiv` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Endofunctor.Coalgebra.V` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.Adjunction.homEquiv` `CategoryTheory.Endofunctor.Coalgebra.str`	—	—
`algebraCoalgebraEquiv_unitIso_hom_app_f` 📖	mathematical	—	`CategoryTheory.Endofunctor.Algebra.Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `Algebra.toCoalgebraOf` `Coalgebra.toAlgebraOf` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.unitIso` `algebraCoalgebraEquiv` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Endofunctor.Algebra.a`	—	—
`algebraCoalgebraEquiv_unitIso_inv_app_f` 📖	mathematical	—	`CategoryTheory.Endofunctor.Algebra.Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `CategoryTheory.Functor.comp` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `Algebra.toCoalgebraOf` `Coalgebra.toAlgebraOf` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.unitIso` `algebraCoalgebraEquiv` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Endofunctor.Algebra.a`	—	—

CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv

Definitions

Name	Category	Theorems
`counitIso` 📖	CompOp	2 math math: `counitIso_inv_app_f`, `counitIso_hom_app_f`
`unitIso` 📖	CompOp	2 math math: `unitIso_inv_app_f`, `unitIso_hom_app_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`counitIso_hom_app_f` 📖	mathematical	—	`CategoryTheory.Endofunctor.Coalgebra.Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `CategoryTheory.Functor.comp` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf` `CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `counitIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Endofunctor.Coalgebra.V`	—	—
`counitIso_inv_app_f` 📖	mathematical	—	`CategoryTheory.Endofunctor.Coalgebra.Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf` `CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `counitIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Endofunctor.Coalgebra.V`	—	—
`unitIso_hom_app_f` 📖	mathematical	—	`CategoryTheory.Endofunctor.Algebra.Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf` `CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `unitIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Endofunctor.Algebra.a`	—	—
`unitIso_inv_app_f` 📖	mathematical	—	`CategoryTheory.Endofunctor.Algebra.Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `CategoryTheory.Functor.comp` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf` `CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `unitIso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Endofunctor.Algebra.a`	—	—

CategoryTheory.Endofunctor.Adjunction.Algebra

Definitions

Name	Category	Theorems
`toCoalgebraOf` 📖	CompOp	11 math math: `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_unitIso_hom_app_f`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso_inv_app_f`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso_inv_app_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_counitIso_inv_app_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_unitIso_inv_app_f`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso_hom_app_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_counitIso_hom_app_f`, `toCoalgebraOf_obj_V`, `toCoalgebraOf_map_f`, `toCoalgebraOf_obj_str`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso_hom_app_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homEquiv_naturality_str` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Endofunctor.Algebra.a` `CategoryTheory.Functor.obj` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Adjunction.homEquiv` `CategoryTheory.Endofunctor.Algebra.str` `CategoryTheory.Functor.map` `CategoryTheory.Endofunctor.Algebra.Hom.f`	—	`CategoryTheory.Adjunction.homEquiv_naturality_right` `CategoryTheory.Adjunction.homEquiv_naturality_left` `CategoryTheory.Endofunctor.Algebra.Hom.h`
`toCoalgebraOf_map_f` 📖	mathematical	—	`CategoryTheory.Endofunctor.Coalgebra.Hom.f` `CategoryTheory.Endofunctor.Algebra.a` `Equiv.toFun` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Adjunction.homEquiv` `CategoryTheory.Endofunctor.Algebra.str` `CategoryTheory.Functor.map` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `toCoalgebraOf` `CategoryTheory.Endofunctor.Algebra.Hom.f`	—	—
`toCoalgebraOf_obj_V` 📖	mathematical	—	`CategoryTheory.Endofunctor.Coalgebra.V` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `toCoalgebraOf` `CategoryTheory.Endofunctor.Algebra.a`	—	—
`toCoalgebraOf_obj_str` 📖	mathematical	—	`CategoryTheory.Endofunctor.Coalgebra.str` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `toCoalgebraOf` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Endofunctor.Algebra.a` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.Adjunction.homEquiv` `CategoryTheory.Endofunctor.Algebra.str`	—	—

CategoryTheory.Endofunctor.Adjunction.Coalgebra

Definitions

Name	Category	Theorems
`toAlgebraOf` 📖	CompOp	11 math math: `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_unitIso_hom_app_f`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso_inv_app_f`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso_inv_app_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_counitIso_inv_app_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_unitIso_inv_app_f`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso_hom_app_f`, `toAlgebraOf_obj_a`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_counitIso_hom_app_f`, `toAlgebraOf_obj_str`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso_hom_app_f`, `toAlgebraOf_map_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homEquiv_naturality_str_symm` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra.V` `CategoryTheory.Functor.map` `CategoryTheory.Endofunctor.Coalgebra.Hom.f` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.Adjunction.homEquiv` `CategoryTheory.Endofunctor.Coalgebra.str`	—	`CategoryTheory.Adjunction.homEquiv_naturality_left_symm` `CategoryTheory.Adjunction.homEquiv_naturality_right_symm` `CategoryTheory.Endofunctor.Coalgebra.Hom.h`
`toAlgebraOf_map_f` 📖	mathematical	—	`CategoryTheory.Endofunctor.Algebra.Hom.f` `CategoryTheory.Endofunctor.Coalgebra.V` `Equiv.invFun` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Adjunction.homEquiv` `CategoryTheory.Endofunctor.Coalgebra.str` `CategoryTheory.Functor.map` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `toAlgebraOf` `CategoryTheory.Endofunctor.Coalgebra.Hom.f`	—	—
`toAlgebraOf_obj_a` 📖	mathematical	—	`CategoryTheory.Endofunctor.Algebra.a` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `toAlgebraOf` `CategoryTheory.Endofunctor.Coalgebra.V`	—	—
`toAlgebraOf_obj_str` 📖	mathematical	—	`CategoryTheory.Endofunctor.Algebra.str` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategory` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategory` `toAlgebraOf` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Endofunctor.Coalgebra.V` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.Adjunction.homEquiv` `CategoryTheory.Endofunctor.Coalgebra.str`	—	—

CategoryTheory.Endofunctor.Algebra

Definitions

Name	Category	Theorems
`a` 📖	CompOp	38 math math: `Hom.h_assoc`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_unitIso_hom_app_f`, `CategoryTheory.Endofunctor.algebraPreadditive_homGroup_neg_f`, `CategoryTheory.Endofunctor.Adjunction.Algebra.homEquiv_naturality_str`, `functorOfNatTransId_inv_app_f`, `ext_iff`, `functorOfNatTransComp_hom_app_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_obj_a`, `Initial.right_inv`, `Initial.str_isIso`, `CategoryTheory.Endofunctor.algebraPreadditive_homGroup_zsmul_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_map_f`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso_inv_app_f`, `id_f`, `functorOfNatTransEq_inv_app_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_unitIso_inv_app_f`, `functorOfNatTrans_map_f`, `functorOfNatTransId_hom_app_f`, `CategoryTheory.Endofunctor.algebraPreadditive_homGroup_sub_f`, `comp_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_obj_V`, `Hom.h`, `functorOfNatTransEq_hom_app_f`, `CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_obj_a`, `functorOfNatTransComp_inv_app_f`, `functorOfNatTrans_obj_str`, `CategoryTheory.Endofunctor.algebraPreadditive_homGroup_zero_f`, `CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_obj_V`, `CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_map_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_obj_str`, `CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_obj_str`, `CategoryTheory.Endofunctor.algebraPreadditive_homGroup_add_f`, `CategoryTheory.Endofunctor.algebraPreadditive_homGroup_nsmul_f`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso_hom_app_f`, `Initial.left_inv'`, `forget_obj`, `functorOfNatTrans_obj_a`, `Initial.left_inv`
`equivOfNatIso` 📖	CompOp	4 math math: `equivOfNatIso_functor`, `equivOfNatIso_inverse`, `equivOfNatIso_counitIso`, `equivOfNatIso_unitIso`
`forget` 📖	CompOp	5 math math: `forget_map`, `forget_reflects_iso`, `forget_faithful`, `CategoryTheory.Algebra.forget_additive`, `forget_obj`
`functorOfNatTrans` 📖	CompOp	13 math math: `equivOfNatIso_functor`, `functorOfNatTransId_inv_app_f`, `functorOfNatTransComp_hom_app_f`, `equivOfNatIso_inverse`, `functorOfNatTransEq_inv_app_f`, `functorOfNatTrans_map_f`, `functorOfNatTransId_hom_app_f`, `equivOfNatIso_counitIso`, `equivOfNatIso_unitIso`, `functorOfNatTransEq_hom_app_f`, `functorOfNatTransComp_inv_app_f`, `functorOfNatTrans_obj_str`, `functorOfNatTrans_obj_a`
`functorOfNatTransComp` 📖	CompOp	4 math math: `functorOfNatTransComp_hom_app_f`, `equivOfNatIso_counitIso`, `equivOfNatIso_unitIso`, `functorOfNatTransComp_inv_app_f`
`functorOfNatTransEq` 📖	CompOp	4 math math: `functorOfNatTransEq_inv_app_f`, `equivOfNatIso_counitIso`, `equivOfNatIso_unitIso`, `functorOfNatTransEq_hom_app_f`
`functorOfNatTransId` 📖	CompOp	4 math math: `functorOfNatTransId_inv_app_f`, `functorOfNatTransId_hom_app_f`, `equivOfNatIso_counitIso`, `equivOfNatIso_unitIso`
`instCategory` 📖	CompOp	49 math math: `equivOfNatIso_functor`, `forget_map`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_unitIso_hom_app_f`, `CategoryTheory.Endofunctor.algebraPreadditive_homGroup_neg_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_obj_str`, `mono_of_mono`, `functorOfNatTransId_inv_app_f`, `functorOfNatTransComp_hom_app_f`, `forget_reflects_iso`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_obj_a`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso_inv_app_f`, `epi_of_epi`, `CategoryTheory.Endofunctor.algebraPreadditive_homGroup_zsmul_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_map_f`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso_inv_app_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_counitIso_inv_app_f`, `equivOfNatIso_inverse`, `isoMk_inv_f`, `forget_faithful`, `functorOfNatTransEq_inv_app_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_unitIso_inv_app_f`, `functorOfNatTrans_map_f`, `functorOfNatTransId_hom_app_f`, `equivOfNatIso_counitIso`, `CategoryTheory.Endofunctor.algebraPreadditive_homGroup_sub_f`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso_hom_app_f`, `CategoryTheory.Algebra.forget_additive`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_obj_V`, `equivOfNatIso_unitIso`, `functorOfNatTransEq_hom_app_f`, `CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_obj_a`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_counitIso_hom_app_f`, `iso_of_iso`, `functorOfNatTransComp_inv_app_f`, `functorOfNatTrans_obj_str`, `CategoryTheory.Endofunctor.algebraPreadditive_homGroup_zero_f`, `CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_obj_V`, `CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_map_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_obj_str`, `CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_obj_str`, `CategoryTheory.Endofunctor.algebraPreadditive_homGroup_add_f`, `CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_obj_str`, `CategoryTheory.Endofunctor.algebraPreadditive_homGroup_nsmul_f`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso_hom_app_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_map_f`, `isoMk_hom_f`, `CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_map_f`, `forget_obj`, `functorOfNatTrans_obj_a`
`instCategoryStruct` 📖	CompOp	5 math math: `comp_eq_comp`, `id_eq_id`, `id_f`, `comp_f`, `Initial.left_inv'`
`isoMk` 📖	CompOp	2 math math: `isoMk_inv_f`, `isoMk_hom_f`
`str` 📖	CompOp	15 math math: `Hom.h_assoc`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_obj_str`, `CategoryTheory.Endofunctor.Adjunction.Algebra.homEquiv_naturality_str`, `Initial.right_inv`, `Initial.str_isIso`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_map_f`, `functorOfNatTrans_map_f`, `Hom.h`, `functorOfNatTrans_obj_str`, `CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_map_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_obj_str`, `CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_obj_str`, `CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_obj_str`, `Initial.left_inv'`, `Initial.left_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_eq_comp` 📖	mathematical	—	`Hom.comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Endofunctor.Algebra` `instCategoryStruct`	—	—
`comp_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Endofunctor.Algebra` `instCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `a`	—	—
`epi_of_epi` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.Endofunctor.Algebra` `instCategory`	—	`CategoryTheory.Functor.epi_of_epi_map` `CategoryTheory.Functor.reflectsEpimorphisms_of_faithful` `forget_faithful`
`equivOfNatIso_counitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.counitIso` `CategoryTheory.Endofunctor.Algebra` `instCategory` `equivOfNatIso` `CategoryTheory.Iso.trans` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `functorOfNatTrans` `CategoryTheory.Iso.hom` `CategoryTheory.Iso.inv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.id` `CategoryTheory.Iso.symm` `functorOfNatTransComp` `CategoryTheory.CategoryStruct.id` `functorOfNatTransEq` `functorOfNatTransId`	—	—
`equivOfNatIso_functor` 📖	mathematical	—	`CategoryTheory.Equivalence.functor` `CategoryTheory.Endofunctor.Algebra` `instCategory` `equivOfNatIso` `functorOfNatTrans` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	—	—
`equivOfNatIso_inverse` 📖	mathematical	—	`CategoryTheory.Equivalence.inverse` `CategoryTheory.Endofunctor.Algebra` `instCategory` `equivOfNatIso` `functorOfNatTrans` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	—	—
`equivOfNatIso_unitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.unitIso` `CategoryTheory.Endofunctor.Algebra` `instCategory` `equivOfNatIso` `CategoryTheory.Iso.trans` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `functorOfNatTrans` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Iso.hom` `CategoryTheory.Iso.symm` `functorOfNatTransId` `CategoryTheory.CategoryStruct.comp` `functorOfNatTransEq` `functorOfNatTransComp`	—	—
`ext` 📖	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `a` `Hom.f`	—	—	`Hom.ext`
`ext_iff` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `a` `Hom.f`	—	`ext`
`forget_faithful` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.Endofunctor.Algebra` `instCategory` `forget`	—	`ext`
`forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Endofunctor.Algebra` `instCategory` `forget` `Hom.f`	—	—
`forget_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra` `instCategory` `forget` `a`	—	—
`forget_reflects_iso` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsIsomorphisms` `CategoryTheory.Endofunctor.Algebra` `instCategory` `forget`	—	`iso_of_iso`
`functorOfNatTransComp_hom_app_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra` `instCategory` `functorOfNatTrans` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `functorOfNatTransComp` `CategoryTheory.CategoryStruct.id` `a`	—	—
`functorOfNatTransComp_inv_app_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra` `instCategory` `CategoryTheory.Functor.comp` `functorOfNatTrans` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `functorOfNatTransComp` `CategoryTheory.CategoryStruct.id` `a`	—	—
`functorOfNatTransEq_hom_app_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra` `instCategory` `functorOfNatTrans` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `functorOfNatTransEq` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `a`	—	—
`functorOfNatTransEq_inv_app_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra` `instCategory` `functorOfNatTrans` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `functorOfNatTransEq` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `a`	—	—
`functorOfNatTransId_hom_app_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra` `instCategory` `functorOfNatTrans` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `functorOfNatTransId` `a`	—	—
`functorOfNatTransId_inv_app_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra` `instCategory` `CategoryTheory.Functor.id` `functorOfNatTrans` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `functorOfNatTransId` `a`	—	—
`functorOfNatTrans_map_f` 📖	mathematical	—	`Hom.f` `a` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.NatTrans.app` `str` `CategoryTheory.Functor.map` `CategoryTheory.Endofunctor.Algebra` `instCategory` `functorOfNatTrans`	—	—
`functorOfNatTrans_obj_a` 📖	mathematical	—	`a` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra` `instCategory` `functorOfNatTrans`	—	—
`functorOfNatTrans_obj_str` 📖	mathematical	—	`str` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra` `instCategory` `functorOfNatTrans` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `a` `CategoryTheory.NatTrans.app`	—	—
`id_eq_id` 📖	mathematical	—	`Hom.id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Endofunctor.Algebra` `instCategoryStruct`	—	—
`id_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Endofunctor.Algebra` `instCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `a`	—	—
`isoMk_hom_f` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `a` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `str`	`Hom.f` `CategoryTheory.Endofunctor.Algebra` `instCategory` `isoMk`	—	—
`isoMk_inv_f` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `a` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `str`	`Hom.f` `CategoryTheory.Iso.inv` `CategoryTheory.Endofunctor.Algebra` `instCategory` `isoMk`	—	—
`iso_of_iso` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Endofunctor.Algebra` `instCategory`	—	`CategoryTheory.Functor.map_isIso` `CategoryTheory.Functor.map_inv` `CategoryTheory.Category.assoc` `Hom.h` `ext` `CategoryTheory.IsIso.hom_inv_id` `CategoryTheory.IsIso.inv_hom_id`
`mono_of_mono` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.Endofunctor.Algebra` `instCategory`	—	`CategoryTheory.Functor.mono_of_mono_map` `CategoryTheory.Functor.reflectsMonomorphisms_of_faithful` `forget_faithful`

CategoryTheory.Endofunctor.Algebra.Hom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	1 math math: `CategoryTheory.Endofunctor.Algebra.comp_eq_comp`
`f` 📖	CompOp	31 math math: `CategoryTheory.Endofunctor.Algebra.forget_map`, `h_assoc`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_unitIso_hom_app_f`, `CategoryTheory.Endofunctor.algebraPreadditive_homGroup_neg_f`, `CategoryTheory.Endofunctor.Adjunction.Algebra.homEquiv_naturality_str`, `CategoryTheory.Endofunctor.Algebra.functorOfNatTransId_inv_app_f`, `CategoryTheory.Endofunctor.Algebra.ext_iff`, `CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp_hom_app_f`, `CategoryTheory.Endofunctor.algebraPreadditive_homGroup_zsmul_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_map_f`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso_inv_app_f`, `CategoryTheory.Endofunctor.Algebra.id_f`, `CategoryTheory.Endofunctor.Algebra.isoMk_inv_f`, `ext_iff`, `CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq_inv_app_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_unitIso_inv_app_f`, `CategoryTheory.Endofunctor.Algebra.functorOfNatTrans_map_f`, `CategoryTheory.Endofunctor.Algebra.functorOfNatTransId_hom_app_f`, `CategoryTheory.Endofunctor.algebraPreadditive_homGroup_sub_f`, `CategoryTheory.Endofunctor.Algebra.comp_f`, `h`, `CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq_hom_app_f`, `CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp_inv_app_f`, `CategoryTheory.Endofunctor.algebraPreadditive_homGroup_zero_f`, `CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_map_f`, `CategoryTheory.Endofunctor.algebraPreadditive_homGroup_add_f`, `CategoryTheory.Endofunctor.algebraPreadditive_homGroup_nsmul_f`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso_hom_app_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_map_f`, `CategoryTheory.Endofunctor.Algebra.isoMk_hom_f`, `CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_map_f`
`id` 📖	CompOp	1 math math: `CategoryTheory.Endofunctor.Algebra.id_eq_id`
`instInhabited` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`f`	—	—	—
`ext_iff` 📖	mathematical	—	`f`	—	`ext`
`h` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra.a` `CategoryTheory.Functor.map` `f` `CategoryTheory.Endofunctor.Algebra.str`	—	—
`h_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra.a` `CategoryTheory.Functor.map` `f` `CategoryTheory.Endofunctor.Algebra.str`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `h`

CategoryTheory.Endofunctor.Algebra.Initial

Definitions

Name	Category	Theorems
`strInv` 📖	CompOp	3 math math: `right_inv`, `left_inv'`, `left_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`left_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Endofunctor.Algebra.a` `CategoryTheory.Functor.obj` `strInv` `CategoryTheory.Endofunctor.Algebra.str` `CategoryTheory.CategoryStruct.id`	—	`left_inv'`
`left_inv'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Endofunctor.Algebra.a` `CategoryTheory.Functor.obj` `strInv` `CategoryTheory.Endofunctor.Algebra.str` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Endofunctor.Algebra` `CategoryTheory.Endofunctor.Algebra.instCategoryStruct`	—	`CategoryTheory.Limits.IsInitial.hom_ext`
`right_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra.a` `CategoryTheory.Endofunctor.Algebra.str` `strInv` `CategoryTheory.CategoryStruct.id`	—	`strInv.eq_1` `CategoryTheory.Endofunctor.Algebra.Hom.h` `CategoryTheory.Functor.map_id` `CategoryTheory.Functor.map_comp` `left_inv`
`str_isIso` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Algebra.a` `CategoryTheory.Endofunctor.Algebra.str`	—	`right_inv` `left_inv`

CategoryTheory.Endofunctor.Coalgebra

Definitions

Name	Category	Theorems
`V` 📖	CompOp	38 math math: `id_f`, `functorOfNatTransComp_inv_app_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_obj_str`, `functorOfNatTrans_obj_str`, `CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_sub_f`, `CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_zero_f`, `CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_neg_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_obj_a`, `Hom.h_assoc`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso_inv_app_f`, `functorOfNatTransId_inv_app_f`, `Terminal.left_inv`, `Terminal.right_inv`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_counitIso_inv_app_f`, `CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_zsmul_f`, `Terminal.str_isIso`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso_hom_app_f`, `functorOfNatTransEq_hom_app_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_obj_V`, `Hom.h`, `CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_obj_a`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_counitIso_hom_app_f`, `forget_obj`, `ext_iff`, `functorOfNatTrans_obj_V`, `CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_obj_V`, `functorOfNatTransId_hom_app_f`, `CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_obj_str`, `CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_add_f`, `CategoryTheory.Endofunctor.Adjunction.Coalgebra.homEquiv_naturality_str_symm`, `functorOfNatTransEq_inv_app_f`, `Terminal.right_inv'`, `CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_nsmul_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_map_f`, `functorOfNatTrans_map_f`, `functorOfNatTransComp_hom_app_f`, `comp_f`, `CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_map_f`
`equivOfNatIso` 📖	CompOp	4 math math: `equivOfNatIso_inverse`, `equivOfNatIso_counitIso`, `equivOfNatIso_unitIso`, `equivOfNatIso_functor`
`forget` 📖	CompOp	5 math math: `forget_faithful`, `forget_map`, `forget_obj`, `CategoryTheory.Coalgebra.forget_additive`, `forget_reflects_iso`
`functorOfNatTrans` 📖	CompOp	13 math math: `functorOfNatTransComp_inv_app_f`, `equivOfNatIso_inverse`, `functorOfNatTrans_obj_str`, `functorOfNatTransId_inv_app_f`, `equivOfNatIso_counitIso`, `equivOfNatIso_unitIso`, `functorOfNatTransEq_hom_app_f`, `equivOfNatIso_functor`, `functorOfNatTrans_obj_V`, `functorOfNatTransId_hom_app_f`, `functorOfNatTransEq_inv_app_f`, `functorOfNatTrans_map_f`, `functorOfNatTransComp_hom_app_f`
`functorOfNatTransComp` 📖	CompOp	4 math math: `functorOfNatTransComp_inv_app_f`, `equivOfNatIso_counitIso`, `equivOfNatIso_unitIso`, `functorOfNatTransComp_hom_app_f`
`functorOfNatTransEq` 📖	CompOp	4 math math: `equivOfNatIso_counitIso`, `equivOfNatIso_unitIso`, `functorOfNatTransEq_hom_app_f`, `functorOfNatTransEq_inv_app_f`
`functorOfNatTransId` 📖	CompOp	4 math math: `functorOfNatTransId_inv_app_f`, `equivOfNatIso_counitIso`, `equivOfNatIso_unitIso`, `functorOfNatTransId_hom_app_f`
`instCategory` 📖	CompOp	49 math math: `functorOfNatTransComp_inv_app_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_unitIso_hom_app_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_obj_str`, `equivOfNatIso_inverse`, `forget_faithful`, `functorOfNatTrans_obj_str`, `CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_sub_f`, `CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_zero_f`, `CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_neg_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_obj_a`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso_inv_app_f`, `forget_map`, `functorOfNatTransId_inv_app_f`, `equivOfNatIso_counitIso`, `isoMk_hom_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_map_f`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso_inv_app_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_counitIso_inv_app_f`, `iso_of_iso`, `isoMk_inv_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_unitIso_inv_app_f`, `CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_zsmul_f`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso_hom_app_f`, `equivOfNatIso_unitIso`, `functorOfNatTransEq_hom_app_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_obj_V`, `CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_obj_a`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_counitIso_hom_app_f`, `equivOfNatIso_functor`, `forget_obj`, `functorOfNatTrans_obj_V`, `CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_obj_V`, `CategoryTheory.Coalgebra.forget_additive`, `epi_of_epi`, `CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_map_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_obj_str`, `CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_obj_str`, `functorOfNatTransId_hom_app_f`, `mono_of_mono`, `CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_obj_str`, `CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_add_f`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso_hom_app_f`, `functorOfNatTransEq_inv_app_f`, `CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_nsmul_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_map_f`, `functorOfNatTrans_map_f`, `functorOfNatTransComp_hom_app_f`, `CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_map_f`, `forget_reflects_iso`
`instCategoryStruct` 📖	CompOp	5 math math: `id_f`, `comp_eq_comp`, `id_eq_id`, `Terminal.right_inv'`, `comp_f`
`isoMk` 📖	CompOp	2 math math: `isoMk_hom_f`, `isoMk_inv_f`
`str` 📖	CompOp	15 math math: `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_obj_str`, `functorOfNatTrans_obj_str`, `Hom.h_assoc`, `Terminal.left_inv`, `Terminal.right_inv`, `Terminal.str_isIso`, `Hom.h`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_obj_str`, `CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_obj_str`, `CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_obj_str`, `CategoryTheory.Endofunctor.Adjunction.Coalgebra.homEquiv_naturality_str_symm`, `Terminal.right_inv'`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_map_f`, `functorOfNatTrans_map_f`, `CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_map_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_eq_comp` 📖	mathematical	—	`Hom.comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Endofunctor.Coalgebra` `instCategoryStruct`	—	—
`comp_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Endofunctor.Coalgebra` `instCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `V`	—	—
`epi_of_epi` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.Endofunctor.Coalgebra` `instCategory`	—	`CategoryTheory.Functor.epi_of_epi_map` `CategoryTheory.Functor.reflectsEpimorphisms_of_faithful` `forget_faithful`
`equivOfNatIso_counitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.counitIso` `CategoryTheory.Endofunctor.Coalgebra` `instCategory` `equivOfNatIso` `CategoryTheory.Iso.trans` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `functorOfNatTrans` `CategoryTheory.Iso.inv` `CategoryTheory.Iso.hom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.id` `CategoryTheory.Iso.symm` `functorOfNatTransComp` `CategoryTheory.CategoryStruct.id` `functorOfNatTransEq` `functorOfNatTransId`	—	—
`equivOfNatIso_functor` 📖	mathematical	—	`CategoryTheory.Equivalence.functor` `CategoryTheory.Endofunctor.Coalgebra` `instCategory` `equivOfNatIso` `functorOfNatTrans` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	—	—
`equivOfNatIso_inverse` 📖	mathematical	—	`CategoryTheory.Equivalence.inverse` `CategoryTheory.Endofunctor.Coalgebra` `instCategory` `equivOfNatIso` `functorOfNatTrans` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	—	—
`equivOfNatIso_unitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.unitIso` `CategoryTheory.Endofunctor.Coalgebra` `instCategory` `equivOfNatIso` `CategoryTheory.Iso.trans` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `functorOfNatTrans` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Iso.inv` `CategoryTheory.Iso.symm` `functorOfNatTransId` `CategoryTheory.CategoryStruct.comp` `functorOfNatTransEq` `functorOfNatTransComp`	—	—
`ext` 📖	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `V` `Hom.f`	—	—	`Hom.ext`
`ext_iff` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `V` `Hom.f`	—	`ext`
`forget_faithful` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.Endofunctor.Coalgebra` `instCategory` `forget`	—	`ext`
`forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Endofunctor.Coalgebra` `instCategory` `forget` `Hom.f`	—	—
`forget_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra` `instCategory` `forget` `V`	—	—
`forget_reflects_iso` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsIsomorphisms` `CategoryTheory.Endofunctor.Coalgebra` `instCategory` `forget`	—	`iso_of_iso`
`functorOfNatTransComp_hom_app_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra` `instCategory` `functorOfNatTrans` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `functorOfNatTransComp` `CategoryTheory.CategoryStruct.id` `V`	—	—
`functorOfNatTransComp_inv_app_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra` `instCategory` `CategoryTheory.Functor.comp` `functorOfNatTrans` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `functorOfNatTransComp` `CategoryTheory.CategoryStruct.id` `V`	—	—
`functorOfNatTransEq_hom_app_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra` `instCategory` `functorOfNatTrans` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `functorOfNatTransEq` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `V`	—	—
`functorOfNatTransEq_inv_app_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra` `instCategory` `functorOfNatTrans` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `functorOfNatTransEq` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `V`	—	—
`functorOfNatTransId_hom_app_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra` `instCategory` `functorOfNatTrans` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `functorOfNatTransId` `V`	—	—
`functorOfNatTransId_inv_app_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra` `instCategory` `CategoryTheory.Functor.id` `functorOfNatTrans` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `functorOfNatTransId` `V`	—	—
`functorOfNatTrans_map_f` 📖	mathematical	—	`Hom.f` `V` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `str` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.map` `CategoryTheory.Endofunctor.Coalgebra` `instCategory` `functorOfNatTrans`	—	—
`functorOfNatTrans_obj_V` 📖	mathematical	—	`V` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra` `instCategory` `functorOfNatTrans`	—	—
`functorOfNatTrans_obj_str` 📖	mathematical	—	`str` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra` `instCategory` `functorOfNatTrans` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `V` `CategoryTheory.NatTrans.app`	—	—
`id_eq_id` 📖	mathematical	—	`Hom.id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Endofunctor.Coalgebra` `instCategoryStruct`	—	—
`id_f` 📖	mathematical	—	`Hom.f` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Endofunctor.Coalgebra` `instCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `V`	—	—
`isoMk_hom_f` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `V` `CategoryTheory.Functor.obj` `CategoryTheory.CategoryStruct.comp` `str` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom`	`Hom.f` `CategoryTheory.Endofunctor.Coalgebra` `instCategory` `isoMk`	—	—
`isoMk_inv_f` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `V` `CategoryTheory.Functor.obj` `CategoryTheory.CategoryStruct.comp` `str` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom`	`Hom.f` `CategoryTheory.Iso.inv` `CategoryTheory.Endofunctor.Coalgebra` `instCategory` `isoMk`	—	—
`iso_of_iso` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Endofunctor.Coalgebra` `instCategory`	—	`CategoryTheory.IsIso.eq_inv_comp` `CategoryTheory.Category.assoc` `Hom.h` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Functor.map_inv` `CategoryTheory.IsIso.hom_inv_id` `CategoryTheory.Category.comp_id` `ext` `CategoryTheory.IsIso.inv_hom_id`
`mono_of_mono` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.Endofunctor.Coalgebra` `instCategory`	—	`CategoryTheory.Functor.mono_of_mono_map` `CategoryTheory.Functor.reflectsMonomorphisms_of_faithful` `forget_faithful`

CategoryTheory.Endofunctor.Coalgebra.Hom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	1 math math: `CategoryTheory.Endofunctor.Coalgebra.comp_eq_comp`
`f` 📖	CompOp	31 math math: `CategoryTheory.Endofunctor.Coalgebra.id_f`, `CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp_inv_app_f`, `CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_sub_f`, `CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_zero_f`, `CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_neg_f`, `h_assoc`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso_inv_app_f`, `CategoryTheory.Endofunctor.Coalgebra.forget_map`, `CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId_inv_app_f`, `CategoryTheory.Endofunctor.Coalgebra.isoMk_hom_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_map_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_counitIso_inv_app_f`, `CategoryTheory.Endofunctor.Coalgebra.isoMk_inv_f`, `CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_zsmul_f`, `CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso_hom_app_f`, `CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq_hom_app_f`, `h`, `ext_iff`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_counitIso_hom_app_f`, `CategoryTheory.Endofunctor.Coalgebra.ext_iff`, `CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_map_f`, `CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId_hom_app_f`, `CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_add_f`, `CategoryTheory.Endofunctor.Adjunction.Coalgebra.homEquiv_naturality_str_symm`, `CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq_inv_app_f`, `CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_nsmul_f`, `CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_map_f`, `CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans_map_f`, `CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp_hom_app_f`, `CategoryTheory.Endofunctor.Coalgebra.comp_f`, `CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_map_f`
`id` 📖	CompOp	1 math math: `CategoryTheory.Endofunctor.Coalgebra.id_eq_id`
`instInhabited` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`f`	—	—	—
`ext_iff` 📖	mathematical	—	`f`	—	`ext`
`h` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Endofunctor.Coalgebra.V` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra.str` `CategoryTheory.Functor.map` `f`	—	—
`h_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Endofunctor.Coalgebra.V` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra.str` `CategoryTheory.Functor.map` `f`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `h`

CategoryTheory.Endofunctor.Coalgebra.Terminal

Definitions

Name	Category	Theorems
`strInv` 📖	CompOp	3 math math: `left_inv`, `right_inv`, `right_inv'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`left_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra.V` `strInv` `CategoryTheory.Endofunctor.Coalgebra.str` `CategoryTheory.CategoryStruct.id`	—	`strInv.eq_1` `CategoryTheory.Endofunctor.Coalgebra.Hom.h` `CategoryTheory.Functor.map_id` `CategoryTheory.Functor.map_comp` `right_inv`
`right_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Endofunctor.Coalgebra.V` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra.str` `strInv` `CategoryTheory.CategoryStruct.id`	—	`right_inv'`
`right_inv'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Endofunctor.Coalgebra.V` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra.str` `strInv` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Endofunctor.Coalgebra` `CategoryTheory.Endofunctor.Coalgebra.instCategoryStruct`	—	`CategoryTheory.Limits.IsTerminal.hom_ext`
`str_isIso` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Endofunctor.Coalgebra.V` `CategoryTheory.Functor.obj` `CategoryTheory.Endofunctor.Coalgebra.str`	—	`right_inv` `left_inv`

---

← Back to Index