Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `BialgCat`, `toBialgHom`, `toBialgHom'`, `carrier`, `category`, `concreteCategory`, `hasForgetToAlgebra`, `hasForgetToCoalgebra`, `instBialgebra`, `instCoeSortType`, `instRing`, `of`, `ofHom`, `toBialgIso`, `toBialgEquiv`	15
Theorems `ext`, `ext_iff`, `toBialgHom_injective`, `forget_reflects_isos`, `forget₂_algebra_map`, `forget₂_algebra_obj`, `forget₂_coalgebra_map`, `forget₂_coalgebra_obj`, `hom_ext`, `hom_ext_iff`, `of_carrier`, `of_comul`, `of_counit`, `of_instBialgebra`, `of_instRing`, `toBialgHom_comp`, `toBialgHom_id`, `toBialgIso_hom`, `toBialgIso_inv`, `toBialgIso_refl`, `toBialgIso_symm`, `toBialgIso_trans`, `toBialgEquiv_refl`, `toBialgEquiv_symm`, `toBialgEquiv_toBialgHom`, `toBialgEquiv_trans`	26
Total	41

BialgCat

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	28 math math: `rightUnitor_def`, `of_counit`, `associator_def`, `whiskerLeft_def`, `CategoryTheory.Iso.toBialgEquiv_refl`, `forget_reflects_isos`, `Hom.toBialgHom_injective`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_εIso`, `CategoryTheory.Iso.toBialgEquiv_trans`, `of_comul`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_μIso`, `forget₂_coalgebra_obj`, `tensorHom_def`, `forget₂_algebra_map`, `HopfAlgCat.forget₂_bialgebra_obj`, `CategoryTheory.Iso.toBialgEquiv_symm`, `whiskerRight_def`, `tensorObj_def`, `MonoidalCategory.inducingFunctorData_μIso`, `toBialgHom_id`, `of_carrier`, `HopfAlgCat.forget₂_bialgebra_map`, `forget₂_coalgebra_map`, `toBialgHom_comp`, `CategoryTheory.Iso.toBialgEquiv_toBialgHom`, `leftUnitor_def`, `forget₂_algebra_obj`, `MonoidalCategory.inducingFunctorData_εIso`
`category` 📖	CompOp	30 math math: `rightUnitor_def`, `BialgEquiv.toBialgIso_refl`, `associator_def`, `whiskerLeft_def`, `tensorUnit_def`, `CategoryTheory.Iso.toBialgEquiv_refl`, `forget_reflects_isos`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_εIso`, `CategoryTheory.Iso.toBialgEquiv_trans`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_μIso`, `forget₂_coalgebra_obj`, `tensorHom_def`, `forget₂_algebra_map`, `BialgEquiv.toBialgIso_symm`, `HopfAlgCat.forget₂_bialgebra_obj`, `CategoryTheory.Iso.toBialgEquiv_symm`, `whiskerRight_def`, `tensorObj_def`, `MonoidalCategory.inducingFunctorData_μIso`, `toBialgHom_id`, `HopfAlgCat.forget₂_bialgebra_map`, `BialgEquiv.toBialgIso_trans`, `forget₂_coalgebra_map`, `BialgEquiv.toBialgIso_hom`, `toBialgHom_comp`, `CategoryTheory.Iso.toBialgEquiv_toBialgHom`, `leftUnitor_def`, `forget₂_algebra_obj`, `MonoidalCategory.inducingFunctorData_εIso`, `BialgEquiv.toBialgIso_inv`
`concreteCategory` 📖	CompOp	11 math math: `forget_reflects_isos`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_εIso`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_μIso`, `forget₂_coalgebra_obj`, `forget₂_algebra_map`, `HopfAlgCat.forget₂_bialgebra_obj`, `MonoidalCategory.inducingFunctorData_μIso`, `HopfAlgCat.forget₂_bialgebra_map`, `forget₂_coalgebra_map`, `forget₂_algebra_obj`, `MonoidalCategory.inducingFunctorData_εIso`
`hasForgetToAlgebra` 📖	CompOp	4 math math: `forget₂_algebra_map`, `MonoidalCategory.inducingFunctorData_μIso`, `forget₂_algebra_obj`, `MonoidalCategory.inducingFunctorData_εIso`
`hasForgetToCoalgebra` 📖	CompOp	2 math math: `forget₂_coalgebra_obj`, `forget₂_coalgebra_map`
`instBialgebra` 📖	CompOp	28 math math: `rightUnitor_def`, `of_counit`, `associator_def`, `whiskerLeft_def`, `CategoryTheory.Iso.toBialgEquiv_refl`, `forget_reflects_isos`, `Hom.toBialgHom_injective`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_εIso`, `CategoryTheory.Iso.toBialgEquiv_trans`, `of_comul`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_μIso`, `forget₂_coalgebra_obj`, `tensorHom_def`, `forget₂_algebra_map`, `HopfAlgCat.forget₂_bialgebra_obj`, `CategoryTheory.Iso.toBialgEquiv_symm`, `whiskerRight_def`, `tensorObj_def`, `MonoidalCategory.inducingFunctorData_μIso`, `toBialgHom_id`, `HopfAlgCat.forget₂_bialgebra_map`, `of_instBialgebra`, `forget₂_coalgebra_map`, `toBialgHom_comp`, `CategoryTheory.Iso.toBialgEquiv_toBialgHom`, `leftUnitor_def`, `forget₂_algebra_obj`, `MonoidalCategory.inducingFunctorData_εIso`
`instCoeSortType` 📖	CompOp	—
`instRing` 📖	CompOp	28 math math: `rightUnitor_def`, `of_counit`, `associator_def`, `whiskerLeft_def`, `CategoryTheory.Iso.toBialgEquiv_refl`, `forget_reflects_isos`, `Hom.toBialgHom_injective`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_εIso`, `CategoryTheory.Iso.toBialgEquiv_trans`, `of_comul`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_μIso`, `forget₂_coalgebra_obj`, `tensorHom_def`, `forget₂_algebra_map`, `HopfAlgCat.forget₂_bialgebra_obj`, `CategoryTheory.Iso.toBialgEquiv_symm`, `whiskerRight_def`, `tensorObj_def`, `MonoidalCategory.inducingFunctorData_μIso`, `toBialgHom_id`, `HopfAlgCat.forget₂_bialgebra_map`, `forget₂_coalgebra_map`, `toBialgHom_comp`, `CategoryTheory.Iso.toBialgEquiv_toBialgHom`, `of_instRing`, `leftUnitor_def`, `forget₂_algebra_obj`, `MonoidalCategory.inducingFunctorData_εIso`
`of` 📖	CompOp	13 math math: `BialgEquiv.toBialgIso_refl`, `of_counit`, `tensorUnit_def`, `of_comul`, `BialgEquiv.toBialgIso_symm`, `HopfAlgCat.forget₂_bialgebra_obj`, `tensorObj_def`, `of_carrier`, `BialgEquiv.toBialgIso_trans`, `of_instBialgebra`, `BialgEquiv.toBialgIso_hom`, `of_instRing`, `BialgEquiv.toBialgIso_inv`
`ofHom` 📖	CompOp	6 math math: `whiskerLeft_def`, `tensorHom_def`, `whiskerRight_def`, `HopfAlgCat.forget₂_bialgebra_map`, `BialgEquiv.toBialgIso_hom`, `BialgEquiv.toBialgIso_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget_reflects_isos` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsIsomorphisms` `BialgCat` `category` `CategoryTheory.types` `CategoryTheory.forget` `BialgHom` `carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `Bialgebra.toAlgebra` `instBialgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `BialgHom.funLike` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `concreteCategory`	—	`Equiv.left_inv` `Equiv.right_inv` `BialgHom.map_mul'` `CategoryTheory.IsIso.out` `CategoryTheory.Iso.isIso_hom`
`forget₂_algebra_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `BialgCat` `category` `AlgCat` `AlgCat.instCategory` `CategoryTheory.forget₂` `BialgHom` `carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `Bialgebra.toAlgebra` `instBialgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `BialgHom.funLike` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `concreteCategory` `AlgHom` `AlgCat.carrier` `AlgCat.isRing` `AlgCat.isAlgebra` `AlgHom.funLike` `AlgCat.instConcreteCategoryAlgHomCarrier` `hasForgetToAlgebra` `AlgCat.ofHom` `AlgHomClass.toAlgHom` `BialgHomClass.toAlgHomClass` `BialgHom.bialgHomClass` `Hom.toBialgHom`	—	—
`forget₂_algebra_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `BialgCat` `category` `AlgCat` `AlgCat.instCategory` `CategoryTheory.forget₂` `BialgHom` `carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `Bialgebra.toAlgebra` `instBialgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `BialgHom.funLike` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `concreteCategory` `AlgHom` `AlgCat.carrier` `AlgCat.isRing` `AlgCat.isAlgebra` `AlgHom.funLike` `AlgCat.instConcreteCategoryAlgHomCarrier` `hasForgetToAlgebra` `AlgCat.of`	—	—
`forget₂_coalgebra_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `BialgCat` `category` `CoalgCat` `CoalgCat.category` `CategoryTheory.forget₂` `BialgHom` `carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `Bialgebra.toAlgebra` `instBialgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `BialgHom.funLike` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `concreteCategory` `CoalgHom` `ModuleCat.carrier` `CommRing.toRing` `CoalgCat.toModuleCat` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `CoalgCat.instCoalgebra` `CoalgHom.funLike` `CoalgCat.concreteCategory` `hasForgetToCoalgebra` `CoalgCat.ofHom` `Ring.toAddCommGroup` `CoalgHomClass.toCoalgHom` `BialgHomClass.toCoalgHomClass` `BialgHom.bialgHomClass` `Hom.toBialgHom`	—	—
`forget₂_coalgebra_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `BialgCat` `category` `CoalgCat` `CoalgCat.category` `CategoryTheory.forget₂` `BialgHom` `carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `Bialgebra.toAlgebra` `instBialgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `BialgHom.funLike` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `concreteCategory` `CoalgHom` `ModuleCat.carrier` `CommRing.toRing` `CoalgCat.toModuleCat` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `CoalgCat.instCoalgebra` `CoalgHom.funLike` `CoalgCat.concreteCategory` `hasForgetToCoalgebra` `CoalgCat.of` `Ring.toAddCommGroup`	—	—
`hom_ext` 📖	—	`Hom.toBialgHom`	—	—	`Hom.ext`
`hom_ext_iff` 📖	mathematical	—	`Hom.toBialgHom`	—	`hom_ext`
`of_carrier` 📖	mathematical	—	`carrier` `of`	—	—
`of_comul` 📖	mathematical	—	`CoalgebraStruct.comul` `carrier` `of` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `Bialgebra.toAlgebra` `Coalgebra.toCoalgebraStruct` `Bialgebra.toCoalgebra` `instRing` `instBialgebra`	—	—
`of_counit` 📖	mathematical	—	`CoalgebraStruct.counit` `carrier` `of` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `Bialgebra.toAlgebra` `Coalgebra.toCoalgebraStruct` `Bialgebra.toCoalgebra` `instRing` `instBialgebra`	—	—
`of_instBialgebra` 📖	mathematical	—	`instBialgebra` `of`	—	—
`of_instRing` 📖	mathematical	—	`instRing` `of`	—	—
`toBialgHom_comp` 📖	mathematical	—	`Hom.toBialgHom` `CategoryTheory.CategoryStruct.comp` `BialgCat` `CategoryTheory.Category.toCategoryStruct` `category` `BialgHom.comp` `carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `Bialgebra.toAlgebra` `instBialgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra`	—	—
`toBialgHom_id` 📖	mathematical	—	`Hom.toBialgHom` `CategoryTheory.CategoryStruct.id` `BialgCat` `CategoryTheory.Category.toCategoryStruct` `category` `BialgHom.id` `carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `Bialgebra.toAlgebra` `instBialgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra`	—	—

