Structures · Category theory
CategoryTheory.IsAddMonHom
The property that a morphism between additive monoid objects is an additive monoid morphism.
- Defined in
- Mathlib.CategoryTheory.Monoidal.Mon
- Shape
- One type argument · adds zero_hom, add_hom
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances1
- CategoryTheory.AddGrp
How is a type an instance?
Loading the hierarchy index…
Assumed by65
- CategoryTheory.IsAddMonHom.addMonoidHom
- CategoryTheory.AddMon.mkIso'
- CategoryTheory.IsAddMonHom.zero_hom
- CategoryTheory.AddMod.scalarRestriction
- CategoryTheory.IsAddMonHom.add_hom
- CategoryTheory.IsAddMonHom.addMonoidHom_apply
- CategoryTheory.AddMod.comap
- CategoryTheory.AddMonObj.add_comp
- CategoryTheory.AddGrp.homMk
- CategoryTheory.AddGrp.mkIso'
- CategoryTheory.Hom.addEquivCongrRight
- CategoryTheory.AddGrpObj.lift_neg_comp_left
- CategoryTheory.AddGrpObj.neg_hom
- CategoryTheory.AddGrpObj.neg_comp
- CategoryTheory.AddMonObj.zero_comp
- CategoryTheory.AddGrpObj.lift_neg_comp_right
- CategoryTheory.AddGrpObj.sub_comp
- CategoryTheory.AddMod.scalarRestriction_vadd
- CategoryTheory.AddMon.ofHom
- CategoryTheory.AddGrpObj.zsmul_comp
- CategoryTheory.AddGrp.ofHom
- CategoryTheory.AddModObj.ofIso
- CategoryTheory.IsAddMonHom.isNormalHom_iff
- CategoryTheory.AddMonObj.nsmul_comp
- CategoryTheory.IsAddMonHom.addMonoidHom.congr_simp
- CategoryTheory.AddGrpObj.lift_neg_comp_left_assoc
- CategoryTheory.AddGrp.mkIso'_inv_hom_hom
- CategoryTheory.AddMonObj.instIsAddMonHomWhiskerLeft
- CategoryTheory.IsAddMonHom.Normal.of_isPullback_η
- CategoryTheory.Functor.map.instIsAddMonHom
- CategoryTheory.instIsAddMonHomHomAsIso
- CategoryTheory.AddGrp.mkIso'_hom_hom_hom
- CategoryTheory.AddMod.scalarRestriction_hom
- CategoryTheory.AddMon.mkIso'_inv_hom
- CategoryTheory.AddGrpObj.lift_neg_comp_right_assoc
- CategoryTheory.AddGrpObj.zsmul_comp_assoc
- CategoryTheory.AddMon.mkIso'_hom_hom
- CategoryTheory.AddGrp.ofHom_hom_hom
- CategoryTheory.AddMonObj.instIsAddMonHomLift
- CategoryTheory.AddMod.comap_obj_addMod
- CategoryTheory.AddMonObj.add_comp_assoc
- CategoryTheory.instIsAddMonHomNegHomOfIsCommAddMonObj
- CategoryTheory.AddGrpObj.sub_comp_assoc
- CategoryTheory.AddModObj.ofIso_vadd
- CategoryTheory.Hom.addEquivCongrRight_symm_apply
- CategoryTheory.AddMonObj.instIsAddMonHomTensorHom
- CategoryTheory.AddMon.Hom.mk.congr_simp
- CategoryTheory.AddGrpObj.neg_comp_assoc
- CategoryTheory.AddGrp.homMk_hom_hom
- CategoryTheory.IsAddMonHom.instNormalOfIsCommAddMonObjOfMono
Ancestors0
No ancestors.