Loogle!

Result

Found 191 declarations mentioning CategoryTheory.Limits.PreservesFiniteColimits.

• CategoryTheory.Limits.PreservesFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Preserves.Finite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Prop
• CategoryTheory.Limits.instPreservesFiniteCoproductsOfPreservesFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Preserves.Finite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Limits.PreservesFiniteCoproducts F
• CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Preserves.Finite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimits F] : CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.Limits.PreservesColimitsOfSize.preservesFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Preserves.Finite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.Limits.PreservesColimitsOfSize0.preservesFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Preserves.Finite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.Limits.preservesColimitsOfShapeOfPreservesFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Preserves.Finite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F] (J : Type w) [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.Limits.PreservesColimitsOfShape J F
• CategoryTheory.Limits.preservesFiniteColimits_of_preservesFiniteColimitsOfSize 📋 Mathlib.CategoryTheory.Limits.Preserves.Finite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (h : ∀ (J : Type w) {𝒥 : CategoryTheory.SmallCategory J} (x : CategoryTheory.FinCategory J), CategoryTheory.Limits.PreservesColimitsOfShape J F) : CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Preserves.Finite
  {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.PreservesFiniteColimits F] (J : Type) [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.Limits.PreservesColimitsOfShape J F
• CategoryTheory.Limits.reflectsFiniteColimitsOfReflectsIsomorphisms 📋 Mathlib.CategoryTheory.Limits.Preserves.Finite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Limits.ReflectsFiniteColimits F
• CategoryTheory.Limits.PreservesFiniteColimits.mk 📋 Mathlib.CategoryTheory.Limits.Preserves.Finite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (preservesFiniteColimits : ∀ (J : Type) [inst : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J], CategoryTheory.Limits.PreservesColimitsOfShape J F := by infer_instance) : CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.Limits.preservesFiniteColimits_of_natIso 📋 Mathlib.CategoryTheory.Limits.Preserves.Finite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Limits.PreservesFiniteColimits G
• CategoryTheory.Limits.comp_preservesFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Preserves.Finite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.Limits.PreservesFiniteColimits G] : CategoryTheory.Limits.PreservesFiniteColimits (F.comp G)
• CategoryTheory.Limits.preservesFiniteColimits_of_reflects_of_preserves 📋 Mathlib.CategoryTheory.Limits.Preserves.Finite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFiniteColimits (F.comp G)] [CategoryTheory.Limits.ReflectsFiniteColimits G] : CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.RightExactFunctor.of 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F] : C ⥤ᵣ D
• CategoryTheory.rightExactFunctor_iff 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : CategoryTheory.rightExactFunctor C D F ↔ CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.ExactFunctor.of 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : C ⥤ₑ D
• CategoryTheory.exactFunctor_iff 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : CategoryTheory.exactFunctor C D F ↔ CategoryTheory.Limits.PreservesFiniteLimits F ∧ CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.instPreservesFiniteColimitsObjFunctorExactFunctor 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : C ⥤ₑ D) : CategoryTheory.Limits.PreservesFiniteColimits F.obj
• CategoryTheory.instPreservesFiniteColimitsObjFunctorRightExactFunctor 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : C ⥤ᵣ D) : CategoryTheory.Limits.PreservesFiniteColimits F.obj
• CategoryTheory.RightExactFunctor.of_fst 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F] : (CategoryTheory.RightExactFunctor.of F).obj = F
• CategoryTheory.ExactFunctor.of_fst 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : (CategoryTheory.ExactFunctor.of F).obj = F
• CategoryTheory.RightExactFunctor.forget_obj_of 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F] : (CategoryTheory.RightExactFunctor.forget C D).obj (CategoryTheory.RightExactFunctor.of F) = F
• CategoryTheory.ExactFunctor.forget_obj_of 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : (CategoryTheory.ExactFunctor.forget C D).obj (CategoryTheory.ExactFunctor.of F) = F
• CategoryTheory.Limits.preservesFiniteColimits_of_createsFiniteColimits_and_hasFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.CreatesFiniteColimits F] [CategoryTheory.Limits.HasFiniteColimits D] : CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.CostructuredArrow.hasFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Comma
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {G : CategoryTheory.Functor A T} {X : T} [CategoryTheory.Limits.HasFiniteColimits A] [CategoryTheory.Limits.PreservesFiniteColimits G] : CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.CostructuredArrow G X)
• CategoryTheory.CostructuredArrow.createsFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Comma
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {G : CategoryTheory.Functor A T} {X : T} [CategoryTheory.Limits.PreservesFiniteColimits G] : CategoryTheory.Limits.CreatesFiniteColimits (CategoryTheory.CostructuredArrow.proj G X)
• CategoryTheory.Comma.hasFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Comma
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} [CategoryTheory.Limits.HasFiniteColimits A] [CategoryTheory.Limits.HasFiniteColimits B] [CategoryTheory.Limits.PreservesFiniteColimits L] : CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.Comma L R)
• CategoryTheory.Limits.preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasCoequalizers C] [CategoryTheory.Limits.HasFiniteCoproducts C] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [CategoryTheory.Limits.PreservesFiniteCoproducts G] : CategoryTheory.Limits.PreservesFiniteColimits G
• CategoryTheory.Limits.preservesFiniteColimits_of_preservesInitial_and_pushouts 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasPushouts C] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) G] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan G] : CategoryTheory.Limits.PreservesFiniteColimits G
• FGModuleCat.instPreservesFiniteColimitsModuleCatForget₂LinearMapIdCarrierObjIsFG 📋 Mathlib.Algebra.Category.FGModuleCat.Colimits
  {k : Type u} [Ring k] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))
