Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `toHopfAlgIso`, `toHopfAlgEquiv`, `HopfAlgCat`, `toBialgHom`, `toBialgHom'`, `carrier`, `category`, `concreteCategory`, `hasForgetToBialgebra`, `instCoeSortType`, `instHopfAlgebra`, `instRing`, `of`, `ofHom`	14
Theorems `toHopfAlgIso_hom`, `toHopfAlgIso_inv`, `toHopfAlgIso_refl`, `toHopfAlgIso_symm`, `toHopfAlgIso_trans`, `toHopfAlgEquiv_refl`, `toHopfAlgEquiv_symm`, `toHopfAlgEquiv_toBialgHom`, `toHopfAlgEquiv_trans`, `ext`, `ext_iff`, `toBialgHom_injective`, `forget_reflects_isos`, `forget₂_bialgebra_map`, `forget₂_bialgebra_obj`, `hom_ext`, `hom_ext_iff`, `of_comul`, `of_counit`, `toBialgHom_comp`, `toBialgHom_id`	21
Total	35

BialgEquiv

Definitions

Name	Category	Theorems
`toHopfAlgIso` 📖	CompOp	8 math math: `HopfAlgCat.rightUnitor_def`, `toHopfAlgIso_refl`, `HopfAlgCat.associator_def`, `toHopfAlgIso_symm`, `toHopfAlgIso_trans`, `HopfAlgCat.leftUnitor_def`, `toHopfAlgIso_hom`, `toHopfAlgIso_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toHopfAlgIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `HopfAlgCat` `HopfAlgCat.category` `HopfAlgCat.of` `toHopfAlgIso` `HopfAlgCat.ofHom` `BialgHomClass.toBialgHom` `BialgEquiv` `CommRing.toCommSemiring` `Ring.toSemiring` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `instFunLike`	—	—
`toHopfAlgIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `HopfAlgCat` `HopfAlgCat.category` `HopfAlgCat.of` `toHopfAlgIso` `HopfAlgCat.ofHom` `BialgHomClass.toBialgHom` `BialgEquiv` `CommRing.toCommSemiring` `Ring.toSemiring` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `instFunLike` `symm`	—	—
`toHopfAlgIso_refl` 📖	mathematical	—	`toHopfAlgIso` `refl` `CommRing.toCommSemiring` `Ring.toSemiring` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `CategoryTheory.Iso.refl` `HopfAlgCat` `HopfAlgCat.category` `HopfAlgCat.of`	—	—
`toHopfAlgIso_symm` 📖	mathematical	—	`toHopfAlgIso` `symm` `CommRing.toCommSemiring` `Ring.toSemiring` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `CategoryTheory.Iso.symm` `HopfAlgCat` `HopfAlgCat.category` `HopfAlgCat.of`	—	—
`toHopfAlgIso_trans` 📖	mathematical	—	`toHopfAlgIso` `trans` `CommRing.toCommSemiring` `Ring.toSemiring` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `CategoryTheory.Iso.trans` `HopfAlgCat` `HopfAlgCat.category` `HopfAlgCat.of`	—	—

CategoryTheory.Iso

Definitions

