CommMon_

📁 Source: Mathlib/CategoryTheory/Monoidal/CommMon_.lean

Statistics

Metric	Count
Definitions mapCommMon, CommMon, commMonToLaxBraided, commMonToLaxBraidedObj, counitIso, instLaxBraidedDiscretePUnitCommMonToLaxBraidedObj, instLaxMonoidalDiscretePUnitCommMonToLaxBraidedObj, laxBraidedToCommMon, unitIso, X, equivLaxBraidedFunctorPUnit, forget, forget₂Mon, forget₂Mon_, fullyFaithfulForget₂Mon, fullyFaithfulForget₂Mon_, homMk, instCategory, instInhabited, mkIso, mkIso', mon, toMon, toMon_, trivial, uniqueHomFromTrivial, CommMon_, mapCommMon, mapCommMon, mapCommMon, mapCommMonCompIso, mapCommMonFunctor, mapCommMonIdIso, mapCommMonNatIso, mapCommMonNatTrans	35
Theorems mapCommMon_counit, mapCommMon_unit, commMonToLaxBraidedObj_map, commMonToLaxBraidedObj_obj, commMonToLaxBraidedObj_ε, commMonToLaxBraidedObj_μ, commMonToLaxBraided_map_hom_hom_app, commMonToLaxBraided_obj, counitIso_aux_mul, counitIso_aux_one, counitIso_hom_app_hom_hom, counitIso_inv_app_hom_hom, laxBraidedToCommMon_map, laxBraidedToCommMon_obj, unitIso_hom_app_hom_hom_app, unitIso_inv_app_hom_hom_app, comm, comp_hom, equivLaxBraidedFunctorPUnit_counitIso, equivLaxBraidedFunctorPUnit_functor, equivLaxBraidedFunctorPUnit_inverse, equivLaxBraidedFunctorPUnit_unitIso, forget_map, forget_obj, forget₂Mon_comp_forget, forget₂Mon_map_hom, forget₂Mon_obj_X, forget₂Mon_obj_mul, forget₂Mon_obj_one, homMk_hom, hom_ext, hom_ext_iff, id_hom, instFaithfulForget, instFaithfulMonForget₂Mon, instFullMonForget₂Mon, instHasInitial, instIsIsoHomHomMon, mkIso'_hom_hom_hom, mkIso'_inv_hom_hom, mkIso_hom_hom_hom, mkIso_inv_hom_hom, toMon_X, trivial_X, trivial_mon_mul, trivial_mon_one, mapCommMon_counitIso, mapCommMon_functor, mapCommMon_inverse, mapCommMon_unitIso, mapCommMon, mapCommMon, mapCommMon_preimage, comp_mapCommMon_mul, comp_mapCommMon_one, isCommMonObj_obj, mapCommMonCompIso_hom_app_hom_hom, mapCommMonCompIso_inv_app_hom_hom, mapCommMonFunctor_map_app, mapCommMonFunctor_obj, mapCommMonIdIso_hom_app_hom_hom, mapCommMonIdIso_inv_app_hom_hom, mapCommMonNatIso_hom_app_hom_hom, mapCommMonNatIso_inv_app_hom_hom, mapCommMonNatTrans_app_hom_hom, mapCommMon_id_mul, mapCommMon_id_one, mapCommMon_map_hom_hom, mapCommMon_obj_X, mapCommMon_obj_mon_mul, mapCommMon_obj_mon_one	71
Total	106

CategoryTheory

Definitions

