Documentation

Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

The snake lemma #

The snake lemma is a standard tool in homological algebra. The basic situation is when we have a diagram as follows in an abelian category C, with exact rows:

L₁.X₁ ⟶ L₁.X₂ ⟶ L₁.X₃ ⟶ 0
|       |       |
|v₁₂.τ₁ |v₁₂.τ₂ |v₁₂.τ₃
v       v       v


0 ⟶ L₂.X₁ ⟶ L₂.X₂ ⟶ L₂.X₃

We shall think of this diagram as the datum of a morphism v₁₂ : L₁ ⟶ L₂ in the category ShortComplex C such that both L₁ and L₂ are exact, and L₁.g is epi and L₂.f is a mono (which is equivalent to saying that L₁.X₃ is the cokernel of L₁.f and L₂.X₁ is the kernel of L₂.g). Then, we may introduce the kernels and cokernels of the vertical maps. In other words, we may introduce short complexes L₀ and L₃ that are respectively the kernel and the cokernel of v₁₂. All these data constitute a SnakeInput C.

Given such a S : SnakeInput C, we define a connecting homomorphism S.δ : L₀.X₃ ⟶ L₃.X₁ and show that it is part of an exact sequence L₀.X₁ ⟶ L₀.X₂ ⟶ L₀.X₃ ⟶ L₃.X₁ ⟶ L₃.X₂ ⟶ L₃.X₃. Each of the four exactness statement is first stated separately as lemmas L₀_exact, L₁'_exact, L₂'_exact and L₃_exact and the full 6-term exact sequence is stated as snake_lemma. This sequence can even be extended with an extra 0 on the left (see mono_L₀_f) if L₁.X₁ ⟶ L₁.X₂ is a mono (i.e. L₁ is short exact), and similarly an extra 0 can be added on the right (epi_L₃_g) if L₂.X₂ ⟶ L₂.X₃ is an epi (i.e. L₂ is short exact).

These results were also obtained in the Liquid Tensor Experiment. The code and the proof here are slightly easier because of the use of the category ShortComplex C, the use of duality (which allows to construct only half of the sequence, and deducing the other half by arguing in the opposite category), and the use of "refinements" (see CategoryTheory.Abelian.Refinements) instead of a weak form of pseudo-elements.

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

A snake input in an abelian category C consists of morphisms of short complexes L₀ ⟶ L₁ ⟶ L₂ ⟶ L₃ (which should be visualized vertically) such that L₀ and L₃ are respectively the kernel and the cokernel of L₁ ⟶ L₂, L₁ and L₂ are exact, L₁.g is epi and L₂.f is mono.

Instances For
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.w₁₃_assoc {C : Type u_1} [] (self : ) {Z : } (h : self.L₃ Z) :
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.w₀₂_assoc {C : Type u_1} [] (self : ) {Z : } (h : self.L₂ Z) :
@[simp]
@[simp]
@[simp]
@[simp]
noncomputable def CategoryTheory.ShortComplex.SnakeInput.op {C : Type u_1} [] :

The snake input in the opposite category that is deduced from a snake input.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₁_assoc {C : Type u_1} [] {Z : C} (h : S.L₂.X₁ Z) :
@[simp]
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₂_assoc {C : Type u_1} [] {Z : C} (h : S.L₂.X₂ Z) :
@[simp]
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₃_assoc {C : Type u_1} [] {Z : C} (h : S.L₂.X₃ Z) :
@[simp]
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₁_assoc {C : Type u_1} [] {Z : C} (h : S.L₃.X₁ Z) :
@[simp]
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₂_assoc {C : Type u_1} [] {Z : C} (h : S.L₃.X₂ Z) :
@[simp]
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₃_assoc {C : Type u_1} [] {Z : C} (h : S.L₃.X₃ Z) :
@[simp]

L₀.X₁ is the kernel of v₁₂.τ₁ : L₁.X₁ ⟶ L₂.X₁.

Equations
Instances For

