CommBialgCat

📁 Source: Mathlib/Algebra/Category/CommBialgCat.lean

Statistics

Metric	Count
Definitions monObjOpOf, CommBialgCat, hom, hom, hom', bialgEquivOfIso, bialgebra, carrier, commRing, hasForgetToCommAlgCat, instBialgebraObjForgetBialgHomCarrier, instCategory, instCoeSortType, instCommRingObjForgetBialgHomCarrier, instConcreteCategoryBialgHomCarrier, instInhabited, isoEquivBialgEquiv, isoMk, of, ofHom, ofSelfIso, commBialgCatEquivComonCommAlgCat, instBialgebraCarrierUnopCommAlgCatOfMonObjOpposite	23
Theorems mul_op_of_unop_hom, one_op_of_unop_hom, ext, ext_iff, bialgEquivOfIso_apply, bialgEquivOfIso_symm_apply, coe_of, comp_apply, forget_map, forget_obj, forget₂_commAlgCat_map, forget₂_commAlgCat_obj, hom_comp, hom_ext, hom_ext_iff, hom_id, hom_inv_apply, hom_ofHom, id_apply, inv_hom_apply, isoEquivBialgEquiv_apply, isoEquivBialgEquiv_symm_apply, isoMk_hom, isoMk_inv, ofHom_apply, ofHom_comp, ofHom_hom, ofHom_id, ofSelfIso_hom, ofSelfIso_inv, reflectsIsomorphisms_forget, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, commBialgCatEquivComonCommAlgCat_counitIso_inv_app, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, commBialgCatEquivComonCommAlgCat_functor_obj_unop_X, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, commBialgCatEquivComonCommAlgCat_inverse_obj, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, instIsCommMonObjOppositeCommAlgCatOpOfOfIsCocomm, instIsCommMonObjOppositeCommAlgCatXUnopMonObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier, instIsMonHomOppositeCommAlgCatOpOfHomToAlgHomBialgHom	42
Total	65

CommAlgCat

Definitions

Name	Category	Theorems
monObjOpOf 📖	CompOp	8 math math: commBialgCatEquivComonCommAlgCat_unitIso_inv_app, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, mul_op_of_unop_hom, instIsMonHomOppositeCommAlgCatOpOfHomToAlgHomBialgHom, one_op_of_unop_hom, instIsCommMonObjOppositeCommAlgCatOpOfOfIsCocomm, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, commBialgCatEquivComonCommAlgCat_counitIso_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_op_of_unop_hom 📖	mathematical	—	Hom.hom Opposite.unop CommAlgCat Opposite.op of Bialgebra.toAlgebra CommRing.toCommSemiring CommSemiring.toSemiring CategoryTheory.MonoidalCategoryStruct.tensorObj Opposite CategoryTheory.Category.opposite instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp instMonoidalCategory Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonObj.mul monObjOpOf Bialgebra.comulAlgHom	—	—
one_op_of_unop_hom 📖	mathematical	—	Hom.hom Opposite.unop CommAlgCat Opposite.op of Bialgebra.toAlgebra CommRing.toCommSemiring CommSemiring.toSemiring CategoryTheory.MonoidalCategoryStruct.tensorUnit Opposite CategoryTheory.Category.opposite instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.monoidalCategoryOp instMonoidalCategory Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonObj.one monObjOpOf Bialgebra.counitAlgHom	—	—

CommBialgCat

Definitions

