ComonEquivalence

📁 Source: Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean

Statistics

Metric	Count
Definitions comonEquivalence, instComonObjModuleCatOfCarrier, instMonoidalCategoryAux, ofComon, ofComonObj, ofComonObjCoalgebraStruct, toComon, toComonObj	8
Theorems associator_hom_toLinearMap, comul_tensorObj, comul_tensorObj_tensorObj_left, comul_tensorObj_tensorObj_right, counit_tensorObj, counit_tensorObj_tensorObj_left, counit_tensorObj_tensorObj_right, leftUnitor_hom_toLinearMap, rightUnitor_hom_toLinearMap, tensorHom_toLinearMap, tensorObj_comul, comonEquivalence_counitIso, comonEquivalence_functor, comonEquivalence_inverse, comonEquivalence_unitIso, comul_def, counit_def, ofComonObjCoalgebraStruct_comul, ofComonObjCoalgebraStruct_counit, toComonObj_X, toComon_map_hom, toComon_obj	22
Total	30

CoalgCat

Definitions

Name	Category	Theorems
comonEquivalence 📖	CompOp	4 math math: comonEquivalence_inverse, comonEquivalence_counitIso, comonEquivalence_functor, comonEquivalence_unitIso
instComonObjModuleCatOfCarrier 📖	CompOp	2 math math: comul_def, counit_def
instMonoidalCategoryAux 📖	CompOp	11 math math: MonoidalCategoryAux.tensorHom_toLinearMap, MonoidalCategoryAux.associator_hom_toLinearMap, MonoidalCategoryAux.counit_tensorObj_tensorObj_right, MonoidalCategoryAux.comul_tensorObj_tensorObj_left, MonoidalCategoryAux.tensorObj_comul, MonoidalCategoryAux.leftUnitor_hom_toLinearMap, MonoidalCategoryAux.counit_tensorObj, MonoidalCategoryAux.counit_tensorObj_tensorObj_left, MonoidalCategoryAux.comul_tensorObj_tensorObj_right, MonoidalCategoryAux.comul_tensorObj, MonoidalCategoryAux.rightUnitor_hom_toLinearMap
ofComon 📖	CompOp	3 math math: comonEquivalence_inverse, comonEquivalence_counitIso, comonEquivalence_unitIso
ofComonObj 📖	CompOp	—
ofComonObjCoalgebraStruct 📖	CompOp	2 math math: ofComonObjCoalgebraStruct_comul, ofComonObjCoalgebraStruct_counit
toComon 📖	CompOp	5 math math: comonEquivalence_counitIso, comonEquivalence_functor, comonEquivalence_unitIso, toComon_map_hom, toComon_obj
toComonObj 📖	CompOp	3 math math: toComonObj_X, toComon_map_hom, toComon_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comonEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CoalgCat CategoryTheory.Comon ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.monoidalCategory category CategoryTheory.Comon.instCategory comonEquivalence CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.comp ofComon toComon CategoryTheory.Functor.id CategoryTheory.Iso.refl CategoryTheory.Functor.obj	—	—
comonEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CoalgCat CategoryTheory.Comon ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.monoidalCategory category CategoryTheory.Comon.instCategory comonEquivalence toComon	—	—
comonEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CoalgCat CategoryTheory.Comon ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.monoidalCategory category CategoryTheory.Comon.instCategory comonEquivalence ofComon	—	—
comonEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CoalgCat CategoryTheory.Comon ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.monoidalCategory category CategoryTheory.Comon.instCategory comonEquivalence CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id CategoryTheory.Functor.comp toComon ofComon CategoryTheory.Iso.refl CategoryTheory.Functor.obj	—	—
comul_def 📖	mathematical	—	CategoryTheory.ComonObj.comul ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.monoidalCategory ModuleCat.of ModuleCat.carrier toModuleCat ModuleCat.isAddCommGroup ModuleCat.isModule instComonObjModuleCatOfCarrier ModuleCat.ofHom TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid TensorProduct.addCommGroup TensorProduct.instModule CoalgebraStruct.comul Coalgebra.toCoalgebraStruct instCoalgebra	—	—
counit_def 📖	mathematical	—	CategoryTheory.ComonObj.counit ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.monoidalCategory ModuleCat.of ModuleCat.carrier toModuleCat ModuleCat.isAddCommGroup ModuleCat.isModule instComonObjModuleCatOfCarrier ModuleCat.ofHom Ring.toAddCommGroup Semiring.toModule Ring.toSemiring CoalgebraStruct.counit CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Coalgebra.toCoalgebraStruct instCoalgebra	—	—
ofComonObjCoalgebraStruct_comul 📖	mathematical	—	CoalgebraStruct.comul ModuleCat.carrier CommRing.toRing CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ofComonObjCoalgebraStruct ModuleCat.Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorObj ModuleCat ModuleCat.moduleCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct ModuleCat.monoidalCategory CategoryTheory.ComonObj.comul	—	—
ofComonObjCoalgebraStruct_counit 📖	mathematical	—	CoalgebraStruct.counit ModuleCat.carrier CommRing.toRing CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ofComonObjCoalgebraStruct ModuleCat.Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorUnit ModuleCat ModuleCat.moduleCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct ModuleCat.monoidalCategory CategoryTheory.ComonObj.counit	—	—
toComonObj_X 📖	mathematical	—	CategoryTheory.Comon.X ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.monoidalCategory toComonObj ModuleCat.of ModuleCat.carrier toModuleCat ModuleCat.isAddCommGroup ModuleCat.isModule	—	—
toComon_map_hom 📖	mathematical	—	CategoryTheory.Comon.Hom.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.monoidalCategory toComonObj CategoryTheory.Functor.map CoalgCat category CategoryTheory.Comon CategoryTheory.Comon.instCategory toComon ModuleCat.ofHom ModuleCat.carrier toModuleCat ModuleCat.isAddCommGroup ModuleCat.isModule SemilinearMapClass.semilinearMap CoalgHom CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Coalgebra.toCoalgebraStruct instCoalgebra CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Hom.toCoalgHom' CoalgHom.funLike	—	—
toComon_obj 📖	mathematical	—	CategoryTheory.Functor.obj CoalgCat category CategoryTheory.Comon ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.monoidalCategory CategoryTheory.Comon.instCategory toComon toComonObj	—	—