L₀.X₂ is the kernel of v₁₂.τ₂ : L₁.X₂ ⟶ L₂.X₂.

Equations
Instances For

L₀.X₃ is the kernel of v₁₂.τ₃ : L₁.X₃ ⟶ L₂.X₃.

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

The upper part of the first column of the snake diagram is exact.

The upper part of the second column of the snake diagram is exact.

The upper part of the third column of the snake diagram is exact.

L₃.X₁ is the cokernel of v₁₂.τ₁ : L₁.X₁ ⟶ L₂.X₁.

Equations
Instances For

L₃.X₂ is the cokernel of v₁₂.τ₂ : L₁.X₂ ⟶ L₂.X₂.

Equations
Instances For

L₃.X₃ is the cokernel of v₁₂.τ₃ : L₁.X₃ ⟶ L₂.X₃.

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

The lower part of the first column of the snake diagram is exact.

The lower part of the second column of the snake diagram is exact.

The lower part of the third column of the snake diagram is exact.

noncomputable def CategoryTheory.ShortComplex.SnakeInput.P {C : Type u_1} [] :
C

The fiber product of L₁.X₂ and L₀.X₃ over L₁.X₃. This is an auxiliary object in the construction of the morphism δ : L₀.X₃ ⟶ L₃.X₁.

Equations
Instances For
noncomputable def CategoryTheory.ShortComplex.SnakeInput.φ₂ {C : Type u_1} [] :

The canonical map P ⟶ L₂.X₂.

Equations
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.lift_φ₂_assoc {C : Type u_1} [] {A : C} (a : A S.L₁.X₂) (b : A S.L₀.X₃) (h : = CategoryTheory.CategoryStruct.comp b S.v₀₁.τ₃) {Z : C} (h : S.L₂.X₂ Z) :
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.lift_φ₂ {C : Type u_1} [] {A : C} (a : A S.L₁.X₂) (b : A S.L₀.X₃) (h : = CategoryTheory.CategoryStruct.comp b S.v₀₁.τ₃) :
noncomputable def CategoryTheory.ShortComplex.SnakeInput.φ₁ {C : Type u_1} [] :

The canonical map P ⟶ L₂.X₁.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f_assoc {C : Type u_1} [] {Z : C} (h : S.L₂.X₂ Z) :
@[simp]
noncomputable def CategoryTheory.ShortComplex.SnakeInput.L₀' {C : Type u_1} [] :

The short complex that is part of an exact sequence L₁.X₁ ⟶ P ⟶ L₀.X₃ ⟶ 0.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.L₁_f_φ₁_assoc {C : Type u_1} [] {Z : C} (h : S.L₂.X₁ Z) :
Equations
Equations
noncomputable def CategoryTheory.ShortComplex.SnakeInput.δ {C : Type u_1} [] :
S.L₀.X₃ S.L₃.X₁

The connecting homomorphism δ : L₀.X₃ ⟶ L₃.X₁.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.snd_δ_assoc {C : Type u_1} [] {Z : C} (h : S.L₃.X₁ Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd =
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.snd_δ {C : Type u_1} [] :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd =
noncomputable def CategoryTheory.ShortComplex.SnakeInput.P' {C : Type u_1} [] :
C

The pushout of L₂.X₂ and L₃.X₁ along L₂.X₁.

Equations
Instances For
theorem CategoryTheory.ShortComplex.SnakeInput.snd_δ_inr {C : Type u_1} [] :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp S.v₁₂.τ₂ CategoryTheory.Limits.pushout.inl)

The canonical morphism L₀.X₂ ⟶ P.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.L₁'_f {C : Type u_1} [] :
= S.L₀.g
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.L₁'_X₁ {C : Type u_1} [] :
= S.L₀.X₂
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.L₁'_X₂ {C : Type u_1} [] :
= S.L₀.X₃
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.L₁'_X₃ {C : Type u_1} [] :
= S.L₃.X₁
@[simp]
noncomputable def CategoryTheory.ShortComplex.SnakeInput.L₁' {C : Type u_1} [] :