BialgCat.Hom

Definitions

Name	Category	Theorems
`toBialgHom` 📖	CompOp	6 math math: `toBialgHom_injective`, `BialgCat.forget₂_algebra_map`, `BialgCat.hom_ext_iff`, `BialgCat.toBialgHom_id`, `BialgCat.forget₂_coalgebra_map`, `BialgCat.toBialgHom_comp`
`toBialgHom'` 📖	CompOp	5 math math: `BialgCat.whiskerLeft_def`, `BialgCat.tensorHom_def`, `BialgCat.whiskerRight_def`, `ext_iff`, `CategoryTheory.Iso.toBialgEquiv_toBialgHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`toBialgHom'`	—	—	—
`ext_iff` 📖	mathematical	—	`toBialgHom'`	—	`ext`
`toBialgHom_injective` 📖	mathematical	—	`BialgCat.Hom` `BialgHom` `BialgCat.carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `BialgCat.instRing` `Bialgebra.toAlgebra` `BialgCat.instBialgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `toBialgHom`	—	—

BialgEquiv

Definitions

Name	Category	Theorems
`toBialgIso` 📖	CompOp	8 math math: `BialgCat.rightUnitor_def`, `toBialgIso_refl`, `BialgCat.associator_def`, `toBialgIso_symm`, `toBialgIso_trans`, `toBialgIso_hom`, `BialgCat.leftUnitor_def`, `toBialgIso_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toBialgIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `BialgCat` `BialgCat.category` `BialgCat.of` `toBialgIso` `BialgCat.ofHom` `BialgHomClass.toBialgHom` `BialgEquiv` `CommRing.toCommSemiring` `Ring.toSemiring` `Bialgebra.toAlgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `instFunLike`	—	—
`toBialgIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `BialgCat` `BialgCat.category` `BialgCat.of` `toBialgIso` `BialgCat.ofHom` `BialgHomClass.toBialgHom` `BialgEquiv` `CommRing.toCommSemiring` `Ring.toSemiring` `Bialgebra.toAlgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `instFunLike` `symm`	—	—
`toBialgIso_refl` 📖	mathematical	—	`toBialgIso` `refl` `CommRing.toCommSemiring` `Ring.toSemiring` `Bialgebra.toAlgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `CategoryTheory.Iso.refl` `BialgCat` `BialgCat.category` `BialgCat.of`	—	—
`toBialgIso_symm` 📖	mathematical	—	`toBialgIso` `symm` `CommRing.toCommSemiring` `Ring.toSemiring` `Bialgebra.toAlgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `CategoryTheory.Iso.symm` `BialgCat` `BialgCat.category` `BialgCat.of`	—	—
`toBialgIso_trans` 📖	mathematical	—	`toBialgIso` `trans` `CommRing.toCommSemiring` `Ring.toSemiring` `Bialgebra.toAlgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `CategoryTheory.Iso.trans` `BialgCat` `BialgCat.category` `BialgCat.of`	—	—

CategoryTheory.Iso

Definitions

Name	Category	Theorems
`toBialgEquiv` 📖	CompOp	4 math math: `toBialgEquiv_refl`, `toBialgEquiv_trans`, `toBialgEquiv_symm`, `toBialgEquiv_toBialgHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toBialgEquiv_refl` 📖	mathematical	—	`toBialgEquiv` `refl` `BialgCat` `BialgCat.category` `BialgEquiv.refl` `BialgCat.carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `BialgCat.instRing` `Bialgebra.toAlgebra` `BialgCat.instBialgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra`	—	—
`toBialgEquiv_symm` 📖	mathematical	—	`toBialgEquiv` `symm` `BialgCat` `BialgCat.category` `BialgEquiv.symm` `BialgCat.carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `BialgCat.instRing` `Bialgebra.toAlgebra` `BialgCat.instBialgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra`	—	—
`toBialgEquiv_toBialgHom` 📖	mathematical	—	`BialgHomClass.toBialgHom` `BialgCat.carrier` `BialgEquiv` `CommRing.toCommSemiring` `Ring.toSemiring` `BialgCat.instRing` `Bialgebra.toAlgebra` `BialgCat.instBialgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `BialgEquiv.instFunLike` `BialgEquivClass.toBialgHomClass` `BialgEquiv.instEquivLike` `BialgEquiv.instBialgEquivClass` `toBialgEquiv` `BialgCat.Hom.toBialgHom'` `hom` `BialgCat` `BialgCat.category`	—	`BialgEquivClass.toBialgHomClass` `BialgEquiv.instBialgEquivClass`
`toBialgEquiv_trans` 📖	mathematical	—	`toBialgEquiv` `trans` `BialgCat` `BialgCat.category` `BialgEquiv.trans` `BialgCat.carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `BialgCat.instRing` `Bialgebra.toAlgebra` `BialgCat.instBialgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra`	—	—

(root)

Definitions

Name	Category	Theorems
`BialgCat` 📖	CompData	30 math math: `BialgCat.rightUnitor_def`, `BialgEquiv.toBialgIso_refl`, `BialgCat.associator_def`, `BialgCat.whiskerLeft_def`, `BialgCat.tensorUnit_def`, `CategoryTheory.Iso.toBialgEquiv_refl`, `BialgCat.forget_reflects_isos`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_εIso`, `CategoryTheory.Iso.toBialgEquiv_trans`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_μIso`, `BialgCat.forget₂_coalgebra_obj`, `BialgCat.tensorHom_def`, `BialgCat.forget₂_algebra_map`, `BialgEquiv.toBialgIso_symm`, `HopfAlgCat.forget₂_bialgebra_obj`, `CategoryTheory.Iso.toBialgEquiv_symm`, `BialgCat.whiskerRight_def`, `BialgCat.tensorObj_def`, `BialgCat.MonoidalCategory.inducingFunctorData_μIso`, `BialgCat.toBialgHom_id`, `HopfAlgCat.forget₂_bialgebra_map`, `BialgEquiv.toBialgIso_trans`, `BialgCat.forget₂_coalgebra_map`, `BialgEquiv.toBialgIso_hom`, `BialgCat.toBialgHom_comp`, `CategoryTheory.Iso.toBialgEquiv_toBialgHom`, `BialgCat.leftUnitor_def`, `BialgCat.forget₂_algebra_obj`, `BialgCat.MonoidalCategory.inducingFunctorData_εIso`, `BialgEquiv.toBialgIso_inv`

---

← Back to Index