noncomputable def
tor_well_defined
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u_1}
[CategoryTheory.Category.{v_1, u_1} D]
[CategoryTheory.Abelian C]
[CategoryTheory.HasProjectiveResolutions C]
[CategoryTheory.Abelian D]
{M : C}
(P Q : CategoryTheory.ProjectiveResolution M)
(F : CategoryTheory.Functor C D)
[F.Additive]
(n : ℕ)
:
(HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).obj
((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≅ (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).obj
((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex)
Instances For
def
theorem_23_75
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u_1}
[CategoryTheory.Category.{v_1, u_1} D]
[CategoryTheory.Abelian C]
[CategoryTheory.HasProjectiveResolutions C]
[CategoryTheory.Abelian D]
{M : C}
(P Q : CategoryTheory.ProjectiveResolution M)
(F : CategoryTheory.Functor C D)
[F.Additive]
(n : ℕ)
:
(HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).obj
((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≅ (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).obj
((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex)
Alias of tor_well_defined.