Grp_

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

Statistics

Metric	Count
Definitions instGrpObj, instMonObj, commutator, ofRepresentableBy, ofRepresentableBy, commGroup, group, yonedaGrp, yonedaGrpFullyFaithful, yonedaGrpObj, yonedaGrpObjIsoOfRepresentableBy, yonedaGrpObjRepresentableBy	12
Theorems map_inv', hom_div, hom_hom_div, hom_hom_inv, hom_hom_zpow, hom_inv, hom_mul, hom_one, hom_pow, hom_zpow, hom_mul, hom_one, instIsCommMonObj, instIsMonHom, comp_div, comp_div_assoc, comp_inv, comp_inv_assoc, comp_zpow, comp_zpow_assoc, div_comp, div_comp_assoc, inv_comp, inv_comp_assoc, inv_eq_inv, lift_commutator_eq_mul_mul_inv_inv, lift_commutator_eq_mul_mul_inv_inv_assoc, ofRepresentableBy_yonedaGrpObjRepresentableBy, one_inv, one_inv_assoc, whiskerLeft_η_commutator, whiskerLeft_η_commutator_assoc, zpow_comp, zpow_comp_assoc, η_whiskerRight_commutator, η_whiskerRight_commutator_assoc, comp_div, comp_inv, comp_zpow, div_comp, inv_comp, inv_eq_inv, ofRepresentableBy_yonedaGrpObjRepresentableBy, zpow_comp, inv_def, essImage_yonedaGrp, instFaithfulGrpFunctorOppositeGrpCatYonedaGrp, instFullGrpFunctorOppositeGrpCatYonedaGrp, instIsMonHomInvHomOfIsCommMonObj, instIsMonHomInvOfIsCommMonObj, isCommMonObj_iff_commutator_eq_toUnit_η, yonedaGrpObjIsoOfRepresentableBy_hom, yonedaGrpObjIsoOfRepresentableBy_inv, yonedaGrpObj_map, yonedaGrpObj_obj_coe, yonedaGrp_map_app, yonedaGrp_naturality, yonedaGrp_naturality_assoc, yonedaGrp_obj	59
Total	71

CategoryTheory

Definitions

