Grp_

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

Statistics

Metric	Count
Definitions mapGrp, mapGrp, grpObj, grp_Class, mapGrp, grpObjObj, mapGrp, instBraided, instMonoidal, mapGrpCompIso, mapGrpFunctor, mapGrpIdIso, mapGrpNatIso, mapGrpNatTrans, X, forget, forget₂Mon, forget₂Mon_, fullyFaithfulForget₂Mon, fullyFaithfulForget₂Mon_, grp, homMk, homMk', homMk'', instBraidedCategory, instCartesianMonoidalCategory, instCategory, instInhabited, instMonoidalCategory, instMonoidalCategoryStruct, instMonoidalMonForget₂Mon, mkIso, mkIso', toMon, toMon_, trivial, uniqueHomFromTrivial, GrpObj, instTensorUnit, inv, mulRight, ofIso, instTensorObj, toMonObj, Grp_Class, termι, «termι[_]»	47
Theorems mapGrp_counit, mapGrp_unit, mapGrp_counitIso, mapGrp_functor, mapGrp_inverse, mapGrp_unitIso, mapGrp, mapGrp, grpObj_inv, grpObj_mul, grpObj_one, mapGrp_preimage, comp_mapGrp_mul, comp_mapGrp_one, essImage_mapGrp, mapGrpCompIso_hom_app_hom_hom, mapGrpCompIso_inv_app_hom_hom, mapGrpFunctor_map_app, mapGrpFunctor_obj, mapGrpIdIso_hom_app_hom_hom, mapGrpIdIso_inv_app_hom_hom, mapGrpNatIso_hom_app_hom_hom, mapGrpNatIso_inv_app_hom_hom, mapGrpNatTrans_app_hom_hom, mapGrp_id_mul, mapGrp_id_one, mapGrp_map_hom_hom, mapGrp_obj_X, mapGrp_obj_grp_inv, mapGrp_obj_grp_mul, mapGrp_obj_grp_one, ι_def, ι_def_assoc, associator_hom_hom, associator_hom_hom_hom, associator_inv_hom, associator_inv_hom_hom, braiding_hom_hom, braiding_hom_hom_hom, braiding_inv_hom, braiding_inv_hom_hom, comp', comp_hom, comp_hom_hom, forget_map, forget_obj, forget₂Mon_comp_forget, forget₂Mon_map_hom, forget₂Mon_obj_X, forget₂Mon_obj_mul, forget₂Mon_obj_one, fst_hom, fst_hom_hom, homMk''_hom_hom, homMk'_hom, homMk_hom_hom, hom_ext, hom_ext_iff, id', id_hom, id_hom_hom, instFaithfulForget, instFaithfulMonForget₂Mon, instFullMonForget₂Mon, instHasInitial, instIsIsoHomHomMon, leftUnitor_hom_hom, leftUnitor_hom_hom_hom, leftUnitor_inv_hom, leftUnitor_inv_hom_hom, lift_hom, mkIso'_hom_hom_hom, mkIso'_inv_hom_hom, mkIso_hom_hom, mkIso_hom_hom_hom, mkIso_inv_hom, mkIso_inv_hom_hom, rightUnitor_hom_hom, rightUnitor_hom_hom_hom, rightUnitor_inv_hom, rightUnitor_inv_hom_hom, snd_hom, snd_hom_hom, tensorHom_hom, tensorObj_X, tensorObj_mul, tensorObj_one, tensorUnit_X, tensorUnit_mul, tensorUnit_one, toMon_X, trivial_X, trivial_grp_inv, trivial_grp_mul, trivial_grp_one, whiskerLeft_hom, whiskerLeft_hom_hom, whiskerRight_hom, whiskerRight_hom_hom, δ_def, ε_def, η_def, μ_def, eq_lift_inv_left, eq_lift_inv_right, ext, ext_iff, instIsIsoInv, inv_comp_inv, inv_comp_inv_assoc, inv_def, inv_hom, inv_hom_assoc, inv_inv, isPullback, left_inv, left_inv_assoc, lift_comp_inv_left, lift_comp_inv_left_assoc, lift_comp_inv_right, lift_comp_inv_right_assoc, lift_inv_comp_left, lift_inv_comp_left_assoc, lift_inv_comp_right, lift_inv_comp_right_assoc, lift_inv_left_eq, lift_inv_right_eq, lift_left_mul_ext, mulRight_hom, mulRight_inv, mulRight_one, mul_inv, mul_inv_assoc, mul_inv_rev, mul_inv_rev_assoc, ofIso_inv, ofIso_mul, ofIso_one, right_inv, right_inv_assoc, tensorHom_inv_inv_mul, tensorHom_inv_inv_mul_assoc, inv_def, toMonObj_injective, toMon_Class_injective	145
Total	192

CategoryTheory

Definitions

