Structures · Category theory
CategoryTheory.AddGrpObj
An additive group object internal to a cartesian monoidal category.
Also see the bundled AddGrp.
- Defined in
- Mathlib.CategoryTheory.Monoidal.Grp
- Shape
- One type argument · adds neg, left_neg, right_neg
Extends1
Extended by1
Concrete types that are instances1
- CategoryTheory.AddGrp
How is a type an instance?
Loading the hierarchy index…
Assumed by100
- CategoryTheory.AddGrpObj.neg
- CategoryTheory.Hom.addGroup
- CategoryTheory.AddGrpObj.comp_neg
- CategoryTheory.yonedaAddGrpObj
- CategoryTheory.AddGrpObj.addCommutator
- CategoryTheory.AddGrpObj.addConj
- CategoryTheory.AddGrpObj.left_neg
- CategoryTheory.AddGrpObj.lift_comp_neg_right
- CategoryTheory.AddGrpObj.lift_comp_neg_left
- CategoryTheory.AddGrpObj.right_neg
- CategoryTheory.AddGrpObj.ofIso
- CategoryTheory.Functor.addGrpObjObj
- CategoryTheory.Functor.FullyFaithful.addGrpObj
- CategoryTheory.AddGrpObj.lift_left_add_ext
- CategoryTheory.AddGrpObj.addRight
- CategoryTheory.AddGrpObj.eq_lift_neg_right
- CategoryTheory.AddGrp.mkIso'
- CategoryTheory.AddGrpObj.neg_comp_neg
- CategoryTheory.AddGrpObj.eq_lift_neg_left
- CategoryTheory.AddGrpObj.lift_neg_comp_left
- CategoryTheory.AddGrpObj.lift_addCommutator_eq_add_add_neg_neg
- CategoryTheory.AddGrpObj.lift_addConj_eq_add_add_neg
- CategoryTheory.AddGrpObj.tensorHom_neg_neg_add
- CategoryTheory.AddGrpObj.neg_hom
- CategoryTheory.AddGrpObj.neg_comp
- CategoryTheory.AddGrpObj.add_neg
- CategoryTheory.AddGrpObj.lift_neg_comp_right
- CategoryTheory.AddGrpObj.η_whiskerRight_addCommutator
- CategoryTheory.AddGrpObj.sub_comp
- CategoryTheory.yonedaAddGrp_naturality
- CategoryTheory.AddGrpObj.isPullback
- CategoryTheory.Functor.obj.neg_def
- CategoryTheory.AddGrpObj.add_neg_rev
- CategoryTheory.AddGrpObj.comp_zsmul
- CategoryTheory.AddGrpObj.zsmul_comp
- CategoryTheory.AddGrp.ofHom
- CategoryTheory.AddGrpObj.zero_neg
- CategoryTheory.AddGrpObj.lift_neg_left_eq
- CategoryTheory.AddGrpObj.whiskerLeft_η_addCommutator
- CategoryTheory.IsAddMonHom.isNormalHom_iff
- CategoryTheory.AddGrpObj.addRight_hom
- CategoryTheory.yonedaAddGrpObjRepresentableBy
- CategoryTheory.AddGrpObj.neg_eq_neg
- CategoryTheory.AddGrpObj.comp_sub
- CategoryTheory.Functor.FullyFaithful.addGrpObj_add
- CategoryTheory.IsAddMonHom.instNormalZero
- CategoryTheory.AddGrpObj.comp_neg_assoc
- CategoryTheory.instIsAddMonHomNegOfIsCommAddMonObj
- CategoryTheory.AddGrpObj.ofIso_neg
- CategoryTheory.IsAddMonHom.instNormalId