Hom

📁 Source: Mathlib/RingTheory/Bialgebra/Hom.lean

Statistics

Metric	Count
Definitions `BialgHom`, `apply`, `comp`, `copy`, `funLike`, `id`, `ofAlgHom`, `toCoalgHom`, `toMonoidHom`, `BialgHomClass`, `instCoeToBialgHom`, `toBialgHom`, `counitBialgHom`, `unitBialgHom`, `«term_→ₐc[_]_»`, `«term_→ₐc_»`	16
Theorems `End_toOne_one`, `End_toSemigroup_toMul_mul`, `bialgHomClass`, `coe_algHom_injective`, `coe_coalgHom_injective`, `coe_coalgHom_mk`, `coe_coe`, `coe_comp`, `coe_copy`, `coe_fn_inj`, `coe_fn_injective`, `coe_id`, `coe_linearMap_injective`, `coe_mk`, `coe_mks`, `coe_toAlgHom`, `coe_toCoalgHom`, `coe_toLinearMap`, `comp_apply`, `comp_assoc`, `comp_id`, `comp_toAlgHom`, `comp_toCoalgHom`, `congr_arg`, `congr_fun`, `copy_eq`, `ext`, `ext_iff`, `ext_of_ring`, `ext_of_ring_iff`, `id_apply`, `id_comp`, `id_toAlgHom`, `id_toCoalgHom`, `map_mul'`, `map_one'`, `map_smul_of_tower`, `mk_coe`, `mul_apply`, `ofAlgHom_apply`, `one_apply`, `toAlgHom_toLinearMap`, `toCoalgHom_apply`, `counitAlgHom_comp`, `map_comp_comulAlgHom`, `toAlgHomClass`, `toCoalgHomClass`, `toMonoidHomClass`, `counitBialgHom_apply`, `counitBialgHom_self`, `counitBialgHom_toCoalgHom`, `ext_to_ring`, `ext_to_ring_iff`, `subsingleton_to_ring`	54
Total	70

BialgHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	17 math math: `End_toSemigroup_toMul_mul`, `CommBialgCat.ofHom_comp`, `MonoidAlgebra.mapDomainBialgHom_comp`, `comp_apply`, `BialgEquiv.symm_comp`, `HopfAlgCat.toBialgHom_comp`, `comp_assoc`, `comp_id`, `coe_comp`, `BialgEquiv.trans_toBialgHom`, `AddMonoidAlgebra.mapDomainBialgHom_comp`, `BialgCat.toBialgHom_comp`, `comp_toAlgHom`, `BialgEquiv.comp_symm`, `CommBialgCat.hom_comp`, `comp_toCoalgHom`, `id_comp`
`copy` 📖	CompOp	—
`funLike` 📖	CompOp	76 math math: `coe_fn_inj`, `coe_coalgHom_injective`, `commBialgCatEquivComonCommAlgCat_unitIso_inv_app`, `BialgEquiv.coe_toBialgHom`, `Bialgebra.TensorProduct.map_toAlgHom`, `ext_iff`, `Bialgebra.counitBialgHom_apply`, `CommBialgCat.id_apply`, `coe_coe`, `coe_fn_injective`, `coe_linearMap_injective`, `commBialgCatEquivComonCommAlgCat_unitIso_hom_app`, `HopfAlgCat.forget_reflects_isos`, `id_apply`, `Bialgebra.TensorProduct.map_toCoalgHom`, `BialgCat.forget_reflects_isos`, `comp_apply`, `MonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom`, `AddMonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom`, `CommBialgCat.forget₂_commAlgCat_obj`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_εIso`, `coe_toAlgHom`, `CommBialgCat.bialgEquivOfIso_apply`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_μIso`, `coe_algHom_injective`, `BialgCat.forget₂_coalgebra_obj`, `AddMonoidAlgebra.mapDomainBialgHom_apply`, `congr_arg`, `coe_coalgHom_mk`, `MonoidAlgebra.mapDomainBialgHom_apply`, `toAlgHom_toLinearMap`, `CommBialgCat.reflectsIsomorphisms_forget`, `BialgCat.forget₂_algebra_map`, `CommBialgCat.inv_hom_apply`, `HopfAlgCat.forget₂_bialgebra_obj`, `instIsMonHomOppositeCommAlgCatOpOfHomToAlgHomBialgHom`, `CommBialgCat.hom_inv_apply`, `BialgEquiv.toCoalgEquiv_toCoalgHom`, `ofAlgHom_apply`, `coe_toLinearMap`, `coe_toCoalgHom`, `bialgHomClass`, `id_toCoalgHom`, `coe_comp`, `Bialgebra.TensorProduct.map_tmul`, `Bialgebra.counitBialgHom_toCoalgHom`, `BialgEquiv.toBialgHom_toAlgHom`, `toCoalgHom_apply`, `CommBialgCat.comp_apply`, `BialgCat.MonoidalCategory.inducingFunctorData_μIso`, `CommBialgCat.bialgEquivOfIso_symm_apply`, `HopfAlgCat.forget₂_bialgebra_map`, `CommBialgCat.forget_obj`, `CommBialgCat.ofHom_apply`, `coe_mks`, `BialgCat.forget₂_coalgebra_map`, `congr_fun`, `commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom`, `map_smul_of_tower`, `CommBialgCat.forget_map`, `CommBialgCat.forget₂_commAlgCat_map`, `ext_of_ring_iff`, `coe_mk`, `comp_toAlgHom`, `BialgCat.forget₂_algebra_obj`, `CommBialgCat.hom_id`, `commBialgCatEquivComonCommAlgCat_counitIso_hom_app`, `mul_apply`, `id_toAlgHom`, `commBialgCatEquivComonCommAlgCat_functor_map_unop_hom`, `BialgCat.MonoidalCategory.inducingFunctorData_εIso`, `one_apply`, `BialgEquiv.coe_coe`, `commBialgCatEquivComonCommAlgCat_counitIso_inv_app`, `comp_toCoalgHom`, `coe_id`
`id` 📖	CompOp	16 math math: `AddMonoidAlgebra.mapDomainBialgHom_id`, `id_apply`, `BialgEquiv.symm_comp`, `Bialgebra.counitBialgHom_self`, `End_toOne_one`, `comp_id`, `id_toCoalgHom`, `BialgEquiv.refl_toBialgHom`, `HopfAlgCat.toBialgHom_id`, `BialgCat.toBialgHom_id`, `CommBialgCat.ofHom_id`, `BialgEquiv.comp_symm`, `id_toAlgHom`, `MonoidAlgebra.mapDomainBialgHom_id`, `id_comp`, `coe_id`
`ofAlgHom` 📖	CompOp	5 math math: `commBialgCatEquivComonCommAlgCat_unitIso_inv_app`, `commBialgCatEquivComonCommAlgCat_unitIso_hom_app`, `ofAlgHom_apply`, `commBialgCatEquivComonCommAlgCat_counitIso_hom_app`, `commBialgCatEquivComonCommAlgCat_counitIso_inv_app`
`toCoalgHom` 📖	CompOp	3 math math: `toCoalgHom_apply`, `map_mul'`, `map_one'`
`toMonoidHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`End_toOne_one` 📖	mathematical	—	`BialgHom` `Monoid.toOne` `End` `id`	—	—
`End_toSemigroup_toMul_mul` 📖	mathematical	—	`BialgHom` `Semigroup.toMul` `Monoid.toSemigroup` `End` `comp`	—	—
`bialgHomClass` 📖	mathematical	—	`BialgHomClass` `BialgHom` `funLike`	—	`AddHom.map_add'` `LinearMap.map_smul'` `CoalgHom.counit_comp` `CoalgHom.map_comp_comul` `map_mul'` `map_one'`
`coe_algHom_injective` 📖	mathematical	—	`BialgHom` `AlgHom` `AlgHomClass.toAlgHom` `funLike` `BialgHomClass.toAlgHomClass` `bialgHomClass`	—	`BialgHomClass.toAlgHomClass` `bialgHomClass` `coe_fn_injective`
`coe_coalgHom_injective` 📖	mathematical	—	`BialgHom` `CoalgHom` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `CoalgHomClass.toCoalgHom` `funLike` `BialgHomClass.toCoalgHomClass` `bialgHomClass`	—	`BialgHomClass.toCoalgHomClass` `bialgHomClass` `coe_fn_injective`
`coe_coalgHom_mk` 📖	mathematical	`AddHom.toFun` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `LinearMap.toAddHom` `CommSemiring.toSemiring` `RingHom.id` `Algebra.toModule` `CoalgHom.toLinearMap` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MulOne.toMul`	`CoalgHomClass.toCoalgHom` `BialgHom` `funLike` `BialgHomClass.toCoalgHomClass` `bialgHomClass`	—	`BialgHomClass.toCoalgHomClass` `bialgHomClass`
`coe_coe` 📖	mathematical	—	`DFunLike.coe` `BialgHom` `funLike` `BialgHomClass.toBialgHom`	—	—
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `BialgHom` `funLike` `comp`	—	—
`coe_copy` 📖	mathematical	`DFunLike.coe` `CoalgHom` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `CoalgHom.funLike`	`CoalgHom.copy`	—	—
`coe_fn_inj` 📖	mathematical	—	`DFunLike.coe` `BialgHom` `funLike`	—	`DFunLike.coe_fn_eq`
`coe_fn_injective` 📖	mathematical	—	`BialgHom` `DFunLike.coe` `funLike`	—	`DFunLike.coe_injective`
`coe_id` 📖	mathematical	—	`DFunLike.coe` `BialgHom` `funLike` `id`	—	—
`coe_linearMap_injective` 📖	mathematical	—	`BialgHom` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `SemilinearMapClass.semilinearMap` `funLike` `CoalgHomClass.toSemilinearMapClass` `BialgHomClass.toCoalgHomClass` `bialgHomClass`	—	`CoalgHomClass.toSemilinearMapClass` `CoalgHom.coalgHomClass` `CoalgHom.coe_linearMap_injective` `coe_coalgHom_injective`
`coe_mk` 📖	mathematical	`AddHom.toFun` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `LinearMap.toAddHom` `CommSemiring.toSemiring` `RingHom.id` `Algebra.toModule` `CoalgHom.toLinearMap` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MulOne.toMul`	`DFunLike.coe` `BialgHom` `funLike` `CoalgHom` `CoalgHom.funLike`	—	—
`coe_mks` 📖	mathematical	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddHom.toFun` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `Algebra.toModule` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `RingHom.id` `LinearMap.comp` `Semiring.toModule` `RingHomCompTriple.ids` `CoalgebraStruct.counit` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.map` `CoalgebraStruct.comul` `LinearMap.toAddHom` `CoalgHom.toLinearMap` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MulOne.toMul`	`BialgHom` `funLike`	—	`RingHomCompTriple.ids`
`coe_toAlgHom` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `AlgHom.funLike` `AlgHomClass.toAlgHom` `BialgHom` `funLike` `BialgHomClass.toAlgHomClass` `bialgHomClass`	—	`BialgHomClass.toAlgHomClass` `bialgHomClass`
`coe_toCoalgHom` 📖	mathematical	—	`DFunLike.coe` `CoalgHom` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `CoalgHom.funLike` `CoalgHomClass.toCoalgHom` `BialgHom` `funLike` `BialgHomClass.toCoalgHomClass` `bialgHomClass`	—	`BialgHomClass.toCoalgHomClass` `bialgHomClass`
`coe_toLinearMap` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `LinearMap.instFunLike` `SemilinearMapClass.semilinearMap` `BialgHom` `funLike` `CoalgHomClass.toSemilinearMapClass` `BialgHomClass.toCoalgHomClass` `bialgHomClass`	—	`CoalgHomClass.toSemilinearMapClass` `BialgHomClass.toCoalgHomClass` `bialgHomClass`
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `BialgHom` `funLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	`ext`
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`comp_toAlgHom` 📖	mathematical	—	`AlgHomClass.toAlgHom` `BialgHom` `funLike` `BialgHomClass.toAlgHomClass` `bialgHomClass` `comp` `AlgHom.comp`	—	`BialgHomClass.toAlgHomClass` `bialgHomClass`
`comp_toCoalgHom` 📖	mathematical	—	`CoalgHomClass.toCoalgHom` `BialgHom` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `funLike` `BialgHomClass.toCoalgHomClass` `bialgHomClass` `comp` `CoalgHom.comp`	—	`BialgHomClass.toCoalgHomClass` `bialgHomClass`
`congr_arg` 📖	mathematical	—	`DFunLike.coe` `BialgHom` `funLike`	—	`DFunLike.congr_arg`
`congr_fun` 📖	mathematical	—	`DFunLike.coe` `BialgHom` `funLike`	—	`DFunLike.congr_fun`
`copy_eq` 📖	mathematical	`DFunLike.coe` `CoalgHom` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `CoalgHom.funLike`	`CoalgHom.copy`	—	`DFunLike.ext'`
`ext` 📖	—	`DFunLike.coe` `BialgHom` `funLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `BialgHom` `funLike`	—	`ext`
`ext_of_ring` 📖	—	`DFunLike.coe` `BialgHom` `CommSemiring.toSemiring` `Algebra.id` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `CommSemiring.toBialgebra` `funLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—	`coe_linearMap_injective` `LinearMap.ext_ring` `CoalgHomClass.toSemilinearMapClass` `BialgHomClass.toCoalgHomClass` `bialgHomClass`
`ext_of_ring_iff` 📖	mathematical	—	`DFunLike.coe` `BialgHom` `CommSemiring.toSemiring` `Algebra.id` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `CommSemiring.toBialgebra` `funLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`ext_of_ring`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `BialgHom` `funLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`id_toAlgHom` 📖	mathematical	—	`AlgHomClass.toAlgHom` `BialgHom` `funLike` `BialgHomClass.toAlgHomClass` `bialgHomClass` `id` `AlgHom.id`	—	`BialgHomClass.toAlgHomClass` `bialgHomClass`
`id_toCoalgHom` 📖	mathematical	—	`CoalgHomClass.toCoalgHom` `BialgHom` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `funLike` `BialgHomClass.toCoalgHomClass` `bialgHomClass` `id` `CoalgHom.id`	—	`BialgHomClass.toCoalgHomClass` `bialgHomClass`
`map_mul'` 📖	mathematical	—	`AddHom.toFun` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `LinearMap.toAddHom` `CommSemiring.toSemiring` `RingHom.id` `Algebra.toModule` `CoalgHom.toLinearMap` `toCoalgHom` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass`	—	—
`map_one'` 📖	mathematical	—	`AddHom.toFun` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `LinearMap.toAddHom` `CommSemiring.toSemiring` `RingHom.id` `Algebra.toModule` `CoalgHom.toLinearMap` `toCoalgHom` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass`	—	—
`map_smul_of_tower` 📖	mathematical	—	`DFunLike.coe` `BialgHom` `funLike`	—	`LinearMap.map_smul_of_tower`
`mk_coe` 📖	—	`DFunLike.coe` `BialgHom` `funLike` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddHom.toFun` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `Algebra.toModule` `RingHom` `RingHom.instFunLike` `RingHom.id` `LinearMap.comp` `Semiring.toModule` `RingHomCompTriple.ids` `CoalgebraStruct.counit` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.map` `CoalgebraStruct.comul` `LinearMap.toAddHom` `CoalgHom.toLinearMap` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MulOne.toMul`	—	—	`RingHomCompTriple.ids`
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `BialgHom` `funLike` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `End`	—	—
`ofAlgHom_apply` 📖	mathematical	`AlgHom.comp` `CommSemiring.toSemiring` `Bialgebra.toAlgebra` `Algebra.id` `Bialgebra.counitAlgHom` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `IsScalarTower.to_smulCommClass` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.TensorProduct.map` `Bialgebra.comulAlgHom` `Algebra.TensorProduct.instAlgebra`	`DFunLike.coe` `BialgHom` `Coalgebra.toCoalgebraStruct` `Bialgebra.toCoalgebra` `funLike` `ofAlgHom` `AlgHom` `AlgHom.funLike`	—	`IsScalarTower.to_smulCommClass` `IsScalarTower.left`
`one_apply` 📖	mathematical	—	`DFunLike.coe` `BialgHom` `funLike` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `End`	—	—
`toAlgHom_toLinearMap` 📖	mathematical	—	`SemilinearMapClass.semilinearMap` `AlgHom` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `RingHom.id` `AlgHomClass.toAlgHom` `BialgHom` `funLike` `BialgHomClass.toAlgHomClass` `bialgHomClass` `AlgHom.funLike` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `CoalgHomClass.toSemilinearMapClass` `BialgHomClass.toCoalgHomClass`	—	`BialgHomClass.toAlgHomClass` `bialgHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass`
`toCoalgHom_apply` 📖	mathematical	—	`DFunLike.coe` `CoalgHom` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `CoalgHom.funLike` `toCoalgHom` `BialgHom` `funLike`	—	—