The short complex L₀.X₂ ⟶ L₀.X₃ ⟶ L₃.X₁.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.L₂'_X₃ {C : Type u_1} [] :
= S.L₃.X₂
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.L₂'_X₂ {C : Type u_1} [] :
= S.L₃.X₁
@[simp]
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.L₂'_X₁ {C : Type u_1} [] :
= S.L₀.X₃
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.L₂'_g {C : Type u_1} [] :
= S.L₃.f
noncomputable def CategoryTheory.ShortComplex.SnakeInput.L₂' {C : Type u_1} [] :

The short complex L₀.X₃ ⟶ L₃.X₁ ⟶ L₃.X₂.

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

Exactness of L₀.X₂ ⟶ L₀.X₃ ⟶ L₃.X₁.

The duality isomorphism S.P ≅ Opposite.unop S.op.P'.

Equations
Instances For

The duality isomorphism S.P' ≅ Opposite.unop S.op.P.

Equations
Instances For

The duality isomorphism S.L₂'.op ≅ S.op.L₁'.

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

Exactness of L₀.X₃ ⟶ L₃.X₁ ⟶ L₃.X₂.

@[inline, reducible]

The diagram S.L₀.X₁ ⟶ S.L₀.X₂ ⟶ S.L₀.X₃ ⟶ S.L₃.X₁ ⟶ S.L₃.X₂ ⟶ S.L₃.X₃ for any S : SnakeInput C.

Equations
Instances For

The diagram S.L₀.X₁ ⟶ S.L₀.X₂ ⟶ S.L₀.X₃ ⟶ S.L₃.X₁ ⟶ S.L₃.X₂ ⟶ S.L₃.X₃ is exact for any S : SnakeInput C.

theorem CategoryTheory.ShortComplex.SnakeInput.δ_eq {C : Type u_1} [] {A : C} (x₃ : A S.L₀.X₃) (x₂ : A S.L₁.X₂) (x₁ : A S.L₂.X₁) (h₂ : = CategoryTheory.CategoryStruct.comp x₃ S.v₀₁.τ₃) (h₁ : = CategoryTheory.CategoryStruct.comp x₂ S.v₁₂.τ₂) :
theorem CategoryTheory.ShortComplex.SnakeInput.Hom.ext_iff {C : Type u_1} :
∀ {inst : } {inst_1 : } {S₁ S₂ : } (x y : ), x = y x.f₀ = y.f₀ x.f₁ = y.f₁ x.f₂ = y.f₂ x.f₃ = y.f₃
theorem CategoryTheory.ShortComplex.SnakeInput.Hom.ext {C : Type u_1} :
∀ {inst : } {inst_1 : } {S₁ S₂ : } (x y : ), x.f₀ = y.f₀x.f₁ = y.f₁x.f₂ = y.f₂x.f₃ = y.f₃x = y

A morphism of snake inputs involve four morphisms of short complexes which make the obvious diagram commute.

Instances For
@[simp]
@[simp]
@[simp]
@[simp]

The identity morphism of a snake input.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₂ {C : Type u_1} [] (f : ) (g : ) :
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₃ {C : Type u_1} [] (f : ) (g : ) :
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₁ {C : Type u_1} [] (f : ) (g : ) :
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₀ {C : Type u_1} [] (f : ) (g : ) :