Name	Category	Theorems
GrpObj 📖	CompData	2 math math: GrpObj.toMon_Class_injective, GrpObj.toMonObj_injective
Grp_Class 📖	CompOp	—

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
mapGrp 📖	CompOp	2 math math: mapGrp_unit, mapGrp_counit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapGrp_counit 📖	mathematical	—	counit CategoryTheory.Grp CategoryTheory.Grp.instCategory CategoryTheory.Functor.mapGrp mapGrp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.Monoidal.instComp CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor.mapGrpCompIso CategoryTheory.Functor.Monoidal.instId CategoryTheory.Functor.mapGrpNatTrans CategoryTheory.Iso.hom CategoryTheory.Functor.mapGrpIdIso	—	—
mapGrp_unit 📖	mathematical	—	unit CategoryTheory.Grp CategoryTheory.Grp.instCategory CategoryTheory.Functor.mapGrp mapGrp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.Monoidal.instId CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor.mapGrpIdIso CategoryTheory.Functor.Monoidal.instComp CategoryTheory.Functor.mapGrpNatTrans CategoryTheory.Iso.hom CategoryTheory.Functor.mapGrpCompIso	—	—

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
mapGrp 📖	CompOp	4 math math: mapGrp_counitIso, mapGrp_inverse, mapGrp_unitIso, mapGrp_functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapGrp_counitIso 📖	mathematical	—	counitIso CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.mapGrp inverse functor CategoryTheory.Functor.Monoidal.instComp CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.id CategoryTheory.Iso.symm CategoryTheory.Functor.mapGrpCompIso CategoryTheory.Functor.Monoidal.instId CategoryTheory.Functor.mapGrpNatIso CategoryTheory.Functor.mapGrpIdIso	—	—
mapGrp_functor 📖	mathematical	—	functor CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp CategoryTheory.Functor.mapGrp	—	—
mapGrp_inverse 📖	mathematical	—	inverse CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp CategoryTheory.Functor.mapGrp	—	—
mapGrp_unitIso 📖	mathematical	—	unitIso CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.mapGrp CategoryTheory.Functor.Monoidal.instId CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.comp functor inverse CategoryTheory.Iso.symm CategoryTheory.Functor.mapGrpIdIso CategoryTheory.Functor.Monoidal.instComp CategoryTheory.Functor.mapGrpNatIso CategoryTheory.Functor.mapGrpCompIso	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
grpObjObj 📖	CompOp	4 math math: map_inv', obj.ι_def, mapGrp_map_hom_hom, obj.ι_def_assoc
mapGrp 📖	CompOp	33 math math: CategoryTheory.Equivalence.mapGrp_counitIso, mapCommGrp_obj_grp_one, FullyFaithful.mapGrp_preimage, comp_mapGrp_mul, mapGrp_id_mul, mapGrpIdIso_hom_app_hom_hom, mapGrpFunctor_obj, mapGrp_obj_grp_one, mapGrp_id_one, CategoryTheory.Adjunction.mapGrp_unit, essImage_mapGrp, mapGrpNatIso_hom_app_hom_hom, mapGrpFunctor_map_app, CategoryTheory.Equivalence.mapGrp_inverse, mapGrpCompIso_hom_app_hom_hom, CategoryTheory.Equivalence.mapGrp_unitIso, mapGrp_map_hom_hom, Full.mapGrp, mapGrpIdIso_inv_app_hom_hom, mapGrp_obj_grp_mul, mapGrpNatTrans_app_hom_hom, mapGrpNatIso_inv_app_hom_hom, mapGrpCompIso_inv_app_hom_hom, mapCommGrp_map_hom_hom_hom, mapGrp_obj_grp_inv, mapCommGrpNatTrans_app_hom_hom_hom, Faithful.mapGrp, mapCommGrp_obj_grp_mul, CategoryTheory.Equivalence.mapGrp_functor, mapGrp_obj_X, mapCommGrp_obj_grp_inv, CategoryTheory.Adjunction.mapGrp_counit, comp_mapGrp_one
mapGrpCompIso 📖	CompOp	6 math math: CategoryTheory.Equivalence.mapGrp_counitIso, CategoryTheory.Adjunction.mapGrp_unit, mapGrpCompIso_hom_app_hom_hom, CategoryTheory.Equivalence.mapGrp_unitIso, mapGrpCompIso_inv_app_hom_hom, CategoryTheory.Adjunction.mapGrp_counit
mapGrpFunctor 📖	CompOp	2 math math: mapGrpFunctor_obj, mapGrpFunctor_map_app
mapGrpIdIso 📖	CompOp	6 math math: CategoryTheory.Equivalence.mapGrp_counitIso, mapGrpIdIso_hom_app_hom_hom, CategoryTheory.Adjunction.mapGrp_unit, CategoryTheory.Equivalence.mapGrp_unitIso, mapGrpIdIso_inv_app_hom_hom, CategoryTheory.Adjunction.mapGrp_counit
mapGrpNatIso 📖	CompOp	4 math math: CategoryTheory.Equivalence.mapGrp_counitIso, mapGrpNatIso_hom_app_hom_hom, CategoryTheory.Equivalence.mapGrp_unitIso, mapGrpNatIso_inv_app_hom_hom
mapGrpNatTrans 📖	CompOp	3 math math: CategoryTheory.Adjunction.mapGrp_unit, mapGrpNatTrans_app_hom_hom, CategoryTheory.Adjunction.mapGrp_counit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_mapGrp_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Grp.X obj CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp comp Monoidal.instComp CategoryTheory.GrpObj.toMonObj CategoryTheory.Grp.grp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct LaxMonoidal.μ LaxMonoidal.comp Monoidal.toLaxMonoidal map	—	—
comp_mapGrp_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Grp.X obj CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp comp Monoidal.instComp CategoryTheory.GrpObj.toMonObj CategoryTheory.Grp.grp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct LaxMonoidal.ε LaxMonoidal.comp Monoidal.toLaxMonoidal map	—	—
essImage_mapGrp 📖	mathematical	—	essImage CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp CategoryTheory.Grp.X	—	FullyFaithful.map_preimage Monoidal.ε_η_assoc CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id Monoidal.μ_δ_assoc
mapGrpCompIso_hom_app_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.Grp.X mapGrp comp Monoidal.instComp CategoryTheory.Grp.grp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp.toMon CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapGrpCompIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
mapGrpCompIso_inv_app_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.Grp.X comp mapGrp CategoryTheory.Grp.grp Monoidal.instComp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp.toMon CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapGrpCompIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
mapGrpFunctor_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor category CategoryTheory.leftExactFunctor Monoidal.ofChosenFiniteProducts map CategoryTheory.LeftExactFunctor CategoryTheory.ObjectProperty.FullSubcategory.category mapGrpFunctor CategoryTheory.Grp.homMk'' obj CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Grp.X	—	—
mapGrpFunctor_obj 📖	mathematical	—	obj CategoryTheory.LeftExactFunctor CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor category CategoryTheory.leftExactFunctor CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrpFunctor mapGrp CategoryTheory.ObjectProperty.FullSubcategory.obj Monoidal.ofChosenFiniteProducts	—	—
mapGrpIdIso_hom_app_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.Grp.X mapGrp id Monoidal.instId CategoryTheory.Grp.grp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp.toMon CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapGrpIdIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
mapGrpIdIso_inv_app_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.Grp.X id CategoryTheory.Grp.grp mapGrp Monoidal.instId CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp.toMon CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapGrpIdIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
mapGrpNatIso_hom_app_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.Grp.X mapGrp CategoryTheory.Grp.grp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp.toMon CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapGrpNatIso	—	—
mapGrpNatIso_inv_app_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.Grp.X mapGrp CategoryTheory.Grp.grp CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp.toMon CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapGrpNatIso	—	—
mapGrpNatTrans_app_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory obj CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon Monoidal.toLaxMonoidal CategoryTheory.Grp.toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp CategoryTheory.NatTrans.app mapGrpNatTrans CategoryTheory.Grp.X	—	—
mapGrp_id_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Grp.X obj CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp id Monoidal.instId CategoryTheory.GrpObj.toMonObj CategoryTheory.Grp.grp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	—
mapGrp_id_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Grp.X obj CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp id Monoidal.instId CategoryTheory.GrpObj.toMonObj CategoryTheory.Grp.grp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	—
mapGrp_map_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory obj CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon Monoidal.toLaxMonoidal CategoryTheory.Grp.toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Grp.X grpObjObj CategoryTheory.Grp.grp map CategoryTheory.Grp.instCategory mapGrp	—	—
mapGrp_obj_X 📖	mathematical	—	CategoryTheory.Grp.X obj CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp	—	—
mapGrp_obj_grp_inv 📖	mathematical	—	CategoryTheory.GrpObj.inv obj CategoryTheory.Grp.X CategoryTheory.Grp.grp CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp map	—	—
mapGrp_obj_grp_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory obj CategoryTheory.Grp.X CategoryTheory.GrpObj.toMonObj CategoryTheory.Grp.grp CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct LaxMonoidal.μ Monoidal.toLaxMonoidal map	—	—
mapGrp_obj_grp_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory obj CategoryTheory.Grp.X CategoryTheory.GrpObj.toMonObj CategoryTheory.Grp.grp CategoryTheory.Grp CategoryTheory.Grp.instCategory mapGrp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct LaxMonoidal.ε Monoidal.toLaxMonoidal map	—	—

CategoryTheory.Functor.Faithful

Theorems

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

CategoryTheory.Functor.Full

Theorems

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

CategoryTheory.Functor.FullyFaithful

Definitions