Name	Category	Theorems
`toHopfAlgEquiv` 📖	CompOp	4 math math: `toHopfAlgEquiv_trans`, `toHopfAlgEquiv_symm`, `toHopfAlgEquiv_refl`, `toHopfAlgEquiv_toBialgHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toHopfAlgEquiv_refl` 📖	mathematical	—	`toHopfAlgEquiv` `refl` `HopfAlgCat` `HopfAlgCat.category` `BialgEquiv.refl` `HopfAlgCat.carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `HopfAlgCat.instRing` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `HopfAlgCat.instHopfAlgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra`	—	—
`toHopfAlgEquiv_symm` 📖	mathematical	—	`toHopfAlgEquiv` `symm` `HopfAlgCat` `HopfAlgCat.category` `BialgEquiv.symm` `HopfAlgCat.carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `HopfAlgCat.instRing` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `HopfAlgCat.instHopfAlgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra`	—	—
`toHopfAlgEquiv_toBialgHom` 📖	mathematical	—	`BialgHomClass.toBialgHom` `HopfAlgCat.carrier` `BialgEquiv` `CommRing.toCommSemiring` `Ring.toSemiring` `HopfAlgCat.instRing` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `HopfAlgCat.instHopfAlgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `BialgEquiv.instFunLike` `BialgEquivClass.toBialgHomClass` `BialgEquiv.instEquivLike` `BialgEquiv.instBialgEquivClass` `toHopfAlgEquiv` `HopfAlgCat.Hom.toBialgHom'` `hom` `HopfAlgCat` `HopfAlgCat.category`	—	`BialgEquivClass.toBialgHomClass` `BialgEquiv.instBialgEquivClass`
`toHopfAlgEquiv_trans` 📖	mathematical	—	`toHopfAlgEquiv` `trans` `HopfAlgCat` `HopfAlgCat.category` `BialgEquiv.trans` `HopfAlgCat.carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `HopfAlgCat.instRing` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `HopfAlgCat.instHopfAlgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra`	—	—

HopfAlgCat

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	24 math math: `of_comul`, `rightUnitor_def`, `CategoryTheory.Iso.toHopfAlgEquiv_trans`, `tensorObj_instRing`, `whiskerLeft_def`, `of_counit`, `tensorObj_instHopfAlgebra`, `Hom.toBialgHom_injective`, `forget_reflects_isos`, `MonoidalCategory.inducingFunctorData_εIso`, `whiskerRight_def`, `MonoidalCategory.inducingFunctorData_μIso`, `toBialgHom_comp`, `associator_def`, `forget₂_bialgebra_obj`, `CategoryTheory.Iso.toHopfAlgEquiv_symm`, `toBialgHom_id`, `tensorHom_def`, `CategoryTheory.Iso.toHopfAlgEquiv_refl`, `forget₂_bialgebra_map`, `tensorObj_carrier`, `leftUnitor_def`, `CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom`, `tensorUnit_carrier`
`category` 📖	CompOp	28 math math: `rightUnitor_def`, `BialgEquiv.toHopfAlgIso_refl`, `CategoryTheory.Iso.toHopfAlgEquiv_trans`, `tensorObj_instRing`, `whiskerLeft_def`, `tensorObj_instHopfAlgebra`, `forget_reflects_isos`, `MonoidalCategory.inducingFunctorData_εIso`, `whiskerRight_def`, `MonoidalCategory.inducingFunctorData_μIso`, `toBialgHom_comp`, `associator_def`, `forget₂_bialgebra_obj`, `BialgEquiv.toHopfAlgIso_symm`, `CategoryTheory.Iso.toHopfAlgEquiv_symm`, `toBialgHom_id`, `tensorHom_def`, `CategoryTheory.Iso.toHopfAlgEquiv_refl`, `forget₂_bialgebra_map`, `BialgEquiv.toHopfAlgIso_trans`, `tensorObj_carrier`, `leftUnitor_def`, `tensorUnit_instRing`, `tensorUnit_instHopfAlgebra`, `BialgEquiv.toHopfAlgIso_hom`, `CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom`, `BialgEquiv.toHopfAlgIso_inv`, `tensorUnit_carrier`
`concreteCategory` 📖	CompOp	5 math math: `forget_reflects_isos`, `MonoidalCategory.inducingFunctorData_εIso`, `MonoidalCategory.inducingFunctorData_μIso`, `forget₂_bialgebra_obj`, `forget₂_bialgebra_map`
`hasForgetToBialgebra` 📖	CompOp	4 math math: `MonoidalCategory.inducingFunctorData_εIso`, `MonoidalCategory.inducingFunctorData_μIso`, `forget₂_bialgebra_obj`, `forget₂_bialgebra_map`
`instCoeSortType` 📖	CompOp	—
`instHopfAlgebra` 📖	CompOp	22 math math: `rightUnitor_def`, `CategoryTheory.Iso.toHopfAlgEquiv_trans`, `tensorObj_instRing`, `whiskerLeft_def`, `tensorObj_instHopfAlgebra`, `Hom.toBialgHom_injective`, `forget_reflects_isos`, `MonoidalCategory.inducingFunctorData_εIso`, `whiskerRight_def`, `MonoidalCategory.inducingFunctorData_μIso`, `toBialgHom_comp`, `associator_def`, `forget₂_bialgebra_obj`, `CategoryTheory.Iso.toHopfAlgEquiv_symm`, `toBialgHom_id`, `tensorHom_def`, `CategoryTheory.Iso.toHopfAlgEquiv_refl`, `forget₂_bialgebra_map`, `tensorObj_carrier`, `leftUnitor_def`, `tensorUnit_instHopfAlgebra`, `CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom`
`instRing` 📖	CompOp	22 math math: `rightUnitor_def`, `CategoryTheory.Iso.toHopfAlgEquiv_trans`, `tensorObj_instRing`, `whiskerLeft_def`, `tensorObj_instHopfAlgebra`, `Hom.toBialgHom_injective`, `forget_reflects_isos`, `MonoidalCategory.inducingFunctorData_εIso`, `whiskerRight_def`, `MonoidalCategory.inducingFunctorData_μIso`, `toBialgHom_comp`, `associator_def`, `forget₂_bialgebra_obj`, `CategoryTheory.Iso.toHopfAlgEquiv_symm`, `toBialgHom_id`, `tensorHom_def`, `CategoryTheory.Iso.toHopfAlgEquiv_refl`, `forget₂_bialgebra_map`, `tensorObj_carrier`, `leftUnitor_def`, `tensorUnit_instRing`, `CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom`
`of` 📖	CompOp	7 math math: `of_comul`, `BialgEquiv.toHopfAlgIso_refl`, `of_counit`, `BialgEquiv.toHopfAlgIso_symm`, `BialgEquiv.toHopfAlgIso_trans`, `BialgEquiv.toHopfAlgIso_hom`, `BialgEquiv.toHopfAlgIso_inv`
`ofHom` 📖	CompOp	5 math math: `whiskerLeft_def`, `whiskerRight_def`, `tensorHom_def`, `BialgEquiv.toHopfAlgIso_hom`, `BialgEquiv.toHopfAlgIso_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forget_reflects_isos` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsIsomorphisms` `HopfAlgCat` `category` `CategoryTheory.types` `CategoryTheory.forget` `BialgHom` `carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `instHopfAlgebra` `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₂_bialgebra_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `HopfAlgCat` `category` `BialgCat` `BialgCat.category` `CategoryTheory.forget₂` `BialgHom` `carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `instHopfAlgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `BialgHom.funLike` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `concreteCategory` `BialgCat.carrier` `BialgCat.instRing` `BialgCat.instBialgebra` `BialgCat.concreteCategory` `hasForgetToBialgebra` `BialgCat.ofHom` `Hom.toBialgHom`	—	—
`forget₂_bialgebra_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `HopfAlgCat` `category` `BialgCat` `BialgCat.category` `CategoryTheory.forget₂` `BialgHom` `carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `instHopfAlgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `BialgHom.funLike` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `concreteCategory` `BialgCat.carrier` `BialgCat.instRing` `BialgCat.instBialgebra` `BialgCat.concreteCategory` `hasForgetToBialgebra` `BialgCat.of`	—	—
`hom_ext` 📖	—	`Hom.toBialgHom`	—	—	`Hom.ext`
`hom_ext_iff` 📖	mathematical	—	`Hom.toBialgHom`	—	`hom_ext`
`of_comul` 📖	mathematical	—	`CoalgebraStruct.comul` `carrier` `of` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `Coalgebra.toCoalgebraStruct` `Bialgebra.toCoalgebra`	—	—
`of_counit` 📖	mathematical	—	`CoalgebraStruct.counit` `carrier` `of` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `Coalgebra.toCoalgebraStruct` `Bialgebra.toCoalgebra`	—	—
`toBialgHom_comp` 📖	mathematical	—	`Hom.toBialgHom` `CategoryTheory.CategoryStruct.comp` `HopfAlgCat` `CategoryTheory.Category.toCategoryStruct` `category` `BialgHom.comp` `carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `instHopfAlgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra`	—	—
`toBialgHom_id` 📖	mathematical	—	`Hom.toBialgHom` `CategoryTheory.CategoryStruct.id` `HopfAlgCat` `CategoryTheory.Category.toCategoryStruct` `category` `BialgHom.id` `carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `instHopfAlgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra`	—	—

HopfAlgCat.Hom

Definitions

Name	Category	Theorems
`toBialgHom` 📖	CompOp	5 math math: `toBialgHom_injective`, `HopfAlgCat.hom_ext_iff`, `HopfAlgCat.toBialgHom_comp`, `HopfAlgCat.toBialgHom_id`, `HopfAlgCat.forget₂_bialgebra_map`
`toBialgHom'` 📖	CompOp	5 math math: `HopfAlgCat.whiskerLeft_def`, `HopfAlgCat.whiskerRight_def`, `HopfAlgCat.tensorHom_def`, `ext_iff`, `CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom`

