Hom

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

Statistics

Metric	Count
Definitions `Hom`, `Hom`, `CoalgHom`, `apply`, `comp`, `copy`, `funLike`, `id`, `toLinearMap`, `CoalgHomClass`, `instCoeToCoalgHom`, `toCoalgHom`, `induced`, `counitCoalgHom`, `«term_→ₗc[_]_»`, `«term_→ₗc_»`	16
Theorems `End_toOne_one`, `End_toSemigroup_toMul_mul`, `coalgHomClass`, `coe_addMonoidHom_injective`, `coe_coe`, `coe_comp`, `coe_copy`, `coe_fn_inj`, `coe_fn_injective`, `coe_id`, `coe_linearMap_injective`, `coe_linearMap_mk`, `coe_mk`, `coe_mks`, `coe_toAddMonoidHom`, `coe_toLinearMap`, `comp_apply`, `comp_assoc`, `comp_id`, `comp_toLinearMap`, `congr_arg`, `congr_fun`, `copy_eq`, `counit_comp`, `ext`, `ext_iff`, `ext_of_ring`, `ext_of_ring_iff`, `id_apply`, `id_comp`, `id_toLinearMap`, `map_comp_comul`, `map_smul_of_tower`, `mk_coe`, `mul_apply`, `one_apply`, `toLinearMap_eq_coe`, `counit_comp`, `counit_comp_apply`, `map_comp_comul`, `map_comp_comul_apply`, `toSemilinearMapClass`, `induced_index`, `induced_left`, `induced_right`, `induced_ι`, `counitCoalgHom_apply`, `counitCoalgHom_toLinearMap`, `ext_to_ring`, `ext_to_ring_iff`, `subsingleton_to_ring`	51
Total	67

CategoryTheory.Comonad.Coalgebra

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	1 math math: `CategoryTheory.Comonad.adj_unit`

CategoryTheory.Endofunctor.Coalgebra

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

CoalgHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	10 math math: `id_comp`, `comp_toLinearMap`, `comp_assoc`, `comp_id`, `CoalgCat.toCoalgHom_comp`, `coe_comp`, `comp_apply`, `CoalgEquiv.trans_toCoalgHom`, `BialgHom.comp_toCoalgHom`, `End_toSemigroup_toMul_mul`
`copy` 📖	CompOp	4 math math: `BialgHom.coe_copy`, `copy_eq`, `coe_copy`, `BialgHom.copy_eq`
`funLike` 📖	CompOp	44 math math: `CoalgEquiv.coe_toCoalgHom`, `ext_of_ring_iff`, `coe_addMonoidHom_injective`, `map_smul_of_tower`, `comp_toLinearMap`, `BialgCat.forget₂_coalgebra_obj`, `id_toLinearMap`, `mul_apply`, `CoalgCat.MonoidalCategory.inducingFunctorData_μIso`, `CoalgCat.MonoidalCategory.inducingFunctorData_εIso`, `coe_mk`, `coe_id`, `CoalgEquiv.coe_coe`, `coe_fn_inj`, `id_apply`, `CoalgCat.forget_reflects_isos`, `Coalgebra.TensorProduct.map_tmul`, `coe_coe`, `Coalgebra.counitCoalgHom_toLinearMap`, `BialgHom.coe_toCoalgHom`, `coe_linearMap_injective`, `congr_fun`, `CoalgEquiv.toLinearEquiv_toLinearMap`, `CoalgCat.forget₂_obj`, `coe_toLinearMap`, `BialgHom.toCoalgHom_apply`, `CoalgEquiv.symm_toCoalgHom`, `CoalgCat.forget₂_map`, `coe_fn_injective`, `coe_linearMap_mk`, `Coalgebra.counitCoalgHom_apply`, `CoalgCat.toComon_map_hom`, `BialgCat.forget₂_coalgebra_map`, `toLinearMap_eq_coe`, `Coalgebra.TensorProduct.map_toLinearMap`, `coe_mks`, `coalgHomClass`, `BialgHom.coe_mk`, `ext_iff`, `congr_arg`, `coe_comp`, `coe_toAddMonoidHom`, `comp_apply`, `one_apply`
`id` 📖	CompOp	9 math math: `id_comp`, `id_toLinearMap`, `coe_id`, `id_apply`, `BialgHom.id_toCoalgHom`, `CoalgEquiv.refl_toCoalgHom`, `comp_id`, `End_toOne_one`, `CoalgCat.toCoalgHom_id`
`toLinearMap` 📖	CompOp	13 math math: `CoalgCat.MonoidalCategoryAux.tensorHom_toLinearMap`, `CoalgCat.MonoidalCategoryAux.associator_hom_toLinearMap`, `CoalgEquiv.left_inv`, `map_comp_comul`, `counit_comp`, `CoalgCat.MonoidalCategoryAux.leftUnitor_hom_toLinearMap`, `BialgEquiv.map_mul'`, `BialgHom.map_mul'`, `LinearMap.convMul_comp_coalgHom_distrib`, `toLinearMap_eq_coe`, `CoalgCat.MonoidalCategoryAux.rightUnitor_hom_toLinearMap`, `CoalgEquiv.right_inv`, `BialgHom.map_one'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`End_toOne_one` 📖	mathematical	—	`CoalgHom` `Monoid.toOne` `End` `id`	—	—
`End_toSemigroup_toMul_mul` 📖	mathematical	—	`CoalgHom` `Semigroup.toMul` `Monoid.toSemigroup` `End` `comp`	—	—
`coalgHomClass` 📖	mathematical	—	`CoalgHomClass` `CoalgHom` `funLike`	—	`AddHom.map_add'` `LinearMap.map_smul'` `counit_comp` `map_comp_comul`
`coe_addMonoidHom_injective` 📖	mathematical	—	`CoalgHom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHomClass.toAddMonoidHom` `funLike` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `RingHom.id` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `SemilinearMapClass.distribMulActionSemiHomClass` `CoalgHomClass.toSemilinearMapClass` `coalgHomClass`	—	`LinearMap.toAddMonoidHom_injective` `coe_linearMap_injective`
`coe_coe` 📖	mathematical	—	`DFunLike.coe` `CoalgHom` `funLike` `CoalgHomClass.toCoalgHom`	—	—
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `CoalgHom` `funLike` `comp`	—	—
`coe_copy` 📖	mathematical	`DFunLike.coe` `CoalgHom` `funLike`	`copy`	—	—
`coe_fn_inj` 📖	mathematical	—	`DFunLike.coe` `CoalgHom` `funLike`	—	`DFunLike.coe_fn_eq`
`coe_fn_injective` 📖	mathematical	—	`CoalgHom` `DFunLike.coe` `funLike`	—	`DFunLike.coe_injective`
`coe_id` 📖	mathematical	—	`DFunLike.coe` `CoalgHom` `funLike` `id`	—	—
`coe_linearMap_injective` 📖	mathematical	—	`CoalgHom` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `SemilinearMapClass.semilinearMap` `funLike` `CoalgHomClass.toSemilinearMapClass` `coalgHomClass`	—	`CoalgHomClass.toSemilinearMapClass` `coalgHomClass` `coe_fn_injective`
`coe_linearMap_mk` 📖	mathematical	`LinearMap.comp` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `RingHomCompTriple.ids` `CoalgebraStruct.counit` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.map` `CoalgebraStruct.comul`	`SemilinearMapClass.semilinearMap` `CoalgHom` `funLike` `CoalgHomClass.toSemilinearMapClass` `coalgHomClass`	—	`RingHomCompTriple.ids` `CoalgHomClass.toSemilinearMapClass` `coalgHomClass`
`coe_mk` 📖	mathematical	`LinearMap.comp` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `RingHomCompTriple.ids` `CoalgebraStruct.counit` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.map` `CoalgebraStruct.comul`	`DFunLike.coe` `CoalgHom` `funLike` `LinearMap` `LinearMap.instFunLike`	—	`RingHomCompTriple.ids`
`coe_mks` 📖	mathematical	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddHom.toFun` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.id` `LinearMap.comp` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `RingHomCompTriple.ids` `CoalgebraStruct.counit` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.map` `CoalgebraStruct.comul`	`CoalgHom` `funLike`	—	`RingHomCompTriple.ids`
`coe_toAddMonoidHom` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `AddMonoidHomClass.toAddMonoidHom` `CoalgHom` `funLike` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `RingHom.id` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `SemilinearMapClass.distribMulActionSemiHomClass` `CoalgHomClass.toSemilinearMapClass` `coalgHomClass`	—	`DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `CoalgHomClass.toSemilinearMapClass` `coalgHomClass`
`coe_toLinearMap` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `SemilinearMapClass.semilinearMap` `CoalgHom` `funLike` `CoalgHomClass.toSemilinearMapClass` `coalgHomClass`	—	`CoalgHomClass.toSemilinearMapClass` `coalgHomClass`
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `CoalgHom` `funLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	`ext`
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`comp_toLinearMap` 📖	mathematical	—	`SemilinearMapClass.semilinearMap` `CoalgHom` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `comp` `funLike` `CoalgHomClass.toSemilinearMapClass` `coalgHomClass` `LinearMap.comp` `RingHomCompTriple.ids`	—	`CoalgHomClass.toSemilinearMapClass` `coalgHomClass`
`congr_arg` 📖	mathematical	—	`DFunLike.coe` `CoalgHom` `funLike`	—	`DFunLike.congr_arg`
`congr_fun` 📖	mathematical	—	`DFunLike.coe` `CoalgHom` `funLike`	—	`DFunLike.congr_fun`
`copy_eq` 📖	mathematical	`DFunLike.coe` `CoalgHom` `funLike`	`copy`	—	`DFunLike.ext'`
`counit_comp` 📖	mathematical	—	`LinearMap.comp` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `RingHomCompTriple.ids` `CoalgebraStruct.counit` `toLinearMap`	—	—
`ext` 📖	—	`DFunLike.coe` `CoalgHom` `funLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `CoalgHom` `funLike`	—	`ext`
`ext_of_ring` 📖	—	`DFunLike.coe` `CoalgHom` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `Coalgebra.toCoalgebraStruct` `CommSemiring.toCoalgebra` `funLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—	`coe_linearMap_injective` `LinearMap.ext_ring` `CoalgHomClass.toSemilinearMapClass` `coalgHomClass`
`ext_of_ring_iff` 📖	mathematical	—	`DFunLike.coe` `CoalgHom` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `Coalgebra.toCoalgebraStruct` `CommSemiring.toCoalgebra` `funLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`ext_of_ring`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `CoalgHom` `funLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`id_toLinearMap` 📖	mathematical	—	`SemilinearMapClass.semilinearMap` `CoalgHom` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `id` `funLike` `CoalgHomClass.toSemilinearMapClass` `coalgHomClass` `LinearMap.id`	—	`CoalgHomClass.toSemilinearMapClass` `coalgHomClass`
`map_comp_comul` 📖	mathematical	—	`LinearMap.comp` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `TensorProduct.map` `toLinearMap` `CoalgebraStruct.comul`	—	—
`map_smul_of_tower` 📖	mathematical	—	`DFunLike.coe` `CoalgHom` `funLike`	—	`LinearMap.map_smul_of_tower`
`mk_coe` 📖	—	`DFunLike.coe` `CoalgHom` `funLike` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddHom.toFun` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.id` `LinearMap.comp` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `RingHomCompTriple.ids` `CoalgebraStruct.counit` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `TensorProduct.map` `CoalgebraStruct.comul`	—	—	`RingHomCompTriple.ids` `ext`
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `CoalgHom` `funLike` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `End`	—	—
`one_apply` 📖	mathematical	—	`DFunLike.coe` `CoalgHom` `funLike` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `End`	—	—
`toLinearMap_eq_coe` 📖	mathematical	—	`toLinearMap` `SemilinearMapClass.semilinearMap` `CoalgHom` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `funLike` `CoalgHomClass.toSemilinearMapClass` `coalgHomClass`	—	—