Name	Category	Theorems
grpObj 📖	CompOp	3 math math: grpObj_inv, grpObj_mul, grpObj_one
grp_Class 📖	CompOp	—
mapGrp 📖	CompOp	1 math math: mapGrp_preimage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
grpObj_inv 📖	mathematical	—	CategoryTheory.GrpObj.inv grpObj preimage CategoryTheory.Functor.obj	—	—
grpObj_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.GrpObj.toMonObj grpObj preimage CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal	—	—
grpObj_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.GrpObj.toMonObj grpObj preimage CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal	—	—
mapGrp_preimage 📖	mathematical	—	preimage CategoryTheory.Grp CategoryTheory.Grp.instCategory CategoryTheory.Functor.mapGrp mapGrp CategoryTheory.Grp.homMk' CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.instCategory CategoryTheory.Functor.mapMon CategoryTheory.Functor.Monoidal.toLaxMonoidal mapMon CategoryTheory.Grp.toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Functor.obj	—	—

CategoryTheory.Functor.mapGrp

Definitions

Name	Category	Theorems
instBraided 📖	CompOp	—
instMonoidal 📖	CompOp	—

CategoryTheory.Functor.obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ι_def 📖	mathematical	—	CategoryTheory.GrpObj.inv CategoryTheory.Functor.obj CategoryTheory.Functor.grpObjObj CategoryTheory.Functor.map	—	—
ι_def_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.GrpObj.inv CategoryTheory.Functor.grpObjObj CategoryTheory.Functor.map	—	Mathlib.Tactic.Reassoc.eq_whisker' ι_def

CategoryTheory.Grp

Definitions

