Structures · Category theory
CategoryTheory.AddMonObj
An additive monoid object internal to a monoidal category.
- Defined in
- Mathlib.CategoryTheory.Monoidal.Mon
- Shape
- One type argument · adds zero, add, zero_add, add_zero, add_assoc
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances2
- CategoryTheory.AddGrp
- CategoryTheory.AddMon
How is a type an instance?
Loading the hierarchy index…
Assumed by192
- CategoryTheory.AddMonObj.add
- CategoryTheory.AddMonObj.zero
- CategoryTheory.Hom.addMonoid
- CategoryTheory.AddMod.X
- CategoryTheory.AddMod.Hom.hom
- CategoryTheory.yonedaAddMonObj
- CategoryTheory.Functor.addMonObjObj
- CategoryTheory.AddMonObj.comp_add
- CategoryTheory.IsAddMonHom.addMonoidHom
- CategoryTheory.AddMonObj.add_zero
- CategoryTheory.AddMonObj.add_assoc
- CategoryTheory.AddMonObj.zero_add
- CategoryTheory.AddMonObj.comp_zero
- CategoryTheory.AddMonObj.lift_comp_zero_right
- CategoryTheory.AddMonObj.lift_lift_assoc
- CategoryTheory.AddMon.mkIso'
- CategoryTheory.AddMonObj.zero_eq_zero
- CategoryTheory.AddMonObj.lift_comp_zero_left
- CategoryTheory.AddMod.scalarRestriction
- CategoryTheory.IsAddMonHom.addMonoidHom_apply
- CategoryTheory.AddMod.comap
- CategoryTheory.Mathlib.Tactic.MonTauto.add_assoc_hom
- CategoryTheory.Mathlib.Tactic.MonTauto.add_assoc_neg
- CategoryTheory.AddMonObj.ofIso
- CategoryTheory.AddMonObj.add_comp
- CategoryTheory.Functor.FullyFaithful.addMonObj
- CategoryTheory.Functor.FullyFaithful.homAddEquiv
- CategoryTheory.AddMod.regular
- CategoryTheory.AddModObj.add_vadd_self
- CategoryTheory.Hom.addCommMonoid
- CategoryTheory.Hom.addEquivCongrRight
- CategoryTheory.AddMonObj.comp_nsmul
- CategoryTheory.AddMonObj.ofIso_zero
- CategoryTheory.AddMonObj.ofIso_add
- CategoryTheory.AddMonObj.zero_comp
- CategoryTheory.IsCommAddMonObj.add_comm'
- CategoryTheory.AddMod.forget
- CategoryTheory.AddModObj.zero_vadd_self
- CategoryTheory.AddMod.id
- CategoryTheory.isCommAddMonObj_iff_isAddCommutative
- CategoryTheory.Functor.map_add'
- CategoryTheory.AddMonObj.add_zero_hom
- CategoryTheory.AddMod.hom_ext
- CategoryTheory.yonedaAddMon_naturality
- CategoryTheory.yonedaAddMonObjRepresentableBy
- CategoryTheory.AddMod.scalarRestriction_vadd
- CategoryTheory.AddMonObj.add_add_add_comm'
- CategoryTheory.AddMon.ofHom
- CategoryTheory.AddMonObj.add_assoc_flip
- CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_neg_tensor_zero_add
Ancestors0
No ancestors.