Name	Category	Theorems
yonedaGrp 📖	CompOp	5 math math: yonedaGrp_obj, instFaithfulGrpFunctorOppositeGrpCatYonedaGrp, essImage_yonedaGrp, instFullGrpFunctorOppositeGrpCatYonedaGrp, yonedaGrp_map_app
yonedaGrpFullyFaithful 📖	CompOp	—
yonedaGrpObj 📖	CompOp	10 math math: yonedaGrp_obj, Grp_Class.ofRepresentableBy_yonedaGrpObjRepresentableBy, yonedaGrp_naturality_assoc, yonedaGrpObj_map, yonedaGrpObjIsoOfRepresentableBy_hom, yonedaGrpObjIsoOfRepresentableBy_inv, yonedaGrpObj_obj_coe, GrpObj.ofRepresentableBy_yonedaGrpObjRepresentableBy, yonedaGrp_map_app, yonedaGrp_naturality
yonedaGrpObjIsoOfRepresentableBy 📖	CompOp	2 math math: yonedaGrpObjIsoOfRepresentableBy_hom, yonedaGrpObjIsoOfRepresentableBy_inv
yonedaGrpObjRepresentableBy 📖	CompOp	2 math math: Grp_Class.ofRepresentableBy_yonedaGrpObjRepresentableBy, GrpObj.ofRepresentableBy_yonedaGrpObjRepresentableBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
essImage_yonedaGrp 📖	mathematical	—	Functor.essImage Grp Functor Opposite Category.opposite GrpCat GrpCat.instCategory Grp.instCategory Functor.category yonedaGrp Set.preimage types Functor.comp forget MonoidHom GrpCat.carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid GrpCat.str MonoidHom.instFunLike GrpCat.instConcreteCategoryMonoidHomCarrier setOf Functor.IsRepresentable	—	—
instFaithfulGrpFunctorOppositeGrpCatYonedaGrp 📖	mathematical	—	Functor.Faithful Grp Grp.instCategory Functor Opposite Category.opposite GrpCat GrpCat.instCategory Functor.category yonedaGrp	—	Functor.FullyFaithful.faithful
instFullGrpFunctorOppositeGrpCatYonedaGrp 📖	mathematical	—	Functor.Full Grp Grp.instCategory Functor Opposite Category.opposite GrpCat GrpCat.instCategory Functor.category yonedaGrp	—	Functor.FullyFaithful.full
instIsMonHomInvHomOfIsCommMonObj 📖	mathematical	—	IsMonHom SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory GrpObj.toMonObj Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Hom.group	—	IsMonHom.one_hom instIsMonHomComp instIsMonHomInvOfIsCommMonObj IsMonHom.mul_hom
instIsMonHomInvOfIsCommMonObj 📖	mathematical	—	IsMonHom SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory GrpObj.toMonObj GrpObj.inv	—	MonObj.one_eq_one inv_one GrpObj.mul_inv_rev IsCommMonObj.mul_comm
isCommMonObj_iff_commutator_eq_toUnit_η 📖	mathematical	—	IsCommMonObj SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory GrpObj.toMonObj GrpObj.commutator CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct MonoidalCategoryStruct.tensorUnit SemiCartesianMonoidalCategory.toUnit MonObj.one	—	isCommMonObj_iff_isMulCommutative mul_inv_cancel_comm mul_inv_cancel MonObj.one_eq_one MonObj.comp_one GrpObj.lift_commutator_eq_mul_mul_inv_inv one_mul
yonedaGrpObjIsoOfRepresentableBy_hom 📖	mathematical	—	Iso.hom Functor Opposite Category.opposite GrpCat GrpCat.instCategory Functor.category yonedaGrpObj GrpObj.ofRepresentableBy yonedaGrpObjIsoOfRepresentableBy GrpCat.ofHom Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop GrpCat.carrier Functor.obj GrpCat.str MonoidHomClass.toMonoidHom MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass Functor.RepresentableBy.homEquiv Functor.comp types forget MonoidHom MonoidHom.instFunLike GrpCat.instConcreteCategoryMonoidHomCarrier MulEquiv.toGrpIso	—	—
yonedaGrpObjIsoOfRepresentableBy_inv 📖	mathematical	—	Iso.inv Functor Opposite Category.opposite GrpCat GrpCat.instCategory Functor.category yonedaGrpObj GrpObj.ofRepresentableBy yonedaGrpObjIsoOfRepresentableBy GrpCat.ofHom GrpCat.carrier Functor.obj Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop GrpCat.str MonoidHomClass.toMonoidHom MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass Equiv.symm Functor.RepresentableBy.homEquiv Functor.comp types forget MonoidHom MonoidHom.instFunLike GrpCat.instConcreteCategoryMonoidHomCarrier MulEquiv.symm_map_mul MulEquiv.toGrpIso	—	—
yonedaGrpObj_map 📖	mathematical	—	Functor.map Opposite Category.opposite GrpCat GrpCat.instCategory yonedaGrpObj GrpCat.ofHom Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop Hom.group MonCat.Hom.hom Functor.obj MonCat MonCat.instCategory yonedaMonObj GrpObj.toMonObj	—	—
yonedaGrpObj_obj_coe 📖	mathematical	—	GrpCat.carrier Functor.obj Opposite Category.opposite GrpCat GrpCat.instCategory yonedaGrpObj Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop	—	—
yonedaGrp_map_app 📖	mathematical	—	NatTrans.app Opposite Category.opposite GrpCat GrpCat.instCategory yonedaGrpObj Grp.X Grp.grp Functor.map Grp Grp.instCategory Functor Functor.category yonedaGrp GrpCat.ofHom Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop Hom.group MonCat.Hom.hom Functor.obj MonCat MonCat.instCategory Mon SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Mon.instCategory yonedaMon Grp.toMon InducedCategory.Hom.hom	—	—
yonedaGrp_naturality 📖	mathematical	—	DFunLike.coe Functor.obj Opposite Category.opposite GrpCat GrpCat.instCategory yonedaGrpObj Opposite.op GrpCat.carrier ConcreteCategory.hom MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid GrpCat.str MonoidHom.instFunLike GrpCat.instConcreteCategoryMonoidHomCarrier NatTrans.app CategoryStruct.comp Category.toCategoryStruct Opposite.unop	—	NatTrans.naturality
yonedaGrp_naturality_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct DFunLike.coe MonoidHom GrpCat.carrier Functor.obj Opposite Category.opposite GrpCat GrpCat.instCategory yonedaGrpObj Opposite.op MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid GrpCat.str MonoidHom.instFunLike ConcreteCategory.hom GrpCat.instConcreteCategoryMonoidHomCarrier NatTrans.app	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' yonedaGrp_naturality
yonedaGrp_obj 📖	mathematical	—	Functor.obj Grp Grp.instCategory Functor Opposite Category.opposite GrpCat GrpCat.instCategory Functor.category yonedaGrp yonedaGrpObj Grp.X Grp.grp	—	—

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_inv' 📖	mathematical	—	map Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CategoryTheory.Hom.group obj grpObjObj	—	eq_inv_iff_mul_eq_one map_mul inv_mul_cancel map_one

