# Short complexes #

This file defines the category ShortComplex C of diagrams X₁ ⟶ X₂ ⟶ X₃ such that the composition is zero.

Note: This structure ShortComplex C was first introduced in the Liquid Tensor Experiment.

structure CategoryTheory.ShortComplex (C : Type u_1) [] :
Type (max u_1 u_3)

A short complex in a category C with zero morphisms is the datum of two composable morphisms f : X₁ ⟶ X₂ and g : X₂ ⟶ X₃ such that f ≫ g = 0.

• X₁ : C

the first (left) object of a ShortComplex

• X₂ : C

the second (middle) object of a ShortComplex

• X₃ : C

the third (right) object of a ShortComplex

• f : self.X₁ self.X₂

the first morphism of a ShortComplex

• g : self.X₂ self.X₃

the second morphism of a ShortComplex

• zero : CategoryTheory.CategoryStruct.comp self.f self.g = 0

the composition of the two given morphisms is zero

Instances For
@[simp]
theorem CategoryTheory.ShortComplex.zero {C : Type u_1} [] (self : ) :

the composition of the two given morphisms is zero

@[simp]
theorem CategoryTheory.ShortComplex.zero_assoc {C : Type u_1} [] (self : ) {Z : C} (h : self.X₃ Z) :
theorem CategoryTheory.ShortComplex.Hom.ext_iff {C : Type u_1} :
∀ {inst : } {inst_1 : } {S₁ S₂ : } {x y : S₁.Hom S₂}, x = y x.τ₁ = y.τ₁ x.τ₂ = y.τ₂ x.τ₃ = y.τ₃
theorem CategoryTheory.ShortComplex.Hom.ext {C : Type u_1} :
∀ {inst : } {inst_1 : } {S₁ S₂ : } {x y : S₁.Hom S₂}, x.τ₁ = y.τ₁x.τ₂ = y.τ₂x.τ₃ = y.τ₃x = y
structure CategoryTheory.ShortComplex.Hom {C : Type u_1} [] (S₁ : ) (S₂ : ) :
Type u_3

Morphisms of short complexes are the commutative diagrams of the obvious shape.

Instances For
theorem CategoryTheory.ShortComplex.Hom.comm₁₂ {C : Type u_1} [] {S₁ : } {S₂ : } (self : S₁.Hom S₂) :

the left commutative square of a morphism in ShortComplex

theorem CategoryTheory.ShortComplex.Hom.comm₂₃ {C : Type u_1} [] {S₁ : } {S₂ : } (self : S₁.Hom S₂) :

the right commutative square of a morphism in ShortComplex

theorem CategoryTheory.ShortComplex.Hom.comm₁₂_assoc {C : Type u_1} [] {S₁ : } {S₂ : } (self : S₁.Hom S₂) {Z : C} (h : S₂.X₂ Z) :
=
theorem CategoryTheory.ShortComplex.Hom.comm₂₃_assoc {C : Type u_1} [] {S₁ : } {S₂ : } (self : S₁.Hom S₂) {Z : C} (h : S₂.X₃ Z) :
=
@[simp]
theorem CategoryTheory.ShortComplex.Hom.id_τ₃ {C : Type u_1} [] (S : ) :
@[simp]
theorem CategoryTheory.ShortComplex.Hom.id_τ₁ {C : Type u_1} [] (S : ) :
@[simp]
theorem CategoryTheory.ShortComplex.Hom.id_τ₂ {C : Type u_1} [] (S : ) :
def CategoryTheory.ShortComplex.Hom.id {C : Type u_1} [] (S : ) :
S.Hom S