The composition of morphisms of snake inputs.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• CategoryTheory.ShortComplex.SnakeInput.instCategorySnakeInput = CategoryTheory.Category.mk
theorem CategoryTheory.ShortComplex.SnakeInput.comp_f₀_assoc {C : Type u_1} [] (f : S₁ S₂) (g : S₂ S₃) {Z : } (h : S₃.L₀ Z) :
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.comp_f₀ {C : Type u_1} [] (f : S₁ S₂) (g : S₂ S₃) :
.f₀ =
theorem CategoryTheory.ShortComplex.SnakeInput.comp_f₁_assoc {C : Type u_1} [] (f : S₁ S₂) (g : S₂ S₃) {Z : } (h : S₃.L₁ Z) :
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.comp_f₁ {C : Type u_1} [] (f : S₁ S₂) (g : S₂ S₃) :
.f₁ =
theorem CategoryTheory.ShortComplex.SnakeInput.comp_f₂_assoc {C : Type u_1} [] (f : S₁ S₂) (g : S₂ S₃) {Z : } (h : S₃.L₂ Z) :
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.comp_f₂ {C : Type u_1} [] (f : S₁ S₂) (g : S₂ S₃) :
.f₂ =
theorem CategoryTheory.ShortComplex.SnakeInput.comp_f₃_assoc {C : Type u_1} [] (f : S₁ S₂) (g : S₂ S₃) {Z : } (h : S₃.L₃ Z) :
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.comp_f₃ {C : Type u_1} [] (f : S₁ S₂) (g : S₂ S₃) :
.f₃ =
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.functorL₉_obj {C : Type u_1} [] :
CategoryTheory.ShortComplex.SnakeInput.functorL₉.obj S = S.L₀
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.functorL₉_map {C : Type u_1} [] :
∀ {X Y : } (f : X Y), CategoryTheory.ShortComplex.SnakeInput.functorL₉.map f = f.f₀

The functor which sends S : SnakeInput C to its zeroth line S.L₀.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.functorL₁_map {C : Type u_1} [] :
∀ {X Y : } (f : X Y), CategoryTheory.ShortComplex.SnakeInput.functorL₁.map f = f.f₁
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.functorL₁_obj {C : Type u_1} [] :
CategoryTheory.ShortComplex.SnakeInput.functorL₁.obj S = S.L₁

The functor which sends S : SnakeInput C to its zeroth line S.L₁.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.functorL₂_map {C : Type u_1} [] :
∀ {X Y : } (f : X Y), CategoryTheory.ShortComplex.SnakeInput.functorL₂.map f = f.f₂
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.functorL₂_obj {C : Type u_1} [] :
CategoryTheory.ShortComplex.SnakeInput.functorL₂.obj S = S.L₂

The functor which sends S : SnakeInput C to its second line S.L₂.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.functorL₃_map {C : Type u_1} [] :
∀ {X Y : } (f : X Y), CategoryTheory.ShortComplex.SnakeInput.functorL₃.map f = f.f₃
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.functorL₃_obj {C : Type u_1} [] :
CategoryTheory.ShortComplex.SnakeInput.functorL₃.obj S = S.L₃

The functor which sends S : SnakeInput C to its third line S.L₃.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.functorP_map {C : Type u_1} [] :
∀ {X Y : } (f : X Y), CategoryTheory.ShortComplex.SnakeInput.functorP.map f = CategoryTheory.Limits.pullback.map X.L₁.g X.v₀₁.τ₃ Y.L₁.g Y.v₀₁.τ₃ f.f₁.τ₂ f.f₀.τ₃ f.f₁.τ₃ (_ : CategoryTheory.CategoryStruct.comp X.L₁.g f.f₁.τ₃ = CategoryTheory.CategoryStruct.comp f.f₁.τ₂ Y.L₁.g) (_ : (CategoryTheory.CategoryStruct.comp X.v₀₁ f.f₁).τ₃ = (CategoryTheory.CategoryStruct.comp f.f₀ Y.v₀₁).τ₃)
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.functorP_obj {C : Type u_1} [] :
CategoryTheory.ShortComplex.SnakeInput.functorP.obj S =
noncomputable def CategoryTheory.ShortComplex.SnakeInput.functorP {C : Type u_1} [] :

