Theorems · Theorem · category theory

CategoryTheory.JointlyReflectIsomorphisms.quasiIsoAt_iff

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{v_2, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyReflectIsomorphisms F →
    ∀ [inst_2 : CategoryTheory.Abelian C] [inst_3 : (i : I) → CategoryTheory.Abelian (D i)]
      [inst_4 : CategoryTheory.CategoryWithHomology C]
      [inst_5 : ∀ (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

Defined in

Mathlib.CategoryTheory.Functor.ReflectsIso.Exact

Cited by

1 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.AbelianCategoryTheory.CategoryWithHomologyCategoryTheory.Limits.PreservesFiniteLimitsCategoryTheory.Limits.PreservesFiniteColimits