Name	Category	Theorems
bialgEquivOfIso 📖	CompOp	3 math math: isoEquivBialgEquiv_apply, bialgEquivOfIso_apply, bialgEquivOfIso_symm_apply
bialgebra 📖	CompOp	24 math math: ofSelfIso_inv, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, id_apply, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, forget₂_commAlgCat_obj, bialgEquivOfIso_apply, commBialgCatEquivComonCommAlgCat_functor_obj_unop_X, reflectsIsomorphisms_forget, ofHom_hom, inv_hom_apply, hom_inv_apply, ofSelfIso_hom, comp_apply, bialgEquivOfIso_symm_apply, forget_obj, ofHom_apply, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, forget_map, forget₂_commAlgCat_map, hom_id, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, hom_comp, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, commBialgCatEquivComonCommAlgCat_counitIso_inv_app
carrier 📖	CompOp	25 math math: ofSelfIso_inv, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, id_apply, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, forget₂_commAlgCat_obj, bialgEquivOfIso_apply, commBialgCatEquivComonCommAlgCat_functor_obj_unop_X, reflectsIsomorphisms_forget, ofHom_hom, inv_hom_apply, coe_of, hom_inv_apply, ofSelfIso_hom, comp_apply, bialgEquivOfIso_symm_apply, forget_obj, ofHom_apply, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, forget_map, forget₂_commAlgCat_map, hom_id, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, hom_comp, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, commBialgCatEquivComonCommAlgCat_counitIso_inv_app
commRing 📖	CompOp	24 math math: ofSelfIso_inv, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, id_apply, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, forget₂_commAlgCat_obj, bialgEquivOfIso_apply, commBialgCatEquivComonCommAlgCat_functor_obj_unop_X, reflectsIsomorphisms_forget, ofHom_hom, inv_hom_apply, hom_inv_apply, ofSelfIso_hom, comp_apply, bialgEquivOfIso_symm_apply, forget_obj, ofHom_apply, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, forget_map, forget₂_commAlgCat_map, hom_id, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, hom_comp, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, commBialgCatEquivComonCommAlgCat_counitIso_inv_app
hasForgetToCommAlgCat 📖	CompOp	2 math math: forget₂_commAlgCat_obj, forget₂_commAlgCat_map
instBialgebraObjForgetBialgHomCarrier 📖	CompOp	—
instCategory 📖	CompOp	31 math math: ofSelfIso_inv, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, id_apply, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, isoEquivBialgEquiv_apply, ofHom_comp, forget₂_commAlgCat_obj, bialgEquivOfIso_apply, commBialgCatEquivComonCommAlgCat_functor_obj_unop_X, reflectsIsomorphisms_forget, inv_hom_apply, hom_inv_apply, isoEquivBialgEquiv_symm_apply, instIsCommMonObjOppositeCommAlgCatXUnopMonObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier, ofSelfIso_hom, comp_apply, bialgEquivOfIso_symm_apply, isoMk_hom, forget_obj, ofHom_apply, commBialgCatEquivComonCommAlgCat_inverse_obj, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, isoMk_inv, forget_map, ofHom_id, forget₂_commAlgCat_map, hom_id, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, hom_comp, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, commBialgCatEquivComonCommAlgCat_counitIso_inv_app
instCoeSortType 📖	CompOp	—
instCommRingObjForgetBialgHomCarrier 📖	CompOp	—
instConcreteCategoryBialgHomCarrier 📖	CompOp	12 math math: id_apply, forget₂_commAlgCat_obj, bialgEquivOfIso_apply, reflectsIsomorphisms_forget, inv_hom_apply, hom_inv_apply, comp_apply, bialgEquivOfIso_symm_apply, forget_obj, ofHom_apply, forget_map, forget₂_commAlgCat_map
instInhabited 📖	CompOp	—
isoEquivBialgEquiv 📖	CompOp	2 math math: isoEquivBialgEquiv_apply, isoEquivBialgEquiv_symm_apply
isoMk 📖	CompOp	3 math math: isoEquivBialgEquiv_symm_apply, isoMk_hom, isoMk_inv
of 📖	CompOp	16 math math: ofSelfIso_inv, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, isoEquivBialgEquiv_apply, ofHom_comp, coe_of, isoEquivBialgEquiv_symm_apply, ofSelfIso_hom, isoMk_hom, ofHom_apply, commBialgCatEquivComonCommAlgCat_inverse_obj, hom_ofHom, isoMk_inv, ofHom_id, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, commBialgCatEquivComonCommAlgCat_counitIso_inv_app
ofHom 📖	CompOp	11 math math: commBialgCatEquivComonCommAlgCat_unitIso_inv_app, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, ofHom_comp, ofHom_hom, isoMk_hom, ofHom_apply, hom_ofHom, isoMk_inv, ofHom_id, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, commBialgCatEquivComonCommAlgCat_counitIso_inv_app
ofSelfIso 📖	CompOp	2 math math: ofSelfIso_inv, ofSelfIso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bialgEquivOfIso_apply 📖	mathematical	—	DFunLike.coe BialgEquiv CommRing.toCommSemiring carrier CommSemiring.toSemiring commRing Bialgebra.toAlgebra bialgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgEquiv.instFunLike bialgEquivOfIso CategoryTheory.ConcreteCategory.hom CommBialgCat instCategory BialgHom BialgHom.funLike NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instConcreteCategoryBialgHomCarrier CategoryTheory.Iso.hom	—	—
bialgEquivOfIso_symm_apply 📖	mathematical	—	DFunLike.coe CoalgEquiv CommRing.toCommSemiring carrier NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commRing Algebra.toModule Bialgebra.toAlgebra bialgebra Coalgebra.toCoalgebraStruct Bialgebra.toCoalgebra CoalgEquiv.instFunLike CoalgEquiv.symm BialgEquiv.toCoalgEquiv bialgEquivOfIso CategoryTheory.ConcreteCategory.hom CommBialgCat instCategory BialgHom BialgHom.funLike NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instConcreteCategoryBialgHomCarrier CategoryTheory.Iso.inv	—	—
coe_of 📖	mathematical	—	carrier of	—	—
comp_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom CommBialgCat instCategory BialgHom CommRing.toCommSemiring CommSemiring.toSemiring commRing Bialgebra.toAlgebra bialgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instConcreteCategoryBialgHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
forget_map 📖	mathematical	—	CategoryTheory.Functor.map CommBialgCat instCategory CategoryTheory.types CategoryTheory.forget BialgHom carrier CommRing.toCommSemiring CommSemiring.toSemiring commRing Bialgebra.toAlgebra bialgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instConcreteCategoryBialgHomCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj CommBialgCat instCategory CategoryTheory.types CategoryTheory.forget BialgHom carrier CommRing.toCommSemiring CommSemiring.toSemiring commRing Bialgebra.toAlgebra bialgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instConcreteCategoryBialgHomCarrier	—	—
forget₂_commAlgCat_map 📖	mathematical	—	CategoryTheory.Functor.map CommBialgCat instCategory CommAlgCat CommAlgCat.instCategory CategoryTheory.forget₂ BialgHom carrier CommRing.toCommSemiring CommSemiring.toSemiring commRing Bialgebra.toAlgebra bialgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instConcreteCategoryBialgHomCarrier AlgHom CommAlgCat.carrier CommAlgCat.commRing CommAlgCat.algebra AlgHom.funLike CommAlgCat.instConcreteCategoryAlgHomCarrier hasForgetToCommAlgCat CommAlgCat.ofHom AlgHomClass.toAlgHom BialgHomClass.toAlgHomClass BialgHom.bialgHomClass Hom.hom	—	—
forget₂_commAlgCat_obj 📖	mathematical	—	CategoryTheory.Functor.obj CommBialgCat instCategory CommAlgCat CommAlgCat.instCategory CategoryTheory.forget₂ BialgHom carrier CommRing.toCommSemiring CommSemiring.toSemiring commRing Bialgebra.toAlgebra bialgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instConcreteCategoryBialgHomCarrier AlgHom CommAlgCat.carrier CommAlgCat.commRing CommAlgCat.algebra AlgHom.funLike CommAlgCat.instConcreteCategoryAlgHomCarrier hasForgetToCommAlgCat CommAlgCat.of	—	—
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp CommBialgCat CategoryTheory.Category.toCategoryStruct instCategory BialgHom.comp carrier CommRing.toCommSemiring CommSemiring.toSemiring commRing Bialgebra.toAlgebra bialgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_id 📖	mathematical	—	AlgHomClass.toAlgHom carrier CommRing.toCommSemiring CommSemiring.toSemiring commRing Bialgebra.toAlgebra bialgebra BialgHom Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike BialgHomClass.toAlgHomClass BialgHom.bialgHomClass Hom.hom CategoryTheory.CategoryStruct.id CommBialgCat CategoryTheory.Category.toCategoryStruct instCategory AlgHom.id	—	BialgHomClass.toAlgHomClass BialgHom.bialgHomClass
hom_inv_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom CommBialgCat instCategory BialgHom CommRing.toCommSemiring CommSemiring.toSemiring commRing Bialgebra.toAlgebra bialgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instConcreteCategoryBialgHomCarrier CategoryTheory.Iso.hom CategoryTheory.Iso.inv	—	CategoryTheory.Iso.inv_hom_id_apply
hom_ofHom 📖	mathematical	—	Hom.hom of ofHom	—	—
id_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom CommBialgCat instCategory BialgHom CommRing.toCommSemiring CommSemiring.toSemiring commRing Bialgebra.toAlgebra bialgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instConcreteCategoryBialgHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.id_apply
inv_hom_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom CommBialgCat instCategory BialgHom CommRing.toCommSemiring CommSemiring.toSemiring commRing Bialgebra.toAlgebra bialgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instConcreteCategoryBialgHomCarrier CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id_apply
isoEquivBialgEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Iso CommBialgCat instCategory of BialgEquiv CommRing.toCommSemiring CommSemiring.toSemiring Bialgebra.toAlgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra EquivLike.toFunLike Equiv.instEquivLike isoEquivBialgEquiv bialgEquivOfIso	—	—
isoEquivBialgEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv BialgEquiv CommRing.toCommSemiring CommSemiring.toSemiring Bialgebra.toAlgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra CategoryTheory.Iso CommBialgCat instCategory of EquivLike.toFunLike Equiv.instEquivLike Equiv.symm isoEquivBialgEquiv isoMk	—	—
isoMk_hom 📖	mathematical	—	CategoryTheory.Iso.hom CommBialgCat instCategory of isoMk ofHom BialgHomClass.toBialgHom BialgEquiv CommRing.toCommSemiring CommSemiring.toSemiring Bialgebra.toAlgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgEquiv.instFunLike	—	—
isoMk_inv 📖	mathematical	—	CategoryTheory.Iso.inv CommBialgCat instCategory of isoMk ofHom BialgHomClass.toBialgHom BialgEquiv CommRing.toCommSemiring CommSemiring.toSemiring Bialgebra.toAlgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgEquiv.instFunLike BialgEquiv.symm	—	—
ofHom_apply 📖	mathematical	—	DFunLike.coe of carrier CategoryTheory.ConcreteCategory.hom CommBialgCat instCategory BialgHom CommRing.toCommSemiring CommSemiring.toSemiring commRing Bialgebra.toAlgebra bialgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instConcreteCategoryBialgHomCarrier ofHom	—	—
ofHom_comp 📖	mathematical	—	ofHom BialgHom.comp CommRing.toCommSemiring CommSemiring.toSemiring Bialgebra.toAlgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra CategoryTheory.CategoryStruct.comp CommBialgCat CategoryTheory.Category.toCategoryStruct instCategory of	—	—
ofHom_hom 📖	mathematical	—	ofHom carrier commRing bialgebra Hom.hom	—	—
ofHom_id 📖	mathematical	—	ofHom BialgHom.id CommRing.toCommSemiring CommSemiring.toSemiring Bialgebra.toAlgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra CategoryTheory.CategoryStruct.id CommBialgCat CategoryTheory.Category.toCategoryStruct instCategory of	—	—
ofSelfIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CommBialgCat instCategory of carrier commRing bialgebra ofSelfIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
ofSelfIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CommBialgCat instCategory of carrier commRing bialgebra ofSelfIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
reflectsIsomorphisms_forget 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms CommBialgCat instCategory CategoryTheory.types CategoryTheory.forget BialgHom carrier CommRing.toCommSemiring CommSemiring.toSemiring commRing Bialgebra.toAlgebra bialgebra Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instConcreteCategoryBialgHomCarrier	—	Equiv.left_inv Equiv.right_inv BialgHom.map_mul' CategoryTheory.Iso.isIso_hom

