Basic

📁 Source: Mathlib/Algebra/Category/CoalgCat/Basic.lean

Statistics

Metric	Count
Definitions toCoalgEquiv, CoalgCat, toCoalgHom, toCoalgHom', category, concreteCategory, hasForgetToModule, instCoalgebra, instCoeSortType, of, ofHom, toModuleCat, toCoalgIso	13
Theorems toCoalgEquiv_refl, toCoalgEquiv_symm, toCoalgEquiv_toCoalgHom, toCoalgEquiv_trans, ext, ext_iff, toCoalgHom_injective, forget_reflects_isos, forget₂_map, forget₂_obj, hom_ext, hom_ext_iff, moduleCat_of_toModuleCat, of_comul, of_counit, toCoalgHom_comp, toCoalgHom_id, toCoalgIso_hom, toCoalgIso_inv, toCoalgIso_refl, toCoalgIso_symm, toCoalgIso_trans	22
Total	35

CategoryTheory.Iso

Definitions

Name	Category	Theorems
toCoalgEquiv 📖	CompOp	4 math math: toCoalgEquiv_symm, toCoalgEquiv_toCoalgHom, toCoalgEquiv_refl, toCoalgEquiv_trans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toCoalgEquiv_refl 📖	mathematical	—	toCoalgEquiv refl CoalgCat CoalgCat.category CoalgEquiv.refl ModuleCat.carrier CommRing.toRing CoalgCat.toModuleCat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct CoalgCat.instCoalgebra	—	—
toCoalgEquiv_symm 📖	mathematical	—	toCoalgEquiv symm CoalgCat CoalgCat.category CoalgEquiv.symm ModuleCat.carrier CommRing.toRing CoalgCat.toModuleCat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct CoalgCat.instCoalgebra	—	—
toCoalgEquiv_toCoalgHom 📖	mathematical	—	CoalgHomClass.toCoalgHom ModuleCat.carrier CommRing.toRing CoalgCat.toModuleCat CoalgEquiv CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct CoalgCat.instCoalgebra CoalgEquiv.instFunLike CoalgEquivClass.toCoalgHomClass CoalgEquiv.instEquivLike CoalgEquiv.instCoalgEquivClass toCoalgEquiv CoalgCat.Hom.toCoalgHom hom CoalgCat CoalgCat.category	—	CoalgEquivClass.toCoalgHomClass CoalgEquiv.instCoalgEquivClass
toCoalgEquiv_trans 📖	mathematical	—	toCoalgEquiv trans CoalgCat CoalgCat.category CoalgEquiv.trans ModuleCat.carrier CommRing.toRing CoalgCat.toModuleCat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct CoalgCat.instCoalgebra	—	—

CoalgCat

Definitions