CoalgHom.Simps

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—

CoalgHomClass

Definitions

Name	Category	Theorems
`instCoeToCoalgHom` 📖	CompOp	—
`toCoalgHom` 📖	CompOp	22 math math: `CoalgEquiv.coe_toCoalgHom`, `CoalgEquiv.coe_ofCoalgHom`, `BialgHom.coe_coalgHom_injective`, `CoalgEquiv.toCoalgHom_inj`, `CoalgEquiv.toCoalgHom_eq_coe`, `CategoryTheory.Iso.toCoalgEquiv_toCoalgHom`, `Bialgebra.TensorProduct.map_toCoalgHom`, `BialgHom.coe_coalgHom_mk`, `CoalgEquiv.coe_coe`, `CoalgEquiv.toCoalgIso_inv`, `BialgEquiv.toCoalgEquiv_toCoalgHom`, `CoalgHom.coe_coe`, `BialgHom.coe_toCoalgHom`, `BialgHom.id_toCoalgHom`, `Bialgebra.counitBialgHom_toCoalgHom`, `CoalgEquiv.toLinearEquiv_toLinearMap`, `CoalgEquiv.symm_toCoalgHom`, `CoalgEquiv.refl_toCoalgHom`, `BialgCat.forget₂_coalgebra_map`, `CoalgEquiv.trans_toCoalgHom`, `CoalgEquiv.toCoalgIso_hom`, `BialgHom.comp_toCoalgHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`counit_comp` 📖	mathematical	—	`LinearMap.comp` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `RingHomCompTriple.ids` `CoalgebraStruct.counit` `SemilinearMapClass.semilinearMap` `toSemilinearMapClass`	—	—
`counit_comp_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `CoalgebraStruct.counit`	—	`LinearMap.congr_fun` `RingHomCompTriple.ids` `toSemilinearMapClass` `counit_comp`
`map_comp_comul` 📖	mathematical	—	`LinearMap.comp` `TensorProduct` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `TensorProduct.map` `SemilinearMapClass.semilinearMap` `toSemilinearMapClass` `CoalgebraStruct.comul`	—	—
`map_comp_comul_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `TensorProduct.map` `SemilinearMapClass.semilinearMap` `toSemilinearMapClass` `CoalgebraStruct.comul`	—	`LinearMap.congr_fun` `RingHomCompTriple.ids` `toSemilinearMapClass` `map_comp_comul`
`toSemilinearMapClass` 📖	mathematical	—	`SemilinearMapClass` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring`	—	—

