CommGrp_

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

Statistics

Metric	Count
Definitions mapCommGrp, CommGrp, X, forget, forget₂CommMon, forget₂CommMon_, forget₂Grp, forget₂Grp_, fullyFaithfulForget₂CommMon, fullyFaithfulForget₂Grp, fullyFaithfulForget₂Grp_, grp, instCategory, instInhabited, mkIso, mkIso', toCommMon, toCommMon_, toGrp, toGrp_, toMon, toMon_, trivial, uniqueHomFromTrivial, mapCommGrp, mapCommGrp, mapCommGrp, mapCommGrpCompIso, mapCommGrpFunctor, mapCommGrpIdIso, mapCommGrpNatIso, mapCommGrpNatTrans	32
Theorems mapCommGrp_counit, mapCommGrp_unit, comm, comp', comp_hom, forget_map, forget_obj, forget₂CommMon_comp_forget, forget₂CommMon_map_hom, forget₂CommMon_obj_mul, forget₂CommMon_obj_one, forget₂Grp_comp_forget, forget₂Grp_map_hom, forget₂Grp_obj_X, forget₂Grp_obj_mul, forget₂Grp_obj_one, hom_ext, hom_ext_iff, id', id_hom, instFaithfulCommMonForget₂CommMon, instFaithfulForget, instFaithfulGrpForget₂Grp, instFullCommMonForget₂CommMon, instFullGrpForget₂Grp, instHasInitial, instIsIsoGrpHom, instIsIsoMonHomGrp, mkIso'_hom_hom_hom_hom, mkIso'_inv_hom_hom_hom, mkIso_hom_hom, mkIso_hom_hom_hom_hom, mkIso_inv_hom, mkIso_inv_hom_hom_hom, toCommMon_X, toGrp_X, trivial_X, trivial_grp_inv, trivial_grp_mul, trivial_grp_one, mapCommGrp_counitIso, mapCommGrp_functor, mapCommGrp_inverse, mapCommGrp_unitIso, mapCommGrp, mapCommGrp, mapCommGrp_preimage, comp_mapCommGrp_mul, comp_mapCommGrp_one, mapCommGrpCompIso_hom_app_hom_hom_hom, mapCommGrpCompIso_inv_app_hom_hom_hom, mapCommGrpFunctor_map, mapCommGrpFunctor_obj, mapCommGrpIdIso_hom_app_hom_hom_hom, mapCommGrpIdIso_inv_app_hom_hom_hom, mapCommGrpNatIso_hom_app_hom_hom_hom, mapCommGrpNatIso_inv_app_hom_hom_hom, mapCommGrpNatTrans_app_hom_hom_hom, mapCommGrp_id_one, mapCommGrp_map_hom_hom_hom, mapCommGrp_obj_X, mapCommGrp_obj_grp_inv, mapCommGrp_obj_grp_mul, mapCommGrp_obj_grp_one, mapCommpGrp_id_mul	65
Total	97

CategoryTheory

Definitions