Name	Category	Theorems
category 📖	CompOp	49 math math: CategoryTheory.Iso.toCoalgEquiv_symm, MonoidalCategoryAux.tensorHom_toLinearMap, MonoidalCategoryAux.associator_hom_toLinearMap, tensorObj_isAddCommGroup, CoalgEquiv.toCoalgIso_refl, comonEquivalence_inverse, MonoidalCategoryAux.counit_tensorObj_tensorObj_right, CategoryTheory.Iso.toCoalgEquiv_toCoalgHom, comonEquivalence_counitIso, tensorHom_def, MonoidalCategoryAux.comul_tensorObj_tensorObj_left, associator_def, BialgCat.forget₂_coalgebra_obj, MonoidalCategoryAux.tensorObj_comul, MonoidalCategory.inducingFunctorData_μIso, whiskerRight_def, MonoidalCategory.inducingFunctorData_εIso, tensorUnit_instCoalgebra, tensorUnit_carrier, CategoryTheory.Iso.toCoalgEquiv_refl, forget_reflects_isos, MonoidalCategoryAux.leftUnitor_hom_toLinearMap, comonEquivalence_functor, tensorUnit_isAddCommGroup, CoalgEquiv.toCoalgIso_inv, CategoryTheory.Iso.toCoalgEquiv_trans, comonEquivalence_unitIso, MonoidalCategoryAux.counit_tensorObj, MonoidalCategoryAux.counit_tensorObj_tensorObj_left, forget₂_obj, whiskerLeft_def, MonoidalCategoryAux.comul_tensorObj_tensorObj_right, forget₂_map, MonoidalCategoryAux.comul_tensorObj, toComon_map_hom, rightUnitor_def, BialgCat.forget₂_coalgebra_map, tensorObj_carrier, tensorObj_instCoalgebra, tensorObj_isModule, CoalgEquiv.toCoalgIso_symm, toCoalgHom_id, tensorUnit_isModule, toCoalgHom_comp, MonoidalCategoryAux.rightUnitor_hom_toLinearMap, leftUnitor_def, CoalgEquiv.toCoalgIso_trans, CoalgEquiv.toCoalgIso_hom, toComon_obj
concreteCategory 📖	CompOp	7 math math: BialgCat.forget₂_coalgebra_obj, MonoidalCategory.inducingFunctorData_μIso, MonoidalCategory.inducingFunctorData_εIso, forget_reflects_isos, forget₂_obj, forget₂_map, BialgCat.forget₂_coalgebra_map
hasForgetToModule 📖	CompOp	4 math math: MonoidalCategory.inducingFunctorData_μIso, MonoidalCategory.inducingFunctorData_εIso, forget₂_obj, forget₂_map
instCoalgebra 📖	CompOp	36 math math: CategoryTheory.Iso.toCoalgEquiv_symm, MonoidalCategoryAux.tensorHom_toLinearMap, MonoidalCategoryAux.associator_hom_toLinearMap, MonoidalCategoryAux.counit_tensorObj_tensorObj_right, CategoryTheory.Iso.toCoalgEquiv_toCoalgHom, tensorHom_def, MonoidalCategoryAux.comul_tensorObj_tensorObj_left, associator_def, BialgCat.forget₂_coalgebra_obj, MonoidalCategoryAux.tensorObj_comul, comul_def, MonoidalCategory.inducingFunctorData_μIso, whiskerRight_def, MonoidalCategory.inducingFunctorData_εIso, tensorUnit_instCoalgebra, CategoryTheory.Iso.toCoalgEquiv_refl, forget_reflects_isos, MonoidalCategoryAux.leftUnitor_hom_toLinearMap, Hom.toCoalgHom_injective, CategoryTheory.Iso.toCoalgEquiv_trans, MonoidalCategoryAux.counit_tensorObj, counit_def, MonoidalCategoryAux.counit_tensorObj_tensorObj_left, forget₂_obj, whiskerLeft_def, MonoidalCategoryAux.comul_tensorObj_tensorObj_right, forget₂_map, MonoidalCategoryAux.comul_tensorObj, toComon_map_hom, rightUnitor_def, BialgCat.forget₂_coalgebra_map, tensorObj_instCoalgebra, toCoalgHom_id, toCoalgHom_comp, MonoidalCategoryAux.rightUnitor_hom_toLinearMap, leftUnitor_def
instCoeSortType 📖	CompOp	—
of 📖	CompOp	18 math math: MonoidalCategoryAux.tensorHom_toLinearMap, of_comul, MonoidalCategoryAux.associator_hom_toLinearMap, CoalgEquiv.toCoalgIso_refl, MonoidalCategoryAux.counit_tensorObj_tensorObj_right, MonoidalCategoryAux.comul_tensorObj_tensorObj_left, BialgCat.forget₂_coalgebra_obj, MonoidalCategoryAux.leftUnitor_hom_toLinearMap, CoalgEquiv.toCoalgIso_inv, MonoidalCategoryAux.counit_tensorObj, MonoidalCategoryAux.counit_tensorObj_tensorObj_left, MonoidalCategoryAux.comul_tensorObj_tensorObj_right, MonoidalCategoryAux.comul_tensorObj, CoalgEquiv.toCoalgIso_symm, MonoidalCategoryAux.rightUnitor_hom_toLinearMap, of_counit, CoalgEquiv.toCoalgIso_trans, CoalgEquiv.toCoalgIso_hom
ofHom 📖	CompOp	7 math math: MonoidalCategoryAux.tensorHom_toLinearMap, tensorHom_def, whiskerRight_def, CoalgEquiv.toCoalgIso_inv, whiskerLeft_def, BialgCat.forget₂_coalgebra_map, CoalgEquiv.toCoalgIso_hom
toModuleCat 📖	CompOp	45 math math: CategoryTheory.Iso.toCoalgEquiv_symm, MonoidalCategoryAux.tensorHom_toLinearMap, of_comul, MonoidalCategoryAux.associator_hom_toLinearMap, tensorObj_isAddCommGroup, MonoidalCategoryAux.counit_tensorObj_tensorObj_right, CategoryTheory.Iso.toCoalgEquiv_toCoalgHom, moduleCat_of_toModuleCat, tensorHom_def, toComonObj_X, MonoidalCategoryAux.comul_tensorObj_tensorObj_left, associator_def, BialgCat.forget₂_coalgebra_obj, MonoidalCategoryAux.tensorObj_comul, comul_def, MonoidalCategory.inducingFunctorData_μIso, whiskerRight_def, MonoidalCategory.inducingFunctorData_εIso, tensorUnit_carrier, CategoryTheory.Iso.toCoalgEquiv_refl, forget_reflects_isos, MonoidalCategoryAux.leftUnitor_hom_toLinearMap, tensorUnit_isAddCommGroup, Hom.toCoalgHom_injective, CategoryTheory.Iso.toCoalgEquiv_trans, MonoidalCategoryAux.counit_tensorObj, counit_def, MonoidalCategoryAux.counit_tensorObj_tensorObj_left, forget₂_obj, whiskerLeft_def, MonoidalCategoryAux.comul_tensorObj_tensorObj_right, forget₂_map, MonoidalCategoryAux.comul_tensorObj, toComon_map_hom, rightUnitor_def, BialgCat.forget₂_coalgebra_map, tensorObj_carrier, tensorObj_instCoalgebra, tensorObj_isModule, toCoalgHom_id, tensorUnit_isModule, toCoalgHom_comp, MonoidalCategoryAux.rightUnitor_hom_toLinearMap, leftUnitor_def, of_counit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forget_reflects_isos 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms CoalgCat category CategoryTheory.types CategoryTheory.forget CoalgHom ModuleCat.carrier CommRing.toRing toModuleCat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct instCoalgebra CoalgHom.funLike concreteCategory	—	Equiv.left_inv Equiv.right_inv CategoryTheory.IsIso.out CategoryTheory.Iso.isIso_hom
forget₂_map 📖	mathematical	—	CategoryTheory.Functor.map CoalgCat category ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.forget₂ CoalgHom ModuleCat.carrier toModuleCat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct instCoalgebra CoalgHom.funLike concreteCategory LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier hasForgetToModule ModuleCat.ofHom SemilinearMapClass.semilinearMap CommSemiring.toSemiring Hom.toCoalgHom CoalgHomClass.toSemilinearMapClass CoalgHom.coalgHomClass	—	—
forget₂_obj 📖	mathematical	—	CategoryTheory.Functor.obj CoalgCat category ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.forget₂ CoalgHom ModuleCat.carrier toModuleCat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct instCoalgebra CoalgHom.funLike concreteCategory LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier hasForgetToModule ModuleCat.of	—	—
hom_ext 📖	—	Hom.toCoalgHom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.toCoalgHom	—	hom_ext
moduleCat_of_toModuleCat 📖	mathematical	—	ModuleCat.of CommRing.toRing ModuleCat.carrier toModuleCat ModuleCat.isAddCommGroup ModuleCat.isModule	—	—
of_comul 📖	mathematical	—	CoalgebraStruct.comul ModuleCat.carrier CommRing.toRing toModuleCat of CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Coalgebra.toCoalgebraStruct	—	—
of_counit 📖	mathematical	—	CoalgebraStruct.counit ModuleCat.carrier CommRing.toRing toModuleCat of CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Coalgebra.toCoalgebraStruct	—	—
toCoalgHom_comp 📖	mathematical	—	Hom.toCoalgHom CategoryTheory.CategoryStruct.comp CoalgCat CategoryTheory.Category.toCategoryStruct category CoalgHom.comp ModuleCat.carrier CommRing.toRing toModuleCat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct instCoalgebra	—	—
toCoalgHom_id 📖	mathematical	—	Hom.toCoalgHom CategoryTheory.CategoryStruct.id CoalgCat CategoryTheory.Category.toCategoryStruct category CoalgHom.id ModuleCat.carrier CommRing.toRing toModuleCat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct instCoalgebra	—	—