Coalgebra

Definitions

Name	Category	Theorems
`counitCoalgHom` 📖	CompOp	3 math math: `counitCoalgHom_toLinearMap`, `Bialgebra.counitBialgHom_toCoalgHom`, `counitCoalgHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`counitCoalgHom_apply` 📖	mathematical	—	`DFunLike.coe` `CoalgHom` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `toCoalgebraStruct` `CommSemiring.toCoalgebra` `CoalgHom.funLike` `counitCoalgHom` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `CoalgebraStruct.counit`	—	—
`counitCoalgHom_toLinearMap` 📖	mathematical	—	`SemilinearMapClass.semilinearMap` `CoalgHom` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `toCoalgebraStruct` `CommSemiring.toCoalgebra` `RingHom.id` `counitCoalgHom` `CoalgHom.funLike` `CoalgHomClass.toSemilinearMapClass` `CoalgHom.coalgHomClass` `CoalgebraStruct.counit`	—	`CoalgHomClass.toSemilinearMapClass` `CoalgHom.coalgHomClass`
`ext_to_ring` 📖	—	—	—	—	`subsingleton_to_ring`
`ext_to_ring_iff` 📖	—	—	—	—	`ext_to_ring`
`subsingleton_to_ring` 📖	mathematical	—	`CoalgHom` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semiring.toModule` `toCoalgebraStruct` `CommSemiring.toCoalgebra`	—	`CoalgHom.ext` `CoalgHomClass.counit_comp_apply` `CoalgHom.coalgHomClass`