Name	Category	Theorems
CommGrp 📖	CompData	79 math math: CommGrp.instFullCommMonForget₂CommMon, Preadditive.commGrpEquivalence_functor_obj_grp_one, Functor.mapCommGrpCompIso_inv_app_hom_hom_hom, Functor.mapCommGrp_obj_grp_one, Preadditive.toCommGrp_map, CommGrpTypeEquivalenceCommGrp.inverse_obj_one, CommGrp.mkIso_inv_hom, CommGrp.id', CommGrp.comp', CommGrp.comp_hom, Preadditive.commGrpEquivalence_unitIso_inv_app, CommGrp.instFaithfulGrpForget₂Grp, Preadditive.commGrpEquivalence_unitIso_hom_app, Preadditive.commGrpEquivalence_functor_obj_grp_mul, CommGrp.instFaithfulForget, Functor.mapCommGrpFunctor_obj, Functor.mapCommGrpCompIso_hom_app_hom_hom_hom, CommGrpTypeEquivalenceCommGrp.inverse_obj_X, Adjunction.mapCommGrp_unit, Functor.Full.mapCommGrp, Preadditive.commGrpEquivalence_functor_obj_grp_inv, CommGrp.instIsIsoMonHomGrp, Equivalence.mapCommGrp_functor, Functor.mapCommGrp_obj_X, CommGrp.forget₂CommMon_map_hom, CommGrp.forget₂Grp_obj_mul, Preadditive.commGrpEquivalenceAux_hom_app_hom_hom_hom, Preadditive.commGrpEquivalence_functor_obj_X, CommGrp.forget₂Grp_obj_X, Equivalence.mapCommGrp_unitIso, Functor.mapCommGrpNatIso_inv_app_hom_hom_hom, CommGrp.instFaithfulCommMonForget₂CommMon, CommGrp.hom_ext_iff, Functor.comp_mapCommGrp_mul, CommGrp.mkIso_inv_hom_hom_hom, CommGrp.mkIso'_inv_hom_hom_hom, yonedaCommGrpGrp_obj, CommGrp.forget₂Grp_obj_one, Functor.mapCommGrp_id_one, CommGrp.forget₂Grp_comp_forget, Preadditive.commGrpEquivalenceAux_inv_app_hom_hom_hom, CommGrp.forget₂Grp_map_hom, CommGrp.forget₂CommMon_obj_mul, Functor.mapCommGrpIdIso_hom_app_hom_hom_hom, CommGrp.mkIso_hom_hom, Preadditive.toCommGrp_obj_grp, CommGrpTypeEquivalenceCommGrp.inverse_obj_inv, Preadditive.commGrpEquivalence_counitIso_inv_app_hom_hom_hom, Equivalence.mapCommGrp_inverse, Functor.FullyFaithful.mapCommGrp_preimage, CommGrp.instIsIsoGrpHom, CommGrp.instHasInitial, CommGrp.mkIso_hom_hom_hom_hom, CommGrp.id_hom, Functor.mapCommpGrp_id_mul, CommGrp.forget₂CommMon_obj_one, Functor.mapCommGrpFunctor_map, Functor.comp_mapCommGrp_one, Preadditive.commGrpEquivalence_counitIso_hom_app_hom_hom_hom, Functor.mapCommGrpIdIso_inv_app_hom_hom_hom, yonedaCommGrpGrp_map_app, CommGrp.forget_obj, Equivalence.mapCommGrp_counitIso, Functor.mapCommGrpNatIso_hom_app_hom_hom_hom, CommGrpTypeEquivalenceCommGrp.inverse_obj_mul, Functor.mapCommGrp_map_hom_hom_hom, Preadditive.commGrpEquivalence_inverse_map, Functor.mapCommGrpNatTrans_app_hom_hom_hom, CommGrp.mkIso'_hom_hom_hom_hom, Functor.mapCommGrp_obj_grp_mul, Preadditive.toCommGrp_obj_X, Preadditive.commGrpEquivalence_functor_map_hom_hom_hom, Functor.Faithful.mapCommGrp, CommGrp.forget₂CommMon_comp_forget, Preadditive.commGrpEquivalence_inverse_obj, Adjunction.mapCommGrp_counit, Functor.mapCommGrp_obj_grp_inv, CommGrp.forget_map, CommGrp.instFullGrpForget₂Grp

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
mapCommGrp 📖	CompOp	2 math math: mapCommGrp_unit, mapCommGrp_counit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapCommGrp_counit 📖	mathematical	—	counit CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory CategoryTheory.Functor.mapCommGrp mapCommGrp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.Braided.instComp CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor.mapCommGrpCompIso CategoryTheory.Functor.Braided.instId CategoryTheory.Functor.mapCommGrpNatTrans CategoryTheory.Iso.hom CategoryTheory.Functor.mapCommGrpIdIso	—	—
mapCommGrp_unit 📖	mathematical	—	unit CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory CategoryTheory.Functor.mapCommGrp mapCommGrp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.Braided.instId CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor.mapCommGrpIdIso CategoryTheory.Functor.Braided.instComp CategoryTheory.Functor.mapCommGrpNatTrans CategoryTheory.Iso.hom CategoryTheory.Functor.mapCommGrpCompIso	—	—

CategoryTheory.CommGrp

Definitions

