Linear

📁 Source: Mathlib/Algebra/Homology/Linear.lean

Statistics

Metric	Count
Definitions instLinear, instModuleHom, instSMulHom	3
Theorems mapHomologicalComplex_linear, smul_f_apply, units_smul_f_apply	3
Total	6

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapHomologicalComplex_linear 📖	mathematical	—	Linear HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomologicalComplex.instPreadditive HomologicalComplex.instLinear mapHomologicalComplex preservesZeroMorphisms_of_additive	—	preservesZeroMorphisms_of_additive HomologicalComplex.hom_ext map_smul

HomologicalComplex

Definitions

Name	Category	Theorems
instLinear 📖	CompOp	6 math math: CategoryTheory.Functor.mapHomologicalComplex_linear, CochainComplex.instLinearIntFunctorSingleFunctors, DerivedCategory.instLinearCochainComplexIntQ, CochainComplex.instLinearHomologicalComplexIntUpShiftFunctor, CochainComplex.instLinearIntShiftFunctor, HomotopyCategory.instLinearHomologicalComplexQuotient
instModuleHom 📖	CompOp	—
instSMulHom 📖	CompOp	3 math math: units_smul_f_apply, smul_f_apply, Homotopy.smul_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul_f_apply 📖	mathematical	—	Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Quiver.Hom HomologicalComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instSMulHom X SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid CategoryTheory.Linear.homModule	—	—
units_smul_f_apply 📖	mathematical	—	Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Quiver.Hom HomologicalComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory Units.instSMul instSMulHom X SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction AddCommGroup.toAddCommMonoid CategoryTheory.Linear.homModule	—	—

---

← Back to Index