• CategoryTheory.Functor.preservesHomologyOfExact 📋 Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : F.PreservesHomology
• CategoryTheory.ShortComplex.instPreservesFiniteColimitsπ₁ 📋 Mathlib.Algebra.Homology.ShortComplex.Limits
  {C : Type u_2} [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.ShortComplex.π₁
• CategoryTheory.ShortComplex.instPreservesFiniteColimitsπ₂ 📋 Mathlib.Algebra.Homology.ShortComplex.Limits
  {C : Type u_2} [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.ShortComplex.π₂
• CategoryTheory.ShortComplex.instPreservesFiniteColimitsπ₃ 📋 Mathlib.Algebra.Homology.ShortComplex.Limits
  {C : Type u_2} [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.ShortComplex.π₃
• CategoryTheory.ShortComplex.ShortExact.map_of_exact 📋 Mathlib.Algebra.Homology.ShortComplex.ShortExact
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : (S.map F).ShortExact
• CategoryTheory.Functor.preservesFiniteColimits_of_preservesCokernels 📋 Mathlib.CategoryTheory.Preadditive.LeftExact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCoequalizers C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F] : CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.Functor.preservesFiniteColimits_of_preservesHomology 📋 Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] [F.PreservesHomology] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.Functor.preservesFiniteColimits_iff_forall_exact_map_and_epi 📋 Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] : CategoryTheory.Limits.PreservesFiniteColimits F ↔ ∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).Exact ∧ CategoryTheory.Epi (F.map S.g)
• CategoryTheory.Functor.exact_tfae 📋 Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] : [∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).ShortExact, ∀ (S : CategoryTheory.ShortComplex C), S.Exact → (S.map F).Exact, F.PreservesHomology, CategoryTheory.Limits.PreservesFiniteLimits F ∧ CategoryTheory.Limits.PreservesFiniteColimits F].TFAE
• CategoryTheory.Functor.preservesFiniteColimits_tfae 📋 Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] : [∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).Exact ∧ CategoryTheory.Epi (F.map S.g), ∀ (S : CategoryTheory.ShortComplex C), S.Exact ∧ CategoryTheory.Epi S.g → (S.map F).Exact ∧ CategoryTheory.Epi (F.map S.g), ∀ ⦃X Y : C⦄ (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F, CategoryTheory.Limits.PreservesFiniteColimits F].TFAE
• CategoryTheory.Limits.instPreservesFiniteColimitsFunctorObjEvaluationOfHasFiniteColimits 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Finite
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {K : Type u_2} [CategoryTheory.Category.{v_2, u_2} K] [CategoryTheory.Limits.HasFiniteColimits C] (k : K) : CategoryTheory.Limits.PreservesFiniteColimits ((CategoryTheory.evaluation K C).obj k)
• CategoryTheory.preservesFiniteColimits_of_evaluation 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [CategoryTheory.Category.{v_2, u_2} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (h : ∀ (d : D), CategoryTheory.Limits.PreservesFiniteColimits (F.comp ((CategoryTheory.evaluation D E).obj d))) : CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.instPreservesFiniteColimitsFunctorObjWhiskeringLeftOfHasFiniteColimits 📋 Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasFiniteColimits E] : CategoryTheory.Limits.PreservesFiniteColimits ((CategoryTheory.Functor.whiskeringLeft C D E).obj F)
• CategoryTheory.HasExactLimitsOfShape.mk 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  {J : Type u'} [CategoryTheory.Category.{v', u'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] (preservesFiniteColimits : CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.Limits.lim) : CategoryTheory.HasExactLimitsOfShape J C
• CategoryTheory.HasExactLimitsOfShape.preservesFiniteColimits 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  {J : Type u'} {inst✝ : CategoryTheory.Category.{v', u'} J} {C : Type u} {inst✝¹ : CategoryTheory.Category.{v, u} C} {inst✝² : CategoryTheory.Limits.HasLimitsOfShape J C} [self : CategoryTheory.HasExactLimitsOfShape J C] : CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.Limits.lim
• CategoryTheory.HasExactLimitsOfShape.domain_of_functor 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} (J : Type u_2) [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Category.{v_2, u_2} J] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasLimitsOfShape J D] [CategoryTheory.HasExactLimitsOfShape J D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.Limits.ReflectsFiniteColimits F] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesLimitsOfShape J F] : CategoryTheory.HasExactLimitsOfShape J C
• CategoryTheory.Adjunction.hasExactLimitsOfShape 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u''} [CategoryTheory.Category.{v'', u''} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Full] [F.Faithful] (J : Type u') [CategoryTheory.Category.{v', u'} J] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.HasLimitsOfShape J D] [CategoryTheory.HasExactLimitsOfShape J D] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesFiniteColimits G] : CategoryTheory.HasExactLimitsOfShape J C
• CategoryTheory.preservesFiniteColimits_liftToFinset 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
  (C : Type u) [CategoryTheory.Category.{v, u} C] {α : Type w} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α)
