Theorems · Theorem · category theory

CategoryTheory.Functor.preservesHomology_of_preservesEpis_and_kernels

∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Abelian A] [inst_3 : CategoryTheory.Abelian B] (L : CategoryTheory.Functor A B)
  [inst_4 : L.PreservesZeroMorphisms] [L.PreservesEpimorphisms]
  [∀ {X Y : A} (f : X ⟶ Y), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) L],
  L.PreservesHomology

A functor preserving zero morphisms, epis, and kernels preserves homology.

Defined in

Mathlib.CategoryTheory.Abelian.Exact

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.AbelianCategoryTheory.Functor.PreservesZeroMorphismsCategoryTheory.Functor.PreservesEpimorphismsCategoryTheory.Limits.PreservesLimit