Coalgebra.Repr

Definitions

Name	Category	Theorems
`induced` 📖	CompOp	4 math math: `induced_ι`, `induced_index`, `induced_right`, `induced_left`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`induced_index` 📖	mathematical	—	`index` `Coalgebra.toCoalgebraStruct` `DFunLike.coe` `induced`	—	—
`induced_left` 📖	mathematical	—	`left` `Coalgebra.toCoalgebraStruct` `DFunLike.coe` `induced` `ι`	—	—
`induced_right` 📖	mathematical	—	`right` `Coalgebra.toCoalgebraStruct` `DFunLike.coe` `induced` `ι`	—	—
`induced_ι` 📖	mathematical	—	`ι` `Coalgebra.toCoalgebraStruct` `DFunLike.coe` `induced`	—	—

(root)

Definitions

Name	Category	Theorems
`CoalgHom` 📖	CompData	50 math math: `CoalgEquiv.coe_toCoalgHom`, `CoalgHom.ext_of_ring_iff`, `CoalgHom.coe_addMonoidHom_injective`, `BialgHom.coe_coalgHom_injective`, `CoalgHom.map_smul_of_tower`, `Coalgebra.subsingleton_to_ring`, `CoalgHom.comp_toLinearMap`, `CoalgEquiv.toCoalgHom_injective`, `BialgCat.forget₂_coalgebra_obj`, `CoalgHom.id_toLinearMap`, `CoalgHom.mul_apply`, `CoalgCat.MonoidalCategory.inducingFunctorData_μIso`, `CoalgCat.MonoidalCategory.inducingFunctorData_εIso`, `CoalgHom.coe_mk`, `CoalgHom.coe_id`, `CoalgEquiv.coe_coe`, `CoalgHom.coe_fn_inj`, `CoalgHom.id_apply`, `CoalgCat.forget_reflects_isos`, `Coalgebra.TensorProduct.map_tmul`, `CoalgHom.coe_coe`, `Coalgebra.counitCoalgHom_toLinearMap`, `CoalgCat.Hom.toCoalgHom_injective`, `BialgHom.coe_toCoalgHom`, `CoalgHom.coe_linearMap_injective`, `CoalgHom.congr_fun`, `CoalgEquiv.toLinearEquiv_toLinearMap`, `CoalgCat.forget₂_obj`, `CoalgHom.coe_toLinearMap`, `BialgHom.toCoalgHom_apply`, `CoalgEquiv.symm_toCoalgHom`, `CoalgCat.forget₂_map`, `CoalgHom.coe_fn_injective`, `CoalgHom.End_toOne_one`, `CoalgHom.coe_linearMap_mk`, `Coalgebra.counitCoalgHom_apply`, `CoalgCat.toComon_map_hom`, `BialgCat.forget₂_coalgebra_map`, `CoalgHom.toLinearMap_eq_coe`, `Coalgebra.TensorProduct.map_toLinearMap`, `CoalgHom.coe_mks`, `CoalgHom.coalgHomClass`, `BialgHom.coe_mk`, `CoalgHom.ext_iff`, `CoalgHom.congr_arg`, `CoalgHom.coe_comp`, `CoalgHom.coe_toAddMonoidHom`, `CoalgHom.comp_apply`, `CoalgHom.one_apply`, `CoalgHom.End_toSemigroup_toMul_mul`
`CoalgHomClass` 📖	CompData	3 math math: `CoalgHom.coalgHomClass`, `CoalgEquivClass.toCoalgHomClass`, `BialgHomClass.toCoalgHomClass`
`«term_→ₗc[_]_»` 📖	CompOp	—
`«term_→ₗc_»` 📖	CompOp	—

---

← Back to Index