• CategoryTheory.CostructuredArrow.projectQuotient 📋 Mathlib.CategoryTheory.Subobject.Comma
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor C D} {T : D} [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesFiniteColimits S] {A : CategoryTheory.CostructuredArrow S T} : CategoryTheory.Subobject (Opposite.op A) → CategoryTheory.Subobject (Opposite.op A.left)
• CategoryTheory.CostructuredArrow.well_copowered_costructuredArrow 📋 Mathlib.CategoryTheory.Subobject.Comma
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor C D} {T : D} [CategoryTheory.LocallySmall.{w, v₁, u₁} C] [CategoryTheory.WellPowered.{w, v₁, u₁} Cᵒᵖ] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesFiniteColimits S] : CategoryTheory.WellPowered.{w, v₁, max u₁ v₂} (CategoryTheory.CostructuredArrow S T)ᵒᵖ
• CategoryTheory.CostructuredArrow.projectQuotient_mk 📋 Mathlib.CategoryTheory.Subobject.Comma
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor C D} {T : D} [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesFiniteColimits S] {A : CategoryTheory.CostructuredArrow S T} {P : (CategoryTheory.CostructuredArrow S T)ᵒᵖ} (f : P ⟶ Opposite.op A) [CategoryTheory.Mono f] : CategoryTheory.CostructuredArrow.projectQuotient (CategoryTheory.Subobject.mk f) = CategoryTheory.Subobject.mk f.unop.left.op
• CategoryTheory.CostructuredArrow.lift_projectQuotient 📋 Mathlib.CategoryTheory.Subobject.Comma
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor C D} {T : D} [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesFiniteColimits S] {A : CategoryTheory.CostructuredArrow S T} (P : CategoryTheory.Subobject (Opposite.op A)) {q : S.obj (Opposite.unop (CategoryTheory.Subobject.underlying.obj (CategoryTheory.CostructuredArrow.projectQuotient P))) ⟶ T} (hq : CategoryTheory.CategoryStruct.comp (S.map (CategoryTheory.CostructuredArrow.projectQuotient P).arrow.unop) q = A.hom) : CategoryTheory.CostructuredArrow.liftQuotient (CategoryTheory.CostructuredArrow.projectQuotient P) hq = P
• CategoryTheory.CostructuredArrow.projectQuotient_factors 📋 Mathlib.CategoryTheory.Subobject.Comma
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor C D} {T : D} [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesFiniteColimits S] {A : CategoryTheory.CostructuredArrow S T} (P : CategoryTheory.Subobject (Opposite.op A)) : ∃ q, CategoryTheory.CategoryStruct.comp (S.map (CategoryTheory.CostructuredArrow.projectQuotient P).arrow.unop) q = A.hom
• CategoryTheory.CostructuredArrow.quotientEquiv 📋 Mathlib.CategoryTheory.Subobject.Comma
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor C D} {T : D} [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Limits.PreservesFiniteColimits S] (A : CategoryTheory.CostructuredArrow S T) : CategoryTheory.Subobject (Opposite.op A) ≃o { P // ∃ q, CategoryTheory.CategoryStruct.comp (S.map P.arrow.unop) q = A.hom }
• CategoryTheory.ObjectProperty.instIsClosedUnderExtensionsInverseImageOfPreservesZeroMorphismsOfPreservesFiniteLimitsOfPreservesFiniteColimits 📋 Mathlib.CategoryTheory.ObjectProperty.Extensions
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasZeroMorphisms C] [P.IsClosedUnderExtensions] (F : CategoryTheory.Functor D C) [CategoryTheory.Limits.HasZeroMorphisms D] [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : (P.inverseImage F).IsClosedUnderExtensions
• CategoryTheory.ObjectProperty.instIsSerreClassInverseImageOfPreservesFiniteLimitsOfPreservesFiniteColimits 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : CategoryTheory.ObjectProperty C) {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [P.IsSerreClass] (F : CategoryTheory.Functor D C) [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : (P.inverseImage F).IsSerreClass
• instPreservesFiniteColimitsModuleCatRestrictScalars 📋 Mathlib.Algebra.Category.ModuleCat.ChangeOfRingsExact
  {R : Type u} [CommRing R] {R' : Type u'} [CommRing R'] (f : R →+* R') : CategoryTheory.Limits.PreservesFiniteColimits (ModuleCat.restrictScalars f)
• HomologicalComplex.instPreservesFiniteColimitsEvalOfHasFiniteColimits 📋 Mathlib.Algebra.Homology.HomologicalComplexLimits
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] (n : ι) : CategoryTheory.Limits.PreservesFiniteColimits (HomologicalComplex.eval C c n)
• HomologicalComplex.instPreservesFiniteColimitsSingle 📋 Mathlib.Algebra.Homology.HomologicalComplexLimits
  {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] [DecidableEq ι] (i : ι) : CategoryTheory.Limits.PreservesFiniteColimits (HomologicalComplex.single C c i)
• CategoryTheory.instPreservesFiniteColimitsHomologicalComplexMapHomologicalComplexOfHasFiniteColimits 📋 Mathlib.Algebra.Homology.HomologicalComplexAbelian
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) {ι : Type u_3} (c : ComplexShape ι) [CategoryTheory.Limits.HasFiniteColimits C] [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Limits.PreservesFiniteColimits (F.mapHomologicalComplex c)
• ModuleCat.instPreservesFiniteColimitsLocalizationLocalizedModuleFunctor 📋 Mathlib.Algebra.Category.ModuleCat.Localization
  {R : Type u} [CommRing R] [Small.{v, u} R] (S : Submonoid R) : CategoryTheory.Limits.PreservesFiniteColimits (ModuleCat.localizedModuleFunctor S)
• PresheafOfModules.Finite.toPresheaf_preservesFiniteColimits 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) : CategoryTheory.Limits.PreservesFiniteColimits (PresheafOfModules.toPresheaf R)
• PresheafOfModules.Finite.evaluation_preservesFiniteColimits 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) (X : Cᵒᵖ) : CategoryTheory.Limits.PreservesFiniteColimits (PresheafOfModules.evaluation R X)
• CategoryTheory.Limits.preservesFiniteColimits_of_op 📋 Mathlib.CategoryTheory.Limits.Preserves.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F.op] : CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.Limits.preservesFiniteColimits_op 📋 Mathlib.CategoryTheory.Limits.Preserves.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.Limits.PreservesFiniteColimits F.op
• CategoryTheory.Limits.preservesFiniteLimits_of_op 📋 Mathlib.CategoryTheory.Limits.Preserves.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F.op] : CategoryTheory.Limits.PreservesFiniteLimits F
• CategoryTheory.Limits.preservesFiniteLimits_op 📋 Mathlib.CategoryTheory.Limits.Preserves.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Limits.PreservesFiniteLimits F.op
• CategoryTheory.Limits.preservesFiniteColimits_leftOp 📋 Mathlib.CategoryTheory.Limits.Preserves.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.Limits.PreservesFiniteColimits F.leftOp
• CategoryTheory.Limits.preservesFiniteColimits_of_leftOp 📋 Mathlib.CategoryTheory.Limits.Preserves.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteLimits F.leftOp] : CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.Limits.preservesFiniteColimits_of_rightOp 📋 Mathlib.CategoryTheory.Limits.Preserves.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesFiniteLimits F.rightOp] : CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.Limits.preservesFiniteColimits_rightOp 📋 Mathlib.CategoryTheory.Limits.Preserves.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.Limits.PreservesFiniteColimits F.rightOp
• CategoryTheory.Limits.preservesFiniteLimits_leftOp 📋 Mathlib.CategoryTheory.Limits.Preserves.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Limits.PreservesFiniteLimits F.leftOp
• CategoryTheory.Limits.preservesFiniteLimits_of_leftOp 📋 Mathlib.CategoryTheory.Limits.Preserves.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteColimits F.leftOp] : CategoryTheory.Limits.PreservesFiniteLimits F
• CategoryTheory.Limits.preservesFiniteLimits_of_rightOp 📋 Mathlib.CategoryTheory.Limits.Preserves.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesFiniteColimits F.rightOp] : CategoryTheory.Limits.PreservesFiniteLimits F
• CategoryTheory.Limits.preservesFiniteLimits_rightOp 📋 Mathlib.CategoryTheory.Limits.Preserves.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Limits.PreservesFiniteLimits F.rightOp
• CategoryTheory.Limits.preservesFiniteColimits_of_unop 📋 Mathlib.CategoryTheory.Limits.Preserves.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteLimits F.unop] : CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.Limits.preservesFiniteColimits_unop 📋 Mathlib.CategoryTheory.Limits.Preserves.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.Limits.PreservesFiniteColimits F.unop
• CategoryTheory.Limits.preservesFiniteLimits_of_unop 📋 Mathlib.CategoryTheory.Limits.Preserves.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteColimits F.unop] : CategoryTheory.Limits.PreservesFiniteLimits F
• CategoryTheory.Limits.preservesFiniteLimits_unop 📋 Mathlib.CategoryTheory.Limits.Preserves.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Limits.PreservesFiniteLimits F.unop
• CategoryTheory.preservesFiniteColimits_of_coflat 📋 Mathlib.CategoryTheory.Functor.Flat
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.RepresentablyCoflat F] : CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.coflat_of_preservesFiniteColimits 📋 Mathlib.CategoryTheory.Functor.Flat
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasFiniteColimits C] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.RepresentablyCoflat F
• CategoryTheory.preservesFiniteColimits_iff_coflat 📋 Mathlib.CategoryTheory.Functor.Flat
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasFiniteColimits C] (F : CategoryTheory.Functor C D) : CategoryTheory.RepresentablyCoflat F ↔ CategoryTheory.Limits.PreservesFiniteColimits F
• ModuleCat.instPreservesFiniteColimitsUliftFunctor 📋 Mathlib.Algebra.Category.ModuleCat.Ulift
  (R : Type u) [Ring R] : CategoryTheory.Limits.PreservesFiniteColimits (ModuleCat.uliftFunctor.{v', v, u} R)
• CategoryTheory.MorphismProperty.Under.instPreservesFiniteColimitsTopUnderForget 📋 Mathlib.CategoryTheory.Limits.MorphismProperty
  {T : Type u_1} [CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T) [CategoryTheory.Limits.HasPushouts T] [P.IsStableUnderComposition] [P.ContainsIdentities] [P.IsStableUnderCobaseChange] [P.HasOfPrecompProperty P] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.MorphismProperty.Under.forget P ⊤ X)
• CategoryTheory.Functor.mapDerivedCategory 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Functor (DerivedCategory C₁) (DerivedCategory C₂)
• CategoryTheory.Functor.instCommShiftDerivedCategoryMapDerivedCategoryInt 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : F.mapDerivedCategory.CommShift ℤ
• CategoryTheory.Functor.mapDerivedCategorySingleFunctor 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (n : ℤ) : (DerivedCategory.singleFunctor C₁ n).comp F.mapDerivedCategory ≅ F.comp (DerivedCategory.singleFunctor C₂ n)
• CategoryTheory.Functor.instIsTriangulatedDerivedCategoryMapDerivedCategory 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : F.mapDerivedCategory.IsTriangulated
• CategoryTheory.Functor.instLinearDerivedCategoryMapDerivedCategory 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (R : Type u_4) [Ring R] [CategoryTheory.Linear R C₁] [CategoryTheory.Linear R C₂] [CategoryTheory.Functor.Linear R F] : CategoryTheory.Functor.Linear R F.mapDerivedCategory
• CategoryTheory.NatTrans.instCommShiftDerivedCategoryMapDerivedCategoryInt 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] {F : CategoryTheory.Functor C₁ C₂} [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {G : CategoryTheory.Functor C₁ C₂} [G.Additive] [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] (τ : F ⟶ G) : CategoryTheory.NatTrans.CommShift (CategoryTheory.NatTrans.mapDerivedCategory τ) ℤ
• CategoryTheory.NatTrans.mapDerivedCategory 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] {F : CategoryTheory.Functor C₁ C₂} [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {G : CategoryTheory.Functor C₁ C₂} [G.Additive] [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] (τ : F ⟶ G) : F.mapDerivedCategory ⟶ G.mapDerivedCategory
• CategoryTheory.Functor.mapDerivedCategoryCompIso 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] {C₃ : Type u_3} [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Abelian C₃] [HasDerivedCategory C₃] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (G : CategoryTheory.Functor C₂ C₃) [G.Additive] [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] : F.mapDerivedCategory.comp G.mapDerivedCategory ≅ (F.comp G).mapDerivedCategory
• CategoryTheory.Functor.instLiftingCochainComplexIntDerivedCategoryQQuasiIsoUpCompHomologicalComplexMapHomologicalComplexMapDerivedCategory 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Localization.Lifting DerivedCategory.Q (HomologicalComplex.quasiIso C₁ (ComplexShape.up ℤ)) ((F.mapHomologicalComplex (ComplexShape.up ℤ)).comp DerivedCategory.Q) F.mapDerivedCategory
• CategoryTheory.Functor.instCommShiftDerivedCategoryHomMapDerivedCategoryCompIsoInt 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] {C₃ : Type u_3} [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Abelian C₃] [HasDerivedCategory C₃] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (G : CategoryTheory.Functor C₂ C₃) [G.Additive] [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] : CategoryTheory.NatTrans.CommShift (F.mapDerivedCategoryCompIso G).hom ℤ
• CategoryTheory.Functor.mapDerivedCategoryFactors 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : DerivedCategory.Q.comp F.mapDerivedCategory ≅ (F.mapHomologicalComplex (ComplexShape.up ℤ)).comp DerivedCategory.Q
• CategoryTheory.Functor.instLiftingHomotopyCategoryIntUpDerivedCategoryQhQuasiIsoCompMapHomotopyCategoryMapDerivedCategory 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Localization.Lifting DerivedCategory.Qh (HomotopyCategory.quasiIso C₁ (ComplexShape.up ℤ)) ((F.mapHomotopyCategory (ComplexShape.up ℤ)).comp DerivedCategory.Qh) F.mapDerivedCategory
• CategoryTheory.Functor.instLiftingCochainComplexIntDerivedCategoryQQuasiIsoUpCompHomologicalComplexMapHomologicalComplexMapDerivedCategory_1 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] {C₃ : Type u_3} [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Abelian C₃] [HasDerivedCategory C₃] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (G : CategoryTheory.Functor C₂ C₃) [G.Additive] [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] : CategoryTheory.Localization.Lifting DerivedCategory.Q (HomologicalComplex.quasiIso C₁ (ComplexShape.up ℤ)) ((F.mapHomologicalComplex (ComplexShape.up ℤ)).comp ((G.mapHomologicalComplex (ComplexShape.up ℤ)).comp DerivedCategory.Q)) (F.mapDerivedCategory.comp G.mapDerivedCategory)
• CategoryTheory.Functor.mapDerivedCategoryFactorsh 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : DerivedCategory.Qh.comp F.mapDerivedCategory ≅ (F.mapHomotopyCategory (ComplexShape.up ℤ)).comp DerivedCategory.Qh
• CategoryTheory.Functor.instCommShiftHomologicalComplexIntUpFunctorQuasiIsoMapHomologicalComplexUpToQuasiIsoLocalizerMorphism 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)).functor.CommShift ℤ
• CategoryTheory.NatTrans.mapDerivedCategory_app_singleFunctor_obj 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] {F : CategoryTheory.Functor C₁ C₂} [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {G : CategoryTheory.Functor C₁ C₂} [G.Additive] [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] (τ : F ⟶ G) (X : C₁) (n : ℤ) : (CategoryTheory.NatTrans.mapDerivedCategory τ).app ((DerivedCategory.singleFunctor C₁ n).obj X) = CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor n).hom.app X) (CategoryTheory.CategoryStruct.comp ((DerivedCategory.singleFunctor C₂ n).map (τ.app X)) ((G.mapDerivedCategorySingleFunctor n).inv.app X))
• CategoryTheory.NatTrans.mapDerivedCategory_app_singleFunctor_obj_assoc 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] {F : CategoryTheory.Functor C₁ C₂} [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {G : CategoryTheory.Functor C₁ C₂} [G.Additive] [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] (τ : F ⟶ G) (X : C₁) (n : ℤ) {Z : DerivedCategory C₂} (h : G.mapDerivedCategory.obj ((DerivedCategory.singleFunctor C₁ n).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.NatTrans.mapDerivedCategory τ).app ((DerivedCategory.singleFunctor C₁ n).obj X)) h = CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor n).hom.app X) (CategoryTheory.CategoryStruct.comp ((DerivedCategory.singleFunctor C₂ n).map (τ.app X)) (CategoryTheory.CategoryStruct.comp ((G.mapDerivedCategorySingleFunctor n).inv.app X) h))
• CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.NatTrans.CommShift F.mapDerivedCategoryFactors.hom ℤ
• CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomIsoQQuasiIsoUpCompHomologicalComplexMapHomologicalComplexMapDerivedCategory 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.NatTrans.CommShift (CategoryTheory.Localization.Lifting.iso DerivedCategory.Q (HomologicalComplex.quasiIso C₁ (ComplexShape.up ℤ)) ((F.mapHomologicalComplex (ComplexShape.up ℤ)).comp DerivedCategory.Q) F.mapDerivedCategory).hom ℤ
• CategoryTheory.Functor.mapDerivedCategoryCompIso_hom_app_comp_mapDerivedCategorySingleFunctor_hom_app 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] {C₃ : Type u_3} [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Abelian C₃] [HasDerivedCategory C₃] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (G : CategoryTheory.Functor C₂ C₃) [G.Additive] [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] (X : C₁) (n : ℤ) : CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategoryCompIso G).hom.app ((DerivedCategory.singleFunctor C₁ n).obj X)) (((F.comp G).mapDerivedCategorySingleFunctor n).hom.app X) = CategoryTheory.CategoryStruct.comp (G.mapDerivedCategory.map ((F.mapDerivedCategorySingleFunctor n).hom.app X)) ((G.mapDerivedCategorySingleFunctor n).hom.app (F.obj X))
• CategoryTheory.Functor.mapDerivedCategorySingleFunctor_inv_app_comp_mapDerivedCategoryCompIso_inv_app 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] {C₃ : Type u_3} [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Abelian C₃] [HasDerivedCategory C₃] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (G : CategoryTheory.Functor C₂ C₃) [G.Additive] [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] (X : C₁) : CategoryTheory.CategoryStruct.comp (((F.comp G).mapDerivedCategorySingleFunctor 0).inv.app X) ((F.mapDerivedCategoryCompIso G).inv.app ((DerivedCategory.singleFunctor C₁ 0).obj X)) = CategoryTheory.CategoryStruct.comp ((G.mapDerivedCategorySingleFunctor 0).inv.app (F.obj X)) (G.mapDerivedCategory.map ((F.mapDerivedCategorySingleFunctor 0).inv.app X))
• CategoryTheory.Functor.mapDerivedCategoryCompIso_hom_app_comp_mapDerivedCategorySingleFunctor_hom_app_assoc 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] {C₃ : Type u_3} [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Abelian C₃] [HasDerivedCategory C₃] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (G : CategoryTheory.Functor C₂ C₃) [G.Additive] [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] (X : C₁) (n : ℤ) {Z : DerivedCategory C₃} (h : (DerivedCategory.singleFunctor C₃ n).obj (G.obj (F.obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategoryCompIso G).hom.app ((DerivedCategory.singleFunctor C₁ n).obj X)) (CategoryTheory.CategoryStruct.comp (((F.comp G).mapDerivedCategorySingleFunctor n).hom.app X) h) = CategoryTheory.CategoryStruct.comp (G.mapDerivedCategory.map ((F.mapDerivedCategorySingleFunctor n).hom.app X)) (CategoryTheory.CategoryStruct.comp ((G.mapDerivedCategorySingleFunctor n).hom.app (F.obj X)) h)
• CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.NatTrans.CommShift F.mapDerivedCategoryFactorsh.hom ℤ
• CategoryTheory.Functor.mapDerivedCategorySingleFunctor_inv_app_comp_mapDerivedCategoryCompIso_inv_app_assoc 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] {C₃ : Type u_3} [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Abelian C₃] [HasDerivedCategory C₃] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (G : CategoryTheory.Functor C₂ C₃) [G.Additive] [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] (X : C₁) {Z : DerivedCategory C₃} (h : G.mapDerivedCategory.obj (F.mapDerivedCategory.obj ((DerivedCategory.singleFunctor C₁ 0).obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (((F.comp G).mapDerivedCategorySingleFunctor 0).inv.app X) (CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategoryCompIso G).inv.app ((DerivedCategory.singleFunctor C₁ 0).obj X)) h) = CategoryTheory.CategoryStruct.comp ((G.mapDerivedCategorySingleFunctor 0).inv.app (F.obj X)) (CategoryTheory.CategoryStruct.comp (G.mapDerivedCategory.map ((F.mapDerivedCategorySingleFunctor 0).inv.app X)) h)
• CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomIsoQQuasiIsoUpCompHomologicalComplexMapHomologicalComplexMapDerivedCategory_1 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] {C₃ : Type u_3} [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Abelian C₃] [HasDerivedCategory C₃] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (G : CategoryTheory.Functor C₂ C₃) [G.Additive] [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] : CategoryTheory.NatTrans.CommShift (CategoryTheory.Localization.Lifting.iso DerivedCategory.Q (HomologicalComplex.quasiIso C₁ (ComplexShape.up ℤ)) ((F.mapHomologicalComplex (ComplexShape.up ℤ)).comp ((G.mapHomologicalComplex (ComplexShape.up ℤ)).comp DerivedCategory.Q)) (F.mapDerivedCategory.comp G.mapDerivedCategory)).hom ℤ
• CategoryTheory.Functor.mapDerivedCategorySingleFunctor_inv_app 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (n : ℤ) (X : C₁) : (F.mapDerivedCategorySingleFunctor n).inv.app X = CategoryTheory.CategoryStruct.comp ((DerivedCategory.singleFunctorIsoCompQ C₂ n).hom.app (F.obj X)) (CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map ((HomologicalComplex.singleMapHomologicalComplex F (ComplexShape.up ℤ) n).inv.app X)) (CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.inv.app ((CochainComplex.singleFunctor C₁ n).obj X)) (F.mapDerivedCategory.map ((DerivedCategory.singleFunctorIsoCompQ C₁ n).inv.app X))))
• CategoryTheory.Functor.mapDerivedCategorySingleFunctor_hom_app 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (n : ℤ) (X : C₁) : (F.mapDerivedCategorySingleFunctor n).hom.app X = CategoryTheory.CategoryStruct.comp (F.mapDerivedCategory.map ((DerivedCategory.singleFunctorIsoCompQ C₁ n).hom.app X)) (CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app ((CochainComplex.singleFunctor C₁ n).obj X)) (CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map ((HomologicalComplex.singleMapHomologicalComplex F (ComplexShape.up ℤ) n).hom.app X)) ((DerivedCategory.singleFunctorIsoCompQ C₂ n).inv.app (F.obj X))))
• CategoryTheory.Functor.mapDerivedCategoryFactors_inv_app_mapDerivedCategorySingleFunctor_hom_app 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C₁) : CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.inv.app ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X)) ((F.mapDerivedCategorySingleFunctor 0).hom.app X) = DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).hom.app X)
• CategoryTheory.Functor.mapDerivedCategorySingleFunctor_inv_app_mapDerivedCategoryFactors_hom_app 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C₁) : CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).inv.app X) (F.mapDerivedCategoryFactors.hom.app ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X)) = DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).inv.app X)
• CategoryTheory.NatTrans.mapDerivedCategory_app_Q_obj 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] {F : CategoryTheory.Functor C₁ C₂} [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {G : CategoryTheory.Functor C₁ C₂} [G.Additive] [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] (τ : F ⟶ G) (X : CochainComplex C₁ ℤ) : (CategoryTheory.NatTrans.mapDerivedCategory τ).app (DerivedCategory.Q.obj X) = CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app X) (CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map ((CategoryTheory.NatTrans.mapHomologicalComplex τ (ComplexShape.up ℤ)).app X)) (G.mapDerivedCategoryFactors.inv.app X))
• CategoryTheory.Functor.mapDerivedCategoryFactors_inv_app_mapDerivedCategorySingleFunctor_hom_app_assoc 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C₁) {Z : DerivedCategory C₂} (h : (DerivedCategory.singleFunctor C₂ 0).obj (F.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.inv.app ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X)) (CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).hom.app X) h) = CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).hom.app X)) h
• CategoryTheory.Functor.mapDerivedCategorySingleFunctor_inv_app_mapDerivedCategoryFactors_hom_app_assoc 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C₁) {Z : DerivedCategory C₂} (h : DerivedCategory.Q.obj ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).inv.app X) (CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X)) h) = CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).inv.app X)) h
• CategoryTheory.Functor.mapDerivedCategoryFactors_hom_naturality 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {X Y : CochainComplex C₁ ℤ} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (F.mapDerivedCategory.map (DerivedCategory.Q.map f)) (F.mapDerivedCategoryFactors.hom.app Y) = CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app X) (DerivedCategory.Q.map ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map f))
• CategoryTheory.NatTrans.mapDerivedCategory_app_Q_obj_assoc 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] {F : CategoryTheory.Functor C₁ C₂} [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {G : CategoryTheory.Functor C₁ C₂} [G.Additive] [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] (τ : F ⟶ G) (X : CochainComplex C₁ ℤ) {Z : DerivedCategory C₂} (h : G.mapDerivedCategory.obj (DerivedCategory.Q.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.NatTrans.mapDerivedCategory τ).app (DerivedCategory.Q.obj X)) h = CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app X) (CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map ((CategoryTheory.NatTrans.mapHomologicalComplex τ (ComplexShape.up ℤ)).app X)) (CategoryTheory.CategoryStruct.comp (G.mapDerivedCategoryFactors.inv.app X) h))
• CategoryTheory.Functor.mapDerivedCategoryFactors_hom_naturality_assoc 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {X Y : CochainComplex C₁ ℤ} (f : X ⟶ Y) {Z : DerivedCategory C₂} (h : DerivedCategory.Q.obj ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.mapDerivedCategory.map (DerivedCategory.Q.map f)) (CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app Y) h) = CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app X) (CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map f)) h)
• CategoryTheory.Functor.mapDerivedCategoryCompIso_hom_app_Q_obj 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] {C₃ : Type u_3} [CategoryTheory.Category.{v_3, u_3} C₃] [CategoryTheory.Abelian C₃] [HasDerivedCategory C₃] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (G : CategoryTheory.Functor C₂ C₃) [G.Additive] [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] (X : CochainComplex C₁ ℤ) : (F.mapDerivedCategoryCompIso G).hom.app (DerivedCategory.Q.obj X) = CategoryTheory.CategoryStruct.comp (G.mapDerivedCategory.map (F.mapDerivedCategoryFactors.hom.app X)) (CategoryTheory.CategoryStruct.comp (G.mapDerivedCategoryFactors.hom.app ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj X)) (CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map ((CategoryTheory.Functor.mapHomologicalComplexCompIso (CategoryTheory.Iso.refl (F.comp G)) (ComplexShape.up ℤ)).hom.app X)) ((F.comp G).mapDerivedCategoryFactors.inv.app X)))
• CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app 📋 Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
  {C₁ : Type u_1} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Abelian C₂] [HasDerivedCategory C₂] (F : CategoryTheory.Functor C₁ C₂) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] (K : CochainComplex C₁ ℤ) : F.mapDerivedCategoryFactorsh.hom.app ((HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)).obj K) = CategoryTheory.CategoryStruct.comp (F.mapDerivedCategory.map ((DerivedCategory.quotientCompQhIso C₁).hom.app K)) (CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app K) (CategoryTheory.CategoryStruct.comp ((DerivedCategory.quotientCompQhIso C₂).inv.app ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K)) (DerivedCategory.Qh.map ((F.mapHomotopyCategoryFactors (ComplexShape.up ℤ)).inv.app K))))
