Transport left resolutions along equivalences

If ι : C ⥤ A is equipped with Λ : LeftResolution ι and ι' : C' ⥤ A' is a functor which corresponds to ι via equivalences of categories A' ≌ A and C' ≌ C, we define Λ.transport .. : LeftResolution ι'.

def CategoryTheory.Abelian.LeftResolution.transport {A : Type u_1} {C : Type u_2} [Category.{u_5, u_2} C] [Category.{u_6, u_1} A] {A' : Type u_3} {C' : Type u_4} [Category.{u_7, u_4} C'] [Category.{u_8, u_3} A'] {ι : Functor C A} (Λ : LeftResolution ι) {ι' : Functor C' A'} (eA : A' ≌ A) (eC : C' ≌ C) (e : ι'.comp eA.functor ≅ eC.functor.comp ι) : LeftResolution ι'

Transport LeftResolution via equivalences of categories.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Abelian.LeftResolution.ofCompIso {A : Type u_1} {C : Type u_2} [Category.{u_5, u_2} C] [Category.{u_6, u_1} A] {C' : Type u_4} [Category.{u_7, u_4} C'] {ι : Functor C A} (Λ : LeftResolution ι) {ι' : Functor C' A} {G : Functor C C'} (e : G.comp ι' ≅ ι) : LeftResolution ι'

If we have an isomorphism e : G ⋙ ι' ≅ ι, then any Λ : LeftResolution ι induces Λ.ofCompIso e : LeftResolution ι'.

Equations

• One or more equations did not get rendered due to their size.