The identity morphism of a short complex.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.Hom.comp_τ₂ {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } (φ₁₂ : S₁.Hom S₂) (φ₂₃ : S₂.Hom S₃) :
(φ₁₂.comp φ₂₃).τ₂ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₂ φ₂₃.τ₂
@[simp]
theorem CategoryTheory.ShortComplex.Hom.comp_τ₁ {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } (φ₁₂ : S₁.Hom S₂) (φ₂₃ : S₂.Hom S₃) :
(φ₁₂.comp φ₂₃).τ₁ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₁ φ₂₃.τ₁
@[simp]
theorem CategoryTheory.ShortComplex.Hom.comp_τ₃ {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } (φ₁₂ : S₁.Hom S₂) (φ₂₃ : S₂.Hom S₃) :
(φ₁₂.comp φ₂₃).τ₃ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₃ φ₂₃.τ₃
def CategoryTheory.ShortComplex.Hom.comp {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } (φ₁₂ : S₁.Hom S₂) (φ₂₃ : S₂.Hom S₃) :
S₁.Hom S₃

The composition of morphisms of short complexes.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• CategoryTheory.ShortComplex.instCategory =
theorem CategoryTheory.ShortComplex.hom_ext_iff {C : Type u_1} [] {S₁ : } {S₂ : } {f : S₁ S₂} {g : S₁ S₂} :
f = g f.τ₁ = g.τ₁ f.τ₂ = g.τ₂ f.τ₃ = g.τ₃
theorem CategoryTheory.ShortComplex.hom_ext {C : Type u_1} [] {S₁ : } {S₂ : } (f : S₁ S₂) (g : S₁ S₂) (h₁ : f.τ₁ = g.τ₁) (h₂ : f.τ₂ = g.τ₂) (h₃ : f.τ₃ = g.τ₃) :
f = g
@[simp]
theorem CategoryTheory.ShortComplex.homMk_τ₂ {C : Type u_1} [] {S₁ : } {S₂ : } (τ₁ : S₁.X₁ S₂.X₁) (τ₂ : S₁.X₂ S₂.X₂) (τ₃ : S₁.X₃ S₂.X₃) (comm₁₂ : ) (comm₂₃ : ) :
(CategoryTheory.ShortComplex.homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃).τ₂ = τ₂
@[simp]
theorem CategoryTheory.ShortComplex.homMk_τ₁ {C : Type u_1} [] {S₁ : } {S₂ : } (τ₁ : S₁.X₁ S₂.X₁) (τ₂ : S₁.X₂ S₂.X₂) (τ₃ : S₁.X₃ S₂.X₃) (comm₁₂ : ) (comm₂₃ : ) :
(CategoryTheory.ShortComplex.homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃).τ₁ = τ₁
@[simp]
theorem CategoryTheory.ShortComplex.homMk_τ₃ {C : Type u_1} [] {S₁ : } {S₂ : } (τ₁ : S₁.X₁ S₂.X₁) (τ₂ : S₁.X₂ S₂.X₂) (τ₃ : S₁.X₃ S₂.X₃) (comm₁₂ : ) (comm₂₃ : ) :
(CategoryTheory.ShortComplex.homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃).τ₃ = τ₃
def CategoryTheory.ShortComplex.homMk {C : Type u_1} [] {S₁ : } {S₂ : } (τ₁ : S₁.X₁ S₂.X₁) (τ₂ : S₁.X₂ S₂.X₂) (τ₃ : S₁.X₃ S₂.X₃) (comm₁₂ : ) (comm₂₃ : ) :
S₁ S₂

A constructor for morphisms in ShortComplex C when the commutativity conditions are not obvious.