• CategoryTheory.Abelian.Ext.mapExactFunctor 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] {X Y : C} {n : ℕ} (f : CategoryTheory.Abelian.Ext X Y n) : CategoryTheory.Abelian.Ext (F.obj X) (F.obj Y) n
• CategoryTheory.Abelian.Ext.mapExactFunctor_mk₀ 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Abelian.Ext.mapExactFunctor F (CategoryTheory.Abelian.Ext.mk₀ f) = CategoryTheory.Abelian.Ext.mk₀ (F.map f)
• CategoryTheory.Abelian.Ext.mapExactFunctor_comp 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] {X Y Z : C} {a b : ℕ} (α : CategoryTheory.Abelian.Ext X Y a) (β : CategoryTheory.Abelian.Ext Y Z b) {c : ℕ} (h : a + b = c) : CategoryTheory.Abelian.Ext.mapExactFunctor F (α.comp β h) = (CategoryTheory.Abelian.Ext.mapExactFunctor F α).comp (CategoryTheory.Abelian.Ext.mapExactFunctor F β) h
• CategoryTheory.Functor.mapExtLinearMap 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (R : Type u_4) [Ring R] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] [CategoryTheory.Functor.Linear R F] (X Y : C) (n : ℕ) : CategoryTheory.Abelian.Ext X Y n →ₗ[R] CategoryTheory.Abelian.Ext (F.obj X) (F.obj Y) n
• CategoryTheory.Abelian.Ext.mapExactFunctor_extClass 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) : CategoryTheory.Abelian.Ext.mapExactFunctor F hS.extClass = ⋯.extClass
• CategoryTheory.Abelian.Ext.comp_mapExactFunctor 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] {E : Type u_3} [CategoryTheory.Category.{v_3, u_3} E] [CategoryTheory.Abelian E] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] [CategoryTheory.HasExt E] {X Y : C} {n : ℕ} (α : CategoryTheory.Abelian.Ext X Y n) (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.Additive] [G.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] : CategoryTheory.Abelian.Ext.mapExactFunctor (F.comp G) α = CategoryTheory.Abelian.Ext.mapExactFunctor G (CategoryTheory.Abelian.Ext.mapExactFunctor F α)
• CategoryTheory.Functor.mapExtAddHom 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (X Y : C) (n : ℕ) : CategoryTheory.Abelian.Ext X Y n →+ CategoryTheory.Abelian.Ext (F.obj X) (F.obj Y) n
• CategoryTheory.Abelian.Ext.mapExactFunctor_comp_mk₀_natTransApp 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] {X Y : C} {n : ℕ} (α : CategoryTheory.Abelian.Ext X Y n) {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] (τ : F ⟶ G) : (CategoryTheory.Abelian.Ext.mapExactFunctor F α).comp (CategoryTheory.Abelian.Ext.mk₀ (τ.app Y)) ⋯ = (CategoryTheory.Abelian.Ext.mk₀ (τ.app X)).comp (CategoryTheory.Abelian.Ext.mapExactFunctor G α) ⋯
• CategoryTheory.Abelian.Ext.mapExactFunctor_zero 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (X Y : C) (n : ℕ) : CategoryTheory.Abelian.Ext.mapExactFunctor F 0 = 0
• CategoryTheory.Abelian.Ext.mapExactFunctor_add 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (X Y : C) (n : ℕ) (f g : CategoryTheory.Abelian.Ext X Y n) : CategoryTheory.Abelian.Ext.mapExactFunctor F (f + g) = CategoryTheory.Abelian.Ext.mapExactFunctor F f + CategoryTheory.Abelian.Ext.mapExactFunctor F g
• CategoryTheory.Functor.mapExtLinearMap_coe 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (X Y : C) (n : ℕ) (R : Type u_4) [Ring R] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] [CategoryTheory.Functor.Linear R F] : ⇑(F.mapExtLinearMap R X Y n) = CategoryTheory.Abelian.Ext.mapExactFunctor F
• CategoryTheory.Functor.mapExtLinearMap_apply 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (X Y : C) (n : ℕ) (R : Type u_4) [Ring R] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] [CategoryTheory.Functor.Linear R F] (e : CategoryTheory.Abelian.Ext X Y n) : (F.mapExtLinearMap R X Y n) e = CategoryTheory.Abelian.Ext.mapExactFunctor F e
• CategoryTheory.Functor.mapExtAddHom_coe 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (X Y : C) (n : ℕ) : ⇑(F.mapExtAddHom X Y n) = CategoryTheory.Abelian.Ext.mapExactFunctor F
• CategoryTheory.Functor.mapExtAddHom_apply 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (X Y : C) (n : ℕ) (e : CategoryTheory.Abelian.Ext X Y n) : (F.mapExtAddHom X Y n) e = CategoryTheory.Abelian.Ext.mapExactFunctor F e
• CategoryTheory.Abelian.Ext.mapExactFunctor₀ 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (X Y : C) : CategoryTheory.Abelian.Ext.mapExactFunctor F = ⇑CategoryTheory.Abelian.Ext.homEquiv₀.symm ∘ F.map ∘ ⇑CategoryTheory.Abelian.Ext.homEquiv₀
• CategoryTheory.Functor.mapExactFunctor_smul 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (X Y : C) (n : ℕ) (R : Type u_4) [Ring R] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] [CategoryTheory.Functor.Linear R F] (r : R) (f : CategoryTheory.Abelian.Ext X Y n) : CategoryTheory.Abelian.Ext.mapExactFunctor F (r • f) = r • CategoryTheory.Abelian.Ext.mapExactFunctor F f
• CategoryTheory.Abelian.Ext.mapExactFunctor_hom 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [HasDerivedCategory C] [HasDerivedCategory D] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] {X Y : C} {n : ℕ} (e : CategoryTheory.Abelian.Ext X Y n) : (CategoryTheory.Abelian.Ext.mapExactFunctor F e).hom = CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).inv.app X) (CategoryTheory.CategoryStruct.comp (e.hom.map F.mapDerivedCategory) ((CategoryTheory.shiftFunctor (DerivedCategory D) ↑n).map ((F.mapDerivedCategorySingleFunctor 0).hom.app Y)))
• CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ' 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).inv.app S.X₃) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShiftedHom.map hS.singleδ F.mapDerivedCategory) ((CategoryTheory.shiftFunctor (DerivedCategory D) 1).map ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₁))) = ⋯.singleδ
• CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.ShiftedHom.map hS.singleδ F.mapDerivedCategory = CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₃) (CategoryTheory.CategoryStruct.comp ⋯.singleδ ((CategoryTheory.shiftFunctor (DerivedCategory D) 1).map ((F.mapDerivedCategorySingleFunctor 0).inv.app S.X₁)))
• CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ'_assoc 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {Z : DerivedCategory D} (h : (CategoryTheory.shiftFunctor (DerivedCategory D) 1).obj ((DerivedCategory.singleFunctor D 0).obj (F.obj S.X₁)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).inv.app S.X₃) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShiftedHom.map hS.singleδ F.mapDerivedCategory) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (DerivedCategory D) 1).map ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₁)) h)) = CategoryTheory.CategoryStruct.comp ⋯.singleδ h
• CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ_assoc 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] {Z : DerivedCategory D} (h : (CategoryTheory.shiftFunctor (DerivedCategory D) 1).obj (F.mapDerivedCategory.obj ((DerivedCategory.singleFunctor C 0).obj S.X₁)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShiftedHom.map hS.singleδ F.mapDerivedCategory) h = CategoryTheory.CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₃) (CategoryTheory.CategoryStruct.comp ⋯.singleδ (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (DerivedCategory D) 1).map ((F.mapDerivedCategorySingleFunctor 0).inv.app S.X₁)) h))
• CategoryTheory.Functor.mapExtLinearMap_toAddMonoidHom 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] (X Y : C) (n : ℕ) (R : Type u_4) [Ring R] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] [CategoryTheory.Functor.Linear R F] : ↑(F.mapExtLinearMap R X Y n) = F.mapExtAddHom X Y n
• CategoryTheory.DerivedCategory.map_triangleOfSESδ 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [HasDerivedCategory C] [HasDerivedCategory D] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact) : F.mapDerivedCategory.map (DerivedCategory.triangleOfSESδ hS) = CategoryTheory.CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app S.X₃) (CategoryTheory.CategoryStruct.comp (DerivedCategory.triangleOfSESδ ⋯) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁)) ((CategoryTheory.Functor.commShiftIso F.mapDerivedCategory 1).inv.app (DerivedCategory.Q.obj S.X₁))))
• CategoryTheory.Functor.mapExt_bijective_of_preservesInjectiveObjects 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [F.Full] [F.Faithful] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] [CategoryTheory.EnoughInjectives C] [F.PreservesInjectiveObjects] (X Y : C) (n : ℕ) : Function.Bijective ⇑(F.mapExtAddHom X Y n)
• CategoryTheory.Functor.mapExt_bijective_of_preservesProjectiveObjects 📋 Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] [F.Full] [F.Faithful] [CategoryTheory.HasExt C] [CategoryTheory.HasExt D] [CategoryTheory.EnoughProjectives C] [F.PreservesProjectiveObjects] (X Y : C) (n : ℕ) : Function.Bijective ⇑(F.mapExtAddHom X Y n)
• 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.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.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.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.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.instIsIsoFromLeftDerivedZero' 📋 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.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] {X : C} (P : CategoryTheory.ProjectiveResolution X) : CategoryTheory.IsIso (P.fromLeftDerivedZero' F)
• CategoryTheory.Sheaf.instHasExactLimitsOfShapeOfHasFiniteColimitsOfPreservesFiniteColimitsFunctorOppositeSheafToPresheaf 📋 Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
  {C : Type u} {A : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} K] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasFiniteColimits A] [CategoryTheory.Limits.HasLimitsOfShape K A] [CategoryTheory.HasExactLimitsOfShape K A] [CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.sheafToPresheaf J A)] : CategoryTheory.HasExactLimitsOfShape K (CategoryTheory.Sheaf J A)