CategoryTheory.Grp

Definitions

Name	Category	Theorems
instGrpObj 📖	CompOp	8 math math: Hom.hom_div, Hom.hom_hom_zpow, CategoryTheory.yonedaCommGrpGrpObj_map, Hom.hom_zpow, Hom.hom_hom_div, Hom.hom_hom_inv, CategoryTheory.yonedaCommGrpGrp_map_app, Hom.hom_inv
instMonObj 📖	CompOp	7 math math: hom_mul, instIsMonHom, Hom.hom_pow, Hom.hom_mul, instIsCommMonObj, hom_one, Hom.hom_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_mul 📖	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.MonObj.mul instMonObj X CategoryTheory.GrpObj.toMonObj grp	—	—
hom_one 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory toMon CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Grp instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.MonObj.one instMonObj X CategoryTheory.GrpObj.toMonObj grp	—	—
instIsCommMonObj 📖	mathematical	—	CategoryTheory.IsCommMonObj CategoryTheory.Grp instCategory instMonoidalCategory instBraidedCategory instMonObj	—	CategoryTheory.MonObj.mul_eq_mul CategoryTheory.MonObj.comp_mul CategoryTheory.CartesianMonoidalCategory.braiding_hom_fst CategoryTheory.CartesianMonoidalCategory.braiding_hom_snd hom_ext CategoryTheory.Mon.instIsCommMonObj mul_comm
instIsMonHom 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.Grp instCategory instMonoidalCategory instMonObj	—	hom_ext CategoryTheory.IsMonHom.one_hom CategoryTheory.Mon.instIsMonHomHom CategoryTheory.IsMonHom.mul_hom

CategoryTheory.Grp.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_div 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Grp.toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Grp.instCategory DivInvMonoid.toDiv Group.toDivInvMonoid CategoryTheory.Hom.group CategoryTheory.Grp.instCartesianMonoidalCategory CategoryTheory.Grp.instGrpObj CategoryTheory.Mon.X CategoryTheory.Grp.grp	—	hom_hom_div
hom_hom_div 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Grp.toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Grp.instCategory DivInvMonoid.toDiv Group.toDivInvMonoid CategoryTheory.Hom.group CategoryTheory.Grp.instCartesianMonoidalCategory CategoryTheory.Grp.instGrpObj CategoryTheory.Mon.X CategoryTheory.Grp.grp	—	—
hom_hom_inv 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Grp.toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Grp.instCategory InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CategoryTheory.Hom.group CategoryTheory.Grp.instCartesianMonoidalCategory CategoryTheory.Grp.instGrpObj CategoryTheory.Mon.X CategoryTheory.Grp.grp	—	—
hom_hom_zpow 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Grp.toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Grp.instCategory DivInvMonoid.toZPow Group.toDivInvMonoid CategoryTheory.Hom.group CategoryTheory.Grp.instCartesianMonoidalCategory CategoryTheory.Grp.instGrpObj CategoryTheory.Mon.X CategoryTheory.Grp.grp	—	zpow_natCast hom_pow CategoryTheory.Mon.Hom.hom_pow zpow_negSucc
hom_inv 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Grp.toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Grp.instCategory InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CategoryTheory.Hom.group CategoryTheory.Grp.instCartesianMonoidalCategory CategoryTheory.Grp.instGrpObj CategoryTheory.Mon.X CategoryTheory.Grp.grp	—	hom_hom_inv
hom_mul 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.instCategory CategoryTheory.Grp.toMon Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Grp.instCategory MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid CategoryTheory.Grp.instCartesianMonoidalCategory CategoryTheory.Grp.instMonObj CategoryTheory.Mon.instCartesianMonoidalCategory CategoryTheory.Mon.instMonObjOfIsCommMonObjX	—	—
hom_one 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.instCategory CategoryTheory.Grp.toMon Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Grp.instCategory MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid CategoryTheory.Grp.instCartesianMonoidalCategory CategoryTheory.Grp.instMonObj CategoryTheory.Mon.instCartesianMonoidalCategory CategoryTheory.Mon.instMonObjOfIsCommMonObjX	—	—
hom_pow 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Mon.instCategory CategoryTheory.Grp.toMon Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Grp.instCategory Monoid.toNatPow CategoryTheory.Hom.monoid CategoryTheory.Grp.instCartesianMonoidalCategory CategoryTheory.Grp.instMonObj CategoryTheory.Mon.instCartesianMonoidalCategory CategoryTheory.Mon.instMonObjOfIsCommMonObjX	—	pow_zero pow_succ
hom_zpow 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Grp.toMon CategoryTheory.InducedCategory.Hom.hom CategoryTheory.Grp CategoryTheory.Mon CategoryTheory.Mon.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Grp.instCategory DivInvMonoid.toZPow Group.toDivInvMonoid CategoryTheory.Hom.group CategoryTheory.Grp.instCartesianMonoidalCategory CategoryTheory.Grp.instGrpObj CategoryTheory.Mon.X CategoryTheory.Grp.grp	—	hom_hom_zpow

