Theorems · Theorem · category theory

CategoryTheory.JointlyReflectIsomorphisms.shortExact_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)]
      [CategoryTheory.CategoryWithHomology C] [inst_5 : ∀ (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

Defined in

Mathlib.CategoryTheory.Functor.ReflectsIso.Exact

Cited by

0 results in Mathlib

Foundations

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

Assumes

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