Equations
• CategoryTheory.ShortComplex.homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃ = { τ₁ := τ₁, τ₂ := τ₂, τ₃ := τ₃, comm₁₂ := comm₁₂, comm₂₃ := comm₂₃ }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.id_τ₁ {C : Type u_1} [] (S : ) :
@[simp]
theorem CategoryTheory.ShortComplex.id_τ₂ {C : Type u_1} [] (S : ) :
@[simp]
theorem CategoryTheory.ShortComplex.id_τ₃ {C : Type u_1} [] (S : ) :
theorem CategoryTheory.ShortComplex.comp_τ₁_assoc {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } (φ₁₂ : S₁ S₂) (φ₂₃ : S₂ S₃) {Z : C} (h : S₃.X₁ Z) :
@[simp]
theorem CategoryTheory.ShortComplex.comp_τ₁ {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } (φ₁₂ : S₁ S₂) (φ₂₃ : S₂ S₃) :
.τ₁ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₁ φ₂₃.τ₁
theorem CategoryTheory.ShortComplex.comp_τ₂_assoc {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } (φ₁₂ : S₁ S₂) (φ₂₃ : S₂ S₃) {Z : C} (h : S₃.X₂ Z) :
@[simp]
theorem CategoryTheory.ShortComplex.comp_τ₂ {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } (φ₁₂ : S₁ S₂) (φ₂₃ : S₂ S₃) :
.τ₂ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₂ φ₂₃.τ₂
theorem CategoryTheory.ShortComplex.comp_τ₃_assoc {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } (φ₁₂ : S₁ S₂) (φ₂₃ : S₂ S₃) {Z : C} (h : S₃.X₃ Z) :
@[simp]
theorem CategoryTheory.ShortComplex.comp_τ₃ {C : Type u_1} [] {S₁ : } {S₂ : } {S₃ : } (φ₁₂ : S₁ S₂) (φ₂₃ : S₂ S₃) :
.τ₃ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₃ φ₂₃.τ₃
instance CategoryTheory.ShortComplex.instZeroHom {C : Type u_1} [] {S₁ : } {S₂ : } :
Zero (S₁ S₂)
Equations
• CategoryTheory.ShortComplex.instZeroHom = { zero := { τ₁ := 0, τ₂ := 0, τ₃ := 0, comm₁₂ := , comm₂₃ := } }
@[simp]
theorem CategoryTheory.ShortComplex.zero_τ₁ {C : Type u_1} [] (S₁ : ) (S₂ : ) :
@[simp]
theorem CategoryTheory.ShortComplex.zero_τ₂ {C : Type u_1} [] (S₁ : ) (S₂ : ) :
@[simp]
theorem CategoryTheory.ShortComplex.zero_τ₃ {C : Type u_1} [] (S₁ : ) (S₂ : ) :
Equations
• CategoryTheory.ShortComplex.instHasZeroMorphisms =
@[simp]
theorem CategoryTheory.ShortComplex.π₁_map {C : Type u_1} [] :
∀ {X Y : } (f : X Y), CategoryTheory.ShortComplex.π₁.map f = f.τ₁
@[simp]
theorem CategoryTheory.ShortComplex.π₁_obj {C : Type u_1} [] (S : ) :
CategoryTheory.ShortComplex.π₁.obj S = S.X₁

The first projection functor ShortComplex C ⥤ C.