BialgHom.Simps

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—

BialgHomClass

Definitions

Name	Category	Theorems
`instCoeToBialgHom` 📖	CompOp	—
`toBialgHom` 📖	CompOp	20 math math: `BialgEquiv.coe_toBialgHom`, `BialgHom.coe_coe`, `BialgEquiv.symm_comp`, `BialgEquiv.toBialgHom_inj`, `BialgEquiv.toCoalgEquiv_toCoalgHom`, `BialgEquiv.toBialgHom_eq_coe`, `BialgEquiv.refl_toBialgHom`, `BialgEquiv.coe_ofBialgHom`, `BialgEquiv.toBialgHom_toAlgHom`, `BialgEquiv.trans_toBialgHom`, `CommBialgCat.isoMk_hom`, `BialgEquiv.toBialgIso_hom`, `CategoryTheory.Iso.toBialgEquiv_toBialgHom`, `CommBialgCat.isoMk_inv`, `BialgEquiv.toHopfAlgIso_hom`, `CategoryTheory.Iso.toHopfAlgEquiv_toBialgHom`, `BialgEquiv.comp_symm`, `BialgEquiv.toHopfAlgIso_inv`, `BialgEquiv.coe_coe`, `BialgEquiv.toBialgIso_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`counitAlgHom_comp` 📖	mathematical	—	`AlgHom.comp` `CommSemiring.toSemiring` `Bialgebra.toAlgebra` `Algebra.id` `Bialgebra.counitAlgHom` `AlgHomClass.toAlgHom` `toAlgHomClass` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra`	—	`AlgHom.toLinearMap_injective` `toAlgHomClass` `CoalgHomClass.counit_comp` `toCoalgHomClass`
`map_comp_comulAlgHom` 📖	mathematical	—	`AlgHom.comp` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toAlgebra` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `IsScalarTower.to_smulCommClass` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.TensorProduct.map` `AlgHomClass.toAlgHom` `toAlgHomClass` `Coalgebra.toCoalgebraStruct` `Bialgebra.toCoalgebra` `Bialgebra.comulAlgHom` `Algebra.TensorProduct.instAlgebra`	—	`AlgHom.toLinearMap_injective` `IsScalarTower.to_smulCommClass` `IsScalarTower.left` `toAlgHomClass` `CoalgHomClass.map_comp_comul` `toCoalgHomClass`
`toAlgHomClass` 📖	mathematical	—	`AlgHomClass`	—	`map_mul` `MonoidHomClass.toMulHomClass` `toMonoidHomClass` `map_one` `MonoidHomClass.toOneHomClass` `map_add` `SemilinearMapClass.toAddHomClass` `CoalgHomClass.toSemilinearMapClass` `toCoalgHomClass` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `Algebra.algebraMap_eq_smul_one` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass`
`toCoalgHomClass` 📖	mathematical	—	`CoalgHomClass` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule`	—	—
`toMonoidHomClass` 📖	mathematical	—	`MonoidHomClass` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring`	—	—

Bialgebra

Definitions

Name	Category	Theorems
`counitBialgHom` 📖	CompOp	3 math math: `counitBialgHom_apply`, `counitBialgHom_self`, `counitBialgHom_toCoalgHom`
`unitBialgHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`counitBialgHom_apply` 📖	mathematical	—	`DFunLike.coe` `BialgHom` `toAlgebra` `CommSemiring.toSemiring` `Algebra.id` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `toCoalgebra` `CommSemiring.toBialgebra` `BialgHom.funLike` `counitBialgHom` `LinearMap` `RingHom.id` `Semiring.toModule` `LinearMap.instFunLike` `CoalgebraStruct.counit`	—	—
`counitBialgHom_self` 📖	mathematical	—	`counitBialgHom` `CommSemiring.toSemiring` `CommSemiring.toBialgebra` `BialgHom.id` `Algebra.id` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `toCoalgebra`	—	—
`counitBialgHom_toCoalgHom` 📖	mathematical	—	`CoalgHomClass.toCoalgHom` `BialgHom` `toAlgebra` `CommSemiring.toSemiring` `Algebra.id` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `toCoalgebra` `CommSemiring.toBialgebra` `BialgHom.funLike` `BialgHomClass.toCoalgHomClass` `BialgHom.bialgHomClass` `counitBialgHom` `Coalgebra.counitCoalgHom`	—	`BialgHomClass.toCoalgHomClass` `BialgHom.bialgHomClass`
`ext_to_ring` 📖	—	—	—	—	`subsingleton_to_ring`
`ext_to_ring_iff` 📖	—	—	—	—	`ext_to_ring`
`subsingleton_to_ring` 📖	mathematical	—	`BialgHom` `toAlgebra` `CommSemiring.toSemiring` `Algebra.id` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `toCoalgebra` `CommSemiring.toBialgebra`	—	`BialgHom.coe_coalgHom_injective` `Coalgebra.subsingleton_to_ring` `BialgHomClass.toCoalgHomClass` `BialgHom.bialgHomClass`