• CategoryTheory.GrothendieckTopology.Point.instPreservesFiniteColimitsSheafSheafFiber 📋 Mathlib.CategoryTheory.Sites.Point.Skyscraper
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] : CategoryTheory.Limits.PreservesFiniteColimits Φ.sheafFiber
• CategoryTheory.preservesFiniteColimits_preadditiveCoyonedaObj_of_projective 📋 Mathlib.CategoryTheory.Abelian.Projective.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : C) [hP : CategoryTheory.Projective P] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveCoyonedaObj P)
• CategoryTheory.projective_of_preservesFiniteColimits_preadditiveCoyonedaObj 📋 Mathlib.CategoryTheory.Abelian.Projective.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : C) [hP : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveCoyonedaObj P)] : CategoryTheory.Projective P
• CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteColimits_embedding 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type v} [CategoryTheory.SmallCategory D] (F : CategoryTheory.Functor D Cᵒᵖ) [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.embedding F)
• CategoryTheory.instPreservesFiniteColimitsIndYoneda 📋 Mathlib.CategoryTheory.Limits.Indization.Category
  {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.Ind.yoneda
• CategoryTheory.Abelian.FreydMitchell.instPreservesFiniteColimitsModuleCatEmbeddingRingFunctor 📋 Mathlib.CategoryTheory.Abelian.FreydMitchell
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.Abelian.FreydMitchell.functor C)
• CategoryTheory.Abelian.freyd_mitchell 📋 Mathlib.CategoryTheory.Abelian.FreydMitchell
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : ∃ R x F, F.Full ∧ F.Faithful ∧ CategoryTheory.Limits.PreservesFiniteLimits F ∧ CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.injective_of_preservesFiniteColimits_preadditiveYonedaObj 📋 Mathlib.CategoryTheory.Abelian.Injective.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (J : C) [hP : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveYonedaObj J)] : CategoryTheory.Injective J
• CategoryTheory.preservesFiniteColimits_preadditiveYonedaObj_of_injective 📋 Mathlib.CategoryTheory.Abelian.Injective.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (J : C) [hP : CategoryTheory.Injective J] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveYonedaObj J)
• CategoryTheory.ObjectProperty.isoModSerre_isInvertedBy_iff 📋 Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : P.isoModSerre.IsInvertedBy F ↔ P ≤ F.kernel
• CategoryTheory.Abelian.isoModSerre_kernel_eq_inverseImage_isomorphisms 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (G : CategoryTheory.Functor D C) [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] : G.kernel.isoModSerre = (CategoryTheory.MorphismProperty.isomorphisms C).inverseImage G
• CategoryTheory.Abelian.isLocalization_isoModSerre_kernel_of_leftAdjoint 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] {G : CategoryTheory.Functor D C} [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] {F : CategoryTheory.Functor C D} (adj : G ⊣ F) [F.Full] [F.Faithful] : G.IsLocalization G.kernel.isoModSerre
• CategoryTheory.Abelian.isoModSerre_kernel_eq_isLocal_of_rightAdjoint 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] {G : CategoryTheory.Functor D C} [CategoryTheory.Limits.PreservesFiniteLimits G] [CategoryTheory.Limits.PreservesFiniteColimits G] {F : CategoryTheory.Functor C D} (adj : G ⊣ F) [F.Full] [F.Faithful] : G.kernel.isoModSerre = CategoryTheory.ObjectProperty.isLocal fun x => x ∈ Set.range F.obj
• CategoryTheory.ObjectProperty.SerreClassLocalization.preservesFiniteColimits 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : CategoryTheory.Limits.PreservesFiniteColimits L
• CategoryTheory.ObjectProperty.SerreClassLocalization.preservesFiniteColimits_comp_iff 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] {E : Type u''} [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.Abelian E] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] (G : CategoryTheory.Functor D E) : CategoryTheory.Limits.PreservesFiniteColimits (L.comp G) ↔ CategoryTheory.Limits.PreservesFiniteColimits G
• CategoryTheory.ShortExact.shortExact_map_iff 📋 Mathlib.CategoryTheory.Abelian.ShortExact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [F.Faithful] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.Limits.PreservesFiniteLimits F] : (S.map F).ShortExact ↔ S.ShortExact
• Action.instPreservesFiniteColimitsForgetOfHasFiniteColimits 📋 Mathlib.CategoryTheory.Action.Limits
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [Monoid G] [CategoryTheory.Limits.HasFiniteColimits V] : CategoryTheory.Limits.PreservesFiniteColimits (Action.forget V G)
• Action.Functor.instPreservesFiniteColimitsMapActionOfHasFiniteColimits 📋 Mathlib.CategoryTheory.Action.Limits
  {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] {W : Type u_3} [CategoryTheory.Category.{v_2, u_3} W] (F : CategoryTheory.Functor V W) (G : Type u_4) [Monoid G] [CategoryTheory.Limits.PreservesFiniteColimits F] [CategoryTheory.Limits.HasFiniteColimits V] : CategoryTheory.Limits.PreservesFiniteColimits (F.mapAction G)