CategoryTheory.GrpObj

Definitions

Name	Category	Theorems
commutator 📖	CompOp	7 math math: η_whiskerRight_commutator_assoc, CategoryTheory.isCommMonObj_iff_commutator_eq_toUnit_η, whiskerLeft_η_commutator, lift_commutator_eq_mul_mul_inv_inv, whiskerLeft_η_commutator_assoc, lift_commutator_eq_mul_mul_inv_inv_assoc, η_whiskerRight_commutator
ofRepresentableBy 📖	CompOp	4 math math: CategoryTheory.Grp_Class.ofRepresentableBy_yonedaGrpObjRepresentableBy, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_hom, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_inv, ofRepresentableBy_yonedaGrpObjRepresentableBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_div 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver DivInvMonoid.toDiv Group.toDivInvMonoid CategoryTheory.Hom.group	—	MonoidHom.map_div
comp_div_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver DivInvMonoid.toDiv Group.toDivInvMonoid CategoryTheory.Hom.group	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_div
comp_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CategoryTheory.Hom.group	—	MonoidHom.map_inv
comp_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CategoryTheory.Hom.group	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_inv
comp_zpow 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver DivInvMonoid.toZPow Group.toDivInvMonoid CategoryTheory.Hom.group	—	zpow_natCast CategoryTheory.MonObj.comp_pow zpow_negSucc comp_inv
comp_zpow_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver DivInvMonoid.toZPow Group.toDivInvMonoid CategoryTheory.Hom.group	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_zpow
div_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver DivInvMonoid.toDiv Group.toDivInvMonoid CategoryTheory.Hom.group	—	MonoidHom.map_div
div_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver DivInvMonoid.toDiv Group.toDivInvMonoid CategoryTheory.Hom.group	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' div_comp
inv_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CategoryTheory.Hom.group	—	CategoryTheory.Category.assoc inv_hom
inv_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CategoryTheory.Hom.group	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inv_comp
inv_eq_inv 📖	mathematical	—	inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CategoryTheory.Hom.group CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.id_comp
lift_commutator_eq_mul_mul_inv_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift commutator Quiver.Hom CategoryTheory.CategoryStruct.toQuiver MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid toMonObj InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CategoryTheory.Hom.group	—	CategoryTheory.MonObj.comp_mul CategoryTheory.CartesianMonoidalCategory.lift_fst CategoryTheory.CartesianMonoidalCategory.lift_snd comp_inv
lift_commutator_eq_mul_mul_inv_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift commutator Quiver.Hom CategoryTheory.CategoryStruct.toQuiver MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Hom.monoid toMonObj InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CategoryTheory.Hom.group	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_commutator_eq_mul_mul_inv_inv
ofRepresentableBy_yonedaGrpObjRepresentableBy 📖	mathematical	—	ofRepresentableBy CategoryTheory.yonedaGrpObj CategoryTheory.yonedaGrpObjRepresentableBy	—	ext CategoryTheory.MonObj.ext CategoryTheory.CartesianMonoidalCategory.lift_fst_snd CategoryTheory.Category.id_comp
one_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonObj.one toMonObj inv	—	CategoryTheory.MonObj.one_eq_one inv_eq_inv comp_inv CategoryTheory.Category.comp_id inv_one
one_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonObj.one toMonObj inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' one_inv
whiskerLeft_η_commutator 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonObj.one toMonObj commutator CategoryTheory.SemiCartesianMonoidalCategory.toUnit	—	CategoryTheory.MonObj.one_eq_one CategoryTheory.MonObj.comp_mul CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst CategoryTheory.CartesianMonoidalCategory.whiskerLeft_snd CategoryTheory.MonObj.comp_one mul_one comp_inv mul_inv_cancel inv_one
whiskerLeft_η_commutator_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonObj.one toMonObj commutator CategoryTheory.SemiCartesianMonoidalCategory.toUnit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_η_commutator
zpow_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver DivInvMonoid.toZPow Group.toDivInvMonoid CategoryTheory.Hom.group	—	MonoidHom.map_zpow
zpow_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver DivInvMonoid.toZPow Group.toDivInvMonoid CategoryTheory.Hom.group	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' zpow_comp
η_whiskerRight_commutator 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one toMonObj commutator CategoryTheory.SemiCartesianMonoidalCategory.toUnit	—	CategoryTheory.MonObj.one_eq_one CategoryTheory.MonObj.comp_mul CategoryTheory.CartesianMonoidalCategory.whiskerRight_fst CategoryTheory.MonObj.comp_one CategoryTheory.CartesianMonoidalCategory.whiskerRight_snd one_mul comp_inv inv_one mul_one mul_inv_cancel
η_whiskerRight_commutator_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one toMonObj commutator CategoryTheory.SemiCartesianMonoidalCategory.toUnit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' η_whiskerRight_commutator

