Short exact short complexes

A short complex S : ShortComplex C is short exact (S.ShortExact) when it is exact, S.f is a mono and S.g is an epi.

structure CategoryTheory.ShortComplex.ShortExact {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : Prop

A short complex S is short exact if it is exact, S.f is a mono and S.g is an epi.

• exact : CategoryTheory.ShortComplex.Exact S
• mono_f : CategoryTheory.Mono S.f
• epi_g : CategoryTheory.Epi S.g

theorem CategoryTheory.ShortComplex.ShortExact.mk' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.Exact S) : CategoryTheory.Mono S.f → CategoryTheory.Epi S.g → CategoryTheory.ShortComplex.ShortExact S

theorem CategoryTheory.ShortComplex.shortExact_of_iso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : CategoryTheory.ShortComplex.ShortExact S₁) : CategoryTheory.ShortComplex.ShortExact S₂

theorem CategoryTheory.ShortComplex.shortExact_iff_of_iso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) : CategoryTheory.ShortComplex.ShortExact S₁ ↔ CategoryTheory.ShortComplex.ShortExact S₂

theorem CategoryTheory.ShortComplex.ShortExact.op {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.ShortExact S) : CategoryTheory.ShortComplex.ShortExact (CategoryTheory.ShortComplex.op S)

theorem CategoryTheory.ShortComplex.ShortExact.unop {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : CategoryTheory.ShortComplex.ShortExact S) : CategoryTheory.ShortComplex.ShortExact (CategoryTheory.ShortComplex.unop S)

theorem CategoryTheory.ShortComplex.shortExact_iff_op {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.ShortComplex.ShortExact S ↔ CategoryTheory.ShortComplex.ShortExact (CategoryTheory.ShortComplex.op S)

theorem CategoryTheory.ShortComplex.shortExact_iff_unop {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex Cᵒᵖ) : CategoryTheory.ShortComplex.ShortExact S ↔ CategoryTheory.ShortComplex.ShortExact (CategoryTheory.ShortComplex.unop S)

theorem CategoryTheory.ShortComplex.ShortExact.map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.ShortExact S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesLeftHomologyOf F S] [CategoryTheory.Functor.PreservesRightHomologyOf F S] [CategoryTheory.Mono (F.toPrefunctor.map S.f)] [CategoryTheory.Epi (F.toPrefunctor.map S.g)] : CategoryTheory.ShortComplex.ShortExact (CategoryTheory.ShortComplex.map S F)

theorem CategoryTheory.ShortComplex.ShortExact.map_of_exact {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (hS : CategoryTheory.ShortComplex.ShortExact S) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.ShortComplex.ShortExact (CategoryTheory.ShortComplex.map S F)

theorem CategoryTheory.ShortComplex.ShortExact.isIso_f_iff {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : CategoryTheory.ShortComplex.ShortExact S) [CategoryTheory.Balanced C] : CategoryTheory.IsIso S.f ↔ CategoryTheory.Limits.IsZero S.X₃

theorem CategoryTheory.ShortComplex.ShortExact.isIso_g_iff {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : CategoryTheory.ShortComplex.ShortExact S) [CategoryTheory.Balanced C] : CategoryTheory.IsIso S.g ↔ CategoryTheory.Limits.IsZero S.X₁

theorem CategoryTheory.ShortComplex.isIso₂_of_shortExact_of_isIso₁₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Balanced C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.ShortExact S₁) (h₂ : CategoryTheory.ShortComplex.ShortExact S₂) [CategoryTheory.IsIso φ.τ₁] [CategoryTheory.IsIso φ.τ₃] : CategoryTheory.IsIso φ.τ₂

theorem CategoryTheory.ShortComplex.isIso₂_of_shortExact_of_isIso₁₃' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Balanced C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.ShortExact S₁) (h₂ : CategoryTheory.ShortComplex.ShortExact S₂) : CategoryTheory.IsIso φ.τ₁ → CategoryTheory.IsIso φ.τ₃ → CategoryTheory.IsIso φ.τ₂

noncomputable def CategoryTheory.ShortComplex.ShortExact.fIsKernel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Balanced C] {S : CategoryTheory.ShortComplex C} (hS : CategoryTheory.ShortComplex.ShortExact S) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))

If S is a short exact short complex in a balanced category, then S.X₁ is the kernel of S.g.

Equations

• CategoryTheory.ShortComplex.ShortExact.fIsKernel hS = let_fun this := (_ : CategoryTheory.Mono S.f); CategoryTheory.ShortComplex.Exact.fIsKernel (_ : CategoryTheory.ShortComplex.Exact S)

noncomputable def CategoryTheory.ShortComplex.ShortExact.gIsCokernel {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Balanced C] {S : CategoryTheory.ShortComplex C} (hS : CategoryTheory.ShortComplex.ShortExact S) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.g (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))

If S is a short exact short complex in a balanced category, then S.X₃ is the cokernel of S.f.

Equations

• CategoryTheory.ShortComplex.ShortExact.gIsCokernel hS = let_fun this := (_ : CategoryTheory.Epi S.g); CategoryTheory.ShortComplex.Exact.gIsCokernel (_ : CategoryTheory.ShortComplex.Exact S)

theorem CategoryTheory.ShortComplex.Splitting.shortExact {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Limits.HasZeroObject C] (s : CategoryTheory.ShortComplex.Splitting S) : CategoryTheory.ShortComplex.ShortExact S

A split short complex is short exact.

noncomputable def CategoryTheory.ShortComplex.ShortExact.splittingOfInjective {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : CategoryTheory.ShortComplex.ShortExact S) [CategoryTheory.Injective S.X₁] [CategoryTheory.Balanced C] : CategoryTheory.ShortComplex.Splitting S

A choice of splitting for a short exact short complex S in a balanced category such that S.X₁ is injective.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.ShortComplex.ShortExact.splittingOfProjective {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (hS : CategoryTheory.ShortComplex.ShortExact S) [CategoryTheory.Projective S.X₃] [CategoryTheory.Balanced C] : CategoryTheory.ShortComplex.Splitting S

A choice of splitting for a short exact short complex S in a balanced category such that S.X₃ is projective.

Equations

• One or more equations did not get rendered due to their size.