Name	Category	Theorems
X 📖	CompOp	68 math math: CategoryTheory.Functor.mapCommGrp_obj_grp_one, CategoryTheory.yonedaGrp_obj, CategoryTheory.Functor.comp_mapGrp_mul, whiskerLeft_hom_hom, CategoryTheory.Functor.mapGrp_id_mul, CategoryTheory.Functor.mapGrpIdIso_hom_app_hom_hom, leftUnitor_hom_hom, rightUnitor_hom_hom_hom, hom_mul, CategoryTheory.Functor.mapGrp_obj_grp_one, CategoryTheory.Functor.mapGrp_id_one, associator_inv_hom_hom, leftUnitor_hom_hom_hom, CategoryTheory.CommGrp.forget₂Grp_obj_mul, rightUnitor_inv_hom_hom, CategoryTheory.Functor.essImage_mapGrp, whiskerRight_hom_hom, snd_hom, tensorUnit_mul, CategoryTheory.CommGrp.forget₂Grp_obj_X, tensorUnit_X, whiskerLeft_hom, CategoryTheory.Functor.mapGrpNatIso_hom_app_hom_hom, CategoryTheory.Functor.mapGrpFunctor_map_app, leftUnitor_inv_hom_hom, rightUnitor_inv_hom, forget₂Mon_obj_mul, associator_hom_hom_hom, toMon_X, braiding_inv_hom, id_hom, CategoryTheory.Functor.mapGrpCompIso_hom_app_hom_hom, fst_hom, tensorUnit_one, CategoryTheory.CommGrp.forget₂Grp_obj_one, CategoryTheory.Functor.mapGrp_map_hom_hom, braiding_inv_hom_hom, tensorObj_X, tensorObj_mul, rightUnitor_hom_hom, forget₂Mon_obj_X, tensorObj_one, CategoryTheory.Functor.mapGrpIdIso_inv_app_hom_hom, leftUnitor_inv_hom, CategoryTheory.Functor.mapGrp_obj_grp_mul, snd_hom_hom, CategoryTheory.Functor.mapGrpNatTrans_app_hom_hom, hom_one, forget₂Mon_obj_one, associator_inv_hom, CategoryTheory.CommGrp.toGrp_X, CategoryTheory.Functor.mapGrpNatIso_inv_app_hom_hom, CategoryTheory.Functor.mapGrpCompIso_inv_app_hom_hom, braiding_hom_hom, CategoryTheory.Functor.mapGrp_obj_grp_inv, associator_hom_hom, forget_obj, CategoryTheory.yonedaGrp_map_app, whiskerRight_hom, CategoryTheory.Functor.mapCommGrp_obj_grp_mul, tensorHom_hom, fst_hom_hom, trivial_X, braiding_hom_hom_hom, CategoryTheory.Functor.mapGrp_obj_X, id_hom_hom, CategoryTheory.Functor.mapCommGrp_obj_grp_inv, CategoryTheory.Functor.comp_mapGrp_one
forget 📖	CompOp	5 math math: forget_map, CategoryTheory.CommGrp.forget₂Grp_comp_forget, forget₂Mon_comp_forget, forget_obj, instFaithfulForget
forget₂Mon 📖	CompOp	35 math math: mkIso_inv_hom, mkIso_hom_hom, CategoryTheory.Functor.mapCommGrpCompIso_inv_app_hom_hom_hom, CategoryTheory.Functor.mapGrpIdIso_hom_app_hom_hom, ε_def, CategoryTheory.Functor.mapCommGrpCompIso_hom_app_hom_hom_hom, mkIso_hom_hom_hom, forget₂Mon_map_hom, CategoryTheory.Preadditive.commGrpEquivalenceAux_hom_app_hom_hom_hom, μ_def, CategoryTheory.Functor.mapGrpNatIso_hom_app_hom_hom, CategoryTheory.Functor.mapCommGrpNatIso_inv_app_hom_hom_hom, forget₂Mon_obj_mul, δ_def, mkIso'_hom_hom_hom, CategoryTheory.Functor.mapGrpCompIso_hom_app_hom_hom, CategoryTheory.CommGrp.mkIso'_inv_hom_hom_hom, CategoryTheory.Preadditive.commGrpEquivalenceAux_inv_app_hom_hom_hom, CategoryTheory.Functor.mapCommGrpIdIso_hom_app_hom_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_inv_app_hom_hom_hom, forget₂Mon_obj_X, forget₂Mon_comp_forget, CategoryTheory.Functor.mapGrpIdIso_inv_app_hom_hom, mkIso_inv_hom_hom, forget₂Mon_obj_one, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_hom_app_hom_hom_hom, CategoryTheory.Functor.mapCommGrpIdIso_inv_app_hom_hom_hom, CategoryTheory.Functor.mapGrpNatIso_inv_app_hom_hom, CategoryTheory.Functor.mapGrpCompIso_inv_app_hom_hom, CategoryTheory.Functor.mapCommGrpNatIso_hom_app_hom_hom_hom, instFaithfulMonForget₂Mon, η_def, CategoryTheory.CommGrp.mkIso'_hom_hom_hom_hom, mkIso'_inv_hom_hom, instFullMonForget₂Mon
forget₂Mon_ 📖	CompOp	—
fullyFaithfulForget₂Mon 📖	CompOp	—
fullyFaithfulForget₂Mon_ 📖	CompOp	—
grp 📖	CompOp	36 math math: Hom.hom_div, Hom.hom_hom_zpow, CategoryTheory.yonedaGrp_obj, trivial_grp_inv, CategoryTheory.Functor.comp_mapGrp_mul, CategoryTheory.Functor.mapGrp_id_mul, CategoryTheory.Functor.mapGrpIdIso_hom_app_hom_hom, hom_mul, Hom.hom_zpow, CategoryTheory.Functor.mapGrp_obj_grp_one, CategoryTheory.Functor.mapGrp_id_one, Hom.hom_hom_div, CategoryTheory.CommGrp.forget₂Grp_obj_mul, Hom.hom_hom_inv, tensorUnit_mul, CategoryTheory.Functor.mapGrpNatIso_hom_app_hom_hom, forget₂Mon_obj_mul, CategoryTheory.Functor.mapGrpCompIso_hom_app_hom_hom, tensorUnit_one, CategoryTheory.CommGrp.forget₂Grp_obj_one, CategoryTheory.Functor.mapGrp_map_hom_hom, tensorObj_mul, tensorObj_one, CategoryTheory.Functor.mapGrpIdIso_inv_app_hom_hom, CategoryTheory.Functor.mapGrp_obj_grp_mul, trivial_grp_one, hom_one, forget₂Mon_obj_one, CategoryTheory.Functor.mapGrpNatIso_inv_app_hom_hom, CategoryTheory.Functor.mapGrpCompIso_inv_app_hom_hom, Hom.hom_inv, CategoryTheory.Functor.mapGrp_obj_grp_inv, CategoryTheory.yonedaGrp_map_app, tensorHom_hom, trivial_grp_mul, CategoryTheory.Functor.comp_mapGrp_one
homMk 📖	CompOp	1 math math: homMk_hom_hom
homMk' 📖	CompOp	3 math math: homMk'_hom, CategoryTheory.Functor.FullyFaithful.mapGrp_preimage, CategoryTheory.Functor.FullyFaithful.mapCommGrp_preimage
homMk'' 📖	CompOp	3 math math: CategoryTheory.Preadditive.toCommGrp_map, CategoryTheory.Functor.mapGrpFunctor_map_app, homMk''_hom_hom
instBraidedCategory 📖	CompOp	7 math math: CategoryTheory.yonedaCommGrpGrpObj_map, braiding_inv_hom, braiding_inv_hom_hom, instIsCommMonObj, CategoryTheory.yonedaCommGrpGrp_map_app, braiding_hom_hom, braiding_hom_hom_hom
instCartesianMonoidalCategory 📖	CompOp	16 math math: Hom.hom_div, Hom.hom_hom_zpow, CategoryTheory.yonedaCommGrpGrpObj_map, lift_hom, Hom.hom_zpow, Hom.hom_hom_div, Hom.hom_hom_inv, snd_hom, Hom.hom_pow, fst_hom, Hom.hom_mul, snd_hom_hom, CategoryTheory.yonedaCommGrpGrp_map_app, Hom.hom_inv, Hom.hom_one, fst_hom_hom
instCategory 📖	CompOp	150 math math: mkIso_inv_hom, Hom.hom_div, comp', mkIso_hom_hom, CategoryTheory.Equivalence.mapGrp_counitIso, Hom.hom_hom_zpow, CategoryTheory.Functor.mapCommGrpCompIso_inv_app_hom_hom_hom, CategoryTheory.Functor.mapCommGrp_obj_grp_one, id', CategoryTheory.Functor.FullyFaithful.mapGrp_preimage, CategoryTheory.yonedaGrp_obj, CategoryTheory.yonedaCommGrpGrpObj_map, CategoryTheory.Preadditive.toCommGrp_map, CategoryTheory.CommGrp.mkIso_inv_hom, CategoryTheory.Functor.comp_mapGrp_mul, whiskerLeft_hom_hom, CategoryTheory.Functor.mapGrp_id_mul, CategoryTheory.Functor.mapGrpIdIso_hom_app_hom_hom, CategoryTheory.instFaithfulGrpFunctorOppositeGrpCatYonedaGrp, leftUnitor_hom_hom, CategoryTheory.CommGrp.id', CategoryTheory.CommGrp.comp', ε_def, rightUnitor_hom_hom_hom, lift_hom, CategoryTheory.CommGrp.comp_hom, hom_mul, instHasInitial, CategoryTheory.CommGrp.instFaithfulGrpForget₂Grp, CategoryTheory.Functor.mapGrpFunctor_obj, Hom.hom_zpow, CategoryTheory.Functor.mapGrp_obj_grp_one, CategoryTheory.Functor.mapCommGrpCompIso_hom_app_hom_hom_hom, CategoryTheory.Functor.mapGrp_id_one, associator_inv_hom_hom, Hom.hom_hom_div, leftUnitor_hom_hom_hom, CategoryTheory.CommGrp.instIsIsoMonHomGrp, forget_map, mkIso_hom_hom_hom, CategoryTheory.CommGrp.forget₂CommMon_map_hom, CategoryTheory.CommGrp.forget₂Grp_obj_mul, CategoryTheory.Adjunction.mapGrp_unit, instIsMonHom, rightUnitor_inv_hom_hom, CategoryTheory.Functor.essImage_mapGrp, forget₂Mon_map_hom, whiskerRight_hom_hom, Hom.hom_hom_inv, CategoryTheory.Preadditive.commGrpEquivalenceAux_hom_app_hom_hom_hom, CategoryTheory.essImage_yonedaGrp, μ_def, snd_hom, tensorUnit_mul, CategoryTheory.CommGrp.forget₂Grp_obj_X, tensorUnit_X, whiskerLeft_hom, CategoryTheory.Functor.mapGrpNatIso_hom_app_hom_hom, CategoryTheory.Functor.mapGrpFunctor_map_app, CategoryTheory.Equivalence.mapGrp_inverse, leftUnitor_inv_hom_hom, CategoryTheory.Functor.mapCommGrpNatIso_inv_app_hom_hom_hom, rightUnitor_inv_hom, CategoryTheory.CommGrp.hom_ext_iff, forget₂Mon_obj_mul, Hom.hom_pow, δ_def, associator_hom_hom_hom, braiding_inv_hom, mkIso'_hom_hom_hom, id_hom, CategoryTheory.Functor.mapGrpCompIso_hom_app_hom_hom, fst_hom, CategoryTheory.CommGrp.mkIso_inv_hom_hom_hom, CategoryTheory.CommGrp.mkIso'_inv_hom_hom_hom, CategoryTheory.Equivalence.mapGrp_unitIso, tensorUnit_one, CategoryTheory.yonedaCommGrpGrp_obj, CategoryTheory.CommGrp.forget₂Grp_obj_one, CategoryTheory.CommGrp.forget₂Grp_comp_forget, CategoryTheory.Preadditive.commGrpEquivalenceAux_inv_app_hom_hom_hom, CategoryTheory.Functor.mapGrp_map_hom_hom, CategoryTheory.CommGrp.forget₂Grp_map_hom, comp_hom_hom, braiding_inv_hom_hom, CategoryTheory.Functor.mapCommGrpIdIso_hom_app_hom_hom_hom, CategoryTheory.CommGrp.mkIso_hom_hom, CategoryTheory.instFullGrpFunctorOppositeGrpCatYonedaGrp, tensorObj_X, Hom.hom_mul, CategoryTheory.yonedaCommGrpGrpObj_obj_coe, tensorObj_mul, rightUnitor_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_inv_app_hom_hom_hom, forget₂Mon_obj_X, instIsCommMonObj, forget₂Mon_comp_forget, CategoryTheory.Functor.Full.mapGrp, CategoryTheory.Functor.FullyFaithful.mapCommGrp_preimage, CategoryTheory.CommGrp.instIsIsoGrpHom, tensorObj_one, CategoryTheory.Functor.mapGrpIdIso_inv_app_hom_hom, CategoryTheory.CommGrp.mkIso_hom_hom_hom_hom, leftUnitor_inv_hom, CategoryTheory.CommGrp.id_hom, CategoryTheory.Functor.mapGrp_obj_grp_mul, mkIso_inv_hom_hom, snd_hom_hom, CategoryTheory.Functor.mapGrpNatTrans_app_hom_hom, hom_one, forget₂Mon_obj_one, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_hom_app_hom_hom_hom, CategoryTheory.Functor.mapCommGrpIdIso_inv_app_hom_hom_hom, CategoryTheory.yonedaCommGrpGrp_map_app, associator_inv_hom, CategoryTheory.Functor.mapGrpNatIso_inv_app_hom_hom, CategoryTheory.Functor.mapGrpCompIso_inv_app_hom_hom, Hom.hom_inv, CategoryTheory.Functor.mapCommGrpNatIso_hom_app_hom_hom_hom, instFaithfulMonForget₂Mon, braiding_hom_hom, CategoryTheory.Functor.mapCommGrp_map_hom_hom_hom, CategoryTheory.Functor.mapGrp_obj_grp_inv, η_def, associator_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_inverse_map, CategoryTheory.Functor.mapCommGrpNatTrans_app_hom_hom_hom, CategoryTheory.Functor.Faithful.mapGrp, forget_obj, CategoryTheory.yonedaGrp_map_app, CategoryTheory.CommGrp.mkIso'_hom_hom_hom_hom, whiskerRight_hom, CategoryTheory.Functor.mapCommGrp_obj_grp_mul, tensorHom_hom, Hom.hom_one, CategoryTheory.Equivalence.mapGrp_functor, fst_hom_hom, mkIso'_inv_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_functor_map_hom_hom_hom, braiding_hom_hom_hom, instFaithfulForget, comp_hom, instFullMonForget₂Mon, CategoryTheory.Functor.mapGrp_obj_X, id_hom_hom, CategoryTheory.Functor.mapCommGrp_obj_grp_inv, CategoryTheory.Adjunction.mapGrp_counit, CategoryTheory.Functor.comp_mapGrp_one, CategoryTheory.CommGrp.forget_map, CategoryTheory.CommGrp.instFullGrpForget₂Grp
instInhabited 📖	CompOp	—
instMonoidalCategory 📖	CompOp	12 math math: ε_def, hom_mul, instIsMonHom, μ_def, δ_def, braiding_inv_hom, braiding_inv_hom_hom, instIsCommMonObj, hom_one, braiding_hom_hom, η_def, braiding_hom_hom_hom
instMonoidalCategoryStruct 📖	CompOp	23 math math: whiskerLeft_hom_hom, leftUnitor_hom_hom, rightUnitor_hom_hom_hom, associator_inv_hom_hom, leftUnitor_hom_hom_hom, rightUnitor_inv_hom_hom, whiskerRight_hom_hom, tensorUnit_mul, tensorUnit_X, whiskerLeft_hom, leftUnitor_inv_hom_hom, rightUnitor_inv_hom, associator_hom_hom_hom, tensorUnit_one, tensorObj_X, tensorObj_mul, rightUnitor_hom_hom, tensorObj_one, leftUnitor_inv_hom, associator_inv_hom, associator_hom_hom, whiskerRight_hom, tensorHom_hom
instMonoidalMonForget₂Mon 📖	CompOp	4 math math: ε_def, μ_def, δ_def, η_def
mkIso 📖	CompOp	4 math math: mkIso_inv_hom, mkIso_hom_hom, mkIso_hom_hom_hom, mkIso_inv_hom_hom
mkIso' 📖	CompOp	2 math math: mkIso'_hom_hom_hom, mkIso'_inv_hom_hom
toMon 📖	CompOp	93 math math: mkIso_inv_hom, Hom.hom_div, comp', mkIso_hom_hom, instIsIsoHomHomMon, homMk'_hom, Hom.hom_hom_zpow, CategoryTheory.Functor.mapCommGrpCompIso_inv_app_hom_hom_hom, id', CategoryTheory.Functor.FullyFaithful.mapGrp_preimage, CategoryTheory.CommGrp.mkIso_inv_hom, whiskerLeft_hom_hom, CategoryTheory.Functor.mapGrpIdIso_hom_app_hom_hom, leftUnitor_hom_hom, rightUnitor_hom_hom_hom, lift_hom, hom_mul, Hom.hom_zpow, CategoryTheory.Functor.mapCommGrpCompIso_hom_app_hom_hom_hom, associator_inv_hom_hom, Hom.hom_hom_div, leftUnitor_hom_hom_hom, CategoryTheory.CommGrp.instIsIsoMonHomGrp, forget_map, mkIso_hom_hom_hom, CategoryTheory.CommGrp.forget₂CommMon_map_hom, rightUnitor_inv_hom_hom, forget₂Mon_map_hom, whiskerRight_hom_hom, Hom.hom_hom_inv, CategoryTheory.Preadditive.commGrpEquivalenceAux_hom_app_hom_hom_hom, snd_hom, whiskerLeft_hom, CategoryTheory.Functor.mapGrpNatIso_hom_app_hom_hom, leftUnitor_inv_hom_hom, CategoryTheory.Functor.mapCommGrpNatIso_inv_app_hom_hom_hom, rightUnitor_inv_hom, CategoryTheory.CommGrp.hom_ext_iff, Hom.hom_pow, associator_hom_hom_hom, toMon_X, braiding_inv_hom, mkIso'_hom_hom_hom, id_hom, CategoryTheory.Functor.mapGrpCompIso_hom_app_hom_hom, fst_hom, CategoryTheory.CommGrp.mkIso_inv_hom_hom_hom, CategoryTheory.CommGrp.mkIso'_inv_hom_hom_hom, CategoryTheory.Preadditive.commGrpEquivalenceAux_inv_app_hom_hom_hom, CategoryTheory.Functor.mapGrp_map_hom_hom, CategoryTheory.CommGrp.forget₂Grp_map_hom, comp_hom_hom, braiding_inv_hom_hom, CategoryTheory.Functor.mapCommGrpIdIso_hom_app_hom_hom_hom, CategoryTheory.CommGrp.mkIso_hom_hom, Hom.hom_mul, rightUnitor_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_inv_app_hom_hom_hom, hom_ext_iff, homMk''_hom_hom, CategoryTheory.Functor.FullyFaithful.mapCommGrp_preimage, CategoryTheory.Functor.mapGrpIdIso_inv_app_hom_hom, CategoryTheory.CommGrp.mkIso_hom_hom_hom_hom, leftUnitor_inv_hom, mkIso_inv_hom_hom, snd_hom_hom, CategoryTheory.Functor.mapGrpNatTrans_app_hom_hom, hom_one, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_hom_app_hom_hom_hom, CategoryTheory.Functor.mapCommGrpIdIso_inv_app_hom_hom_hom, associator_inv_hom, homMk_hom_hom, CategoryTheory.Functor.mapGrpNatIso_inv_app_hom_hom, CategoryTheory.Functor.mapGrpCompIso_inv_app_hom_hom, Hom.hom_inv, CategoryTheory.Functor.mapCommGrpNatIso_hom_app_hom_hom_hom, braiding_hom_hom, CategoryTheory.Functor.mapCommGrp_map_hom_hom_hom, associator_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_inverse_map, CategoryTheory.Functor.mapCommGrpNatTrans_app_hom_hom_hom, CategoryTheory.yonedaGrp_map_app, CategoryTheory.CommGrp.mkIso'_hom_hom_hom_hom, whiskerRight_hom, tensorHom_hom, Hom.hom_one, fst_hom_hom, mkIso'_inv_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_functor_map_hom_hom_hom, braiding_hom_hom_hom, comp_hom, id_hom_hom, CategoryTheory.CommGrp.forget_map
toMon_ 📖	CompOp	—
trivial 📖	CompOp	4 math math: trivial_grp_inv, trivial_grp_one, trivial_grp_mul, trivial_X
uniqueHomFromTrivial 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	associator_hom_hom_hom
associator_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	—
associator_inv_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	associator_inv_hom_hom
associator_inv_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	—
braiding_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding instBraidedCategory X	—	braiding_hom_hom_hom
braiding_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding instBraidedCategory X	—	—
braiding_inv_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Iso.inv CategoryTheory.BraidedCategory.braiding instBraidedCategory X	—	braiding_inv_hom_hom
braiding_inv_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Iso.inv CategoryTheory.BraidedCategory.braiding instBraidedCategory X	—	—
comp' 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.instCategory toMon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct instCategory	—	—
comp_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Mon.X	—	comp_hom_hom
comp_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Mon.X	—	—
forget_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Grp instCategory forget CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Grp instCategory forget X	—	—
forget₂Mon_comp_forget 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.Grp instCategory CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.instCategory forget₂Mon CategoryTheory.Mon.forget forget	—	—
forget₂Mon_map_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Grp 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.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Grp instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory forget₂Mon X	—	—
forget₂Mon_obj_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.X CategoryTheory.Functor.obj CategoryTheory.Grp instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory forget₂Mon CategoryTheory.Mon.mon X CategoryTheory.GrpObj.toMonObj grp	—	—
forget₂Mon_obj_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.X CategoryTheory.Functor.obj CategoryTheory.Grp instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory forget₂Mon CategoryTheory.Mon.mon X CategoryTheory.GrpObj.toMonObj grp	—	—
fst_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instCartesianMonoidalCategory CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.SemiCartesianMonoidalCategory.fst X	—	fst_hom_hom
fst_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instCartesianMonoidalCategory CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.SemiCartesianMonoidalCategory.fst X	—	—
homMk''_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.MonoidalCategoryStruct.tensorObj CategoryTheory.MonObj.mul CategoryTheory.MonoidalCategoryStruct.tensorHom	CategoryTheory.Mon.Hom.hom toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory homMk''	—	—
homMk'_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.instCategory toMon homMk'	—	—
homMk_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory homMk	—	—
hom_ext 📖	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory	—	—	CategoryTheory.InducedCategory.hom_ext CategoryTheory.Mon.Hom.ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory	—	hom_ext
id' 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.instCategory toMon CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct instCategory	—	—
id_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct instCategory X	—	id_hom_hom
id_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct instCategory X	—	—
instFaithfulForget 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Grp instCategory forget	—	hom_ext
instFaithfulMonForget₂Mon 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Grp instCategory CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.instCategory forget₂Mon	—	CategoryTheory.InducedCategory.faithful
instFullMonForget₂Mon 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Grp instCategory CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.instCategory forget₂Mon	—	CategoryTheory.InducedCategory.full
instHasInitial 📖	mathematical	—	CategoryTheory.Limits.HasInitial CategoryTheory.Grp instCategory	—	CategoryTheory.Limits.hasInitial_of_unique Unique.instSubsingleton
instIsIsoHomHomMon 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Mon.X CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.Mon.Hom.hom CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory	—	CategoryTheory.Functor.map_isIso
leftUnitor_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	leftUnitor_hom_hom_hom
leftUnitor_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	—
leftUnitor_inv_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	leftUnitor_inv_hom_hom
leftUnitor_inv_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	—
lift_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.instCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.Mon.instCartesianMonoidalCategory	—	—
mkIso'_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Grp 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.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Grp instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory forget₂Mon CategoryTheory.InducedCategory.Hom.hom toMon 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.Functor.obj CategoryTheory.Grp instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory forget₂Mon CategoryTheory.InducedCategory.Hom.hom toMon mkIso	—	mkIso_hom_hom_hom
mkIso_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.Functor.obj CategoryTheory.Grp instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory forget₂Mon CategoryTheory.InducedCategory.Hom.hom toMon 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.Functor.obj CategoryTheory.Grp instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory forget₂Mon CategoryTheory.InducedCategory.Hom.hom toMon CategoryTheory.Iso.inv mkIso	—	mkIso_inv_hom_hom
mkIso_inv_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.Functor.obj CategoryTheory.Grp instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory forget₂Mon CategoryTheory.InducedCategory.Hom.hom toMon CategoryTheory.Iso.inv mkIso	—	—
rightUnitor_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	rightUnitor_hom_hom_hom
rightUnitor_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	—
rightUnitor_inv_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	rightUnitor_inv_hom_hom
rightUnitor_inv_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	—
snd_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instCartesianMonoidalCategory CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.SemiCartesianMonoidalCategory.snd X	—	snd_hom_hom
snd_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instCartesianMonoidalCategory CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.SemiCartesianMonoidalCategory.snd X	—	—
tensorHom_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.instCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X CategoryTheory.GrpObj.tensorObj.instTensorObj grp CategoryTheory.MonoidalCategoryStruct.tensorHom instCategory instMonoidalCategoryStruct CategoryTheory.Mon.monMonoidalStruct	—	—
tensorObj_X 📖	mathematical	—	X CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory	—	—
tensorObj_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory X CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.GrpObj.toMonObj grp CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.instMonObjTensorObj	—	—
tensorObj_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory X CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.GrpObj.toMonObj grp CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.instMonObjTensorObj	—	—
tensorUnit_X 📖	mathematical	—	X CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory	—	—
tensorUnit_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory X CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.GrpObj.toMonObj grp CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.instTensorUnit	—	—
tensorUnit_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory X CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.GrpObj.toMonObj grp CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.instTensorUnit	—	—
toMon_X 📖	mathematical	—	CategoryTheory.Mon.X CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon 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	—	—
whiskerLeft_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.X X	—	whiskerLeft_hom_hom
whiskerLeft_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.X X	—	—
whiskerRight_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X CategoryTheory.Mon.X	—	whiskerRight_hom_hom
whiskerRight_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Grp instCategory instMonoidalCategoryStruct CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X CategoryTheory.Mon.X	—	—
δ_def 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Grp instCategory instMonoidalCategory CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal forget₂Mon CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalMonForget₂Mon CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
ε_def 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Grp instCategory instMonoidalCategory CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal forget₂Mon CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalMonForget₂Mon CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
η_def 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Grp instCategory instMonoidalCategory CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal forget₂Mon CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalMonForget₂Mon CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
μ_def 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Grp instCategory instMonoidalCategory CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal forget₂Mon CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalMonForget₂Mon CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—