Name	Category	Theorems
CommMon 📖	CompData	84 math math: Functor.Faithful.mapCommMon, CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_map, CommGrp.instFullCommMonForget₂CommMon, CommMon.comp_hom, Functor.mapCommMonNatIso_inv_app_hom_hom, Functor.mapCommMon_obj_mon_mul, Equivalence.mapCommMon_inverse, CommMon.forget_map, Monoidal.CommMonFunctorCategoryEquivalence.counitIso_inv_app_app_hom_hom, Functor.mapCommMonNatTrans_app_hom_hom, CommMon.EquivLaxBraidedFunctorPUnit.unitIso_hom_app_hom_hom_app, CommMon.mkIso'_inv_hom_hom, Adjunction.mapCommMon_unit, Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_mul_app, CommMon.equivLaxBraidedFunctorPUnit_unitIso, Adjunction.mapCommMon_counit, Monoidal.CommMonFunctorCategoryEquivalence.unitIso_inv_app_hom_hom_app, Functor.mapCommMonNatIso_hom_app_hom_hom, CommMon.instIsIsoHomHomMon, CommGrp.forget₂CommMon_map_hom, Functor.mapCommMon_obj_X, CommMon.equivLaxBraidedFunctorPUnit_functor, Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_one_app, CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_hom_hom_app, CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_obj, Monoidal.CommMonFunctorCategoryEquivalence.unitIso_hom_app_hom_hom_app, Functor.mapCommMonFunctor_map_app, Functor.mapCommMonCompIso_inv_app_hom_hom, Functor.mapCommMonIdIso_hom_app_hom_hom, Monoidal.commMonFunctorCategoryEquivalence_counitIso, Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_X, Functor.comp_mapCommMon_mul, Functor.mapCommMonFunctor_obj, Equivalence.mapCommMon_unitIso, CommGrp.instFaithfulCommMonForget₂CommMon, Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_map_hom_hom, Monoidal.CommMonFunctorCategoryEquivalence.counitIso_hom_app_app_hom_hom, CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_obj, CommMon.mkIso_inv_hom_hom, Monoidal.commMonFunctorCategoryEquivalence_unitIso, Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_X_obj, Functor.mapCommMon_id_mul, CommMon.forget₂Mon_obj_mul, Functor.Full.mapCommMon, CommMon.equivLaxBraidedFunctorPUnit_inverse, Functor.mapCommMon_map_hom_hom, Functor.FullyFaithful.mapCommMon_preimage, Monoidal.CommMonFunctorCategoryEquivalence.inverse_map_hom_hom_app, Equivalence.mapCommMon_counitIso, CommGrp.forget₂CommMon_obj_mul, Functor.mapCommMon_obj_mon_one, CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_one, CommMon.id_hom, Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_X_map, Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_mul, CommMon.instFaithfulForget, CommMon.homMk_hom, CommMon.mkIso_hom_hom_hom, CommGrp.forget₂CommMon_obj_one, CommMon.hom_ext_iff, CommMon.instFullMonForget₂Mon, Monoidal.commMonFunctorCategoryEquivalence_functor, CommMon.forget_obj, CommMon.EquivLaxBraidedFunctorPUnit.unitIso_inv_app_hom_hom_app, CommMon.forget₂Mon_comp_forget, CommMon.instHasInitial, Functor.mapCommMonIdIso_inv_app_hom_hom, CommMon.EquivLaxBraidedFunctorPUnit.counitIso_inv_app_hom_hom, CommMon.forget₂Mon_obj_X, Functor.mapCommMon_id_one, CommMon.mkIso'_hom_hom_hom, CommMon.instFaithfulMonForget₂Mon, CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_mul, CommMon.EquivLaxBraidedFunctorPUnit.counitIso_hom_app_hom_hom, Equivalence.mapCommMon_functor, CommGrp.forget₂CommMon_comp_forget, CommMon.equivLaxBraidedFunctorPUnit_counitIso, CommMon.forget₂Mon_map_hom, Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_one, Monoidal.CommMonFunctorCategoryEquivalence.functor_map_app_hom_hom, Monoidal.commMonFunctorCategoryEquivalence_inverse, CommMon.forget₂Mon_obj_one, Functor.comp_mapCommMon_one, Functor.mapCommMonCompIso_hom_app_hom_hom
CommMon_ 📖	CompOp	—

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
mapCommMon 📖	CompOp	2 math math: mapCommMon_unit, mapCommMon_counit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapCommMon_counit 📖	mathematical	—	counit CategoryTheory.CommMon CategoryTheory.CommMon.instCategory CategoryTheory.Functor.mapCommMon CategoryTheory.Functor.Braided.toLaxBraided mapCommMon CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.LaxBraided.instComp CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor.mapCommMonCompIso CategoryTheory.Functor.LaxBraided.id CategoryTheory.Functor.mapCommMonNatTrans CategoryTheory.Iso.hom CategoryTheory.Functor.mapCommMonIdIso	—	—
mapCommMon_unit 📖	mathematical	—	unit CategoryTheory.CommMon CategoryTheory.CommMon.instCategory CategoryTheory.Functor.mapCommMon CategoryTheory.Functor.Braided.toLaxBraided mapCommMon CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.LaxBraided.id CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor.mapCommMonIdIso CategoryTheory.Functor.LaxBraided.instComp CategoryTheory.Functor.mapCommMonNatTrans CategoryTheory.Iso.hom CategoryTheory.Functor.mapCommMonCompIso	—	—

CategoryTheory.CommMon

Definitions