The functor which sends S : SnakeInput C to the auxiliary object S.P, which is pullback S.L₁.g S.v₀₁.τ₃.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.ShortComplex.SnakeInput.naturality_φ₂_assoc {C : Type u_1} [] (f : S₁ S₂) {Z : C} (h : S₂.L₂.X₂ Z) :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.SnakeInput.functorP.map f)
theorem CategoryTheory.ShortComplex.SnakeInput.naturality_φ₂ {C : Type u_1} [] (f : S₁ S₂) :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.SnakeInput.functorP.map f)
theorem CategoryTheory.ShortComplex.SnakeInput.naturality_φ₁_assoc {C : Type u_1} [] (f : S₁ S₂) {Z : C} (h : S₂.L₂.X₁ Z) :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.SnakeInput.functorP.map f)
theorem CategoryTheory.ShortComplex.SnakeInput.naturality_φ₁ {C : Type u_1} [] (f : S₁ S₂) :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.SnakeInput.functorP.map f)
theorem CategoryTheory.ShortComplex.SnakeInput.naturality_δ_assoc {C : Type u_1} [] (f : S₁ S₂) {Z : C} (h : S₂.L₃.X₁ Z) :
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₃ {C : Type u_1} [] :
∀ {X Y : } (f : X Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₁'.map f).τ₃ = f.f₃.τ₁
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.functorL₁'_obj {C : Type u_1} [] :
CategoryTheory.ShortComplex.SnakeInput.functorL₁'.obj S =
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₁ {C : Type u_1} [] :
∀ {X Y : } (f : X Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₁'.map f).τ₁ = f.f₀.τ₂
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₂ {C : Type u_1} [] :
∀ {X Y : } (f : X Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₁'.map f).τ₂ = f.f₀.τ₃

The functor which sends S : SnakeInput C to S.L₁' which is S.L₀.X₂ ⟶ S.L₀.X₃ ⟶ S.L₃.X₁.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₃ {C : Type u_1} [] :
∀ {X Y : } (f : X Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₂'.map f).τ₃ = f.f₃.τ₂
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₂ {C : Type u_1} [] :
∀ {X Y : } (f : X Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₂'.map f).τ₂ = f.f₃.τ₁
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.functorL₂'_obj {C : Type u_1} [] :
CategoryTheory.ShortComplex.SnakeInput.functorL₂'.obj S =
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₁ {C : Type u_1} [] :
∀ {X Y : } (f : X Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₂'.map f).τ₁ = f.f₀.τ₃

The functor which sends S : SnakeInput C to S.L₂' which is S.L₀.X₃ ⟶ S.L₃.X₁ ⟶ S.L₃.X₂.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor_map {C : Type u_1} [] :
∀ {X Y : } (f : X Y), CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor.map f = CategoryTheory.ComposableArrows.homMk₅ f.f₀.τ₁ f.f₀.τ₂ f.f₀.τ₃ f.f₃.τ₁ f.f₃.τ₂ f.f₃.τ₃ (_ : CategoryTheory.CategoryStruct.comp X.L₀.f f.f₀.τ₂ = CategoryTheory.CategoryStruct.comp f.f₀.τ₁ Y.L₀.f) (_ : CategoryTheory.CategoryStruct.comp X.L₀.g f.f₀.τ₃ = CategoryTheory.CategoryStruct.comp f.f₀.τ₂ Y.L₀.g) (_ : ) (_ : CategoryTheory.CategoryStruct.comp X.L₃.f f.f₃.τ₂ = CategoryTheory.CategoryStruct.comp f.f₃.τ₁ Y.L₃.f) (_ : CategoryTheory.CategoryStruct.comp X.L₃.g f.f₃.τ₃ = CategoryTheory.CategoryStruct.comp f.f₃.τ₂ Y.L₃.g)
@[simp]
theorem CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor_obj {C : Type u_1} [] :
CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor.obj S =

The functor which maps S : SnakeInput C to the diagram S.L₀.X₁ ⟶ S.L₀.X₂ ⟶ S.L₀.X₃ ⟶ S.L₃.X₁ ⟶ S.L₃.X₂ ⟶ S.L₃.X₃.

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