Structures · Category theory
CategoryTheory.IsModHom
A morphism in D is a morphism of A-module objects if it commutes with
the action maps
- Defined in
- Mathlib.CategoryTheory.Monoidal.Mod
- Shape
- 2 explicit arguments · adds smul_hom
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by11
- CategoryTheory.IsModHom.smul_hom
- CategoryTheory.Mod.scalarRestriction_hom
- CategoryTheory.IsModHom.map_smul
- CategoryTheory.IsModHom.mulActionHom
- CategoryTheory.IsModHom.map_smul_assoc
- CategoryTheory.IsMod_Hom.smul_hom
- CategoryTheory.IsModHom.mulActionHom_apply
- CategoryTheory.Mod_.scalarRestriction_hom
- CategoryTheory.instIsModHomInvOfHom
- CategoryTheory.instIsModHomComp
- CategoryTheory.IsModHom.smul_hom_assoc
Ancestors0
No ancestors.