The category of homological complexes is linear #
In this file, we define the instance Linear R (HomologicalComplex C c) when the
category C is R-linear.
TODO #
- show lemmas like
HomologicalComplex.homologyMap_smul(after doing the same for short complexes inMathlib.Algebra.Homology.ShortComplex.Linear)
instance
HomologicalComplex.instSMulHomHomologicalComplexPreadditiveHasZeroMorphismsToQuiverToCategoryStructInstCategoryHomologicalComplex
{R : Type u_1}
[Semiring R]
{C : Type u_2}
[CategoryTheory.Category.{u_5, u_2} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
{ι : Type u_4}
{c : ComplexShape ι}
{X : HomologicalComplex C c}
{Y : HomologicalComplex C c}
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
HomologicalComplex.smul_f_apply
{R : Type u_1}
[Semiring R]
{C : Type u_2}
[CategoryTheory.Category.{u_5, u_2} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
{ι : Type u_4}
{c : ComplexShape ι}
{X : HomologicalComplex C c}
{Y : HomologicalComplex C c}
(r : R)
(f : X ⟶ Y)
(n : ι)
:
@[simp]
theorem
HomologicalComplex.units_smul_f_apply
{R : Type u_1}
[Semiring R]
{C : Type u_2}
[CategoryTheory.Category.{u_5, u_2} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
{ι : Type u_4}
{c : ComplexShape ι}
{X : HomologicalComplex C c}
{Y : HomologicalComplex C c}
(r : Rˣ)
(f : X ⟶ Y)
(n : ι)
:
instance
HomologicalComplex.instModuleHomHomologicalComplexPreadditiveHasZeroMorphismsToQuiverToCategoryStructInstCategoryHomologicalComplexToAddCommMonoidInstAddCommGroupHomHomologicalComplexPreadditiveHasZeroMorphismsToQuiverToCategoryStructInstCategoryHomologicalComplex
{R : Type u_1}
[Semiring R]
{C : Type u_2}
[CategoryTheory.Category.{u_5, u_2} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
{ι : Type u_4}
{c : ComplexShape ι}
(X : HomologicalComplex C c)
(Y : HomologicalComplex C c)
:
Equations
- One or more equations did not get rendered due to their size.
instance
HomologicalComplex.instLinearHomologicalComplexPreadditiveHasZeroMorphismsInstCategoryHomologicalComplexInstPreadditiveHomologicalComplexPreadditiveHasZeroMorphismsInstCategoryHomologicalComplex
{R : Type u_1}
[Semiring R]
{C : Type u_2}
[CategoryTheory.Category.{u_5, u_2} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear R C]
{ι : Type u_4}
{c : ComplexShape ι}
:
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Functor.mapHomologicalComplex_linear
{R : Type u_1}
[Semiring R]
{C : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_5, u_2} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Category.{u_6, u_3} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear R C]
[CategoryTheory.Linear R D]
{ι : Type u_4}
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.Additive F]
[CategoryTheory.Functor.Linear R F]
(c : ComplexShape ι)
:
Equations
- ⋯ = ⋯