CategoryTheory.GrpObj

Definitions

Name	Category	Theorems
instTensorUnit 📖	CompOp	1 math math: inv_def
inv 📖	CompOp	48 math math: lift_inv_comp_left, inv_hom, lift_inv_right_eq, lift_inv_comp_left_assoc, CategoryTheory.Grp.trivial_grp_inv, left_inv_assoc, lift_inv_comp_right, CategoryTheory.Functor.FullyFaithful.grpObj_inv, one_inv_assoc, lift_comp_inv_right_assoc, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_inv, tensorHom_inv_inv_mul_assoc, one_inv, tensorObj.inv_def, CategoryTheory.instIsMonHomInvOfIsCommMonObj, lift_inv_left_eq, CategoryTheory.Hom.inv_def, CategoryTheory.Functor.obj.ι_def, inv_eq_inv, eq_lift_inv_right, left_inv, CommGrpTypeEquivalenceCommGrp.inverse_obj_inv, mul_inv_rev_assoc, tensorHom_inv_inv_mul, mul_inv, inv_def, mul_inv_rev, CategoryTheory.Preadditive.inv_def, lift_comp_inv_left_assoc, inv_hom_assoc, ofIso_inv, CategoryTheory.Grp_Class.inv_eq_inv, mulRight_inv, mul_inv_assoc, inv_comp_inv_assoc, right_inv, CategoryTheory.Functor.obj.ι_def_assoc, lift_comp_inv_left, eq_lift_inv_left, CategoryTheory.Functor.mapGrp_obj_grp_inv, CategoryTheory.CommGrp.trivial_grp_inv, lift_comp_inv_right, inv_comp_inv, right_inv_assoc, instIsIsoInv, lift_inv_comp_right_assoc, inv_inv, CategoryTheory.Functor.mapCommGrp_obj_grp_inv
mulRight 📖	CompOp	3 math math: mulRight_one, mulRight_hom, mulRight_inv
ofIso 📖	CompOp	3 math math: ofIso_inv, ofIso_mul, ofIso_one
toMonObj 📖	CompOp	87 math math: lift_inv_comp_left, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_one, AlgebraicGeometry.isCommMonObj_of_isProper_of_geometricallyIntegral, CategoryTheory.CommGrp.comm, CategoryTheory.Functor.mapCommGrp_obj_grp_one, lift_inv_right_eq, lift_inv_comp_left_assoc, CommGrpTypeEquivalenceCommGrp.inverse_obj_one, CategoryTheory.Functor.comp_mapGrp_mul, left_inv_assoc, CategoryTheory.Functor.mapGrp_id_mul, CategoryTheory.Over.grpObjMkPullbackSnd_one, CategoryTheory.Over.grpObjMkPullbackSnd_mul, lift_inv_comp_right, CategoryTheory.Grp.hom_mul, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_mul, CategoryTheory.Preadditive.instIsCommMonObj, one_inv_assoc, CategoryTheory.Functor.mapGrp_obj_grp_one, CategoryTheory.Functor.mapGrp_id_one, η_whiskerRight_commutator_assoc, lift_comp_inv_right_assoc, AlgebraicGeometry.instIsClosedImmersionLeftSchemeDiscretePUnitOneOverSpecOf, CategoryTheory.isCommMonObj_iff_commutator_eq_toUnit_η, CategoryTheory.CommGrp.forget₂Grp_obj_mul, tensorHom_inv_inv_mul_assoc, CategoryTheory.Grp.tensorUnit_mul, CategoryTheory.CommGrp.trivial_grp_one, one_inv, mulRight_one, CategoryTheory.Grp.forget₂Mon_obj_mul, whiskerLeft_η_commutator, lift_commutator_eq_mul_mul_inv_inv, CategoryTheory.instIsMonHomInvOfIsCommMonObj, ext_iff, lift_inv_left_eq, CategoryTheory.Functor.comp_mapCommGrp_mul, CategoryTheory.Grp.tensorUnit_one, CategoryTheory.instIsMonHomInvHomOfIsCommMonObj, CategoryTheory.CommGrp.forget₂Grp_obj_one, whiskerLeft_η_commutator_assoc, isPullback, CategoryTheory.yonedaGrpObj_map, CategoryTheory.Functor.mapCommGrp_id_one, toMon_Class_injective, CategoryTheory.CommGrp.forget₂CommMon_obj_mul, eq_lift_inv_right, left_inv, mul_inv_rev_assoc, CategoryTheory.CommGrpObj.toIsCommMonObj, CategoryTheory.Grp.tensorObj_mul, tensorHom_inv_inv_mul, lift_commutator_eq_mul_mul_inv_inv_assoc, mul_inv, CategoryTheory.Grp.tensorObj_one, CategoryTheory.Functor.mapGrp_obj_grp_mul, CategoryTheory.Functor.mapCommpGrp_id_mul, CategoryTheory.CommGrp.forget₂CommMon_obj_one, mul_inv_rev, mulRight_hom, CategoryTheory.Preadditive.mul_def, CategoryTheory.Grp.trivial_grp_one, lift_comp_inv_left_assoc, CategoryTheory.Functor.comp_mapCommGrp_one, CategoryTheory.Grp.hom_one, CategoryTheory.Grp.forget₂Mon_obj_one, CategoryTheory.Functor.FullyFaithful.grpObj_mul, mulRight_inv, mul_inv_assoc, η_whiskerRight_commutator, right_inv, lift_comp_inv_left, eq_lift_inv_left, CommGrpTypeEquivalenceCommGrp.inverse_obj_mul, CategoryTheory.Functor.FullyFaithful.grpObj_one, CategoryTheory.CommGrp.trivial_grp_mul, CategoryTheory.Preadditive.one_def, ofIso_mul, lift_comp_inv_right, CategoryTheory.Functor.mapCommGrp_obj_grp_mul, toMonObj_injective, ofIso_one, CategoryTheory.Grp.trivial_grp_mul, right_inv_assoc, AlgebraicGeometry.isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed, lift_inv_comp_right_assoc, CategoryTheory.Functor.comp_mapGrp_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_lift_inv_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift inv CategoryTheory.MonObj.mul toMonObj	—	lift_comp_inv_right CategoryTheory.MonObj.lift_comp_one_left lift_comp_inv_left
eq_lift_inv_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift inv CategoryTheory.MonObj.mul toMonObj	—	CategoryTheory.MonObj.lift_lift_assoc lift_comp_inv_left CategoryTheory.MonObj.lift_comp_one_right lift_comp_inv_right
ext 📖	—	toMonObj	—	—	toMonObj_injective
ext_iff 📖	mathematical	—	toMonObj	—	ext
instIsIsoInv 📖	mathematical	—	CategoryTheory.IsIso inv	—	inv_comp_inv
inv_comp_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct inv CategoryTheory.CategoryStruct.id	—	lift_left_mul_ext right_inv CategoryTheory.SemiCartesianMonoidalCategory.comp_toUnit_assoc left_inv CategoryTheory.CartesianMonoidalCategory.comp_lift_assoc CategoryTheory.Category.comp_id
inv_comp_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct inv	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inv_comp_inv
inv_def 📖	mathematical	—	inv CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instTensorUnit CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inv_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct inv	—	CategoryTheory.IsPullback.hom_ext isPullback CategoryTheory.CartesianMonoidalCategory.hom_ext CategoryTheory.CartesianMonoidalCategory.lift_whiskerRight lift_inv_comp_right CategoryTheory.CartesianMonoidalCategory.lift_fst lift_comp_inv_right CategoryTheory.CartesianMonoidalCategory.lift_snd CategoryTheory.CartesianMonoidalCategory.lift_lift_associator_hom_assoc CategoryTheory.CartesianMonoidalCategory.lift_whiskerLeft lift_inv_comp_left lift_comp_inv_left CategoryTheory.eq_whisker
inv_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inv_hom
inv_inv 📖	mathematical	—	CategoryTheory.inv inv instIsIsoInv	—	instIsIsoInv CategoryTheory.IsIso.inv_isIso CategoryTheory.inv_comp_eq_id CategoryTheory.IsIso.inv_inv inv_comp_inv
isPullback 📖	mathematical	—	CategoryTheory.IsPullback CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul toMonObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.MonObj.mul_assoc CategoryTheory.Category.assoc CategoryTheory.CartesianMonoidalCategory.hom_ext CategoryTheory.CartesianMonoidalCategory.lift_whiskerRight CategoryTheory.CartesianMonoidalCategory.lift_fst CategoryTheory.MonObj.lift_lift_assoc lift_comp_inv_right CategoryTheory.MonObj.lift_comp_one_left CategoryTheory.CartesianMonoidalCategory.lift_snd CategoryTheory.CartesianMonoidalCategory.lift_lift_associator_hom_assoc CategoryTheory.CartesianMonoidalCategory.lift_whiskerLeft eq_lift_inv_right lift_inv_left_eq CategoryTheory.CartesianMonoidalCategory.lift_comp_fst_snd CategoryTheory.Limits.PullbackCone.condition lift_comp_inv_left CategoryTheory.MonObj.lift_comp_one_right CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst CategoryTheory.CartesianMonoidalCategory.associator_hom_fst CategoryTheory.eq_whisker eq_lift_inv_left CategoryTheory.CartesianMonoidalCategory.whiskerRight_fst CategoryTheory.CartesianMonoidalCategory.whiskerRight_snd
left_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift inv CategoryTheory.CategoryStruct.id CategoryTheory.MonObj.mul toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.MonObj.one	—	—
left_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift inv CategoryTheory.CategoryStruct.id CategoryTheory.MonObj.mul toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.MonObj.one	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' left_inv
lift_comp_inv_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift inv CategoryTheory.MonObj.mul toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.MonObj.one	—	CategoryTheory.whisker_eq left_inv CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique CategoryTheory.Category.comp_id CategoryTheory.CartesianMonoidalCategory.comp_lift_assoc
lift_comp_inv_left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift inv CategoryTheory.MonObj.mul toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.MonObj.one	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_comp_inv_left
lift_comp_inv_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift inv CategoryTheory.MonObj.mul toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.MonObj.one	—	CategoryTheory.whisker_eq right_inv CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique CategoryTheory.Category.comp_id CategoryTheory.CartesianMonoidalCategory.comp_lift_assoc
lift_comp_inv_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift inv CategoryTheory.MonObj.mul toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.MonObj.one	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_comp_inv_right
lift_inv_comp_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift inv CategoryTheory.MonObj.mul toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.MonObj.one	—	CategoryTheory.eq_whisker left_inv CategoryTheory.Category.id_comp CategoryTheory.CartesianMonoidalCategory.lift_map_assoc CategoryTheory.IsMonHom.one_hom CategoryTheory.Category.assoc CategoryTheory.IsMonHom.mul_hom
lift_inv_comp_left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift inv CategoryTheory.MonObj.mul toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.MonObj.one	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_inv_comp_left
lift_inv_comp_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift inv CategoryTheory.MonObj.mul toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.MonObj.one	—	CategoryTheory.eq_whisker right_inv CategoryTheory.Category.id_comp CategoryTheory.CartesianMonoidalCategory.lift_map_assoc CategoryTheory.IsMonHom.one_hom CategoryTheory.Category.assoc CategoryTheory.IsMonHom.mul_hom
lift_inv_comp_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift inv CategoryTheory.MonObj.mul toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.MonObj.one	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_inv_comp_right
lift_inv_left_eq 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift inv CategoryTheory.MonObj.mul toMonObj	—	eq_lift_inv_left
lift_inv_right_eq 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift inv CategoryTheory.MonObj.mul toMonObj	—	eq_lift_inv_right
lift_left_mul_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.MonObj.mul toMonObj	—	—	CategoryTheory.MonObj.lift_comp_one_right lift_comp_inv_right CategoryTheory.MonObj.lift_lift_assoc eq_lift_inv_right
mulRight_hom 📖	mathematical	—	CategoryTheory.Iso.hom mulRight CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.MonObj.mul toMonObj	—	—
mulRight_inv 📖	mathematical	—	CategoryTheory.Iso.inv mulRight CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.SemiCartesianMonoidalCategory.toUnit inv CategoryTheory.MonObj.mul toMonObj	—	—
mulRight_one 📖	mathematical	—	mulRight CategoryTheory.MonObj.one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMonObj CategoryTheory.Iso.refl	—	CategoryTheory.Iso.ext CategoryTheory.MonObj.lift_comp_one_right
mul_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonObj.mul toMonObj inv CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding CategoryTheory.MonoidalCategoryStruct.tensorHom	—	lift_left_mul_ext CategoryTheory.Category.comp_id CategoryTheory.CartesianMonoidalCategory.comp_lift CategoryTheory.Category.assoc left_inv CategoryTheory.CartesianMonoidalCategory.lift_snd_fst CategoryTheory.CartesianMonoidalCategory.lift_map CategoryTheory.MonObj.lift_lift_assoc CategoryTheory.Category.id_comp CategoryTheory.CartesianMonoidalCategory.lift_fst_snd lift_comp_inv_left CategoryTheory.MonObj.lift_comp_one_left CategoryTheory.SemiCartesianMonoidalCategory.comp_toUnit_assoc
mul_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonObj.mul toMonObj inv CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mul_inv
mul_inv_rev 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonObj.mul toMonObj inv CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding	—	CategoryTheory.BraidedCategory.braiding_naturality_assoc tensorHom_inv_inv_mul CategoryTheory.SymmetricCategory.symmetry_assoc
mul_inv_rev_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonObj.mul toMonObj inv CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mul_inv_rev
ofIso_inv 📖	mathematical	—	inv ofIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	—
ofIso_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMonObj ofIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	—
ofIso_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMonObj ofIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom	—	—
right_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.CategoryStruct.id inv CategoryTheory.MonObj.mul toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.MonObj.one	—	—
right_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.CategoryStruct.id inv CategoryTheory.MonObj.mul toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.SemiCartesianMonoidalCategory.toUnit CategoryTheory.MonObj.one	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' right_inv
tensorHom_inv_inv_mul 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorHom inv CategoryTheory.MonObj.mul toMonObj CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding	—	mul_inv CategoryTheory.SymmetricCategory.symmetry_assoc
tensorHom_inv_inv_mul_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorHom inv CategoryTheory.MonObj.mul toMonObj CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' tensorHom_inv_inv_mul
toMonObj_injective 📖	mathematical	—	CategoryTheory.GrpObj CategoryTheory.MonObj CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMonObj	—	lift_left_mul_ext left_inv right_inv
toMon_Class_injective 📖	mathematical	—	CategoryTheory.GrpObj CategoryTheory.MonObj CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMonObj	—	toMonObj_injective

CategoryTheory.GrpObj.tensorObj

Definitions

Name	Category	Theorems
instTensorObj 📖	CompOp	2 math math: inv_def, CategoryTheory.Grp.tensorHom_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inv_def 📖	mathematical	—	CategoryTheory.GrpObj.inv CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instTensorObj CategoryTheory.MonoidalCategoryStruct.tensorHom	—	—

CategoryTheory.MonObj

Definitions

Name	Category	Theorems
termι 📖	CompOp	—
«termι[_]» 📖	CompOp	—

---

← Back to Index