(root)

Definitions

Name	Category	Theorems
`BialgHom` 📖	CompData	82 math math: `BialgHom.coe_fn_inj`, `BialgHom.coe_coalgHom_injective`, `commBialgCatEquivComonCommAlgCat_unitIso_inv_app`, `BialgEquiv.coe_toBialgHom`, `Bialgebra.TensorProduct.map_toAlgHom`, `BialgHom.ext_iff`, `Bialgebra.counitBialgHom_apply`, `CommBialgCat.id_apply`, `BialgHom.coe_coe`, `BialgHom.coe_fn_injective`, `BialgHom.coe_linearMap_injective`, `commBialgCatEquivComonCommAlgCat_unitIso_hom_app`, `HopfAlgCat.Hom.toBialgHom_injective`, `BialgHom.End_toSemigroup_toMul_mul`, `HopfAlgCat.forget_reflects_isos`, `BialgHom.id_apply`, `Bialgebra.TensorProduct.map_toCoalgHom`, `BialgCat.forget_reflects_isos`, `BialgHom.comp_apply`, `MonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom`, `AddMonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom`, `BialgCat.Hom.toBialgHom_injective`, `CommBialgCat.forget₂_commAlgCat_obj`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_εIso`, `BialgHom.coe_toAlgHom`, `CommBialgCat.bialgEquivOfIso_apply`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_μIso`, `BialgHom.coe_algHom_injective`, `BialgCat.forget₂_coalgebra_obj`, `AddMonoidAlgebra.mapDomainBialgHom_apply`, `BialgHom.congr_arg`, `BialgHom.coe_coalgHom_mk`, `MonoidAlgebra.mapDomainBialgHom_apply`, `BialgHom.toAlgHom_toLinearMap`, `CommBialgCat.reflectsIsomorphisms_forget`, `BialgCat.forget₂_algebra_map`, `CommBialgCat.inv_hom_apply`, `HopfAlgCat.forget₂_bialgebra_obj`, `instIsMonHomOppositeCommAlgCatOpOfHomToAlgHomBialgHom`, `CommBialgCat.hom_inv_apply`, `BialgEquiv.toCoalgEquiv_toCoalgHom`, `BialgHom.ofAlgHom_apply`, `BialgHom.End_toOne_one`, `BialgHom.coe_toLinearMap`, `BialgHom.coe_toCoalgHom`, `BialgHom.bialgHomClass`, `BialgHom.id_toCoalgHom`, `BialgHom.coe_comp`, `Bialgebra.TensorProduct.map_tmul`, `BialgEquiv.toBialgHom_injective`, `Bialgebra.counitBialgHom_toCoalgHom`, `BialgEquiv.toBialgHom_toAlgHom`, `BialgHom.toCoalgHom_apply`, `CommBialgCat.comp_apply`, `BialgCat.MonoidalCategory.inducingFunctorData_μIso`, `CommBialgCat.bialgEquivOfIso_symm_apply`, `HopfAlgCat.forget₂_bialgebra_map`, `CommBialgCat.forget_obj`, `CommBialgCat.ofHom_apply`, `BialgHom.coe_mks`, `BialgCat.forget₂_coalgebra_map`, `Bialgebra.subsingleton_to_ring`, `BialgHom.congr_fun`, `commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom`, `BialgHom.map_smul_of_tower`, `CommBialgCat.forget_map`, `CommBialgCat.forget₂_commAlgCat_map`, `BialgHom.ext_of_ring_iff`, `BialgHom.coe_mk`, `BialgHom.comp_toAlgHom`, `BialgCat.forget₂_algebra_obj`, `CommBialgCat.hom_id`, `commBialgCatEquivComonCommAlgCat_counitIso_hom_app`, `BialgHom.mul_apply`, `BialgHom.id_toAlgHom`, `commBialgCatEquivComonCommAlgCat_functor_map_unop_hom`, `BialgCat.MonoidalCategory.inducingFunctorData_εIso`, `BialgHom.one_apply`, `BialgEquiv.coe_coe`, `commBialgCatEquivComonCommAlgCat_counitIso_inv_app`, `BialgHom.comp_toCoalgHom`, `BialgHom.coe_id`
`BialgHomClass` 📖	CompData	2 math math: `BialgEquivClass.toBialgHomClass`, `BialgHom.bialgHomClass`
`«term_→ₐc[_]_»` 📖	CompOp	—
`«term_→ₐc_»` 📖	CompOp	—

---

← Back to Index