Equations
• CategoryTheory.ShortComplex.π₁ = { obj := fun (S : ) => S.X₁, map := fun {X Y : } (f : X Y) => f.τ₁, map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.π₂_map {C : Type u_1} [] :
∀ {X Y : } (f : X Y), CategoryTheory.ShortComplex.π₂.map f = f.τ₂
@[simp]
theorem CategoryTheory.ShortComplex.π₂_obj {C : Type u_1} [] (S : ) :
CategoryTheory.ShortComplex.π₂.obj S = S.X₂

The second projection functor ShortComplex C ⥤ C.

Equations
• CategoryTheory.ShortComplex.π₂ = { obj := fun (S : ) => S.X₂, map := fun {X Y : } (f : X Y) => f.τ₂, map_id := , map_comp := }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.π₃_map {C : Type u_1} [] :
∀ {X Y : } (f : X Y), CategoryTheory.ShortComplex.π₃.map f = f.τ₃
@[simp]
theorem CategoryTheory.ShortComplex.π₃_obj {C : Type u_1} [] (S : ) :
CategoryTheory.ShortComplex.π₃.obj S = S.X₃

The third projection functor ShortComplex C ⥤ C.

Equations
• CategoryTheory.ShortComplex.π₃ = { obj := fun (S : ) => S.X₃, map := fun {X Y : } (f : X Y) => f.τ₃, map_id := , map_comp := }
Instances For
instance CategoryTheory.ShortComplex.preservesZeroMorphisms_π₁ {C : Type u_1} [] :
CategoryTheory.ShortComplex.π₁.PreservesZeroMorphisms
Equations
• =
instance CategoryTheory.ShortComplex.preservesZeroMorphisms_π₂ {C : Type u_1} [] :
CategoryTheory.ShortComplex.π₂.PreservesZeroMorphisms
Equations
• =
instance CategoryTheory.ShortComplex.preservesZeroMorphisms_π₃ {C : Type u_1} [] :
CategoryTheory.ShortComplex.π₃.PreservesZeroMorphisms
Equations
• =
instance CategoryTheory.ShortComplex.instIsIsoτ₁ {C : Type u_1} [] {S₁ : } {S₂ : } (f : S₁ S₂) :
Equations
• =
instance CategoryTheory.ShortComplex.instIsIsoτ₂ {C : Type u_1} [] {S₁ : } {S₂ : } (f : S₁ S₂) :
Equations
• =
instance CategoryTheory.ShortComplex.instIsIsoτ₃ {C : Type u_1} [] {S₁ : } {S₂ : } (f : S₁ S₂) :
Equations
• =
@[simp]
theorem CategoryTheory.ShortComplex.π₁Toπ₂_app {C : Type u_1} [] (S : ) :
CategoryTheory.ShortComplex.π₁Toπ₂.app S = S.f
def CategoryTheory.ShortComplex.π₁Toπ₂ {C : Type u_1} [] :
CategoryTheory.ShortComplex.π₁ CategoryTheory.ShortComplex.π₂

The natural transformation π₁ ⟶ π₂ induced by S.f for all S : ShortComplex C.

Equations
• CategoryTheory.ShortComplex.π₁Toπ₂ = { app := fun (S : ) => S.f, naturality := }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.π₂Toπ₃_app {C : Type u_1} [] (S : ) :
CategoryTheory.ShortComplex.π₂Toπ₃.app S = S.g
def CategoryTheory.ShortComplex.π₂Toπ₃ {C : Type u_1} [] :
CategoryTheory.ShortComplex.π₂ CategoryTheory.ShortComplex.π₃

The natural transformation π₂ ⟶ π₃ induced by S.g for all S : ShortComplex C.

Equations
• CategoryTheory.ShortComplex.π₂Toπ₃ = { app := fun (S : ) => S.g, naturality := }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.π₁Toπ₂_comp_π₂Toπ₃_assoc {C : Type u_1} [] (h : CategoryTheory.ShortComplex.π₃ Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex.π₁Toπ₂ (CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex.π₂Toπ₃ h) =
@[simp]
theorem CategoryTheory.ShortComplex.π₁Toπ₂_comp_π₂Toπ₃ {C : Type u_1} [] :
CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex.π₁Toπ₂ CategoryTheory.ShortComplex.π₂Toπ₃ = 0
@[simp]
theorem CategoryTheory.ShortComplex.map_X₂ {C : Type u_1} {D : Type u_2} [] [] (S : ) (F : ) [F.PreservesZeroMorphisms] :
(S.map F).X₂ = F.obj S.X₂
@[simp]
theorem CategoryTheory.ShortComplex.map_X₃ {C : Type u_1} {D : Type u_2} [] [] (S : ) (F : ) [F.PreservesZeroMorphisms] :
(S.map F).X₃ = F.obj S.X₃
@[simp]
theorem CategoryTheory.ShortComplex.map_g {C : Type u_1} {D : Type u_2} [] [] (S : ) (F : ) [F.PreservesZeroMorphisms] :
(S.map F).g = F.map S.g
@[simp]
theorem CategoryTheory.ShortComplex.map_f {C : Type u_1} {D : Type u_2} [] [] (S : ) (F : ) [F.PreservesZeroMorphisms] :
(S.map F).f = F.map S.f
@[simp]
theorem CategoryTheory.ShortComplex.map_X₁ {C : Type u_1} {D : Type u_2} [] [] (S : ) (F : ) [F.PreservesZeroMorphisms] :
(S.map F).X₁ = F.obj S.X₁
def CategoryTheory.ShortComplex.map {C : Type u_1} {D : Type u_2} [] [] (S : ) (F : ) [F.PreservesZeroMorphisms] :

The short complex in D obtained by applying a functor F : C ⥤ D to a short complex in C, assuming that F preserves zero morphisms.

Equations
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.mapNatTrans_τ₁ {C : Type u_1} {D : Type u_2} [] [] (S : ) {F : } {G : } [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (τ : F G) :
(S.mapNatTrans τ).τ₁ = τ.app S.X₁
@[simp]
theorem CategoryTheory.ShortComplex.mapNatTrans_τ₂ {C : Type u_1} {D : Type u_2} [] [] (S : ) {F : } {G : } [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (τ : F G) :
(S.mapNatTrans τ).τ₂ = τ.app S.X₂
@[simp]
theorem CategoryTheory.ShortComplex.mapNatTrans_τ₃ {C : Type u_1} {D : Type u_2} [] [] (S : ) {F : } {G : } [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (τ : F G) :
(S.mapNatTrans τ).τ₃ = τ.app S.X₃
def CategoryTheory.ShortComplex.mapNatTrans {C : Type u_1} {D : Type u_2} [] [] (S : ) {F : } {G : } [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (τ : F G) :
S.map F S.map G

The morphism of short complexes S.map F ⟶ S.map G induced by a natural transformation F ⟶ G.

Equations
• S.mapNatTrans τ = { τ₁ := τ.app S.X₁, τ₂ := τ.app S.X₂, τ₃ := τ.app S.X₃, comm₁₂ := , comm₂₃ := }
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.mapNatIso_hom {C : Type u_1} {D : Type u_2} [] [] (S : ) {F : } {G : } [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (τ : F G) :
(S.mapNatIso τ).hom = S.mapNatTrans τ.hom
@[simp]
theorem CategoryTheory.ShortComplex.mapNatIso_inv {C : Type u_1} {D : Type u_2} [] [] (S : ) {F : } {G : } [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (τ : F G) :
(S.mapNatIso τ).inv = S.mapNatTrans τ.inv
def CategoryTheory.ShortComplex.mapNatIso {C : Type u_1} {D : Type u_2} [] [] (S : ) {F : } {G : } [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (τ : F G) :
S.map F S.map G

The isomorphism of short complexes S.map F ≅ S.map G induced by a natural isomorphism F ≅ G.

Equations
• S.mapNatIso τ = { hom := S.mapNatTrans τ.hom, inv := S.mapNatTrans τ.inv, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem CategoryTheory.Functor.mapShortComplex_map_τ₁ {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.PreservesZeroMorphisms] :
∀ {X Y : } (φ : X Y), (F.mapShortComplex.map φ).τ₁ = F.map φ.τ₁
@[simp]
theorem CategoryTheory.Functor.mapShortComplex_map_τ₃ {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.PreservesZeroMorphisms] :
∀ {X Y : } (φ : X Y), (F.mapShortComplex.map φ).τ₃ = F.map φ.τ₃
@[simp]
theorem CategoryTheory.Functor.mapShortComplex_obj {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.PreservesZeroMorphisms] (S : ) :
F.mapShortComplex.obj S = S.map F
@[simp]
theorem CategoryTheory.Functor.mapShortComplex_map_τ₂ {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.PreservesZeroMorphisms] :
∀ {X Y : } (φ : X Y), (F.mapShortComplex.map φ).τ₂ = F.map φ.τ₂
def CategoryTheory.Functor.mapShortComplex {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.PreservesZeroMorphisms] :

The functor ShortComplex C ⥤ ShortComplex D induced by a functor C ⥤ D which preserves zero morphisms.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.isoMk_hom_τ₃ {C : Type u_1} [] {S₁ : } {S₂ : } (e₁ : S₁.X₁ S₂.X₁) (e₂ : S₁.X₂ S₂.X₂) (e₃ : S₁.X₃ S₂.X₃) (comm₁₂ : autoParam (CategoryTheory.CategoryStruct.comp e₁.hom S₂.f = CategoryTheory.CategoryStruct.comp S₁.f e₂.hom) _auto✝) (comm₂₃ : autoParam (CategoryTheory.CategoryStruct.comp e₂.hom S₂.g = CategoryTheory.CategoryStruct.comp S₁.g e₃.hom) _auto✝) :
(CategoryTheory.ShortComplex.isoMk e₁ e₂ e₃ comm₁₂ comm₂₃).hom.τ₃ = e₃.hom
@[simp]
theorem CategoryTheory.ShortComplex.isoMk_inv {C : Type u_1} [] {S₁ : } {S₂ : } (e₁ : S₁.X₁ S₂.X₁) (e₂ : S₁.X₂ S₂.X₂) (e₃ : S₁.X₃ S₂.X₃) (comm₁₂ : autoParam (CategoryTheory.CategoryStruct.comp e₁.hom S₂.f = CategoryTheory.CategoryStruct.comp S₁.f e₂.hom) _auto✝) (comm₂₃ : autoParam (CategoryTheory.CategoryStruct.comp e₂.hom S₂.g = CategoryTheory.CategoryStruct.comp S₁.g e₃.hom) _auto✝) :
(CategoryTheory.ShortComplex.isoMk e₁ e₂ e₃ comm₁₂ comm₂₃).inv = CategoryTheory.ShortComplex.homMk e₁.inv e₂.inv e₃.inv
@[simp]
theorem CategoryTheory.ShortComplex.isoMk_hom_τ₂ {C : Type u_1} [] {S₁ : } {S₂ : } (e₁ : S₁.X₁ S₂.X₁) (e₂ : S₁.X₂ S₂.X₂) (e₃ : S₁.X₃ S₂.X₃) (comm₁₂ : autoParam (CategoryTheory.CategoryStruct.comp e₁.hom S₂.f = CategoryTheory.CategoryStruct.comp S₁.f e₂.hom) _auto✝) (comm₂₃ : autoParam (CategoryTheory.CategoryStruct.comp e₂.hom S₂.g = CategoryTheory.CategoryStruct.comp S₁.g e₃.hom) _auto✝) :
(CategoryTheory.ShortComplex.isoMk e₁ e₂ e₃ comm₁₂ comm₂₃).hom.τ₂ = e₂.hom
@[simp]
theorem CategoryTheory.ShortComplex.isoMk_hom_τ₁ {C : Type u_1} [] {S₁ : } {S₂ : } (e₁ : S₁.X₁ S₂.X₁) (e₂ : S₁.X₂ S₂.X₂) (e₃ : S₁.X₃ S₂.X₃) (comm₁₂ : autoParam (CategoryTheory.CategoryStruct.comp e₁.hom S₂.f = CategoryTheory.CategoryStruct.comp S₁.f e₂.hom) _auto✝) (comm₂₃ : autoParam (CategoryTheory.CategoryStruct.comp e₂.hom S₂.g = CategoryTheory.CategoryStruct.comp S₁.g e₃.hom) _auto✝) :
(CategoryTheory.ShortComplex.isoMk e₁ e₂ e₃ comm₁₂ comm₂₃).hom.τ₁ = e₁.hom
def CategoryTheory.ShortComplex.isoMk {C : Type u_1} [] {S₁ : } {S₂ : } (e₁ : S₁.X₁ S₂.X₁) (e₂ : S₁.X₂ S₂.X₂) (e₃ : S₁.X₃ S₂.X₃) (comm₁₂ : autoParam (CategoryTheory.CategoryStruct.comp e₁.hom S₂.f = CategoryTheory.CategoryStruct.comp S₁.f e₂.hom) _auto✝) (comm₂₃ : autoParam (CategoryTheory.CategoryStruct.comp e₂.hom S₂.g = CategoryTheory.CategoryStruct.comp S₁.g e₃.hom) _auto✝) :
S₁ S₂

A constructor for isomorphisms in the category ShortComplex C

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.ShortComplex.isIso_of_isIso {C : Type u_1} [] {S₁ : } {S₂ : } (f : S₁ S₂) [] [] [] :
@[simp]
theorem CategoryTheory.ShortComplex.op_X₁ {C : Type u_1} [] (S : ) :
S.op.X₁ = Opposite.op S.X₃
@[simp]
theorem CategoryTheory.ShortComplex.op_g {C : Type u_1} [] (S : ) :
S.op.g = S.f.op
@[simp]
theorem CategoryTheory.ShortComplex.op_X₂ {C : Type u_1} [] (S : ) :
S.op.X₂ = Opposite.op S.X₂
@[simp]
theorem CategoryTheory.ShortComplex.op_f {C : Type u_1} [] (S : ) :
S.op.f = S.g.op
@[simp]
theorem CategoryTheory.ShortComplex.op_X₃ {C : Type u_1} [] (S : ) :
S.op.X₃ = Opposite.op S.X₁

The opposite ShortComplex in Cᵒᵖ associated to a short complex in C.

Equations
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.opMap_τ₂ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) :
= φ.τ₂.op
@[simp]
theorem CategoryTheory.ShortComplex.opMap_τ₁ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) :
= φ.τ₃.op
@[simp]
theorem CategoryTheory.ShortComplex.opMap_τ₃ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) :
= φ.τ₁.op
def CategoryTheory.ShortComplex.opMap {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) :
S₂.op S₁.op

The opposite morphism in ShortComplex Cᵒᵖ associated to a morphism in ShortComplex C

Equations
• = { τ₁ := φ.τ₃.op, τ₂ := φ.τ₂.op, τ₃ := φ.τ₁.op, comm₁₂ := , comm₂₃ := }
Instances For
@[simp]
@[simp]
theorem CategoryTheory.ShortComplex.unop_X₁ {C : Type u_1} [] :
S.unop.X₁ = Opposite.unop S.X₃
@[simp]
theorem CategoryTheory.ShortComplex.unop_X₃ {C : Type u_1} [] :
S.unop.X₃ = Opposite.unop S.X₁
@[simp]
theorem CategoryTheory.ShortComplex.unop_f {C : Type u_1} [] :
S.unop.f = S.g.unop
@[simp]
theorem CategoryTheory.ShortComplex.unop_X₂ {C : Type u_1} [] :
S.unop.X₂ = Opposite.unop S.X₂
@[simp]
theorem CategoryTheory.ShortComplex.unop_g {C : Type u_1} [] :
S.unop.g = S.f.unop

The ShortComplex in C associated to a short complex in Cᵒᵖ.

Equations
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.unopMap_τ₃ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) :
= φ.τ₁.unop
@[simp]
theorem CategoryTheory.ShortComplex.unopMap_τ₂ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) :
= φ.τ₂.unop
@[simp]
theorem CategoryTheory.ShortComplex.unopMap_τ₁ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) :
= φ.τ₃.unop
def CategoryTheory.ShortComplex.unopMap {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) :
S₂.unop S₁.unop

The morphism in ShortComplex C associated to a morphism in ShortComplex Cᵒᵖ

Equations
• = { τ₁ := φ.τ₃.unop, τ₂ := φ.τ₂.unop, τ₃ := φ.τ₁.unop, comm₁₂ := , comm₂₃ := }
Instances For
@[simp]
@[simp]
theorem CategoryTheory.ShortComplex.opFunctor_map (C : Type u_1) [] :
∀ {X Y : } (φ : X Y),
@[simp]
theorem CategoryTheory.ShortComplex.opFunctor_obj (C : Type u_1) [] (S : ) :
= .op

The obvious functor (ShortComplex C)ᵒᵖ ⥤ ShortComplex Cᵒᵖ.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.unopFunctor_map (C : Type u_1) [] :
∀ {X Y : } (φ : X Y),

The obvious functor ShortComplex Cᵒᵖ ⥤ (ShortComplex C)ᵒᵖ.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
@[simp]

The obvious equivalence of categories (ShortComplex C)ᵒᵖ ≌ ShortComplex Cᵒᵖ.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev CategoryTheory.ShortComplex.unopOp {C : Type u_1} [] :
S.unop.op S

The canonical isomorphism S.unop.op ≅ S for a short complex S in Cᵒᵖ

Equations
• S.unopOp = .counitIso.app S
Instances For
@[reducible, inline]
abbrev CategoryTheory.ShortComplex.opUnop {C : Type u_1} [] (S : ) :
S.op.unop S

The canonical isomorphism S.op.unop ≅ S for a short complex S

Equations
Instances For