CoalgCat.Hom

Definitions

Name	Category	Theorems
toCoalgHom 📖	CompOp	5 math math: CategoryTheory.Iso.toCoalgEquiv_toCoalgHom, CoalgCat.forget₂_map, CoalgCat.toCoalgHom_id, CoalgCat.toCoalgHom_comp, CoalgCat.hom_ext_iff
toCoalgHom' 📖	CompOp	10 math math: CoalgCat.MonoidalCategoryAux.tensorHom_toLinearMap, CoalgCat.MonoidalCategoryAux.associator_hom_toLinearMap, ext_iff, CoalgCat.tensorHom_def, CoalgCat.whiskerRight_def, CoalgCat.MonoidalCategoryAux.leftUnitor_hom_toLinearMap, toCoalgHom_injective, CoalgCat.whiskerLeft_def, CoalgCat.toComon_map_hom, CoalgCat.MonoidalCategoryAux.rightUnitor_hom_toLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	toCoalgHom'	—	—	—
ext_iff 📖	mathematical	—	toCoalgHom'	—	ext
toCoalgHom_injective 📖	mathematical	—	CoalgCat.Hom CoalgHom ModuleCat.carrier CommRing.toRing CoalgCat.toModuleCat CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct CoalgCat.instCoalgebra toCoalgHom'	—	—