CommBialgCat.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	12 math math: commBialgCatEquivComonCommAlgCat_unitIso_inv_app, CommBialgCat.hom_ext_iff, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, CommBialgCat.ofHom_hom, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, CommBialgCat.hom_ofHom, CommBialgCat.forget₂_commAlgCat_map, CommBialgCat.hom_id, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, CommBialgCat.hom_comp, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, commBialgCatEquivComonCommAlgCat_counitIso_inv_app
hom' 📖	CompOp	1 math math: ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	hom'	—	—	—
ext_iff 📖	mathematical	—	hom'	—	ext

CommBialgCat.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
CommBialgCat 📖	CompData	31 math math: CommBialgCat.ofSelfIso_inv, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, CommBialgCat.id_apply, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, CommBialgCat.isoEquivBialgEquiv_apply, CommBialgCat.ofHom_comp, CommBialgCat.forget₂_commAlgCat_obj, CommBialgCat.bialgEquivOfIso_apply, commBialgCatEquivComonCommAlgCat_functor_obj_unop_X, CommBialgCat.reflectsIsomorphisms_forget, CommBialgCat.inv_hom_apply, CommBialgCat.hom_inv_apply, CommBialgCat.isoEquivBialgEquiv_symm_apply, instIsCommMonObjOppositeCommAlgCatXUnopMonObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier, CommBialgCat.ofSelfIso_hom, CommBialgCat.comp_apply, CommBialgCat.bialgEquivOfIso_symm_apply, CommBialgCat.isoMk_hom, CommBialgCat.forget_obj, CommBialgCat.ofHom_apply, commBialgCatEquivComonCommAlgCat_inverse_obj, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, CommBialgCat.isoMk_inv, CommBialgCat.forget_map, CommBialgCat.ofHom_id, CommBialgCat.forget₂_commAlgCat_map, CommBialgCat.hom_id, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, CommBialgCat.hom_comp, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, commBialgCatEquivComonCommAlgCat_counitIso_inv_app
commBialgCatEquivComonCommAlgCat 📖	CompOp	9 math math: commBialgCatEquivComonCommAlgCat_unitIso_inv_app, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, commBialgCatEquivComonCommAlgCat_functor_obj_unop_X, instIsCommMonObjOppositeCommAlgCatXUnopMonObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier, commBialgCatEquivComonCommAlgCat_inverse_obj, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, commBialgCatEquivComonCommAlgCat_counitIso_inv_app
instBialgebraCarrierUnopCommAlgCatOfMonObjOpposite 📖	CompOp	5 math math: commBialgCatEquivComonCommAlgCat_unitIso_inv_app, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, commBialgCatEquivComonCommAlgCat_inverse_obj, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, commBialgCatEquivComonCommAlgCat_counitIso_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commBialgCatEquivComonCommAlgCat_counitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Mon CommAlgCat CategoryTheory.Category.opposite CommAlgCat.instCategory CategoryTheory.monoidalCategoryOp CommAlgCat.instMonoidalCategory CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CommBialgCat CommBialgCat.instCategory CommBialgCat.of CommAlgCat.carrier Opposite.unop CategoryTheory.Mon.X CommAlgCat.commRing instBialgebraCarrierUnopCommAlgCatOfMonObjOpposite CategoryTheory.Mon.mon CommBialgCat.ofHom BialgHom.ofAlgHom CommRing.toCommSemiring CommSemiring.toSemiring CommAlgCat.Hom.hom Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.Hom.hom Opposite.op CommAlgCat.of CommBialgCat.carrier CommBialgCat.commRing Bialgebra.toAlgebra CommBialgCat.bialgebra CommAlgCat.monObjOpOf Quiver.Hom.op CategoryTheory.Mon.Hom.mk' CommAlgCat.ofHom AlgHomClass.toAlgHom BialgHom Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike CommBialgCat.Hom.hom CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Equivalence.counitIso commBialgCatEquivComonCommAlgCat CategoryTheory.CategoryStruct.id	—	—
commBialgCatEquivComonCommAlgCat_counitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Mon CommAlgCat CategoryTheory.Category.opposite CommAlgCat.instCategory CategoryTheory.monoidalCategoryOp CommAlgCat.instMonoidalCategory CategoryTheory.Mon.instCategory CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CommBialgCat CommBialgCat.instCategory CommBialgCat.of CommAlgCat.carrier Opposite.unop CategoryTheory.Mon.X CommAlgCat.commRing instBialgebraCarrierUnopCommAlgCatOfMonObjOpposite CategoryTheory.Mon.mon CommBialgCat.ofHom BialgHom.ofAlgHom CommRing.toCommSemiring CommSemiring.toSemiring CommAlgCat.Hom.hom Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.Hom.hom Opposite.op CommAlgCat.of CommBialgCat.carrier CommBialgCat.commRing Bialgebra.toAlgebra CommBialgCat.bialgebra CommAlgCat.monObjOpOf Quiver.Hom.op CategoryTheory.Mon.Hom.mk' CommAlgCat.ofHom AlgHomClass.toAlgHom BialgHom Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike CommBialgCat.Hom.hom CategoryTheory.Equivalence.counitIso commBialgCatEquivComonCommAlgCat CategoryTheory.CategoryStruct.id	—	—
commBialgCatEquivComonCommAlgCat_functor_map_unop_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom Opposite CommAlgCat CategoryTheory.Category.opposite CommAlgCat.instCategory CategoryTheory.monoidalCategoryOp CommAlgCat.instMonoidalCategory Opposite.unop CategoryTheory.Mon CategoryTheory.Functor.obj CommBialgCat CommBialgCat.instCategory CategoryTheory.Mon.instCategory CategoryTheory.Equivalence.functor commBialgCatEquivComonCommAlgCat Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map Quiver.Hom.op CommAlgCat.of CommBialgCat.carrier CommBialgCat.commRing Bialgebra.toAlgebra CommRing.toCommSemiring CommSemiring.toSemiring CommBialgCat.bialgebra CommAlgCat.ofHom AlgHomClass.toAlgHom BialgHom Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike BialgHomClass.toAlgHomClass BialgHom.bialgHomClass CommBialgCat.Hom.hom	—	—
commBialgCatEquivComonCommAlgCat_functor_obj_unop_X 📖	mathematical	—	CategoryTheory.Mon.X Opposite CommAlgCat CategoryTheory.Category.opposite CommAlgCat.instCategory CategoryTheory.monoidalCategoryOp CommAlgCat.instMonoidalCategory Opposite.unop CategoryTheory.Mon CategoryTheory.Functor.obj CommBialgCat CommBialgCat.instCategory CategoryTheory.Mon.instCategory CategoryTheory.Equivalence.functor commBialgCatEquivComonCommAlgCat Opposite.op CommAlgCat.of CommBialgCat.carrier CommBialgCat.commRing Bialgebra.toAlgebra CommRing.toCommSemiring CommSemiring.toSemiring CommBialgCat.bialgebra	—	—
commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom 📖	mathematical	—	AlgHomClass.toAlgHom CommBialgCat.carrier CategoryTheory.Functor.obj Opposite CategoryTheory.Mon CommAlgCat CategoryTheory.Category.opposite CommAlgCat.instCategory CategoryTheory.monoidalCategoryOp CommAlgCat.instMonoidalCategory CategoryTheory.Mon.instCategory CommBialgCat CommBialgCat.instCategory CategoryTheory.Equivalence.inverse commBialgCatEquivComonCommAlgCat CommRing.toCommSemiring CommSemiring.toSemiring CommBialgCat.commRing Bialgebra.toAlgebra CommBialgCat.bialgebra BialgHom Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike BialgHomClass.toAlgHomClass BialgHom.bialgHomClass CommBialgCat.Hom.hom CategoryTheory.Functor.map CommAlgCat.Hom.hom Opposite.unop CategoryTheory.Mon.X Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.Hom.hom	—	BialgHomClass.toAlgHomClass BialgHom.bialgHomClass
commBialgCatEquivComonCommAlgCat_inverse_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Mon CommAlgCat CategoryTheory.Category.opposite CommAlgCat.instCategory CategoryTheory.monoidalCategoryOp CommAlgCat.instMonoidalCategory CategoryTheory.Mon.instCategory CommBialgCat CommBialgCat.instCategory CategoryTheory.Equivalence.inverse commBialgCatEquivComonCommAlgCat CommBialgCat.of CommAlgCat.carrier Opposite.unop CategoryTheory.Mon.X CommAlgCat.commRing instBialgebraCarrierUnopCommAlgCatOfMonObjOpposite CategoryTheory.Mon.mon	—	—
commBialgCatEquivComonCommAlgCat_unitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CommBialgCat CommBialgCat.instCategory CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp Opposite CategoryTheory.Mon CommAlgCat CategoryTheory.Category.opposite CommAlgCat.instCategory CategoryTheory.monoidalCategoryOp CommAlgCat.instMonoidalCategory CategoryTheory.Mon.instCategory Opposite.op CommAlgCat.of CommBialgCat.carrier CommBialgCat.commRing Bialgebra.toAlgebra CommRing.toCommSemiring CommSemiring.toSemiring CommBialgCat.bialgebra CommAlgCat.monObjOpOf Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.Hom.mk' CommAlgCat.ofHom AlgHomClass.toAlgHom BialgHom Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike CommBialgCat.Hom.hom CommBialgCat.of CommAlgCat.carrier Opposite.unop CategoryTheory.Mon.X CommAlgCat.commRing instBialgebraCarrierUnopCommAlgCatOfMonObjOpposite CategoryTheory.Mon.mon CommBialgCat.ofHom BialgHom.ofAlgHom CommAlgCat.Hom.hom Quiver.Hom.unop CategoryTheory.Mon.Hom.hom CategoryTheory.Equivalence.unitIso commBialgCatEquivComonCommAlgCat CategoryTheory.CategoryStruct.id	—	—
commBialgCatEquivComonCommAlgCat_unitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CommBialgCat CommBialgCat.instCategory CategoryTheory.Functor.comp Opposite CategoryTheory.Mon CommAlgCat CategoryTheory.Category.opposite CommAlgCat.instCategory CategoryTheory.monoidalCategoryOp CommAlgCat.instMonoidalCategory CategoryTheory.Mon.instCategory Opposite.op CommAlgCat.of CommBialgCat.carrier CommBialgCat.commRing Bialgebra.toAlgebra CommRing.toCommSemiring CommSemiring.toSemiring CommBialgCat.bialgebra CommAlgCat.monObjOpOf Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.Hom.mk' CommAlgCat.ofHom AlgHomClass.toAlgHom BialgHom Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike CommBialgCat.Hom.hom CommBialgCat.of CommAlgCat.carrier Opposite.unop CategoryTheory.Mon.X CommAlgCat.commRing instBialgebraCarrierUnopCommAlgCatOfMonObjOpposite CategoryTheory.Mon.mon CommBialgCat.ofHom BialgHom.ofAlgHom CommAlgCat.Hom.hom Quiver.Hom.unop CategoryTheory.Mon.Hom.hom CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Equivalence.unitIso commBialgCatEquivComonCommAlgCat CategoryTheory.CategoryStruct.id	—	—
instIsCommMonObjOppositeCommAlgCatOpOfOfIsCocomm 📖	mathematical	—	CategoryTheory.IsCommMonObj Opposite CommAlgCat CategoryTheory.Category.opposite CommAlgCat.instCategory CategoryTheory.monoidalCategoryOp CommAlgCat.instMonoidalCategory CategoryTheory.instBraidedCategoryOpposite CommAlgCat.instBraidedCategory Opposite.op CommAlgCat.of Bialgebra.toAlgebra CommRing.toCommSemiring CommSemiring.toSemiring CommAlgCat.monObjOpOf	—	CommAlgCat.hom_ext AlgHom.ext Coalgebra.comm_comul
instIsCommMonObjOppositeCommAlgCatXUnopMonObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier 📖	mathematical	—	CategoryTheory.IsCommMonObj Opposite CommAlgCat CategoryTheory.Category.opposite CommAlgCat.instCategory CategoryTheory.monoidalCategoryOp CommAlgCat.instMonoidalCategory CategoryTheory.instBraidedCategoryOpposite CommAlgCat.instBraidedCategory CategoryTheory.Mon.X Opposite.unop CategoryTheory.Mon CategoryTheory.Functor.obj CommBialgCat CommBialgCat.instCategory CategoryTheory.Mon.instCategory CategoryTheory.Equivalence.functor commBialgCatEquivComonCommAlgCat CategoryTheory.Mon.mon	—	instIsCommMonObjOppositeCommAlgCatOpOfOfIsCocomm
instIsMonHomOppositeCommAlgCatOpOfHomToAlgHomBialgHom 📖	mathematical	—	CategoryTheory.IsMonHom Opposite CommAlgCat CategoryTheory.Category.opposite CommAlgCat.instCategory CategoryTheory.monoidalCategoryOp CommAlgCat.instMonoidalCategory Opposite.op CommAlgCat.of Bialgebra.toAlgebra CommRing.toCommSemiring CommSemiring.toSemiring CommAlgCat.monObjOpOf Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CommAlgCat.ofHom AlgHomClass.toAlgHom BialgHom Coalgebra.toCoalgebraStruct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Bialgebra.toCoalgebra BialgHom.funLike BialgHomClass.toAlgHomClass BialgHom.bialgHomClass	—	BialgHomClass.toAlgHomClass BialgHom.bialgHomClass CommAlgCat.hom_ext AlgHom.ext BialgHomClass.counitAlgHom_comp BialgHomClass.map_comp_comulAlgHom

---

← Back to Index