Name	Category	Theorems
X 📖	CompOp	37 math math: CategoryTheory.Functor.mapCommGrpCompIso_inv_app_hom_hom_hom, comm, CategoryTheory.Functor.mapCommGrp_obj_grp_one, CommGrpTypeEquivalenceCommGrp.inverse_obj_one, toCommMon_X, CategoryTheory.Functor.mapCommGrpCompIso_hom_app_hom_hom_hom, CommGrpTypeEquivalenceCommGrp.inverse_obj_X, CategoryTheory.Functor.mapCommGrp_obj_X, trivial_X, forget₂Grp_obj_mul, CategoryTheory.Preadditive.commGrpEquivalenceAux_hom_app_hom_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_X, forget₂Grp_obj_X, CategoryTheory.Functor.mapCommGrpNatIso_inv_app_hom_hom_hom, CategoryTheory.Functor.comp_mapCommGrp_mul, forget₂Grp_obj_one, CategoryTheory.Functor.mapCommGrp_id_one, CategoryTheory.Preadditive.commGrpEquivalenceAux_inv_app_hom_hom_hom, forget₂CommMon_obj_mul, CategoryTheory.Functor.mapCommGrpIdIso_hom_app_hom_hom_hom, CommGrpTypeEquivalenceCommGrp.inverse_obj_inv, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_inv_app_hom_hom_hom, CategoryTheory.Functor.mapCommpGrp_id_mul, forget₂CommMon_obj_one, CategoryTheory.Functor.comp_mapCommGrp_one, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_hom_app_hom_hom_hom, CategoryTheory.Functor.mapCommGrpIdIso_inv_app_hom_hom_hom, toGrp_X, forget_obj, CategoryTheory.Functor.mapCommGrpNatIso_hom_app_hom_hom_hom, CommGrpTypeEquivalenceCommGrp.inverse_obj_mul, CategoryTheory.Functor.mapCommGrp_map_hom_hom_hom, CategoryTheory.Functor.mapCommGrpNatTrans_app_hom_hom_hom, CategoryTheory.Functor.mapCommGrp_obj_grp_mul, CategoryTheory.Preadditive.toCommGrp_obj_X, CategoryTheory.Preadditive.commGrpEquivalence_inverse_obj, CategoryTheory.Functor.mapCommGrp_obj_grp_inv
forget 📖	CompOp	9 math math: instFaithfulForget, CategoryTheory.Preadditive.commGrpEquivalenceAux_hom_app_hom_hom_hom, forget₂Grp_comp_forget, CategoryTheory.Preadditive.commGrpEquivalenceAux_inv_app_hom_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_inv_app_hom_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_hom_app_hom_hom_hom, forget_obj, forget₂CommMon_comp_forget, forget_map
forget₂CommMon 📖	CompOp	6 math math: instFullCommMonForget₂CommMon, forget₂CommMon_map_hom, instFaithfulCommMonForget₂CommMon, forget₂CommMon_obj_mul, forget₂CommMon_obj_one, forget₂CommMon_comp_forget
forget₂CommMon_ 📖	CompOp	—
forget₂Grp 📖	CompOp	21 math math: CategoryTheory.Functor.mapCommGrpCompIso_inv_app_hom_hom_hom, instFaithfulGrpForget₂Grp, CategoryTheory.Functor.mapCommGrpCompIso_hom_app_hom_hom_hom, forget₂Grp_obj_mul, CategoryTheory.Preadditive.commGrpEquivalenceAux_hom_app_hom_hom_hom, forget₂Grp_obj_X, CategoryTheory.Functor.mapCommGrpNatIso_inv_app_hom_hom_hom, mkIso'_inv_hom_hom_hom, forget₂Grp_obj_one, forget₂Grp_comp_forget, CategoryTheory.Preadditive.commGrpEquivalenceAux_inv_app_hom_hom_hom, forget₂Grp_map_hom, CategoryTheory.Functor.mapCommGrpIdIso_hom_app_hom_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_inv_app_hom_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_hom_app_hom_hom_hom, CategoryTheory.Functor.mapCommGrpIdIso_inv_app_hom_hom_hom, CategoryTheory.Functor.mapCommGrpNatIso_hom_app_hom_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_inverse_map, mkIso'_hom_hom_hom_hom, forget_map, instFullGrpForget₂Grp
forget₂Grp_ 📖	CompOp	—
fullyFaithfulForget₂CommMon 📖	CompOp	—
fullyFaithfulForget₂Grp 📖	CompOp	—
fullyFaithfulForget₂Grp_ 📖	CompOp	—
grp 📖	CompOp	32 math math: CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_one, CategoryTheory.Functor.mapCommGrpCompIso_inv_app_hom_hom_hom, comm, CategoryTheory.Functor.mapCommGrp_obj_grp_one, CommGrpTypeEquivalenceCommGrp.inverse_obj_one, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_mul, CategoryTheory.Functor.mapCommGrpCompIso_hom_app_hom_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_inv, forget₂Grp_obj_mul, CategoryTheory.Preadditive.commGrpEquivalenceAux_hom_app_hom_hom_hom, trivial_grp_one, CategoryTheory.Functor.mapCommGrpNatIso_inv_app_hom_hom_hom, CategoryTheory.Functor.comp_mapCommGrp_mul, forget₂Grp_obj_one, CategoryTheory.Functor.mapCommGrp_id_one, CategoryTheory.Preadditive.commGrpEquivalenceAux_inv_app_hom_hom_hom, forget₂CommMon_obj_mul, CategoryTheory.Functor.mapCommGrpIdIso_hom_app_hom_hom_hom, CategoryTheory.Preadditive.toCommGrp_obj_grp, CommGrpTypeEquivalenceCommGrp.inverse_obj_inv, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_inv_app_hom_hom_hom, CategoryTheory.Functor.mapCommpGrp_id_mul, forget₂CommMon_obj_one, CategoryTheory.Functor.comp_mapCommGrp_one, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_hom_app_hom_hom_hom, CategoryTheory.Functor.mapCommGrpIdIso_inv_app_hom_hom_hom, CategoryTheory.Functor.mapCommGrpNatIso_hom_app_hom_hom_hom, CommGrpTypeEquivalenceCommGrp.inverse_obj_mul, trivial_grp_mul, trivial_grp_inv, CategoryTheory.Functor.mapCommGrp_obj_grp_mul, CategoryTheory.Functor.mapCommGrp_obj_grp_inv
instCategory 📖	CompOp	76 math math: instFullCommMonForget₂CommMon, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_one, CategoryTheory.Functor.mapCommGrpCompIso_inv_app_hom_hom_hom, CategoryTheory.Functor.mapCommGrp_obj_grp_one, CategoryTheory.Preadditive.toCommGrp_map, CommGrpTypeEquivalenceCommGrp.inverse_obj_one, mkIso_inv_hom, id', comp', comp_hom, CategoryTheory.Preadditive.commGrpEquivalence_unitIso_inv_app, instFaithfulGrpForget₂Grp, CategoryTheory.Preadditive.commGrpEquivalence_unitIso_hom_app, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_mul, instFaithfulForget, CategoryTheory.Functor.mapCommGrpFunctor_obj, CategoryTheory.Functor.mapCommGrpCompIso_hom_app_hom_hom_hom, CommGrpTypeEquivalenceCommGrp.inverse_obj_X, CategoryTheory.Adjunction.mapCommGrp_unit, CategoryTheory.Functor.Full.mapCommGrp, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_inv, CategoryTheory.Equivalence.mapCommGrp_functor, CategoryTheory.Functor.mapCommGrp_obj_X, forget₂CommMon_map_hom, forget₂Grp_obj_mul, CategoryTheory.Preadditive.commGrpEquivalenceAux_hom_app_hom_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_X, forget₂Grp_obj_X, CategoryTheory.Equivalence.mapCommGrp_unitIso, CategoryTheory.Functor.mapCommGrpNatIso_inv_app_hom_hom_hom, instFaithfulCommMonForget₂CommMon, CategoryTheory.Functor.comp_mapCommGrp_mul, mkIso_inv_hom_hom_hom, mkIso'_inv_hom_hom_hom, CategoryTheory.yonedaCommGrpGrp_obj, forget₂Grp_obj_one, CategoryTheory.Functor.mapCommGrp_id_one, forget₂Grp_comp_forget, CategoryTheory.Preadditive.commGrpEquivalenceAux_inv_app_hom_hom_hom, forget₂Grp_map_hom, forget₂CommMon_obj_mul, CategoryTheory.Functor.mapCommGrpIdIso_hom_app_hom_hom_hom, mkIso_hom_hom, CategoryTheory.Preadditive.toCommGrp_obj_grp, CommGrpTypeEquivalenceCommGrp.inverse_obj_inv, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_inv_app_hom_hom_hom, CategoryTheory.Equivalence.mapCommGrp_inverse, CategoryTheory.Functor.FullyFaithful.mapCommGrp_preimage, instHasInitial, mkIso_hom_hom_hom_hom, id_hom, CategoryTheory.Functor.mapCommpGrp_id_mul, forget₂CommMon_obj_one, CategoryTheory.Functor.mapCommGrpFunctor_map, CategoryTheory.Functor.comp_mapCommGrp_one, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_hom_app_hom_hom_hom, CategoryTheory.Functor.mapCommGrpIdIso_inv_app_hom_hom_hom, CategoryTheory.yonedaCommGrpGrp_map_app, forget_obj, CategoryTheory.Equivalence.mapCommGrp_counitIso, CategoryTheory.Functor.mapCommGrpNatIso_hom_app_hom_hom_hom, CommGrpTypeEquivalenceCommGrp.inverse_obj_mul, CategoryTheory.Functor.mapCommGrp_map_hom_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_inverse_map, CategoryTheory.Functor.mapCommGrpNatTrans_app_hom_hom_hom, mkIso'_hom_hom_hom_hom, CategoryTheory.Functor.mapCommGrp_obj_grp_mul, CategoryTheory.Preadditive.toCommGrp_obj_X, CategoryTheory.Preadditive.commGrpEquivalence_functor_map_hom_hom_hom, CategoryTheory.Functor.Faithful.mapCommGrp, forget₂CommMon_comp_forget, CategoryTheory.Preadditive.commGrpEquivalence_inverse_obj, CategoryTheory.Adjunction.mapCommGrp_counit, CategoryTheory.Functor.mapCommGrp_obj_grp_inv, forget_map, instFullGrpForget₂Grp
instInhabited 📖	CompOp	—
mkIso 📖	CompOp	4 math math: mkIso_inv_hom, mkIso_inv_hom_hom_hom, mkIso_hom_hom, mkIso_hom_hom_hom_hom
mkIso' 📖	CompOp	2 math math: mkIso'_inv_hom_hom_hom, mkIso'_hom_hom_hom_hom
toCommMon 📖	CompOp	1 math math: toCommMon_X
toCommMon_ 📖	CompOp	—
toGrp 📖	CompOp	39 math math: CategoryTheory.Functor.mapCommGrpCompIso_inv_app_hom_hom_hom, CategoryTheory.Functor.mapCommGrp_obj_grp_one, CategoryTheory.yonedaCommGrpGrpObj_map, CategoryTheory.Preadditive.toCommGrp_map, mkIso_inv_hom, id', comp', comp_hom, CategoryTheory.Functor.mapCommGrpCompIso_hom_app_hom_hom_hom, instIsIsoMonHomGrp, forget₂CommMon_map_hom, CategoryTheory.Preadditive.commGrpEquivalenceAux_hom_app_hom_hom_hom, CategoryTheory.Functor.mapCommGrpNatIso_inv_app_hom_hom_hom, hom_ext_iff, mkIso_inv_hom_hom_hom, mkIso'_inv_hom_hom_hom, CategoryTheory.Preadditive.commGrpEquivalenceAux_inv_app_hom_hom_hom, forget₂Grp_map_hom, CategoryTheory.Functor.mapCommGrpIdIso_hom_app_hom_hom_hom, mkIso_hom_hom, CategoryTheory.yonedaCommGrpGrpObj_obj_coe, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_inv_app_hom_hom_hom, CategoryTheory.Functor.FullyFaithful.mapCommGrp_preimage, instIsIsoGrpHom, mkIso_hom_hom_hom_hom, id_hom, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_hom_app_hom_hom_hom, CategoryTheory.Functor.mapCommGrpIdIso_inv_app_hom_hom_hom, CategoryTheory.yonedaCommGrpGrp_map_app, toGrp_X, CategoryTheory.Functor.mapCommGrpNatIso_hom_app_hom_hom_hom, CategoryTheory.Functor.mapCommGrp_map_hom_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_inverse_map, CategoryTheory.Functor.mapCommGrpNatTrans_app_hom_hom_hom, mkIso'_hom_hom_hom_hom, CategoryTheory.Functor.mapCommGrp_obj_grp_mul, CategoryTheory.Preadditive.commGrpEquivalence_functor_map_hom_hom_hom, CategoryTheory.Functor.mapCommGrp_obj_grp_inv, forget_map
toGrp_ 📖	CompOp	—
toMon 📖	CompOp	—
toMon_ 📖	CompOp	—
trivial 📖	CompOp	4 math math: trivial_X, trivial_grp_one, trivial_grp_mul, trivial_grp_inv
uniqueHomFromTrivial 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	—	CategoryTheory.IsCommMonObj CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory X CategoryTheory.GrpObj.toMonObj grp	—	—
comp' 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommGrp CategoryTheory.Grp CategoryTheory.Grp.instCategory toGrp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct instCategory	—	comp_hom
comp_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommGrp CategoryTheory.Grp CategoryTheory.Grp.instCategory toGrp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct instCategory	—	—
forget_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.CommGrp instCategory forget CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Grp.toMon CategoryTheory.Functor.obj CategoryTheory.Grp CategoryTheory.Grp.instCategory forget₂Grp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory toGrp	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.CommGrp instCategory forget X	—	—
forget₂CommMon_comp_forget 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.CommGrp instCategory CategoryTheory.CommMon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CommMon.instCategory forget₂CommMon CategoryTheory.CommMon.forget forget	—	—
forget₂CommMon_map_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommMon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CommMon.toMon CategoryTheory.Functor.obj CategoryTheory.CommGrp instCategory CategoryTheory.CommMon.instCategory forget₂CommMon CategoryTheory.Functor.map CategoryTheory.Grp CategoryTheory.Grp.toMon toGrp CategoryTheory.Grp.instCategory	—	—
forget₂CommMon_obj_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CommMon.X CategoryTheory.Functor.obj CategoryTheory.CommGrp instCategory CategoryTheory.CommMon CategoryTheory.CommMon.instCategory forget₂CommMon CategoryTheory.CommMon.mon X CategoryTheory.GrpObj.toMonObj grp	—	—
forget₂CommMon_obj_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CommMon.X CategoryTheory.Functor.obj CategoryTheory.CommGrp instCategory CategoryTheory.CommMon CategoryTheory.CommMon.instCategory forget₂CommMon CategoryTheory.CommMon.mon X CategoryTheory.GrpObj.toMonObj grp	—	—
forget₂Grp_comp_forget 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.CommGrp instCategory CategoryTheory.Grp CategoryTheory.Grp.instCategory forget₂Grp CategoryTheory.Grp.forget forget	—	—
forget₂Grp_map_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.instCategory CategoryTheory.Grp.toMon CategoryTheory.Functor.obj CategoryTheory.CommGrp instCategory CategoryTheory.Grp.instCategory forget₂Grp CategoryTheory.Functor.map toGrp	—	—
forget₂Grp_obj_X 📖	mathematical	—	CategoryTheory.Grp.X CategoryTheory.Functor.obj CategoryTheory.CommGrp instCategory CategoryTheory.Grp CategoryTheory.Grp.instCategory forget₂Grp X	—	—
forget₂Grp_obj_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Grp.X CategoryTheory.Functor.obj CategoryTheory.CommGrp instCategory CategoryTheory.Grp CategoryTheory.Grp.instCategory forget₂Grp CategoryTheory.GrpObj.toMonObj CategoryTheory.Grp.grp X grp	—	—
forget₂Grp_obj_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Grp.X CategoryTheory.Functor.obj CategoryTheory.CommGrp instCategory CategoryTheory.Grp CategoryTheory.Grp.instCategory forget₂Grp CategoryTheory.GrpObj.toMonObj CategoryTheory.Grp.grp X grp	—	—
hom_ext 📖	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Grp.toMon toGrp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CommGrp CategoryTheory.Grp.instCategory	—	—	CategoryTheory.InducedCategory.hom_ext CategoryTheory.Grp.hom_ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Grp.toMon toGrp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CommGrp CategoryTheory.Grp.instCategory	—	hom_ext
id' 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommGrp CategoryTheory.Grp CategoryTheory.Grp.instCategory toGrp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct instCategory	—	id_hom
id_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommGrp CategoryTheory.Grp CategoryTheory.Grp.instCategory toGrp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct instCategory	—	—
instFaithfulCommMonForget₂CommMon 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.CommGrp instCategory CategoryTheory.CommMon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CommMon.instCategory forget₂CommMon	—	CategoryTheory.Functor.FullyFaithful.faithful
instFaithfulForget 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.CommGrp instCategory forget	—	hom_ext
instFaithfulGrpForget₂Grp 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.CommGrp instCategory CategoryTheory.Grp CategoryTheory.Grp.instCategory forget₂Grp	—	CategoryTheory.InducedCategory.faithful
instFullCommMonForget₂CommMon 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.CommGrp instCategory CategoryTheory.CommMon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CommMon.instCategory forget₂CommMon	—	CategoryTheory.Functor.FullyFaithful.full
instFullGrpForget₂Grp 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.CommGrp instCategory CategoryTheory.Grp CategoryTheory.Grp.instCategory forget₂Grp	—	CategoryTheory.InducedCategory.full
instHasInitial 📖	mathematical	—	CategoryTheory.Limits.HasInitial CategoryTheory.CommGrp instCategory	—	CategoryTheory.Limits.hasInitial_of_unique Unique.instSubsingleton
instIsIsoGrpHom 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Grp CategoryTheory.Grp.instCategory toGrp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.CommGrp	—	CategoryTheory.Functor.map_isIso
instIsIsoMonHomGrp 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.instCategory CategoryTheory.Grp.toMon toGrp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.CommGrp CategoryTheory.Grp.instCategory	—	CategoryTheory.Functor.map_isIso
mkIso'_hom_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Grp CategoryTheory.Grp.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Grp.forget₂Mon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp.toMon CategoryTheory.CommGrp instCategory forget₂Grp toGrp CategoryTheory.Iso.hom mkIso'	—	—
mkIso'_inv_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Grp CategoryTheory.Grp.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Grp.forget₂Mon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp.toMon CategoryTheory.CommGrp instCategory forget₂Grp toGrp CategoryTheory.Iso.inv mkIso'	—	—
mkIso_hom_hom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory X CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.GrpObj.toMonObj grp CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonObj.mul CategoryTheory.MonoidalCategoryStruct.tensorHom	CategoryTheory.Mon.Hom.hom CategoryTheory.Grp.toMon toGrp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CommGrp CategoryTheory.Grp.instCategory instCategory mkIso	—	mkIso_hom_hom_hom_hom
mkIso_hom_hom_hom_hom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory X CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.GrpObj.toMonObj grp CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonObj.mul CategoryTheory.MonoidalCategoryStruct.tensorHom	CategoryTheory.Mon.Hom.hom CategoryTheory.Grp.toMon toGrp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CommGrp CategoryTheory.Grp.instCategory instCategory mkIso	—	—
mkIso_inv_hom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory X CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.GrpObj.toMonObj grp CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonObj.mul CategoryTheory.MonoidalCategoryStruct.tensorHom	CategoryTheory.Mon.Hom.hom CategoryTheory.Grp.toMon toGrp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CommGrp CategoryTheory.Grp.instCategory CategoryTheory.Iso.inv instCategory mkIso	—	mkIso_inv_hom_hom_hom
mkIso_inv_hom_hom_hom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory X CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.GrpObj.toMonObj grp CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonObj.mul CategoryTheory.MonoidalCategoryStruct.tensorHom	CategoryTheory.Mon.Hom.hom CategoryTheory.Grp.toMon toGrp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CommGrp CategoryTheory.Grp.instCategory CategoryTheory.Iso.inv instCategory mkIso	—	—
toCommMon_X 📖	mathematical	—	CategoryTheory.CommMon.X CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toCommMon X	—	—
toGrp_X 📖	mathematical	—	CategoryTheory.Grp.X toGrp X	—	—
trivial_X 📖	mathematical	—	X trivial CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory	—	—
trivial_grp_inv 📖	mathematical	—	CategoryTheory.GrpObj.inv CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory grp trivial CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
trivial_grp_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.GrpObj.toMonObj grp trivial CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
trivial_grp_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.GrpObj.toMonObj grp trivial CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
mapCommGrp 📖	CompOp	4 math math: mapCommGrp_functor, mapCommGrp_unitIso, mapCommGrp_inverse, mapCommGrp_counitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapCommGrp_counitIso 📖	mathematical	—	counitIso CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory mapCommGrp CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.mapCommGrp inverse functor CategoryTheory.Functor.Braided.instComp CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.id CategoryTheory.Iso.symm CategoryTheory.Functor.mapCommGrpCompIso CategoryTheory.Functor.Braided.instId CategoryTheory.Functor.mapCommGrpNatIso CategoryTheory.Functor.mapCommGrpIdIso	—	—
mapCommGrp_functor 📖	mathematical	—	functor CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory mapCommGrp CategoryTheory.Functor.mapCommGrp	—	—
mapCommGrp_inverse 📖	mathematical	—	inverse CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory mapCommGrp CategoryTheory.Functor.mapCommGrp	—	—
mapCommGrp_unitIso 📖	mathematical	—	unitIso CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory mapCommGrp CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.mapCommGrp CategoryTheory.Functor.Braided.instId CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.comp functor inverse CategoryTheory.Iso.symm CategoryTheory.Functor.mapCommGrpIdIso CategoryTheory.Functor.Braided.instComp CategoryTheory.Functor.mapCommGrpNatIso CategoryTheory.Functor.mapCommGrpCompIso	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
mapCommGrp 📖	CompOp	26 math math: mapCommGrpCompIso_inv_app_hom_hom_hom, mapCommGrp_obj_grp_one, mapCommGrpFunctor_obj, mapCommGrpCompIso_hom_app_hom_hom_hom, CategoryTheory.Adjunction.mapCommGrp_unit, Full.mapCommGrp, CategoryTheory.Equivalence.mapCommGrp_functor, mapCommGrp_obj_X, CategoryTheory.Equivalence.mapCommGrp_unitIso, mapCommGrpNatIso_inv_app_hom_hom_hom, comp_mapCommGrp_mul, mapCommGrp_id_one, mapCommGrpIdIso_hom_app_hom_hom_hom, CategoryTheory.Equivalence.mapCommGrp_inverse, FullyFaithful.mapCommGrp_preimage, mapCommpGrp_id_mul, comp_mapCommGrp_one, mapCommGrpIdIso_inv_app_hom_hom_hom, CategoryTheory.Equivalence.mapCommGrp_counitIso, mapCommGrpNatIso_hom_app_hom_hom_hom, mapCommGrp_map_hom_hom_hom, mapCommGrpNatTrans_app_hom_hom_hom, mapCommGrp_obj_grp_mul, Faithful.mapCommGrp, CategoryTheory.Adjunction.mapCommGrp_counit, mapCommGrp_obj_grp_inv
mapCommGrpCompIso 📖	CompOp	6 math math: mapCommGrpCompIso_inv_app_hom_hom_hom, mapCommGrpCompIso_hom_app_hom_hom_hom, CategoryTheory.Adjunction.mapCommGrp_unit, CategoryTheory.Equivalence.mapCommGrp_unitIso, CategoryTheory.Equivalence.mapCommGrp_counitIso, CategoryTheory.Adjunction.mapCommGrp_counit
mapCommGrpFunctor 📖	CompOp	2 math math: mapCommGrpFunctor_obj, mapCommGrpFunctor_map
mapCommGrpIdIso 📖	CompOp	6 math math: CategoryTheory.Adjunction.mapCommGrp_unit, CategoryTheory.Equivalence.mapCommGrp_unitIso, mapCommGrpIdIso_hom_app_hom_hom_hom, mapCommGrpIdIso_inv_app_hom_hom_hom, CategoryTheory.Equivalence.mapCommGrp_counitIso, CategoryTheory.Adjunction.mapCommGrp_counit
mapCommGrpNatIso 📖	CompOp	4 math math: CategoryTheory.Equivalence.mapCommGrp_unitIso, mapCommGrpNatIso_inv_app_hom_hom_hom, CategoryTheory.Equivalence.mapCommGrp_counitIso, mapCommGrpNatIso_hom_app_hom_hom_hom
mapCommGrpNatTrans 📖	CompOp	4 math math: CategoryTheory.Adjunction.mapCommGrp_unit, mapCommGrpFunctor_map, mapCommGrpNatTrans_app_hom_hom_hom, CategoryTheory.Adjunction.mapCommGrp_counit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_mapCommGrp_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CommGrp.X obj CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory mapCommGrp comp Braided.instComp CategoryTheory.GrpObj.toMonObj CategoryTheory.CommGrp.grp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct LaxMonoidal.μ LaxMonoidal.comp LaxBraided.toLaxMonoidal Braided.toLaxBraided map	—	—
comp_mapCommGrp_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CommGrp.X obj CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory mapCommGrp comp Braided.instComp CategoryTheory.GrpObj.toMonObj CategoryTheory.CommGrp.grp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct LaxMonoidal.ε LaxMonoidal.comp LaxBraided.toLaxMonoidal Braided.toLaxBraided map	—	—
mapCommGrpCompIso_hom_app_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory obj CategoryTheory.Grp CategoryTheory.Grp.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Grp.forget₂Mon CategoryTheory.CommGrp.X CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory mapCommGrp comp Braided.instComp CategoryTheory.CommGrp.grp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp.toMon CategoryTheory.CommGrp.forget₂Grp CategoryTheory.CommGrp.comm CategoryTheory.CommGrp.toGrp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapCommGrpCompIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.CommGrp.comm
mapCommGrpCompIso_inv_app_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory obj CategoryTheory.Grp CategoryTheory.Grp.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Grp.forget₂Mon CategoryTheory.CommGrp.X CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory comp mapCommGrp CategoryTheory.CommGrp.grp Braided.instComp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp.toMon CategoryTheory.CommGrp.forget₂Grp CategoryTheory.CommGrp.comm CategoryTheory.CommGrp.toGrp CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapCommGrpCompIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.CommGrp.comm
mapCommGrpFunctor_map 📖	mathematical	—	map CategoryTheory.LeftExactFunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor category CategoryTheory.leftExactFunctor CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory mapCommGrpFunctor mapCommGrpNatTrans CategoryTheory.ObjectProperty.FullSubcategory.obj Braided.ofChosenFiniteProducts CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	—
mapCommGrpFunctor_obj 📖	mathematical	—	obj CategoryTheory.LeftExactFunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor category CategoryTheory.leftExactFunctor CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory mapCommGrpFunctor mapCommGrp CategoryTheory.ObjectProperty.FullSubcategory.obj Braided.ofChosenFiniteProducts	—	—
mapCommGrpIdIso_hom_app_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory obj CategoryTheory.Grp CategoryTheory.Grp.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Grp.forget₂Mon CategoryTheory.CommGrp.X CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory mapCommGrp id Braided.instId CategoryTheory.CommGrp.grp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp.toMon CategoryTheory.CommGrp.forget₂Grp CategoryTheory.CommGrp.comm CategoryTheory.CommGrp.toGrp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapCommGrpIdIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.CommGrp.comm
mapCommGrpIdIso_inv_app_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory obj CategoryTheory.Grp CategoryTheory.Grp.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Grp.forget₂Mon CategoryTheory.CommGrp.X CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory id CategoryTheory.CommGrp.grp mapCommGrp Braided.instId CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp.toMon CategoryTheory.CommGrp.forget₂Grp CategoryTheory.CommGrp.comm CategoryTheory.CommGrp.toGrp CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapCommGrpIdIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.CommGrp.comm
mapCommGrpNatIso_hom_app_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory obj CategoryTheory.Grp CategoryTheory.Grp.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Grp.forget₂Mon CategoryTheory.CommGrp.X CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory mapCommGrp CategoryTheory.CommGrp.grp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp.toMon CategoryTheory.CommGrp.forget₂Grp CategoryTheory.CommGrp.comm CategoryTheory.CommGrp.toGrp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapCommGrpNatIso	—	CategoryTheory.CommGrp.comm
mapCommGrpNatIso_inv_app_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory obj CategoryTheory.Grp CategoryTheory.Grp.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Grp.forget₂Mon CategoryTheory.CommGrp.X CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory mapCommGrp CategoryTheory.CommGrp.grp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp.toMon CategoryTheory.CommGrp.forget₂Grp CategoryTheory.CommGrp.comm CategoryTheory.CommGrp.toGrp CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapCommGrpNatIso	—	CategoryTheory.CommGrp.comm
mapCommGrpNatTrans_app_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory obj CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon Monoidal.toLaxMonoidal Braided.toMonoidal CategoryTheory.Grp.toMon CategoryTheory.CommGrp.toGrp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory mapCommGrp CategoryTheory.NatTrans.app mapCommGrpNatTrans CategoryTheory.CommGrp.X	—	—
mapCommGrp_id_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CommGrp.X obj CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory mapCommGrp id Braided.instId CategoryTheory.GrpObj.toMonObj CategoryTheory.CommGrp.grp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	—
mapCommGrp_map_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory obj CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon Monoidal.toLaxMonoidal Braided.toMonoidal CategoryTheory.Grp.toMon CategoryTheory.CommGrp.toGrp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp CategoryTheory.CommGrp map CategoryTheory.CommGrp.instCategory mapCommGrp CategoryTheory.CommGrp.X	—	—
mapCommGrp_obj_X 📖	mathematical	—	CategoryTheory.CommGrp.X obj CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory mapCommGrp	—	—
mapCommGrp_obj_grp_inv 📖	mathematical	—	CategoryTheory.GrpObj.inv CategoryTheory.Grp.X obj CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp Braided.toMonoidal CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CommGrp.toGrp CategoryTheory.CommGrp.grp CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory mapCommGrp map CategoryTheory.CommGrp.X	—	—
mapCommGrp_obj_grp_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Grp.X obj CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp Braided.toMonoidal CategoryTheory.CommGrp.toGrp CategoryTheory.GrpObj.toMonObj CategoryTheory.CommGrp.grp CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory mapCommGrp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CommGrp.X LaxMonoidal.μ Monoidal.toLaxMonoidal map	—	—
mapCommGrp_obj_grp_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Grp.X obj CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp Braided.toMonoidal CategoryTheory.CommGrp.toGrp CategoryTheory.GrpObj.toMonObj CategoryTheory.CommGrp.grp CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory mapCommGrp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CommGrp.X LaxMonoidal.ε Monoidal.toLaxMonoidal map	—	—
mapCommpGrp_id_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CommGrp.X obj CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory mapCommGrp id Braided.instId CategoryTheory.GrpObj.toMonObj CategoryTheory.CommGrp.grp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	—

CategoryTheory.Functor.Faithful

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapCommGrp 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory CategoryTheory.Functor.mapCommGrp	—	CategoryTheory.Functor.map_injective comp CategoryTheory.CommGrp.instFaithfulForget CategoryTheory.Functor.congr_map

CategoryTheory.Functor.Full

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapCommGrp 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory CategoryTheory.Functor.mapCommGrp	—	CategoryTheory.Functor.FullyFaithful.full

CategoryTheory.Functor.FullyFaithful

Definitions

Name	Category	Theorems
mapCommGrp 📖	CompOp	1 math math: mapCommGrp_preimage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapCommGrp_preimage 📖	mathematical	—	preimage CategoryTheory.CommGrp CategoryTheory.CommGrp.instCategory CategoryTheory.Functor.mapCommGrp mapCommGrp CategoryTheory.InducedCategory.homMk CategoryTheory.Grp CategoryTheory.Grp.instCategory CategoryTheory.CommGrp.toGrp CategoryTheory.Grp.homMk' CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.instCategory CategoryTheory.Functor.mapMon CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.Functor.Braided.toMonoidal mapMon CategoryTheory.Grp.toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Functor.obj	—	—

---

← Back to Index