• CategoryTheory.JointlyReflectIsomorphisms.shortExact_iff 📋 Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → CategoryTheory.Category.{v_2, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)} (hP : CategoryTheory.JointlyReflectIsomorphisms F) [CategoryTheory.Abelian C] [(i : I) → CategoryTheory.Abelian (D i)] [CategoryTheory.CategoryWithHomology C] [∀ (i : I), CategoryTheory.Limits.PreservesFiniteLimits (F i)] [∀ (i : I), CategoryTheory.Limits.PreservesFiniteColimits (F i)] (S : CategoryTheory.ShortComplex C) : S.ShortExact ↔ ∀ (i : I), (S.map (F i)).ShortExact
• CategoryTheory.JointlyReflectIsomorphisms.quasiIsoAt_iff 📋 Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → CategoryTheory.Category.{v_2, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)} (hP : CategoryTheory.JointlyReflectIsomorphisms F) [CategoryTheory.Abelian C] [(i : I) → CategoryTheory.Abelian (D i)] [CategoryTheory.CategoryWithHomology C] [∀ (i : I), CategoryTheory.Limits.PreservesFiniteLimits (F i)] [∀ (i : I), CategoryTheory.Limits.PreservesFiniteColimits (F i)] {α : Type u_4} {c : ComplexShape α} {K L : HomologicalComplex C c} (f : K ⟶ L) (a : α) : QuasiIsoAt f a ↔ ∀ (i : I), QuasiIsoAt (((F i).mapHomologicalComplex c).map f) a
• CategoryTheory.JointlyReflectIsomorphisms.quasiIso_iff 📋 Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → CategoryTheory.Category.{v_2, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)} (hP : CategoryTheory.JointlyReflectIsomorphisms F) [CategoryTheory.Abelian C] [(i : I) → CategoryTheory.Abelian (D i)] [CategoryTheory.CategoryWithHomology C] [∀ (i : I), CategoryTheory.Limits.PreservesFiniteLimits (F i)] [∀ (i : I), CategoryTheory.Limits.PreservesFiniteColimits (F i)] {α : Type u_4} {c : ComplexShape α} {K L : HomologicalComplex C c} (f : K ⟶ L) : QuasiIso f ↔ ∀ (i : I), QuasiIso (((F i).mapHomologicalComplex c).map f)
• CategoryTheory.JointlyReflectIsomorphisms.shortComplexQuasiIso_iff 📋 Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → CategoryTheory.Category.{v_2, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)} (hP : CategoryTheory.JointlyReflectIsomorphisms F) [CategoryTheory.Abelian C] [(i : I) → CategoryTheory.Abelian (D i)] [CategoryTheory.CategoryWithHomology C] [∀ (i : I), CategoryTheory.Limits.PreservesFiniteLimits (F i)] [∀ (i : I), CategoryTheory.Limits.PreservesFiniteColimits (F i)] {S₁ S₂ : CategoryTheory.ShortComplex C} (f : S₁ ⟶ S₂) : CategoryTheory.ShortComplex.QuasiIso f ↔ ∀ (i : I), CategoryTheory.ShortComplex.QuasiIso ((F i).mapShortComplex.map f)
• CategoryTheory.Limits.FintypeCat.inclusion_preservesFiniteColimits 📋 Mathlib.CategoryTheory.Limits.FintypeCat
  : CategoryTheory.Limits.PreservesFiniteColimits FintypeCat.incl