CoalgEquiv

Definitions

Name	Category	Theorems
toCoalgIso 📖	CompOp	8 math math: toCoalgIso_refl, CoalgCat.associator_def, toCoalgIso_inv, CoalgCat.rightUnitor_def, toCoalgIso_symm, CoalgCat.leftUnitor_def, toCoalgIso_trans, toCoalgIso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toCoalgIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CoalgCat CoalgCat.category CoalgCat.of toCoalgIso CoalgCat.ofHom CoalgHomClass.toCoalgHom CoalgEquiv CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Coalgebra.toCoalgebraStruct instFunLike	—	—
toCoalgIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CoalgCat CoalgCat.category CoalgCat.of toCoalgIso CoalgCat.ofHom CoalgHomClass.toCoalgHom CoalgEquiv CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Coalgebra.toCoalgebraStruct instFunLike symm	—	—
toCoalgIso_refl 📖	mathematical	—	toCoalgIso refl CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Coalgebra.toCoalgebraStruct CategoryTheory.Iso.refl CoalgCat CoalgCat.category CoalgCat.of	—	—
toCoalgIso_symm 📖	mathematical	—	toCoalgIso symm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Coalgebra.toCoalgebraStruct CategoryTheory.Iso.symm CoalgCat CoalgCat.category CoalgCat.of	—	—
toCoalgIso_trans 📖	mathematical	—	toCoalgIso trans CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Coalgebra.toCoalgebraStruct CategoryTheory.Iso.trans CoalgCat CoalgCat.category CoalgCat.of	—	—

(root)

Definitions

Name	Category	Theorems
CoalgCat 📖	CompData	49 math math: CategoryTheory.Iso.toCoalgEquiv_symm, CoalgCat.MonoidalCategoryAux.tensorHom_toLinearMap, CoalgCat.MonoidalCategoryAux.associator_hom_toLinearMap, CoalgCat.tensorObj_isAddCommGroup, CoalgEquiv.toCoalgIso_refl, CoalgCat.comonEquivalence_inverse, CoalgCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_right, CategoryTheory.Iso.toCoalgEquiv_toCoalgHom, CoalgCat.comonEquivalence_counitIso, CoalgCat.tensorHom_def, CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_left, CoalgCat.associator_def, BialgCat.forget₂_coalgebra_obj, CoalgCat.MonoidalCategoryAux.tensorObj_comul, CoalgCat.MonoidalCategory.inducingFunctorData_μIso, CoalgCat.whiskerRight_def, CoalgCat.MonoidalCategory.inducingFunctorData_εIso, CoalgCat.tensorUnit_instCoalgebra, CoalgCat.tensorUnit_carrier, CategoryTheory.Iso.toCoalgEquiv_refl, CoalgCat.forget_reflects_isos, CoalgCat.MonoidalCategoryAux.leftUnitor_hom_toLinearMap, CoalgCat.comonEquivalence_functor, CoalgCat.tensorUnit_isAddCommGroup, CoalgEquiv.toCoalgIso_inv, CategoryTheory.Iso.toCoalgEquiv_trans, CoalgCat.comonEquivalence_unitIso, CoalgCat.MonoidalCategoryAux.counit_tensorObj, CoalgCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_left, CoalgCat.forget₂_obj, CoalgCat.whiskerLeft_def, CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_right, CoalgCat.forget₂_map, CoalgCat.MonoidalCategoryAux.comul_tensorObj, CoalgCat.toComon_map_hom, CoalgCat.rightUnitor_def, BialgCat.forget₂_coalgebra_map, CoalgCat.tensorObj_carrier, CoalgCat.tensorObj_instCoalgebra, CoalgCat.tensorObj_isModule, CoalgEquiv.toCoalgIso_symm, CoalgCat.toCoalgHom_id, CoalgCat.tensorUnit_isModule, CoalgCat.toCoalgHom_comp, CoalgCat.MonoidalCategoryAux.rightUnitor_hom_toLinearMap, CoalgCat.leftUnitor_def, CoalgEquiv.toCoalgIso_trans, CoalgEquiv.toCoalgIso_hom, CoalgCat.toComon_obj

---

← Back to Index