Loogle!

Result

Found 58 declarations mentioning CategoryTheory.HasProjectiveResolutions.

CategoryTheory.HasProjectiveResolutions 📋 Mathlib.CategoryTheory.Preadditive.Projective.Resolution
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] : Prop
CategoryTheory.HasProjectiveResolutions.mk 📋 Mathlib.CategoryTheory.Preadditive.Projective.Resolution
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (out : ∀ (Z : C), CategoryTheory.HasProjectiveResolution Z) : CategoryTheory.HasProjectiveResolutions C
CategoryTheory.HasProjectiveResolutions.out 📋 Mathlib.CategoryTheory.Preadditive.Projective.Resolution
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Limits.HasZeroObject C} {inst✝² : CategoryTheory.Limits.HasZeroMorphisms C} [self : CategoryTheory.HasProjectiveResolutions C] (Z : C) : CategoryTheory.HasProjectiveResolution Z
CategoryTheory.ProjectiveResolution.instHasProjectiveResolutions 📋 Mathlib.CategoryTheory.Abelian.Projective.Resolution
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] : CategoryTheory.HasProjectiveResolutions C
CategoryTheory.projectiveResolutions 📋 Mathlib.CategoryTheory.Abelian.Projective.Resolution
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] : CategoryTheory.Functor C (HomotopyCategory C (ComplexShape.down ℕ))
CategoryTheory.ProjectiveResolution.iso 📋 Mathlib.CategoryTheory.Abelian.Projective.Resolution
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] {X : C} (P : CategoryTheory.ProjectiveResolution X) : (CategoryTheory.projectiveResolutions C).obj X ≅ (HomotopyCategory.quotient C (ComplexShape.down ℕ)).obj P.complex
CategoryTheory.ProjectiveResolution.iso_inv_naturality 📋 Mathlib.CategoryTheory.Abelian.Projective.Resolution
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) : CategoryTheory.CategoryStruct.comp P.iso.inv ((CategoryTheory.projectiveResolutions C).map f) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ) Q.iso.inv
CategoryTheory.ProjectiveResolution.iso_hom_naturality 📋 Mathlib.CategoryTheory.Abelian.Projective.Resolution
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.projectiveResolutions C).map f) Q.iso.hom = CategoryTheory.CategoryStruct.comp P.iso.hom ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ)
CategoryTheory.ProjectiveResolution.iso_inv_naturality_assoc 📋 Mathlib.CategoryTheory.Abelian.Projective.Resolution
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) {Z : HomotopyCategory C (ComplexShape.down ℕ)} (h : (CategoryTheory.projectiveResolutions C).obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp P.iso.inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.projectiveResolutions C).map f) h) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ) (CategoryTheory.CategoryStruct.comp Q.iso.inv h)
CategoryTheory.ProjectiveResolution.iso_hom_naturality_assoc 📋 Mathlib.CategoryTheory.Abelian.Projective.Resolution
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) {Z : HomotopyCategory C (ComplexShape.down ℕ)} (h : (HomotopyCategory.quotient C (ComplexShape.down ℕ)).obj Q.complex ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.projectiveResolutions C).map f) (CategoryTheory.CategoryStruct.comp Q.iso.hom h) = CategoryTheory.CategoryStruct.comp P.iso.hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ) h)
CategoryTheory.Functor.leftDerived 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) : CategoryTheory.Functor C D
CategoryTheory.Functor.leftDerivedZeroIsoSelf 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] : F.leftDerived 0 ≅ F
CategoryTheory.Functor.isZero_leftDerived_obj_projective_succ 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) (X : C) [CategoryTheory.Projective X] : CategoryTheory.Limits.IsZero ((F.leftDerived (n + 1)).obj X)
CategoryTheory.Functor.fromLeftDerivedZero 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] : F.leftDerived 0 ⟶ F
CategoryTheory.instIsIsoFunctorFromLeftDerivedZero 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.IsIso F.fromLeftDerivedZero
CategoryTheory.instIsIsoAppFromLeftDerivedZeroOfProjective 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] (X : C) [CategoryTheory.Projective X] : CategoryTheory.IsIso (F.fromLeftDerivedZero.app X)
CategoryTheory.instIsIsoAppFromLeftDerivedZero 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) : CategoryTheory.IsIso (F.fromLeftDerivedZero.app X)
CategoryTheory.NatTrans.leftDerived 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (α : F ⟶ G) (n : ℕ) : F.leftDerived n ⟶ G.leftDerived n
CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] : F.leftDerivedZeroIsoSelf.hom = F.fromLeftDerivedZero
CategoryTheory.NatTrans.leftDerived_id 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) : CategoryTheory.NatTrans.leftDerived (CategoryTheory.CategoryStruct.id F) n = CategoryTheory.CategoryStruct.id (F.leftDerived n)
CategoryTheory.Functor.leftDerivedToHomotopyCategory 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] : CategoryTheory.Functor C (HomotopyCategory D (ComplexShape.down ℕ))
CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.CategoryStruct.comp F.leftDerivedZeroIsoSelf.inv F.fromLeftDerivedZero = CategoryTheory.CategoryStruct.id F
CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id_app 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) : CategoryTheory.CategoryStruct.comp (F.leftDerivedZeroIsoSelf.inv.app X) (F.fromLeftDerivedZero.app X) = CategoryTheory.CategoryStruct.id (F.obj X)
CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id_assoc 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] {Z : CategoryTheory.Functor C D} (h : F ⟶ Z) : CategoryTheory.CategoryStruct.comp F.leftDerivedZeroIsoSelf.inv (CategoryTheory.CategoryStruct.comp F.fromLeftDerivedZero h) = h
CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.CategoryStruct.comp F.fromLeftDerivedZero F.leftDerivedZeroIsoSelf.inv = CategoryTheory.CategoryStruct.id (F.leftDerived 0)
CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id_app_assoc 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) {Z : D} (h : F.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.leftDerivedZeroIsoSelf.inv.app X) (CategoryTheory.CategoryStruct.comp (F.fromLeftDerivedZero.app X) h) = h
CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id_assoc 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] {Z : CategoryTheory.Functor C D} (h : F.leftDerived 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp F.fromLeftDerivedZero (CategoryTheory.CategoryStruct.comp F.leftDerivedZeroIsoSelf.inv h) = h
CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id_app 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) : CategoryTheory.CategoryStruct.comp (F.fromLeftDerivedZero.app X) (F.leftDerivedZeroIsoSelf.inv.app X) = CategoryTheory.CategoryStruct.id ((F.leftDerived 0).obj X)
CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id_app_assoc 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) {Z : D} (h : (F.leftDerived 0).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.fromLeftDerivedZero.app X) (CategoryTheory.CategoryStruct.comp (F.leftDerivedZeroIsoSelf.inv.app X) h) = h
CategoryTheory.NatTrans.leftDerived_comp 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] {F G H : CategoryTheory.Functor C D} [F.Additive] [G.Additive] [H.Additive] (α : F ⟶ G) (β : G ⟶ H) (n : ℕ) : CategoryTheory.NatTrans.leftDerived (CategoryTheory.CategoryStruct.comp α β) n = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerived α n) (CategoryTheory.NatTrans.leftDerived β n)
CategoryTheory.NatTrans.leftDerived_comp_assoc 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] {F G H : CategoryTheory.Functor C D} [F.Additive] [G.Additive] [H.Additive] (α : F ⟶ G) (β : G ⟶ H) (n : ℕ) {Z : CategoryTheory.Functor C D} (h : H.leftDerived n ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerived (CategoryTheory.CategoryStruct.comp α β) n) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerived α n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerived β n) h)
CategoryTheory.ProjectiveResolution.isoLeftDerivedObj 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] {X : C} (P : CategoryTheory.ProjectiveResolution X) (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) : (F.leftDerived n).obj X ≅ (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).obj ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)
CategoryTheory.NatTrans.leftDerivedToHomotopyCategory 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (α : F ⟶ G) : F.leftDerivedToHomotopyCategory ⟶ G.leftDerivedToHomotopyCategory
CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_id 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] : CategoryTheory.NatTrans.leftDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.leftDerivedToHomotopyCategory
CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] {X : C} (P : CategoryTheory.ProjectiveResolution X) (F : CategoryTheory.Functor C D) [F.Additive] : F.leftDerivedToHomotopyCategory.obj X ≅ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.down ℕ))).obj P.complex
CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) [F.Additive] [G.Additive] [H.Additive] : CategoryTheory.NatTrans.leftDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory α) (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory β)
CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp_assoc 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) [F.Additive] [G.Additive] [H.Additive] {Z : CategoryTheory.Functor C (HomotopyCategory D (ComplexShape.down ℕ))} (h : H.leftDerivedToHomotopyCategory ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.comp α β)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory α) (CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory β) h)
CategoryTheory.ProjectiveResolution.leftDerived_app_eq 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : CategoryTheory.ProjectiveResolution X) (n : ℕ) : (CategoryTheory.NatTrans.leftDerived α n).app X = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)) (P.isoLeftDerivedObj G n).inv)
CategoryTheory.Functor.leftDerived_map_eq 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) {X Y : C} (f : X ⟶ Y) {P : CategoryTheory.ProjectiveResolution X} {Q : CategoryTheory.ProjectiveResolution Y} (g : P.complex ⟶ Q.complex) (w : CategoryTheory.CategoryStruct.comp g Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)) : (F.leftDerived n).map f = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom (CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).map g) (Q.isoLeftDerivedObj F n).inv)
CategoryTheory.ProjectiveResolution.fromLeftDerivedZero_eq 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] {X : C} (P : CategoryTheory.ProjectiveResolution X) (F : CategoryTheory.Functor C D) [F.Additive] : F.fromLeftDerivedZero.app X = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F 0).hom (CategoryTheory.CategoryStruct.comp (ChainComplex.isoHomologyι₀ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)).hom (P.fromLeftDerivedZero' F))
CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) : CategoryTheory.CategoryStruct.comp ((F.leftDerived n).map f) (Q.isoLeftDerivedObj F n).hom = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).map φ)
CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) : CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).inv ((F.leftDerived n).map f) = CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).map φ) (Q.isoLeftDerivedObj F n).inv
CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality_assoc 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) {Z : D} (h : (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).obj ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.leftDerived n).map f) (CategoryTheory.CategoryStruct.comp (Q.isoLeftDerivedObj F n).hom h) = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ)) h)
CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality_assoc 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) {Z : D} (h : (F.leftDerived n).obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).inv (CategoryTheory.CategoryStruct.comp ((F.leftDerived n).map f) h) = CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ)) (CategoryTheory.CategoryStruct.comp (Q.isoLeftDerivedObj F n).inv h)
CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : CategoryTheory.ProjectiveResolution X) : (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory α).app X = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)) (P.isoLeftDerivedToHomotopyCategoryObj G).inv)
CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [F.Additive] : CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).inv (F.leftDerivedToHomotopyCategory.map f) = CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.down ℕ))).map φ) (Q.isoLeftDerivedToHomotopyCategoryObj F).inv
CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [F.Additive] : CategoryTheory.CategoryStruct.comp (F.leftDerivedToHomotopyCategory.map f) (Q.isoLeftDerivedToHomotopyCategoryObj F).hom = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).hom (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.down ℕ))).map φ)
CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [F.Additive] {Z : HomotopyCategory D (ComplexShape.down ℕ)} (h : F.leftDerivedToHomotopyCategory.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).inv (CategoryTheory.CategoryStruct.comp (F.leftDerivedToHomotopyCategory.map f) h) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ)) (CategoryTheory.CategoryStruct.comp (Q.isoLeftDerivedToHomotopyCategoryObj F).inv h)
CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality_assoc 📋 Mathlib.CategoryTheory.Abelian.LeftDerived
{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] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [F.Additive] {Z : HomotopyCategory D (ComplexShape.down ℕ)} (h : (HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.leftDerivedToHomotopyCategory.map f) (CategoryTheory.CategoryStruct.comp (Q.isoLeftDerivedToHomotopyCategoryObj F).hom h) = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ)) h)
CategoryTheory.Tor 📋 Mathlib.CategoryTheory.Monoidal.Tor
(C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) : CategoryTheory.Functor C (CategoryTheory.Functor C C)
CategoryTheory.Tor' 📋 Mathlib.CategoryTheory.Monoidal.Tor
(C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) : CategoryTheory.Functor C (CategoryTheory.Functor C C)
CategoryTheory.isZero_Tor'_succ_of_projective 📋 Mathlib.CategoryTheory.Monoidal.Tor
(C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (X Y : C) [CategoryTheory.Projective X] (n : ℕ) : CategoryTheory.Limits.IsZero (((CategoryTheory.Tor' C (n + 1)).obj X).obj Y)
CategoryTheory.isZero_Tor_succ_of_projective 📋 Mathlib.CategoryTheory.Monoidal.Tor
(C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (X Y : C) [CategoryTheory.Projective Y] (n : ℕ) : CategoryTheory.Limits.IsZero (((CategoryTheory.Tor C (n + 1)).obj X).obj Y)
CategoryTheory.Tor_obj 📋 Mathlib.CategoryTheory.Monoidal.Tor
(C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) (X : C) : (CategoryTheory.Tor C n).obj X = ((CategoryTheory.MonoidalCategory.tensoringLeft C).obj X).leftDerived n
CategoryTheory.Tor'_obj_obj 📋 Mathlib.CategoryTheory.Monoidal.Tor
(C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) (k j : C) : ((CategoryTheory.Tor' C n).obj k).obj j = (((CategoryTheory.MonoidalCategory.tensoringRight C).obj j).leftDerived n).obj k
CategoryTheory.Tor_map 📋 Mathlib.CategoryTheory.Monoidal.Tor
(C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.Tor C n).map f = CategoryTheory.NatTrans.leftDerived ((CategoryTheory.MonoidalCategory.tensoringLeft C).map f) n
CategoryTheory.Tor'_obj_map 📋 Mathlib.CategoryTheory.Monoidal.Tor
(C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) (k : C) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Tor' C n).obj k).map f = (CategoryTheory.NatTrans.leftDerived ((CategoryTheory.MonoidalCategory.tensoringRight C).map f) n).app k
CategoryTheory.Tor'_map_app 📋 Mathlib.CategoryTheory.Monoidal.Tor
(C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.HasProjectiveResolutions C] (n : ℕ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (j : C) : ((CategoryTheory.Tor' C n).map f).app j = (((CategoryTheory.MonoidalCategory.tensoringRight C).obj j).leftDerived n).map f

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c