CategoryTheory.Grp_Class

Definitions

Name	Category	Theorems
ofRepresentableBy 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_div 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver DivInvMonoid.toDiv Group.toDivInvMonoid CategoryTheory.Hom.group	—	CategoryTheory.GrpObj.comp_div
comp_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CategoryTheory.Hom.group	—	CategoryTheory.GrpObj.comp_inv
comp_zpow 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver DivInvMonoid.toZPow Group.toDivInvMonoid CategoryTheory.Hom.group	—	CategoryTheory.GrpObj.comp_zpow
div_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver DivInvMonoid.toDiv Group.toDivInvMonoid CategoryTheory.Hom.group	—	CategoryTheory.GrpObj.div_comp
inv_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CategoryTheory.Hom.group	—	CategoryTheory.GrpObj.inv_comp
inv_eq_inv 📖	mathematical	—	CategoryTheory.GrpObj.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CategoryTheory.Hom.group CategoryTheory.CategoryStruct.id	—	CategoryTheory.GrpObj.inv_eq_inv
ofRepresentableBy_yonedaGrpObjRepresentableBy 📖	mathematical	—	CategoryTheory.GrpObj.ofRepresentableBy CategoryTheory.yonedaGrpObj CategoryTheory.yonedaGrpObjRepresentableBy	—	CategoryTheory.GrpObj.ofRepresentableBy_yonedaGrpObjRepresentableBy
zpow_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver DivInvMonoid.toZPow Group.toDivInvMonoid CategoryTheory.Hom.group	—	CategoryTheory.GrpObj.zpow_comp

CategoryTheory.Hom

Definitions

Name	Category	Theorems
commGroup 📖	CompOp	2 math math: CategoryTheory.yonedaCommGrpGrpObj_map, CategoryTheory.yonedaCommGrpGrp_map_app
group 📖	CompOp	33 math math: CategoryTheory.Grp.Hom.hom_div, CategoryTheory.Grp.Hom.hom_hom_zpow, CategoryTheory.Grp_Class.comp_inv, CategoryTheory.Grp_Class.comp_zpow, CategoryTheory.GrpObj.comp_zpow, CategoryTheory.Grp.Hom.hom_zpow, CategoryTheory.Functor.map_inv', CategoryTheory.Grp.Hom.hom_hom_div, CategoryTheory.GrpObj.inv_comp_assoc, CategoryTheory.Grp.Hom.hom_hom_inv, CategoryTheory.Grp_Class.zpow_comp, CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv, inv_def, CategoryTheory.Grp_Class.inv_comp, CategoryTheory.instIsMonHomInvHomOfIsCommMonObj, CategoryTheory.GrpObj.div_comp_assoc, CategoryTheory.Grp_Class.comp_div, CategoryTheory.yonedaGrpObj_map, CategoryTheory.GrpObj.comp_div, CategoryTheory.GrpObj.comp_zpow_assoc, CategoryTheory.GrpObj.inv_eq_inv, CategoryTheory.GrpObj.zpow_comp, CategoryTheory.GrpObj.inv_comp, CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv_assoc, CategoryTheory.GrpObj.div_comp, CategoryTheory.GrpObj.comp_inv_assoc, CategoryTheory.GrpObj.comp_div_assoc, CategoryTheory.Grp_Class.inv_eq_inv, CategoryTheory.GrpObj.comp_inv, CategoryTheory.Grp.Hom.hom_inv, CategoryTheory.yonedaGrp_map_app, CategoryTheory.Grp_Class.div_comp, CategoryTheory.GrpObj.zpow_comp_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inv_def 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid group CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv	—	—

---

← Back to Index