Structures · Category theory
CategoryTheory.Functor.Linear
An additive functor F is R-linear provided F.map is an R-module morphism.
- Shape
- 2 explicit arguments · adds map_smul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- Int
- Nat
- Rat
How is a type an instance?
Loading the hierarchy index…
Assumed by34
- CategoryTheory.Functor.map_smul
- CategoryTheory.Functor.map_units_smul
- CategoryTheory.Functor.mapExtLinearMap
- CategoryTheory.ShiftedHom.comp_smul
- CategoryTheory.Functor.Linear.map_smul
- CategoryTheory.Functor.mapLinearMap
- CategoryTheory.Localization.functor_linear_iff
- CategoryTheory.Functor.linear_of_iso
- CategoryTheory.ShiftedHom.map_smul
- CategoryTheory.Functor.linear_of_full_essSurj_comp
- CategoryTheory.Shift.instLinearLocalizationShiftFunctorOfCommShiftOfQ
- CategoryTheory.Pretriangulated.Triangle.smul_hom₃
- CategoryTheory.Functor.instLinearComp
- CategoryTheory.Functor.instLinearDerivedCategoryMapDerivedCategory
- CategoryTheory.Shift.linear_of_localization
- CategoryTheory.Pretriangulated.Triangle.instLinear
- CategoryTheory.Equivalence.inverseLinear
- CategoryTheory.Functor.mapExactFunctor_smul
- CategoryTheory.Functor.mapLinearMap_apply
- CategoryTheory.Pretriangulated.Triangle.smul_hom₁
- CategoryTheory.Functor.mapExtLinearMap_coe
- CategoryTheory.Functor.mapExtLinearMap_apply
- CategoryTheory.MonoidalLinear.ofFaithful
- CategoryTheory.Functor.linear_comp_iff_of_full_of_essSurj
- CategoryTheory.Functor.mapAction_linear
- CategoryTheory.instLinearHomotopyCategoryMapHomotopyCategory
- CategoryTheory.Shift.instLinearLocalization'ShiftFunctorOfCommShiftOfQ'
- CategoryTheory.Pretriangulated.Triangle.smul_hom₂
- CategoryTheory.Free.liftUnique
- CategoryTheory.Pretriangulated.Triangle.instModuleHom
- CategoryTheory.Functor.mapHomologicalComplex_linear
- CategoryTheory.Functor.mapExtLinearMap_toAddMonoidHom
- CategoryTheory.Pretriangulated.Triangle.instSMulHom
- CategoryTheory.Functor.coe_mapLinearMap
Ancestors0
No ancestors.