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 : S.Exact
• mono_f : CategoryTheory.Mono S.f
• epi_g : CategoryTheory.Epi S.g

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

theorem CategoryTheory.ShortComplex.ShortExact.mono_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (self : S.ShortExact) : CategoryTheory.Mono S.f

theorem CategoryTheory.ShortComplex.ShortExact.epi_g {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (self : S.ShortExact) : 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 : S.Exact) : CategoryTheory.Mono S.f → CategoryTheory.Epi S.g → S.ShortExact

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 : S₁.ShortExact) : S₂.ShortExact

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₂) : S₁.ShortExact ↔ S₂.ShortExact

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 : S.ShortExact) : S.op.ShortExact

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 : S.ShortExact) : S.unop.ShortExact

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) : S.ShortExact ↔ S.op.ShortExact

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ᵒᵖ) : S.ShortExact ↔ S.unop.ShortExact

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 : S.ShortExact) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] [CategoryTheory.Mono (F.map S.f)] [CategoryTheory.Epi (F.map S.g)] : (S.map F).ShortExact

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 : S.ShortExact) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F] : (S.map F).ShortExact

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 : S.ShortExact) [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 : S.ShortExact) [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₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) [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₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) : 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 : S.ShortExact) : CategoryTheory.Limits.IsLimit (CategoryTheory.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 = let_fun this := ⋯; ⋯.fIsKernel

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 : S.ShortExact) : CategoryTheory.Limits.IsColimit (CategoryTheory.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 = let_fun this := ⋯; ⋯.gIsCokernel

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 : S.Splitting) : S.ShortExact

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 : S.ShortExact) [CategoryTheory.Injective S.X₁] [CategoryTheory.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

• 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 : S.ShortExact) [CategoryTheory.Projective S.X₃] [CategoryTheory.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 = let_fun this := ⋯; CategoryTheory.ShortComplex.Splitting.ofExactOfSection S ⋯ (CategoryTheory.Projective.factorThru (CategoryTheory.CategoryStruct.id S.X₃) S.g) ⋯ ⋯