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} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] (S : 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 : S.Exact
• mono_f : Mono S.f
• epi_g : Epi S.g

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Equations

• hS.fIsKernel = ⋯.fIsKernel

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

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

Equations

• hS.gIsCokernel = ⋯.gIsCokernel

theorem CategoryTheory.ShortComplex.Exact.shortExact {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) (h : S.HomologyData) : { X₁ := h.left.K, X₂ := S.X₂, X₃ := h.right.Q, f := h.left.i, g := h.right.p, zero := ⋯ }.ShortExact

Is S is an exact short complex and h : S.HomologyData, there is a short exact sequence 0 ⟶ h.left.K ⟶ S.X₂ ⟶ h.right.Q ⟶ 0.

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

A split short complex is short exact.

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

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

Equations

• hS.splittingOfInjective = CategoryTheory.ShortComplex.Splitting.ofExactOfRetraction S ⋯ (CategoryTheory.Injective.factorThru (CategoryTheory.CategoryStruct.id S.X₁) S.f) ⋯ ⋯

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

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

Equations

• hS.splittingOfProjective = CategoryTheory.ShortComplex.Splitting.ofExactOfSection S ⋯ (CategoryTheory.Projective.factorThru (CategoryTheory.CategoryStruct.id S.X₃) S.g) ⋯ ⋯