Theorems

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

(root)

Definitions

Name	Category	Theorems
`HopfAlgCat` 📖	CompData	28 math math: `HopfAlgCat.rightUnitor_def`, `BialgEquiv.toHopfAlgIso_refl`, `CategoryTheory.Iso.toHopfAlgEquiv_trans`, `HopfAlgCat.tensorObj_instRing`, `HopfAlgCat.whiskerLeft_def`, `HopfAlgCat.tensorObj_instHopfAlgebra`, `HopfAlgCat.forget_reflects_isos`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_εIso`, `HopfAlgCat.whiskerRight_def`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_μIso`, `HopfAlgCat.toBialgHom_comp`, `HopfAlgCat.associator_def`, `HopfAlgCat.forget₂_bialgebra_obj`, `BialgEquiv.toHopfAlgIso_symm`, `CategoryTheory.Iso.toHopfAlgEquiv_symm`, `HopfAlgCat.toBialgHom_id`, `HopfAlgCat.tensorHom_def`, `CategoryTheory.Iso.toHopfAlgEquiv_refl`, `HopfAlgCat.forget₂_bialgebra_map`, `BialgEquiv.toHopfAlgIso_trans`, `HopfAlgCat.tensorObj_carrier`, `HopfAlgCat.leftUnitor_def`, `HopfAlgCat.tensorUnit_instRing`, `HopfAlgCat.tensorUnit_instHopfAlgebra`, `BialgEquiv.toHopfAlgIso_hom`, `CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom`, `BialgEquiv.toHopfAlgIso_inv`, `HopfAlgCat.tensorUnit_carrier`

---

← Back to Index