Theorems · Inductive type · category theory
CategoryTheory.AddGrpObj
{C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.CartesianMonoidalCategory C] → C → Type v₁An additive group object internal to a cartesian monoidal category.
Also see the bundled AddGrp.
- Defined in
- Mathlib.CategoryTheory.Monoidal.Grp
- Cited by
- 88 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
- CategoryTheory.CartesianMonoidalCategorystatement · cited by 947
Cited by121
Results whose statement or proof uses this declaration.
- CategoryTheory.AddGrpObj.negstatement and proof · cited by 44
- CategoryTheory.Hom.addGroupstatement and proof · cited by 25
- CategoryTheory.AddGrpObj.comp_negstatement and proof · cited by 9
- CategoryTheory.yonedaAddGrpObjstatement and proof · cited by 9
- CategoryTheory.AddGrpObj.addCommutatorstatement and proof · cited by 7
- CategoryTheory.AddGrpObj.addConjstatement and proof · cited by 7
- CategoryTheory.AddGrpObj.left_negstatement and proof · cited by 6
- CategoryTheory.AddGrpObj.lift_comp_neg_leftstatement and proof · cited by 6
- CategoryTheory.AddGrpObj.lift_comp_neg_rightstatement and proof · cited by 6
- CategoryTheory.AddGrpObj.right_negstatement and proof · cited by 5
- CategoryTheory.AddGrpObj.ofIsostatement and proof · cited by 4
- CategoryTheory.AddGrpObj.ofRepresentableBystatement · cited by 4