CoalgCat.MonoidalCategoryAux

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_hom_toLinearMap 📖	mathematical	—	CoalgHom.toLinearMap ModuleCat.carrier CommRing.toRing CoalgCat.toModuleCat CategoryTheory.MonoidalCategoryStruct.tensorObj CoalgCat CoalgCat.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CoalgCat.instMonoidalCategoryAux CoalgCat.of CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct CoalgCat.instCoalgebra CoalgCat.Hom.toCoalgHom' CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator LinearEquiv.toLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.assoc	—	TensorProduct.ext RingHomInvPair.ids smulCommClass_self RingHomCompTriple.ids LinearMap.ext
comul_tensorObj 📖	mathematical	—	CoalgebraStruct.comul ModuleCat.carrier CommRing.toRing CoalgCat.toModuleCat CategoryTheory.MonoidalCategoryStruct.tensorObj CoalgCat CoalgCat.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CoalgCat.instMonoidalCategoryAux CoalgCat.of CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct CoalgCat.instCoalgebra TensorProduct TensorProduct.instCoalgebraStruct Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	IsScalarTower.left CoalgCat.ofComonObjCoalgebraStruct_comul IsScalarTower.to_smulCommClass' TensorProduct.isScalarTower IsScalarTower.to_smulCommClass RingHomCompTriple.ids RingHomInvPair.ids TensorProduct.smulCommClass_left CategoryTheory.BraidedCategory.unop_tensorμ ModuleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm
comul_tensorObj_tensorObj_left 📖	mathematical	—	CoalgebraStruct.comul ModuleCat.carrier CommRing.toRing CoalgCat.toModuleCat CategoryTheory.MonoidalCategoryStruct.tensorObj CoalgCat CoalgCat.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CoalgCat.instMonoidalCategoryAux CoalgCat.of CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct CoalgCat.instCoalgebra TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.instCoalgebraStruct Algebra.id TensorProduct.isScalarTower MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction Algebra.toSMul IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid	—	TensorProduct.isScalarTower IsScalarTower.left CoalgCat.ofComonObjCoalgebraStruct_comul RingHomCompTriple.ids RingHomInvPair.ids IsScalarTower.to_smulCommClass' IsScalarTower.to_smulCommClass TensorProduct.smulCommClass_left LinearMap.comp.congr_simp CategoryTheory.BraidedCategory.unop_tensorμ ModuleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm
comul_tensorObj_tensorObj_right 📖	mathematical	—	CoalgebraStruct.comul ModuleCat.carrier CommRing.toRing CoalgCat.toModuleCat CategoryTheory.MonoidalCategoryStruct.tensorObj CoalgCat CoalgCat.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CoalgCat.instMonoidalCategoryAux CoalgCat.of CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct CoalgCat.instCoalgebra TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.instCoalgebraStruct Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	IsScalarTower.left CoalgCat.ofComonObjCoalgebraStruct_comul RingHomCompTriple.ids RingHomInvPair.ids IsScalarTower.to_smulCommClass' IsScalarTower.to_smulCommClass TensorProduct.isScalarTower TensorProduct.smulCommClass_left CategoryTheory.BraidedCategory.unop_tensorμ ModuleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm
counit_tensorObj 📖	mathematical	—	CoalgebraStruct.counit ModuleCat.carrier CommRing.toRing CoalgCat.toModuleCat CategoryTheory.MonoidalCategoryStruct.tensorObj CoalgCat CoalgCat.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CoalgCat.instMonoidalCategoryAux CoalgCat.of CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct CoalgCat.instCoalgebra TensorProduct TensorProduct.instCoalgebraStruct Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	IsScalarTower.left CoalgCat.ofComonObjCoalgebraStruct_counit IsScalarTower.to_smulCommClass IsScalarTower.right RingHomCompTriple.ids RingHomInvPair.ids LinearMap.comp.congr_simp
counit_tensorObj_tensorObj_left 📖	mathematical	—	CoalgebraStruct.counit ModuleCat.carrier CommRing.toRing CoalgCat.toModuleCat CategoryTheory.MonoidalCategoryStruct.tensorObj CoalgCat CoalgCat.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CoalgCat.instMonoidalCategoryAux CoalgCat.of CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct CoalgCat.instCoalgebra TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.instCoalgebraStruct Algebra.id TensorProduct.isScalarTower MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction Algebra.toSMul IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid	—	TensorProduct.isScalarTower IsScalarTower.left CoalgCat.ofComonObjCoalgebraStruct_counit IsScalarTower.to_smulCommClass IsScalarTower.right RingHomCompTriple.ids RingHomInvPair.ids LinearMap.comp.congr_simp
counit_tensorObj_tensorObj_right 📖	mathematical	—	CoalgebraStruct.counit ModuleCat.carrier CommRing.toRing CoalgCat.toModuleCat CategoryTheory.MonoidalCategoryStruct.tensorObj CoalgCat CoalgCat.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CoalgCat.instMonoidalCategoryAux CoalgCat.of CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct CoalgCat.instCoalgebra TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.instCoalgebraStruct Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	IsScalarTower.left CoalgCat.ofComonObjCoalgebraStruct_counit IsScalarTower.to_smulCommClass IsScalarTower.right RingHomCompTriple.ids RingHomInvPair.ids LinearMap.comp.congr_simp
leftUnitor_hom_toLinearMap 📖	mathematical	—	CoalgHom.toLinearMap ModuleCat.carrier CommRing.toRing CoalgCat.toModuleCat CategoryTheory.MonoidalCategoryStruct.tensorObj CoalgCat CoalgCat.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CoalgCat.instMonoidalCategoryAux CategoryTheory.MonoidalCategoryStruct.tensorUnit CoalgCat.of CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct CoalgCat.instCoalgebra CoalgCat.Hom.toCoalgHom' CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor LinearEquiv.toLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.lid	—	TensorProduct.ext RingHomInvPair.ids LinearMap.ext_ring smulCommClass_self RingHomCompTriple.ids LinearMap.ext
rightUnitor_hom_toLinearMap 📖	mathematical	—	CoalgHom.toLinearMap ModuleCat.carrier CommRing.toRing CoalgCat.toModuleCat CategoryTheory.MonoidalCategoryStruct.tensorObj CoalgCat CoalgCat.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CoalgCat.instMonoidalCategoryAux CoalgCat.of CategoryTheory.MonoidalCategoryStruct.tensorUnit CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct CoalgCat.instCoalgebra CoalgCat.Hom.toCoalgHom' CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor LinearEquiv.toLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.rid	—	TensorProduct.ext RingHomInvPair.ids LinearMap.ext smulCommClass_self RingHomCompTriple.ids LinearMap.ext_ring
tensorHom_toLinearMap 📖	mathematical	—	CoalgHom.toLinearMap ModuleCat.carrier CommRing.toRing CoalgCat.toModuleCat CategoryTheory.MonoidalCategoryStruct.tensorObj CoalgCat CoalgCat.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CoalgCat.instMonoidalCategoryAux CoalgCat.of CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct CoalgCat.instCoalgebra CoalgCat.Hom.toCoalgHom' CategoryTheory.MonoidalCategoryStruct.tensorHom CoalgCat.ofHom TensorProduct.map RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	—
tensorObj_comul 📖	mathematical	—	CoalgebraStruct.comul ModuleCat.carrier CommRing.toRing CoalgCat.toModuleCat CategoryTheory.MonoidalCategoryStruct.tensorObj CoalgCat CoalgCat.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CoalgCat.instMonoidalCategoryAux CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Coalgebra.toCoalgebraStruct CoalgCat.instCoalgebra LinearMap.comp TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids TensorProduct.tensorTensorTensorComm TensorProduct.map	—	RingHomCompTriple.ids RingHomInvPair.ids CoalgCat.ofComonObjCoalgebraStruct_comul CategoryTheory.BraidedCategory.unop_tensorμ ModuleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm

---

← Back to Index