• CategoryTheory.Limits.FintypeCat.instPreservesFiniteColimitsFintypeCatForgetFunObjFinite 📋 Mathlib.CategoryTheory.Limits.FintypeCat
  : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.forget FintypeCat)
• CategoryTheory.Limits.CompleteLattice.instPreservesFiniteColimitsToFunctorToOrderHom 📋 Mathlib.CategoryTheory.Limits.Preserves.Lattice
  {α : Type u} {β : Type v} {F : Type u_1} [FunLike F α β] (f : F) [SemilatticeSup α] [OrderBot α] [SemilatticeSup β] [OrderBot β] [SupBotHomClass F α β] : CategoryTheory.Limits.PreservesFiniteColimits (↑f).toFunctor
• CategoryTheory.Limits.PreservesFiniteColimits.underPost 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.Under.post F)
• CategoryTheory.ObjectProperty.preservesFiniteColimits_iff 📋 Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_3, u_1} J] [CategoryTheory.Category.{v_4, u_2} C] (F : CategoryTheory.Functor J C) : CategoryTheory.ObjectProperty.preservesFiniteColimits F ↔ CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.ObjectProperty.IsClosedUnderFiniteColimits.instPreservesFiniteColimitsFullSubcategoryι 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteLimits
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasFiniteColimits C] [P.IsClosedUnderFiniteColimits] : CategoryTheory.Limits.PreservesFiniteColimits P.ι
• CategoryTheory.instPreservesFiniteColimitsSheafExtensiveTopologyFunctorOppositeSheafToPresheafOfPreadditiveOfHasFiniteColimits 📋 Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
  {A : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.FinitaryExtensive C] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasFiniteColimits A] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.sheafToPresheaf (CategoryTheory.extensiveTopology C) A)
• FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ 📋 Mathlib.RepresentationTheory.FDRep
  {R : Type u} {G : Type v} [CommRing R] [Monoid G] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.forget₂ (FDRep R G) (Rep.{u, u, v} R G))
• TateCohomology.preservesFiniteColimits_tateComplexFunctor 📋 Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
  {R G : Type u} [CommRing R] [Group G] [Fintype G] : CategoryTheory.Limits.PreservesFiniteColimits (tateComplexFunctor R G)

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 69fae59