Loogle!

Result

Found 49 declarations mentioning CategoryTheory.HasInjectiveResolutions.

• CategoryTheory.HasInjectiveResolutions 📋 Mathlib.CategoryTheory.Preadditive.Injective.Resolution
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] : Prop
• CategoryTheory.HasInjectiveResolutions.mk 📋 Mathlib.CategoryTheory.Preadditive.Injective.Resolution
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (out : ∀ (Z : C), CategoryTheory.HasInjectiveResolution Z) : CategoryTheory.HasInjectiveResolutions C
• CategoryTheory.HasInjectiveResolutions.out 📋 Mathlib.CategoryTheory.Preadditive.Injective.Resolution
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Limits.HasZeroObject C} {inst✝² : CategoryTheory.Limits.HasZeroMorphisms C} [self : CategoryTheory.HasInjectiveResolutions C] (Z : C) : CategoryTheory.HasInjectiveResolution Z
• CategoryTheory.InjectiveResolution.instHasInjectiveResolutions 📋 Mathlib.CategoryTheory.Abelian.Injective.Resolution
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] : CategoryTheory.HasInjectiveResolutions C
• CategoryTheory.injectiveResolutions 📋 Mathlib.CategoryTheory.Abelian.Injective.Resolution
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] : CategoryTheory.Functor C (HomotopyCategory C (ComplexShape.up ℕ))
• CategoryTheory.InjectiveResolution.iso 📋 Mathlib.CategoryTheory.Abelian.Injective.Resolution
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] {X : C} (I : CategoryTheory.InjectiveResolution X) : (CategoryTheory.injectiveResolutions C).obj X ≅ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).obj I.cocomplex
• CategoryTheory.InjectiveResolution.iso_inv_naturality 📋 Mathlib.CategoryTheory.Abelian.Injective.Resolution
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) : CategoryTheory.CategoryStruct.comp I.iso.inv ((CategoryTheory.injectiveResolutions C).map f) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ) J.iso.inv
• CategoryTheory.InjectiveResolution.iso_hom_naturality 📋 Mathlib.CategoryTheory.Abelian.Injective.Resolution
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.injectiveResolutions C).map f) J.iso.hom = CategoryTheory.CategoryStruct.comp I.iso.hom ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ)
• CategoryTheory.InjectiveResolution.iso_inv_naturality_assoc 📋 Mathlib.CategoryTheory.Abelian.Injective.Resolution
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) {Z : HomotopyCategory C (ComplexShape.up ℕ)} (h : (CategoryTheory.injectiveResolutions C).obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp I.iso.inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.injectiveResolutions C).map f) h) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ) (CategoryTheory.CategoryStruct.comp J.iso.inv h)
• CategoryTheory.InjectiveResolution.iso_hom_naturality_assoc 📋 Mathlib.CategoryTheory.Abelian.Injective.Resolution
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) {Z : HomotopyCategory C (ComplexShape.up ℕ)} (h : (HomotopyCategory.quotient C (ComplexShape.up ℕ)).obj J.cocomplex ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.injectiveResolutions C).map f) (CategoryTheory.CategoryStruct.comp J.iso.hom h) = CategoryTheory.CategoryStruct.comp I.iso.hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ) h)
• CategoryTheory.Functor.rightDerived 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) : CategoryTheory.Functor C D
• CategoryTheory.Functor.rightDerivedZeroIsoSelf 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] : F.rightDerived 0 ≅ F
• CategoryTheory.Functor.isZero_rightDerived_obj_injective_succ 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) (X : C) [CategoryTheory.Injective X] : CategoryTheory.Limits.IsZero ((F.rightDerived (n + 1)).obj X)
• CategoryTheory.Functor.toRightDerivedZero 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] : F ⟶ F.rightDerived 0
• CategoryTheory.instIsIsoFunctorToRightDerivedZero 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.IsIso F.toRightDerivedZero
• CategoryTheory.instIsIsoAppToRightDerivedZeroOfInjective 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (X : C) [CategoryTheory.Injective X] : CategoryTheory.IsIso (F.toRightDerivedZero.app X)
• CategoryTheory.instIsIsoAppToRightDerivedZero 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] (X : C) : CategoryTheory.IsIso (F.toRightDerivedZero.app X)
• CategoryTheory.NatTrans.rightDerived 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (α : F ⟶ G) (n : ℕ) : F.rightDerived n ⟶ G.rightDerived n
• CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] : F.rightDerivedZeroIsoSelf.inv = F.toRightDerivedZero
• CategoryTheory.NatTrans.rightDerived_id 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) : CategoryTheory.NatTrans.rightDerived (CategoryTheory.CategoryStruct.id F) n = CategoryTheory.CategoryStruct.id (F.rightDerived n)
• CategoryTheory.Functor.rightDerivedToHomotopyCategory 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] : CategoryTheory.Functor C (HomotopyCategory D (ComplexShape.up ℕ))
• CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.CategoryStruct.comp F.toRightDerivedZero F.rightDerivedZeroIsoSelf.hom = CategoryTheory.CategoryStruct.id F
• CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id_app 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] (X : C) : CategoryTheory.CategoryStruct.comp (F.toRightDerivedZero.app X) (F.rightDerivedZeroIsoSelf.hom.app X) = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id_assoc 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] {Z : CategoryTheory.Functor C D} (h : F ⟶ Z) : CategoryTheory.CategoryStruct.comp F.toRightDerivedZero (CategoryTheory.CategoryStruct.comp F.rightDerivedZeroIsoSelf.hom h) = h
• CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.CategoryStruct.comp F.rightDerivedZeroIsoSelf.hom F.toRightDerivedZero = CategoryTheory.CategoryStruct.id (F.rightDerived 0)
• CategoryTheory.Functor.rightDerivedZeroIsoSelf_inv_hom_id_app_assoc 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] (X : C) {Z : D} (h : F.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.toRightDerivedZero.app X) (CategoryTheory.CategoryStruct.comp (F.rightDerivedZeroIsoSelf.hom.app X) h) = h
• CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id_assoc 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] {Z : CategoryTheory.Functor C D} (h : F.rightDerived 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp F.rightDerivedZeroIsoSelf.hom (CategoryTheory.CategoryStruct.comp F.toRightDerivedZero h) = h
• CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id_app 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] (X : C) : CategoryTheory.CategoryStruct.comp (F.rightDerivedZeroIsoSelf.hom.app X) (F.toRightDerivedZero.app X) = CategoryTheory.CategoryStruct.id ((F.rightDerived 0).obj X)
• CategoryTheory.Functor.rightDerivedZeroIsoSelf_hom_inv_id_app_assoc 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] (X : C) {Z : D} (h : (F.rightDerived 0).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.rightDerivedZeroIsoSelf.hom.app X) (CategoryTheory.CategoryStruct.comp (F.toRightDerivedZero.app X) h) = h
• CategoryTheory.NatTrans.rightDerived_comp 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {F G H : CategoryTheory.Functor C D} [F.Additive] [G.Additive] [H.Additive] (α : F ⟶ G) (β : G ⟶ H) (n : ℕ) : CategoryTheory.NatTrans.rightDerived (CategoryTheory.CategoryStruct.comp α β) n = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerived α n) (CategoryTheory.NatTrans.rightDerived β n)
• CategoryTheory.NatTrans.rightDerived_comp_assoc 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions 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.rightDerived n ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerived (CategoryTheory.CategoryStruct.comp α β) n) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerived α n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerived β n) h)
• CategoryTheory.InjectiveResolution.isoRightDerivedObj 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} (I : CategoryTheory.InjectiveResolution X) (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) : (F.rightDerived n).obj X ≅ (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).obj ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex)
• CategoryTheory.NatTrans.rightDerivedToHomotopyCategory 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (α : F ⟶ G) : F.rightDerivedToHomotopyCategory ⟶ G.rightDerivedToHomotopyCategory
• CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_id 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] : CategoryTheory.NatTrans.rightDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.rightDerivedToHomotopyCategory
• CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} (I : CategoryTheory.InjectiveResolution X) (F : CategoryTheory.Functor C D) [F.Additive] : F.rightDerivedToHomotopyCategory.obj X ≅ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.up ℕ))).obj I.cocomplex
• CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) [F.Additive] [G.Additive] [H.Additive] : CategoryTheory.NatTrans.rightDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory α) (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory β)
• CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp_assoc 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions 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.up ℕ))} (h : H.rightDerivedToHomotopyCategory ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.comp α β)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory α) (CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory β) h)
• CategoryTheory.InjectiveResolution.rightDerived_app_eq 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : CategoryTheory.InjectiveResolution X) (n : ℕ) : (CategoryTheory.NatTrans.rightDerived α n).app X = CategoryTheory.CategoryStruct.comp (P.isoRightDerivedObj F n).hom (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) (P.isoRightDerivedObj G n).inv)
• CategoryTheory.Functor.rightDerived_map_eq 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) {X Y : C} (f : X ⟶ Y) {P : CategoryTheory.InjectiveResolution X} {Q : CategoryTheory.InjectiveResolution Y} (g : P.cocomplex ⟶ Q.cocomplex) (w : CategoryTheory.CategoryStruct.comp P.ι g = CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).map f) Q.ι) : (F.rightDerived n).map f = CategoryTheory.CategoryStruct.comp (P.isoRightDerivedObj F n).hom (CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).map g) (Q.isoRightDerivedObj F n).inv)
• CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) : CategoryTheory.CategoryStruct.comp ((F.rightDerived n).map f) (J.isoRightDerivedObj F n).hom = CategoryTheory.CategoryStruct.comp (I.isoRightDerivedObj F n).hom (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).map φ)
• CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) : CategoryTheory.CategoryStruct.comp (I.isoRightDerivedObj F n).inv ((F.rightDerived n).map f) = CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).map φ) (J.isoRightDerivedObj F n).inv
• CategoryTheory.InjectiveResolution.toRightDerivedZero_eq 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} (I : CategoryTheory.InjectiveResolution X) (F : CategoryTheory.Functor C D) [F.Additive] : F.toRightDerivedZero.app X = CategoryTheory.CategoryStruct.comp (I.toRightDerivedZero' F) (CategoryTheory.CategoryStruct.comp (CochainComplex.isoHomologyπ₀ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex)).hom (I.isoRightDerivedObj F 0).inv)
• CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality_assoc 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) {Z : D} (h : (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).obj ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj J.cocomplex) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.rightDerived n).map f) (CategoryTheory.CategoryStruct.comp (J.isoRightDerivedObj F n).hom h) = CategoryTheory.CategoryStruct.comp (I.isoRightDerivedObj F n).hom (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)) h)
• CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality_assoc 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) {Z : D} (h : (F.rightDerived n).obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.isoRightDerivedObj F n).inv (CategoryTheory.CategoryStruct.comp ((F.rightDerived n).map f) h) = CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)) (CategoryTheory.CategoryStruct.comp (J.isoRightDerivedObj F n).inv h)
• CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : CategoryTheory.InjectiveResolution X) : (CategoryTheory.NatTrans.rightDerivedToHomotopyCategory α).app X = CategoryTheory.CategoryStruct.comp (P.isoRightDerivedToHomotopyCategoryObj F).hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)) (P.isoRightDerivedToHomotopyCategoryObj G).inv)
• CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) (F : CategoryTheory.Functor C D) [F.Additive] : CategoryTheory.CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).inv (F.rightDerivedToHomotopyCategory.map f) = CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.up ℕ))).map φ) (J.isoRightDerivedToHomotopyCategoryObj F).inv
• CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) (F : CategoryTheory.Functor C D) [F.Additive] : CategoryTheory.CategoryStruct.comp (F.rightDerivedToHomotopyCategory.map f) (J.isoRightDerivedToHomotopyCategoryObj F).hom = CategoryTheory.CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).hom (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.up ℕ))).map φ)
• CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality_assoc 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) (F : CategoryTheory.Functor C D) [F.Additive] {Z : HomotopyCategory D (ComplexShape.up ℕ)} (h : F.rightDerivedToHomotopyCategory.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).inv (CategoryTheory.CategoryStruct.comp (F.rightDerivedToHomotopyCategory.map f) h) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)) (CategoryTheory.CategoryStruct.comp (J.isoRightDerivedToHomotopyCategoryObj F).inv h)
• CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc 📋 Mathlib.CategoryTheory.Abelian.RightDerived
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] [CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X) (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0)) (F : CategoryTheory.Functor C D) [F.Additive] {Z : HomotopyCategory D (ComplexShape.up ℕ)} (h : (HomotopyCategory.quotient D (ComplexShape.up ℕ)).obj ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj J.cocomplex) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.rightDerivedToHomotopyCategory.map f) (CategoryTheory.CategoryStruct.comp (J.isoRightDerivedToHomotopyCategoryObj F).hom h) = CategoryTheory.CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)) h)

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:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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

4. 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.

5. 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