Structures · Category theory
CategoryTheory.Linear
A category is called R-linear if P ⟶ Q is an R-module such that composition is
R-linear in both variables.
- Defined in
- Mathlib.CategoryTheory.Linear.Basic
- Shape
- 2 explicit arguments · adds homModule, smul_comp, comp_smul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Int
- Nat
How is a type an instance?
Loading the hierarchy index…
Assumed by241
- CategoryTheory.Linear.comp_units_smul
- CategoryTheory.Linear.units_smul_comp
- CategoryTheory.Linear.smul_comp
- CategoryTheory.Linear.comp_smul
- CategoryTheory.Functor.map_smul
- CategoryTheory.Linear.leftComp
- CategoryTheory.linearYoneda
- CochainComplex.HomComplex.δ_hom
- ChainComplex.linearYonedaObj
- CategoryTheory.Linear.rightComp
- CategoryTheory.ShortComplex.LeftHomologyMapData.smul
- CategoryTheory.ShortComplex.RightHomologyMapData.smul
- CochainComplex.HomComplex.δ_units_smul
- CategoryTheory.linearCoyoneda
- CategoryTheory.Abelian.Ext.smul_hom
- CategoryTheory.Functor.map_units_smul
- CategoryTheory.ShortComplex.Homotopy.smul
- CategoryTheory.Abelian.Ext.mk₀_smul
- CategoryTheory.ShiftedHom.mk₀_smul
- CategoryTheory.Functor.mapExtLinearMap
- CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv
- CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv
- CategoryTheory.Free.lift
- CategoryTheory.ShiftedHom.comp_smul
- CategoryTheory.Linear.toCatCenter
- CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv
- CategoryTheory.InducedCategory.homLinearEquiv
- CategoryTheory.finrank_hom_simple_simple_le_one
- CategoryTheory.Linear.homCongr
- CategoryTheory.Abelian.Ext.comp_smul
- CategoryTheory.Abelian.Ext.homLinearEquiv
- CategoryTheory.Functor.mapLinearMap
- CategoryTheory.ShortComplex.HomologyMapData.smul
- CategoryTheory.finrank_hom_simple_simple_eq_one_iff
- CategoryTheory.Abelian.Ext.linearEquiv₀
- CategoryTheory.Abelian.Ext.smul_comp
- CochainComplex.HomComplex.Cochain.comp_units_smul
- CategoryTheory.ShortComplex.leftHomologyMap'_smul
- CategoryTheory.finrank_endomorphism_simple_eq_one
- CochainComplex.HomComplex.Cochain.leftShift_units_smul
- CochainComplex.HomComplex.Cochain.comp_smul
- CochainComplex.HomComplex.Cochain.rightUnshift_units_smul
- CategoryTheory.NatTrans.appLinearMap
- CategoryTheory.Functor.linear_iff
- CategoryTheory.Localization.functor_linear_iff
- CochainComplex.HomComplex.Cochain.leftUnshift_units_smul
- CategoryTheory.Localization.linear
- Ext
- CochainComplex.HomComplex.δ_smul
- CategoryTheory.Linear.comp
Ancestors0
No ancestors.