Name	Category	Theorems
X 📖	CompOp	48 math math: EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_obj, CategoryTheory.Functor.mapCommMonNatIso_inv_app_hom_hom, CategoryTheory.Functor.mapCommMon_obj_mon_mul, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso_inv_app_app_hom_hom, CategoryTheory.Functor.mapCommMonNatTrans_app_hom_hom, CategoryTheory.CommGrp.toCommMon_X, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_mul_app, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_inv_app_hom_hom_app, CategoryTheory.Functor.mapCommMonNatIso_hom_app_hom_hom, CategoryTheory.Functor.mapCommMon_obj_X, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_one_app, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_hom_app_hom_hom_app, CategoryTheory.Functor.mapCommMonFunctor_map_app, CategoryTheory.Functor.mapCommMonCompIso_inv_app_hom_hom, CategoryTheory.Functor.mapCommMonIdIso_hom_app_hom_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_X, CategoryTheory.Functor.comp_mapCommMon_mul, toMon_X, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_map_hom_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso_hom_app_app_hom_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_X_obj, CategoryTheory.Functor.mapCommMon_id_mul, forget₂Mon_obj_mul, CategoryTheory.Functor.mapCommMon_map_hom_hom, CategoryTheory.CommGrp.forget₂CommMon_obj_mul, CategoryTheory.Functor.mapCommMon_obj_mon_one, EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_μ, EquivLaxBraidedFunctorPUnit.counitIso_aux_one, id_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_X_map, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_mul, CategoryTheory.CommGrp.forget₂CommMon_obj_one, comm, forget_obj, EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_ε, CategoryTheory.Functor.mapCommMonIdIso_inv_app_hom_hom, EquivLaxBraidedFunctorPUnit.counitIso_inv_app_hom_hom, forget₂Mon_obj_X, CategoryTheory.Functor.mapCommMon_id_one, EquivLaxBraidedFunctorPUnit.counitIso_aux_mul, EquivLaxBraidedFunctorPUnit.counitIso_hom_app_hom_hom, EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_map, trivial_X, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_one, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_map_app_hom_hom, forget₂Mon_obj_one, CategoryTheory.Functor.comp_mapCommMon_one, CategoryTheory.Functor.mapCommMonCompIso_hom_app_hom_hom
equivLaxBraidedFunctorPUnit 📖	CompOp	4 math math: equivLaxBraidedFunctorPUnit_unitIso, equivLaxBraidedFunctorPUnit_functor, equivLaxBraidedFunctorPUnit_inverse, equivLaxBraidedFunctorPUnit_counitIso
forget 📖	CompOp	5 math math: forget_map, instFaithfulForget, forget_obj, forget₂Mon_comp_forget, CategoryTheory.CommGrp.forget₂CommMon_comp_forget
forget₂Mon 📖	CompOp	24 math math: CategoryTheory.Functor.mapCommMonNatIso_inv_app_hom_hom, mkIso'_inv_hom_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_mul_app, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_inv_app_hom_hom_app, CategoryTheory.Functor.mapCommMonNatIso_hom_app_hom_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_one_app, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_hom_app_hom_hom_app, CategoryTheory.Functor.mapCommMonCompIso_inv_app_hom_hom, CategoryTheory.Functor.mapCommMonIdIso_hom_app_hom_hom, mkIso_inv_hom_hom, forget₂Mon_obj_mul, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_map_hom_hom_app, mkIso_hom_hom_hom, instFullMonForget₂Mon, forget₂Mon_comp_forget, CategoryTheory.Functor.mapCommMonIdIso_inv_app_hom_hom, EquivLaxBraidedFunctorPUnit.counitIso_inv_app_hom_hom, forget₂Mon_obj_X, mkIso'_hom_hom_hom, instFaithfulMonForget₂Mon, EquivLaxBraidedFunctorPUnit.counitIso_hom_app_hom_hom, forget₂Mon_map_hom, forget₂Mon_obj_one, CategoryTheory.Functor.mapCommMonCompIso_hom_app_hom_hom
forget₂Mon_ 📖	CompOp	—
fullyFaithfulForget₂Mon 📖	CompOp	—
fullyFaithfulForget₂Mon_ 📖	CompOp	—
homMk 📖	CompOp	4 math math: CategoryTheory.Functor.mapCommMonFunctor_map_app, CategoryTheory.Functor.FullyFaithful.mapCommMon_preimage, homMk_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_map_app_hom_hom
instCategory 📖	CompOp	81 math math: CategoryTheory.Functor.Faithful.mapCommMon, EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_map, CategoryTheory.CommGrp.instFullCommMonForget₂CommMon, comp_hom, CategoryTheory.Functor.mapCommMonNatIso_inv_app_hom_hom, CategoryTheory.Functor.mapCommMon_obj_mon_mul, CategoryTheory.Equivalence.mapCommMon_inverse, forget_map, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso_inv_app_app_hom_hom, CategoryTheory.Functor.mapCommMonNatTrans_app_hom_hom, EquivLaxBraidedFunctorPUnit.unitIso_hom_app_hom_hom_app, mkIso'_inv_hom_hom, CategoryTheory.Adjunction.mapCommMon_unit, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_mul_app, equivLaxBraidedFunctorPUnit_unitIso, CategoryTheory.Adjunction.mapCommMon_counit, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_inv_app_hom_hom_app, CategoryTheory.Functor.mapCommMonNatIso_hom_app_hom_hom, CategoryTheory.CommGrp.forget₂CommMon_map_hom, CategoryTheory.Functor.mapCommMon_obj_X, equivLaxBraidedFunctorPUnit_functor, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_one_app, EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_hom_hom_app, EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_obj, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_hom_app_hom_hom_app, CategoryTheory.Functor.mapCommMonFunctor_map_app, CategoryTheory.Functor.mapCommMonCompIso_inv_app_hom_hom, CategoryTheory.Functor.mapCommMonIdIso_hom_app_hom_hom, CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_counitIso, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_X, CategoryTheory.Functor.comp_mapCommMon_mul, CategoryTheory.Functor.mapCommMonFunctor_obj, CategoryTheory.Equivalence.mapCommMon_unitIso, CategoryTheory.CommGrp.instFaithfulCommMonForget₂CommMon, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_map_hom_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso_hom_app_app_hom_hom, EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_obj, mkIso_inv_hom_hom, CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_unitIso, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_X_obj, CategoryTheory.Functor.mapCommMon_id_mul, forget₂Mon_obj_mul, CategoryTheory.Functor.Full.mapCommMon, equivLaxBraidedFunctorPUnit_inverse, CategoryTheory.Functor.mapCommMon_map_hom_hom, CategoryTheory.Functor.FullyFaithful.mapCommMon_preimage, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_map_hom_hom_app, CategoryTheory.Equivalence.mapCommMon_counitIso, CategoryTheory.CommGrp.forget₂CommMon_obj_mul, CategoryTheory.Functor.mapCommMon_obj_mon_one, EquivLaxBraidedFunctorPUnit.counitIso_aux_one, id_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_X_map, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_mul, instFaithfulForget, mkIso_hom_hom_hom, CategoryTheory.CommGrp.forget₂CommMon_obj_one, instFullMonForget₂Mon, CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_functor, forget_obj, EquivLaxBraidedFunctorPUnit.unitIso_inv_app_hom_hom_app, forget₂Mon_comp_forget, instHasInitial, CategoryTheory.Functor.mapCommMonIdIso_inv_app_hom_hom, EquivLaxBraidedFunctorPUnit.counitIso_inv_app_hom_hom, forget₂Mon_obj_X, CategoryTheory.Functor.mapCommMon_id_one, mkIso'_hom_hom_hom, instFaithfulMonForget₂Mon, EquivLaxBraidedFunctorPUnit.counitIso_aux_mul, EquivLaxBraidedFunctorPUnit.counitIso_hom_app_hom_hom, CategoryTheory.Equivalence.mapCommMon_functor, CategoryTheory.CommGrp.forget₂CommMon_comp_forget, equivLaxBraidedFunctorPUnit_counitIso, forget₂Mon_map_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_one, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_map_app_hom_hom, CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_inverse, forget₂Mon_obj_one, CategoryTheory.Functor.comp_mapCommMon_one, CategoryTheory.Functor.mapCommMonCompIso_hom_app_hom_hom
instInhabited 📖	CompOp	—
mkIso 📖	CompOp	2 math math: mkIso_inv_hom_hom, mkIso_hom_hom_hom
mkIso' 📖	CompOp	2 math math: mkIso'_inv_hom_hom, mkIso'_hom_hom_hom
mon 📖	CompOp	31 math math: CategoryTheory.Functor.mapCommMonNatIso_inv_app_hom_hom, CategoryTheory.Functor.mapCommMon_obj_mon_mul, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_mul_app, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_inv_app_hom_hom_app, CategoryTheory.Functor.mapCommMonNatIso_hom_app_hom_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_one_app, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_hom_app_hom_hom_app, CategoryTheory.Functor.mapCommMonCompIso_inv_app_hom_hom, CategoryTheory.Functor.mapCommMonIdIso_hom_app_hom_hom, CategoryTheory.Functor.comp_mapCommMon_mul, CategoryTheory.Functor.mapCommMon_id_mul, forget₂Mon_obj_mul, CategoryTheory.CommGrp.forget₂CommMon_obj_mul, CategoryTheory.Functor.mapCommMon_obj_mon_one, EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_μ, trivial_mon_one, EquivLaxBraidedFunctorPUnit.counitIso_aux_one, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_mul, CategoryTheory.CommGrp.forget₂CommMon_obj_one, trivial_mon_mul, comm, EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_ε, CategoryTheory.Functor.mapCommMonIdIso_inv_app_hom_hom, EquivLaxBraidedFunctorPUnit.counitIso_inv_app_hom_hom, CategoryTheory.Functor.mapCommMon_id_one, EquivLaxBraidedFunctorPUnit.counitIso_aux_mul, EquivLaxBraidedFunctorPUnit.counitIso_hom_app_hom_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_one, forget₂Mon_obj_one, CategoryTheory.Functor.comp_mapCommMon_one, CategoryTheory.Functor.mapCommMonCompIso_hom_app_hom_hom
toMon 📖	CompOp	38 math math: comp_hom, CategoryTheory.Functor.mapCommMonNatIso_inv_app_hom_hom, CategoryTheory.Functor.mapCommMon_obj_mon_mul, forget_map, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso_inv_app_app_hom_hom, CategoryTheory.Functor.mapCommMonNatTrans_app_hom_hom, mkIso'_inv_hom_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_inv_app_hom_hom_app, CategoryTheory.Functor.mapCommMonNatIso_hom_app_hom_hom, instIsIsoHomHomMon, CategoryTheory.CommGrp.forget₂CommMon_map_hom, EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_hom_hom_app, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_hom_app_hom_hom_app, CategoryTheory.Functor.mapCommMonFunctor_map_app, CategoryTheory.Functor.mapCommMonCompIso_inv_app_hom_hom, CategoryTheory.Functor.mapCommMonIdIso_hom_app_hom_hom, toMon_X, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_map_hom_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso_hom_app_app_hom_hom, mkIso_inv_hom_hom, CategoryTheory.Functor.mapCommMon_map_hom_hom, CategoryTheory.Functor.FullyFaithful.mapCommMon_preimage, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_map_hom_hom_app, CategoryTheory.Functor.mapCommMon_obj_mon_one, id_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_X_map, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_mul, homMk_hom, mkIso_hom_hom_hom, hom_ext_iff, CategoryTheory.Functor.mapCommMonIdIso_inv_app_hom_hom, EquivLaxBraidedFunctorPUnit.counitIso_inv_app_hom_hom, mkIso'_hom_hom_hom, EquivLaxBraidedFunctorPUnit.counitIso_hom_app_hom_hom, forget₂Mon_map_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_one, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_map_app_hom_hom, CategoryTheory.Functor.mapCommMonCompIso_hom_app_hom_hom
toMon_ 📖	CompOp	—
trivial 📖	CompOp	5 math math: EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_map, EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_obj, trivial_mon_one, trivial_mon_mul, trivial_X
uniqueHomFromTrivial 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	—	CategoryTheory.IsCommMonObj X mon	—	—
comp_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommMon CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Mon.X	—	—
equivLaxBraidedFunctorPUnit_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.LaxBraidedFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.instBraidedCategoryDiscrete CommGroup.toCommMonoid PUnit.commGroup CategoryTheory.CommMon CategoryTheory.LaxBraidedFunctor.instCategory instCategory equivLaxBraidedFunctorPUnit EquivLaxBraidedFunctorPUnit.counitIso	—	—
equivLaxBraidedFunctorPUnit_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.LaxBraidedFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.instBraidedCategoryDiscrete CommGroup.toCommMonoid PUnit.commGroup CategoryTheory.CommMon CategoryTheory.LaxBraidedFunctor.instCategory instCategory equivLaxBraidedFunctorPUnit EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon	—	—
equivLaxBraidedFunctorPUnit_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.LaxBraidedFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.instBraidedCategoryDiscrete CommGroup.toCommMonoid PUnit.commGroup CategoryTheory.CommMon CategoryTheory.LaxBraidedFunctor.instCategory instCategory equivLaxBraidedFunctorPUnit EquivLaxBraidedFunctorPUnit.commMonToLaxBraided	—	—
equivLaxBraidedFunctorPUnit_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.LaxBraidedFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.instBraidedCategoryDiscrete CommGroup.toCommMonoid PUnit.commGroup CategoryTheory.CommMon CategoryTheory.LaxBraidedFunctor.instCategory instCategory equivLaxBraidedFunctorPUnit EquivLaxBraidedFunctorPUnit.unitIso	—	—
forget_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.CommMon instCategory forget CategoryTheory.Mon.Hom.hom toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.CommMon instCategory forget X	—	—
forget₂Mon_comp_forget 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.CommMon instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory forget₂Mon CategoryTheory.Mon.forget forget	—	—
forget₂Mon_map_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.Functor.obj CategoryTheory.CommMon instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory forget₂Mon CategoryTheory.Functor.map toMon CategoryTheory.InducedCategory.Hom.hom	—	—
forget₂Mon_obj_X 📖	mathematical	—	CategoryTheory.Mon.X CategoryTheory.Functor.obj CategoryTheory.CommMon instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory forget₂Mon X	—	—
forget₂Mon_obj_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.Mon.X CategoryTheory.Functor.obj CategoryTheory.CommMon instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory forget₂Mon CategoryTheory.Mon.mon X mon	—	—
forget₂Mon_obj_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.Mon.X CategoryTheory.Functor.obj CategoryTheory.CommMon instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory forget₂Mon CategoryTheory.Mon.mon X mon	—	—
homMk_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommMon CategoryTheory.Mon CategoryTheory.Mon.instCategory toMon homMk	—	—
hom_ext 📖	—	CategoryTheory.Mon.Hom.hom toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommMon CategoryTheory.Mon CategoryTheory.Mon.instCategory	—	—	CategoryTheory.InducedCategory.hom_ext CategoryTheory.Mon.Hom.ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.Mon.Hom.hom toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommMon CategoryTheory.Mon CategoryTheory.Mon.instCategory	—	hom_ext
id_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommMon CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct instCategory X	—	—
instFaithfulForget 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.CommMon instCategory forget	—	hom_ext
instFaithfulMonForget₂Mon 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.CommMon instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory forget₂Mon	—	CategoryTheory.InducedCategory.faithful
instFullMonForget₂Mon 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.CommMon instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory forget₂Mon	—	CategoryTheory.InducedCategory.full
instHasInitial 📖	mathematical	—	CategoryTheory.Limits.HasInitial CategoryTheory.CommMon instCategory	—	CategoryTheory.Limits.hasInitial_of_unique Unique.instSubsingleton
instIsIsoHomHomMon 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Mon.X toMon CategoryTheory.Mon.Hom.hom CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommMon CategoryTheory.Mon CategoryTheory.Mon.instCategory	—	CategoryTheory.Functor.map_isIso
mkIso'_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.Functor.obj CategoryTheory.CommMon instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory forget₂Mon CategoryTheory.InducedCategory.Hom.hom toMon CategoryTheory.Iso.hom mkIso'	—	—
mkIso'_inv_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.Functor.obj CategoryTheory.CommMon instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory forget₂Mon CategoryTheory.InducedCategory.Hom.hom toMon CategoryTheory.Iso.inv mkIso'	—	—
mkIso_hom_hom_hom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one mon CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonObj.mul CategoryTheory.MonoidalCategoryStruct.tensorHom	CategoryTheory.Mon.Hom.hom CategoryTheory.Functor.obj CategoryTheory.CommMon instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory forget₂Mon comm CategoryTheory.InducedCategory.Hom.hom toMon mkIso	—	comm
mkIso_inv_hom_hom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one mon CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonObj.mul CategoryTheory.MonoidalCategoryStruct.tensorHom	CategoryTheory.Mon.Hom.hom CategoryTheory.Functor.obj CategoryTheory.CommMon instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory forget₂Mon comm CategoryTheory.InducedCategory.Hom.hom toMon CategoryTheory.Iso.inv mkIso	—	comm
toMon_X 📖	mathematical	—	CategoryTheory.Mon.X toMon X	—	—
trivial_X 📖	mathematical	—	X trivial CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
trivial_mon_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct mon trivial CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
trivial_mon_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct mon trivial CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—

CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit

Definitions

Name	Category	Theorems
commMonToLaxBraided 📖	CompOp	9 math math: unitIso_hom_app_hom_hom_app, commMonToLaxBraided_map_hom_hom_app, commMonToLaxBraided_obj, CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_inverse, counitIso_aux_one, unitIso_inv_app_hom_hom_app, counitIso_inv_app_hom_hom, counitIso_aux_mul, counitIso_hom_app_hom_hom
commMonToLaxBraidedObj 📖	CompOp	6 math math: commMonToLaxBraidedObj_obj, commMonToLaxBraided_map_hom_hom_app, commMonToLaxBraided_obj, commMonToLaxBraidedObj_μ, commMonToLaxBraidedObj_ε, commMonToLaxBraidedObj_map
counitIso 📖	CompOp	3 math math: counitIso_inv_app_hom_hom, counitIso_hom_app_hom_hom, CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_counitIso
instLaxBraidedDiscretePUnitCommMonToLaxBraidedObj 📖	CompOp	2 math math: commMonToLaxBraided_map_hom_hom_app, commMonToLaxBraided_obj
instLaxMonoidalDiscretePUnitCommMonToLaxBraidedObj 📖	CompOp	2 math math: commMonToLaxBraidedObj_μ, commMonToLaxBraidedObj_ε
laxBraidedToCommMon 📖	CompOp	9 math math: laxBraidedToCommMon_map, unitIso_hom_app_hom_hom_app, CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_functor, laxBraidedToCommMon_obj, counitIso_aux_one, unitIso_inv_app_hom_hom_app, counitIso_inv_app_hom_hom, counitIso_aux_mul, counitIso_hom_app_hom_hom
unitIso 📖	CompOp	3 math math: unitIso_hom_app_hom_hom_app, CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_unitIso, unitIso_inv_app_hom_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commMonToLaxBraidedObj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Discrete CategoryTheory.discreteCategory commMonToLaxBraidedObj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.CommMon.X	—	—
commMonToLaxBraidedObj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory commMonToLaxBraidedObj CategoryTheory.CommMon.X	—	—
commMonToLaxBraidedObj_ε 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup commMonToLaxBraidedObj instLaxMonoidalDiscretePUnitCommMonToLaxBraidedObj CategoryTheory.MonObj.one CategoryTheory.CommMon.X CategoryTheory.CommMon.mon	—	—
commMonToLaxBraidedObj_μ 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup commMonToLaxBraidedObj instLaxMonoidalDiscretePUnitCommMonToLaxBraidedObj CategoryTheory.MonObj.mul CategoryTheory.CommMon.X CategoryTheory.CommMon.mon	—	—
commMonToLaxBraided_map_hom_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.LaxMonoidalFunctor.toFunctor CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.LaxBraidedFunctor.toLaxMonoidalFunctor CategoryTheory.instBraidedCategoryDiscrete CommGroup.toCommMonoid PUnit.commGroup CategoryTheory.LaxBraidedFunctor.of commMonToLaxBraidedObj instLaxBraidedDiscretePUnitCommMonToLaxBraidedObj CategoryTheory.LaxMonoidalFunctor.Hom.hom CategoryTheory.InducedCategory.Hom.hom CategoryTheory.LaxBraidedFunctor CategoryTheory.LaxMonoidalFunctor CategoryTheory.LaxMonoidalFunctor.instCategory CategoryTheory.Functor.map CategoryTheory.CommMon CategoryTheory.CommMon.instCategory CategoryTheory.LaxBraidedFunctor.instCategory commMonToLaxBraided CategoryTheory.Mon.Hom.hom CategoryTheory.CommMon.toMon CategoryTheory.Mon CategoryTheory.Mon.instCategory	—	—
commMonToLaxBraided_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.CommMon CategoryTheory.CommMon.instCategory CategoryTheory.LaxBraidedFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.instBraidedCategoryDiscrete CommGroup.toCommMonoid PUnit.commGroup CategoryTheory.LaxBraidedFunctor.instCategory commMonToLaxBraided CategoryTheory.LaxBraidedFunctor.of commMonToLaxBraidedObj instLaxBraidedDiscretePUnitCommMonToLaxBraidedObj	—	—
counitIso_aux_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.CommMon.X CategoryTheory.Functor.obj CategoryTheory.CommMon CategoryTheory.CommMon.instCategory CategoryTheory.Functor.comp CategoryTheory.LaxBraidedFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.instBraidedCategoryDiscrete CommGroup.toCommMonoid PUnit.commGroup CategoryTheory.LaxBraidedFunctor.instCategory commMonToLaxBraided laxBraidedToCommMon CategoryTheory.CommMon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	—
counitIso_aux_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.CommMon.X CategoryTheory.Functor.obj CategoryTheory.CommMon CategoryTheory.CommMon.instCategory CategoryTheory.Functor.comp CategoryTheory.LaxBraidedFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.instBraidedCategoryDiscrete CommGroup.toCommMonoid PUnit.commGroup CategoryTheory.LaxBraidedFunctor.instCategory commMonToLaxBraided laxBraidedToCommMon CategoryTheory.CommMon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	—
counitIso_hom_app_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.Functor.obj CategoryTheory.CommMon CategoryTheory.CommMon.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CommMon.forget₂Mon CategoryTheory.CommMon.X CategoryTheory.Functor.comp CategoryTheory.LaxBraidedFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.instBraidedCategoryDiscrete CommGroup.toCommMonoid PUnit.commGroup CategoryTheory.LaxBraidedFunctor.instCategory commMonToLaxBraided laxBraidedToCommMon CategoryTheory.CommMon.mon CategoryTheory.CommMon.comm CategoryTheory.Functor.id CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommMon.toMon CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.CommMon.comm
counitIso_inv_app_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.Functor.obj CategoryTheory.CommMon CategoryTheory.CommMon.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CommMon.forget₂Mon CategoryTheory.CommMon.X CategoryTheory.Functor.id CategoryTheory.CommMon.mon CategoryTheory.CommMon.comm CategoryTheory.Functor.comp CategoryTheory.LaxBraidedFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.instBraidedCategoryDiscrete CommGroup.toCommMonoid PUnit.commGroup CategoryTheory.LaxBraidedFunctor.instCategory commMonToLaxBraided laxBraidedToCommMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommMon.toMon CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.CommMon.comm
laxBraidedToCommMon_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.LaxBraidedFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.instBraidedCategoryDiscrete CommGroup.toCommMonoid PUnit.commGroup CategoryTheory.LaxBraidedFunctor.instCategory CategoryTheory.CommMon CategoryTheory.CommMon.instCategory laxBraidedToCommMon CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.mapCommMonFunctor CategoryTheory.CommMon.trivial	—	—
laxBraidedToCommMon_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.LaxBraidedFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.instBraidedCategoryDiscrete CommGroup.toCommMonoid PUnit.commGroup CategoryTheory.LaxBraidedFunctor.instCategory CategoryTheory.CommMon CategoryTheory.CommMon.instCategory laxBraidedToCommMon CategoryTheory.Functor.mapCommMon CategoryTheory.LaxBraidedFunctor.toFunctor CategoryTheory.LaxBraidedFunctor.laxBraided CategoryTheory.CommMon.trivial	—	—
unitIso_hom_app_hom_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.LaxMonoidalFunctor.toFunctor CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.Functor.obj CategoryTheory.LaxBraidedFunctor CategoryTheory.instBraidedCategoryDiscrete CommGroup.toCommMonoid PUnit.commGroup CategoryTheory.LaxBraidedFunctor.instCategory CategoryTheory.LaxMonoidalFunctor CategoryTheory.LaxMonoidalFunctor.instCategory CategoryTheory.LaxBraidedFunctor.forget CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.CommMon CategoryTheory.CommMon.instCategory laxBraidedToCommMon commMonToLaxBraided CategoryTheory.LaxMonoidalFunctor.Hom.hom CategoryTheory.InducedCategory.Hom.hom CategoryTheory.LaxBraidedFunctor.toLaxMonoidalFunctor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category unitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.LaxBraidedFunctor.toFunctor	—	CategoryTheory.Discrete.functor_map_id
unitIso_inv_app_hom_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.LaxMonoidalFunctor.toFunctor CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.Functor.obj CategoryTheory.LaxBraidedFunctor CategoryTheory.instBraidedCategoryDiscrete CommGroup.toCommMonoid PUnit.commGroup CategoryTheory.LaxBraidedFunctor.instCategory CategoryTheory.LaxMonoidalFunctor CategoryTheory.LaxMonoidalFunctor.instCategory CategoryTheory.LaxBraidedFunctor.forget CategoryTheory.Functor.comp CategoryTheory.CommMon CategoryTheory.CommMon.instCategory laxBraidedToCommMon commMonToLaxBraided CategoryTheory.Functor.id CategoryTheory.LaxMonoidalFunctor.Hom.hom CategoryTheory.InducedCategory.Hom.hom CategoryTheory.LaxBraidedFunctor.toLaxMonoidalFunctor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category unitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.LaxBraidedFunctor.toFunctor CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	CategoryTheory.Discrete.functor_map_id

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
mapCommMon 📖	CompOp	4 math math: mapCommMon_inverse, mapCommMon_unitIso, mapCommMon_counitIso, mapCommMon_functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapCommMon_counitIso 📖	mathematical	—	counitIso CategoryTheory.CommMon CategoryTheory.CommMon.instCategory mapCommMon CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.mapCommMon inverse CategoryTheory.Functor.Braided.toLaxBraided functor CategoryTheory.Functor.LaxBraided.instComp CategoryTheory.Functor.id CategoryTheory.Iso.symm CategoryTheory.Functor.mapCommMonCompIso CategoryTheory.Functor.LaxBraided.id CategoryTheory.Functor.mapCommMonNatIso CategoryTheory.Functor.mapCommMonIdIso	—	—
mapCommMon_functor 📖	mathematical	—	functor CategoryTheory.CommMon CategoryTheory.CommMon.instCategory mapCommMon CategoryTheory.Functor.mapCommMon CategoryTheory.Functor.Braided.toLaxBraided	—	—
mapCommMon_inverse 📖	mathematical	—	inverse CategoryTheory.CommMon CategoryTheory.CommMon.instCategory mapCommMon CategoryTheory.Functor.mapCommMon CategoryTheory.Functor.Braided.toLaxBraided	—	—
mapCommMon_unitIso 📖	mathematical	—	unitIso CategoryTheory.CommMon CategoryTheory.CommMon.instCategory mapCommMon CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.mapCommMon CategoryTheory.Functor.LaxBraided.id CategoryTheory.Functor.comp functor CategoryTheory.Functor.Braided.toLaxBraided inverse CategoryTheory.Iso.symm CategoryTheory.Functor.mapCommMonIdIso CategoryTheory.Functor.LaxBraided.instComp CategoryTheory.Functor.mapCommMonNatIso CategoryTheory.Functor.mapCommMonCompIso	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
mapCommMon 📖	CompOp	27 math math: Faithful.mapCommMon, mapCommMonNatIso_inv_app_hom_hom, mapCommMon_obj_mon_mul, CategoryTheory.Equivalence.mapCommMon_inverse, mapCommMonNatTrans_app_hom_hom, CategoryTheory.Adjunction.mapCommMon_unit, CategoryTheory.Adjunction.mapCommMon_counit, mapCommMonNatIso_hom_app_hom_hom, mapCommMon_obj_X, mapCommMonFunctor_map_app, mapCommMonCompIso_inv_app_hom_hom, mapCommMonIdIso_hom_app_hom_hom, comp_mapCommMon_mul, mapCommMonFunctor_obj, CategoryTheory.Equivalence.mapCommMon_unitIso, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_obj, mapCommMon_id_mul, Full.mapCommMon, mapCommMon_map_hom_hom, FullyFaithful.mapCommMon_preimage, CategoryTheory.Equivalence.mapCommMon_counitIso, mapCommMon_obj_mon_one, mapCommMonIdIso_inv_app_hom_hom, mapCommMon_id_one, CategoryTheory.Equivalence.mapCommMon_functor, comp_mapCommMon_one, mapCommMonCompIso_hom_app_hom_hom
mapCommMonCompIso 📖	CompOp	6 math math: CategoryTheory.Adjunction.mapCommMon_unit, CategoryTheory.Adjunction.mapCommMon_counit, mapCommMonCompIso_inv_app_hom_hom, CategoryTheory.Equivalence.mapCommMon_unitIso, CategoryTheory.Equivalence.mapCommMon_counitIso, mapCommMonCompIso_hom_app_hom_hom
mapCommMonFunctor 📖	CompOp	3 math math: CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon_map, mapCommMonFunctor_map_app, mapCommMonFunctor_obj
mapCommMonIdIso 📖	CompOp	6 math math: CategoryTheory.Adjunction.mapCommMon_unit, CategoryTheory.Adjunction.mapCommMon_counit, mapCommMonIdIso_hom_app_hom_hom, CategoryTheory.Equivalence.mapCommMon_unitIso, CategoryTheory.Equivalence.mapCommMon_counitIso, mapCommMonIdIso_inv_app_hom_hom
mapCommMonNatIso 📖	CompOp	4 math math: mapCommMonNatIso_inv_app_hom_hom, mapCommMonNatIso_hom_app_hom_hom, CategoryTheory.Equivalence.mapCommMon_unitIso, CategoryTheory.Equivalence.mapCommMon_counitIso
mapCommMonNatTrans 📖	CompOp	3 math math: mapCommMonNatTrans_app_hom_hom, CategoryTheory.Adjunction.mapCommMon_unit, CategoryTheory.Adjunction.mapCommMon_counit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_mapCommMon_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.CommMon.X obj CategoryTheory.CommMon CategoryTheory.CommMon.instCategory mapCommMon comp LaxBraided.instComp CategoryTheory.CommMon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct LaxMonoidal.μ LaxMonoidal.comp LaxBraided.toLaxMonoidal map	—	—
comp_mapCommMon_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.CommMon.X obj CategoryTheory.CommMon CategoryTheory.CommMon.instCategory mapCommMon comp LaxBraided.instComp CategoryTheory.CommMon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct LaxMonoidal.ε LaxMonoidal.comp LaxBraided.toLaxMonoidal map	—	—
isCommMonObj_obj 📖	mathematical	—	CategoryTheory.IsCommMonObj obj monObjObj LaxBraided.toLaxMonoidal	—	LaxBraided.braided_assoc map_comp CategoryTheory.IsCommMonObj.mul_comm
mapCommMonCompIso_hom_app_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom obj CategoryTheory.CommMon CategoryTheory.CommMon.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CommMon.forget₂Mon CategoryTheory.CommMon.X mapCommMon comp LaxBraided.instComp CategoryTheory.CommMon.mon CategoryTheory.CommMon.comm CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommMon.toMon CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapCommMonCompIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.CommMon.comm
mapCommMonCompIso_inv_app_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom obj CategoryTheory.CommMon CategoryTheory.CommMon.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CommMon.forget₂Mon CategoryTheory.CommMon.X comp mapCommMon CategoryTheory.CommMon.mon CategoryTheory.CommMon.comm LaxBraided.instComp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommMon.toMon CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapCommMonCompIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.CommMon.comm
mapCommMonFunctor_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.CommMon CategoryTheory.CommMon.instCategory mapCommMon CategoryTheory.LaxBraidedFunctor.toFunctor CategoryTheory.LaxBraidedFunctor.laxBraided map CategoryTheory.LaxBraidedFunctor CategoryTheory.LaxBraidedFunctor.instCategory CategoryTheory.Functor category mapCommMonFunctor CategoryTheory.CommMon.homMk obj CategoryTheory.Mon.Hom.mk' CategoryTheory.CommMon.toMon CategoryTheory.LaxMonoidalFunctor.toFunctor CategoryTheory.LaxBraidedFunctor.toLaxMonoidalFunctor CategoryTheory.LaxMonoidalFunctor.Hom.hom CategoryTheory.InducedCategory.Hom.hom CategoryTheory.LaxMonoidalFunctor CategoryTheory.LaxMonoidalFunctor.instCategory CategoryTheory.CommMon.X	—	—
mapCommMonFunctor_obj 📖	mathematical	—	obj CategoryTheory.LaxBraidedFunctor CategoryTheory.LaxBraidedFunctor.instCategory CategoryTheory.Functor CategoryTheory.CommMon CategoryTheory.CommMon.instCategory category mapCommMonFunctor mapCommMon CategoryTheory.LaxBraidedFunctor.toFunctor CategoryTheory.LaxBraidedFunctor.laxBraided	—	—
mapCommMonIdIso_hom_app_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom obj CategoryTheory.CommMon CategoryTheory.CommMon.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CommMon.forget₂Mon CategoryTheory.CommMon.X mapCommMon id LaxBraided.id CategoryTheory.CommMon.mon CategoryTheory.CommMon.comm CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommMon.toMon CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapCommMonIdIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.CommMon.comm
mapCommMonIdIso_inv_app_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom obj CategoryTheory.CommMon CategoryTheory.CommMon.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CommMon.forget₂Mon CategoryTheory.CommMon.X id CategoryTheory.CommMon.mon CategoryTheory.CommMon.comm mapCommMon LaxBraided.id CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommMon.toMon CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapCommMonIdIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.CommMon.comm
mapCommMonNatIso_hom_app_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom obj CategoryTheory.CommMon CategoryTheory.CommMon.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CommMon.forget₂Mon CategoryTheory.CommMon.X mapCommMon CategoryTheory.CommMon.mon CategoryTheory.CommMon.comm CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommMon.toMon CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapCommMonNatIso	—	CategoryTheory.CommMon.comm
mapCommMonNatIso_inv_app_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom obj CategoryTheory.CommMon CategoryTheory.CommMon.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CommMon.forget₂Mon CategoryTheory.CommMon.X mapCommMon CategoryTheory.CommMon.mon CategoryTheory.CommMon.comm CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommMon.toMon CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapCommMonNatIso	—	CategoryTheory.CommMon.comm
mapCommMonNatTrans_app_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.CommMon.toMon obj CategoryTheory.CommMon CategoryTheory.CommMon.instCategory mapCommMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.NatTrans.app mapCommMonNatTrans CategoryTheory.CommMon.X	—	—
mapCommMon_id_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.CommMon.X obj CategoryTheory.CommMon CategoryTheory.CommMon.instCategory mapCommMon id LaxBraided.id CategoryTheory.CommMon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	—
mapCommMon_id_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.CommMon.X obj CategoryTheory.CommMon CategoryTheory.CommMon.instCategory mapCommMon id LaxBraided.id CategoryTheory.CommMon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	—
mapCommMon_map_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom obj CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon LaxBraided.toLaxMonoidal CategoryTheory.CommMon.toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommMon map CategoryTheory.CommMon.instCategory mapCommMon CategoryTheory.CommMon.X	—	—
mapCommMon_obj_X 📖	mathematical	—	CategoryTheory.CommMon.X obj CategoryTheory.CommMon CategoryTheory.CommMon.instCategory mapCommMon	—	—
mapCommMon_obj_mon_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.Mon.X obj CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon LaxBraided.toLaxMonoidal CategoryTheory.CommMon.toMon CategoryTheory.CommMon.mon CategoryTheory.CommMon CategoryTheory.CommMon.instCategory mapCommMon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CommMon.X LaxMonoidal.μ map	—	—
mapCommMon_obj_mon_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.Mon.X obj CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon LaxBraided.toLaxMonoidal CategoryTheory.CommMon.toMon CategoryTheory.CommMon.mon CategoryTheory.CommMon CategoryTheory.CommMon.instCategory mapCommMon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CommMon.X LaxMonoidal.ε map	—	—

CategoryTheory.Functor.Faithful

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapCommMon 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.CommMon CategoryTheory.CommMon.instCategory CategoryTheory.Functor.mapCommMon	—	CategoryTheory.Functor.map_injective comp CategoryTheory.CommMon.instFaithfulMonForget₂Mon mapMon CategoryTheory.Functor.congr_map

CategoryTheory.Functor.Full

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapCommMon 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.CommMon CategoryTheory.CommMon.instCategory CategoryTheory.Functor.mapCommMon CategoryTheory.Functor.Braided.toLaxBraided	—	CategoryTheory.Functor.FullyFaithful.full

CategoryTheory.Functor.FullyFaithful

Definitions

Name	Category	Theorems
mapCommMon 📖	CompOp	1 math math: mapCommMon_preimage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapCommMon_preimage 📖	mathematical	—	preimage CategoryTheory.CommMon CategoryTheory.CommMon.instCategory CategoryTheory.Functor.mapCommMon CategoryTheory.Functor.Braided.toLaxBraided mapCommMon CategoryTheory.CommMon.homMk CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.mapMon CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.Functor.Braided.toMonoidal mapMon CategoryTheory.CommMon.toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Functor.obj	—	—

---

← Back to Index