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) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : 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.

• L₀ : CategoryTheory.ShortComplex C

  the zeroth row

• L₁ : CategoryTheory.ShortComplex C

  the first row

• L₂ : CategoryTheory.ShortComplex C

  the second row

• L₃ : CategoryTheory.ShortComplex C

  the third row

• v₀₁ : self.L₀ ⟶ self.L₁

  the morphism from the zeroth row to the first row

• v₁₂ : self.L₁ ⟶ self.L₂

  the morphism from the first row to the second row

• v₂₃ : self.L₂ ⟶ self.L₃

  the morphism from the second row to the third row

• w₀₂ : CategoryTheory.CategoryStruct.comp self.v₀₁ self.v₁₂ = 0
• w₁₃ : CategoryTheory.CategoryStruct.comp self.v₁₂ self.v₂₃ = 0
• h₀ : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι self.v₀₁ ⋯)

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

• h₃ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ self.v₂₃ ⋯)

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

• L₁_exact : self.L₁.Exact
• epi_L₁_g : CategoryTheory.Epi self.L₁.g
• L₂_exact : self.L₂.Exact
• mono_L₂_f : CategoryTheory.Mono self.L₂.f

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.w₀₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (self : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.CategoryStruct.comp self.v₀₁ self.v₁₂ = 0

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.w₁₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (self : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.CategoryStruct.comp self.v₁₂ self.v₂₃ = 0

theorem CategoryTheory.ShortComplex.SnakeInput.L₁_exact {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (self : CategoryTheory.ShortComplex.SnakeInput C) : self.L₁.Exact

theorem CategoryTheory.ShortComplex.SnakeInput.epi_L₁_g {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (self : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.Epi self.L₁.g

theorem CategoryTheory.ShortComplex.SnakeInput.L₂_exact {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (self : CategoryTheory.ShortComplex.SnakeInput C) : self.L₂.Exact

theorem CategoryTheory.ShortComplex.SnakeInput.mono_L₂_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (self : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.Mono self.L₂.f

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.w₁₃_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (self : CategoryTheory.ShortComplex.SnakeInput C) {Z : CategoryTheory.ShortComplex C} (h : self.L₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp self.v₁₂ (CategoryTheory.CategoryStruct.comp self.v₂₃ h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.w₀₂_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (self : CategoryTheory.ShortComplex.SnakeInput C) {Z : CategoryTheory.ShortComplex C} (h : self.L₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp self.v₀₁ (CategoryTheory.CategoryStruct.comp self.v₁₂ h) = CategoryTheory.CategoryStruct.comp 0 h

noncomputable def CategoryTheory.ShortComplex.SnakeInput.op {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.ShortComplex.SnakeInput Cᵒᵖ

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.

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.op_v₁₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.op.v₁₂ = CategoryTheory.ShortComplex.opMap S.v₁₂

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.op_v₀₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.op.v₀₁ = CategoryTheory.ShortComplex.opMap S.v₂₃

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.op_L₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.op.L₀ = S.L₃.op

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.op_L₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.op.L₃ = S.L₀.op

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.op_v₂₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.op.v₂₃ = CategoryTheory.ShortComplex.opMap S.v₀₁

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.op_L₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.op.L₁ = S.L₂.op

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.op_L₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.op.L₂ = S.L₁.op

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.CategoryStruct.comp S.v₀₁.τ₁ S.v₁₂.τ₁ = 0

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₁_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₂.X₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp S.v₀₁.τ₁ (CategoryTheory.CategoryStruct.comp S.v₁₂.τ₁ h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.CategoryStruct.comp S.v₀₁.τ₂ S.v₁₂.τ₂ = 0

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₂_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₂.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp S.v₀₁.τ₂ (CategoryTheory.CategoryStruct.comp S.v₁₂.τ₂ h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.CategoryStruct.comp S.v₀₁.τ₃ S.v₁₂.τ₃ = 0

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₃_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₂.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp S.v₀₁.τ₃ (CategoryTheory.CategoryStruct.comp S.v₁₂.τ₃ h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.CategoryStruct.comp S.v₁₂.τ₁ S.v₂₃.τ₁ = 0

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₁_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₃.X₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp S.v₁₂.τ₁ (CategoryTheory.CategoryStruct.comp S.v₂₃.τ₁ h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.CategoryStruct.comp S.v₁₂.τ₂ S.v₂₃.τ₂ = 0

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₂_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₃.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp S.v₁₂.τ₂ (CategoryTheory.CategoryStruct.comp S.v₂₃.τ₂ h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.CategoryStruct.comp S.v₁₂.τ₃ S.v₂₃.τ₃ = 0

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₃_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₃.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp S.v₁₂.τ₃ (CategoryTheory.CategoryStruct.comp S.v₂₃.τ₃ h) = CategoryTheory.CategoryStruct.comp 0 h

noncomputable def CategoryTheory.ShortComplex.SnakeInput.h₀τ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.v₀₁.τ₁ ⋯)

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

Equations

• S.h₀τ₁ = CategoryTheory.Limits.isLimitForkMapOfIsLimit' CategoryTheory.ShortComplex.π₁ ⋯ S.h₀

noncomputable def CategoryTheory.ShortComplex.SnakeInput.h₀τ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.v₀₁.τ₂ ⋯)

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

Equations

• S.h₀τ₂ = CategoryTheory.Limits.isLimitForkMapOfIsLimit' CategoryTheory.ShortComplex.π₂ ⋯ S.h₀

noncomputable def CategoryTheory.ShortComplex.SnakeInput.h₀τ₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.v₀₁.τ₃ ⋯)

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

Equations

• S.h₀τ₃ = CategoryTheory.Limits.isLimitForkMapOfIsLimit' CategoryTheory.ShortComplex.π₃ ⋯ S.h₀

instance CategoryTheory.ShortComplex.SnakeInput.mono_v₀₁_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.Mono S.v₀₁.τ₁

Equations

• ⋯ = ⋯

instance CategoryTheory.ShortComplex.SnakeInput.mono_v₀₁_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.Mono S.v₀₁.τ₂

Equations

• ⋯ = ⋯

instance CategoryTheory.ShortComplex.SnakeInput.mono_v₀₁_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.Mono S.v₀₁.τ₃

Equations

• ⋯ = ⋯

theorem CategoryTheory.ShortComplex.SnakeInput.exact_C₁_up {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : (CategoryTheory.ShortComplex.mk S.v₀₁.τ₁ S.v₁₂.τ₁ ⋯).Exact

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

theorem CategoryTheory.ShortComplex.SnakeInput.exact_C₂_up {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : (CategoryTheory.ShortComplex.mk S.v₀₁.τ₂ S.v₁₂.τ₂ ⋯).Exact

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

theorem CategoryTheory.ShortComplex.SnakeInput.exact_C₃_up {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : (CategoryTheory.ShortComplex.mk S.v₀₁.τ₃ S.v₁₂.τ₃ ⋯).Exact

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

instance CategoryTheory.ShortComplex.SnakeInput.mono_L₀_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) [CategoryTheory.Mono S.L₁.f] : CategoryTheory.Mono S.L₀.f

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.ShortComplex.SnakeInput.h₃τ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.v₂₃.τ₁ ⋯)

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

Equations

• S.h₃τ₁ = CategoryTheory.Limits.isColimitCoforkMapOfIsColimit' CategoryTheory.ShortComplex.π₁ ⋯ S.h₃

noncomputable def CategoryTheory.ShortComplex.SnakeInput.h₃τ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.v₂₃.τ₂ ⋯)

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

Equations

• S.h₃τ₂ = CategoryTheory.Limits.isColimitCoforkMapOfIsColimit' CategoryTheory.ShortComplex.π₂ ⋯ S.h₃

noncomputable def CategoryTheory.ShortComplex.SnakeInput.h₃τ₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.v₂₃.τ₃ ⋯)

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

Equations

• S.h₃τ₃ = CategoryTheory.Limits.isColimitCoforkMapOfIsColimit' CategoryTheory.ShortComplex.π₃ ⋯ S.h₃

instance CategoryTheory.ShortComplex.SnakeInput.epi_v₂₃_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.Epi S.v₂₃.τ₁

Equations

• ⋯ = ⋯

instance CategoryTheory.ShortComplex.SnakeInput.epi_v₂₃_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.Epi S.v₂₃.τ₂

Equations

• ⋯ = ⋯

instance CategoryTheory.ShortComplex.SnakeInput.epi_v₂₃_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.Epi S.v₂₃.τ₃

Equations

• ⋯ = ⋯

theorem CategoryTheory.ShortComplex.SnakeInput.exact_C₁_down {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : (CategoryTheory.ShortComplex.mk S.v₁₂.τ₁ S.v₂₃.τ₁ ⋯).Exact

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

theorem CategoryTheory.ShortComplex.SnakeInput.exact_C₂_down {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : (CategoryTheory.ShortComplex.mk S.v₁₂.τ₂ S.v₂₃.τ₂ ⋯).Exact

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

theorem CategoryTheory.ShortComplex.SnakeInput.exact_C₃_down {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : (CategoryTheory.ShortComplex.mk S.v₁₂.τ₃ S.v₂₃.τ₃ ⋯).Exact

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

instance CategoryTheory.ShortComplex.SnakeInput.epi_L₃_g {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) [CategoryTheory.Epi S.L₂.g] : CategoryTheory.Epi S.L₃.g

Equations

• ⋯ = ⋯

theorem CategoryTheory.ShortComplex.SnakeInput.L₀_exact {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.L₀.Exact

theorem CategoryTheory.ShortComplex.SnakeInput.L₃_exact {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.L₃.Exact

noncomputable def CategoryTheory.ShortComplex.SnakeInput.P {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : 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

• S.P = CategoryTheory.Limits.pullback S.L₁.g S.v₀₁.τ₃

noncomputable def CategoryTheory.ShortComplex.SnakeInput.φ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.P ⟶ S.L₂.X₂

The canonical map P ⟶ L₂.X₂.

Equations

• S.φ₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst S.L₁.g S.v₀₁.τ₃) S.v₁₂.τ₂

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.lift_φ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) {A : C} (a : A ⟶ S.L₁.X₂) (b : A ⟶ S.L₀.X₃) (h : CategoryTheory.CategoryStruct.comp a S.L₁.g = CategoryTheory.CategoryStruct.comp b S.v₀₁.τ₃) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift a b h) S.φ₂ = CategoryTheory.CategoryStruct.comp a S.v₁₂.τ₂

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.lift_φ₂_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) {A : C} (a : A ⟶ S.L₁.X₂) (b : A ⟶ S.L₀.X₃) (h : CategoryTheory.CategoryStruct.comp a S.L₁.g = CategoryTheory.CategoryStruct.comp b S.v₀₁.τ₃) {Z : C} (h : S.L₂.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift a b h✝) (CategoryTheory.CategoryStruct.comp S.φ₂ h) = CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp S.v₁₂.τ₂ h)

noncomputable def CategoryTheory.ShortComplex.SnakeInput.φ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.P ⟶ S.L₂.X₁

The canonical map P ⟶ L₂.X₁.

Equations

• S.φ₁ = ⋯.lift S.φ₂ ⋯

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.CategoryStruct.comp S.φ₁ S.L₂.f = S.φ₂

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₂.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp S.φ₁ (CategoryTheory.CategoryStruct.comp S.L₂.f h) = CategoryTheory.CategoryStruct.comp S.φ₂ h

noncomputable def CategoryTheory.ShortComplex.SnakeInput.L₀' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.ShortComplex C

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

Equations

• S.L₀' = CategoryTheory.ShortComplex.mk (CategoryTheory.Limits.pullback.lift S.L₁.f 0 ⋯) (CategoryTheory.Limits.pullback.snd S.L₁.g S.v₀₁.τ₃) ⋯

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.L₁_f_φ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.CategoryStruct.comp S.L₀'.f S.φ₁ = S.v₁₂.τ₁

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.L₁_f_φ₁_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₂.X₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp S.L₀'.f (CategoryTheory.CategoryStruct.comp S.φ₁ h) = CategoryTheory.CategoryStruct.comp S.v₁₂.τ₁ h

instance CategoryTheory.ShortComplex.SnakeInput.instEpiGL₀' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.Epi S.L₀'.g

Equations

• ⋯ = ⋯

instance CategoryTheory.ShortComplex.SnakeInput.instMonoFL₀'OfL₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) [CategoryTheory.Mono S.L₁.f] : CategoryTheory.Mono S.L₀'.f

Equations

• ⋯ = ⋯

theorem CategoryTheory.ShortComplex.SnakeInput.L₀'_exact {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.L₀'.Exact

noncomputable def CategoryTheory.ShortComplex.SnakeInput.δ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.L₀.X₃ ⟶ S.L₃.X₁

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

Equations

• S.δ = ⋯.desc (CategoryTheory.CategoryStruct.comp S.φ₁ S.v₂₃.τ₁) ⋯

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.snd_δ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd S.L₁.g S.v₀₁.τ₃) S.δ = CategoryTheory.CategoryStruct.comp S.φ₁ S.v₂₃.τ₁

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.snd_δ_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₃.X₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd S.L₁.g S.v₀₁.τ₃) (CategoryTheory.CategoryStruct.comp S.δ h) = CategoryTheory.CategoryStruct.comp S.φ₁ (CategoryTheory.CategoryStruct.comp S.v₂₃.τ₁ h)

noncomputable def CategoryTheory.ShortComplex.SnakeInput.P' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : C

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

Equations

• S.P' = CategoryTheory.Limits.pushout S.L₂.f S.v₂₃.τ₁

theorem CategoryTheory.ShortComplex.SnakeInput.snd_δ_inr {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd S.L₁.g S.v₀₁.τ₃) (CategoryTheory.CategoryStruct.comp S.δ (CategoryTheory.Limits.pushout.inr S.L₂.f S.v₂₃.τ₁)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst S.L₁.g S.v₀₁.τ₃) (CategoryTheory.CategoryStruct.comp S.v₁₂.τ₂ (CategoryTheory.Limits.pushout.inl S.L₂.f S.v₂₃.τ₁))

noncomputable def CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.L₀.X₂ ⟶ S.P

The canonical morphism L₀.X₂ ⟶ P.

Equations

• S.L₀X₂ToP = CategoryTheory.Limits.pullback.lift S.v₀₁.τ₂ S.L₀.g ⋯

theorem CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_pullback_snd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.CategoryStruct.comp S.L₀X₂ToP (CategoryTheory.Limits.pullback.snd S.L₁.g S.v₀₁.τ₃) = S.L₀.g

theorem CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_pullback_snd_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₀.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp S.L₀X₂ToP (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd S.L₁.g S.v₀₁.τ₃) h) = CategoryTheory.CategoryStruct.comp S.L₀.g h

theorem CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_φ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.CategoryStruct.comp S.L₀X₂ToP S.φ₁ = 0

theorem CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_φ₁_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₂.X₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp S.L₀X₂ToP (CategoryTheory.CategoryStruct.comp S.φ₁ h) = CategoryTheory.CategoryStruct.comp 0 h

theorem CategoryTheory.ShortComplex.SnakeInput.L₀_g_δ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.CategoryStruct.comp S.L₀.g S.δ = 0

theorem CategoryTheory.ShortComplex.SnakeInput.δ_L₃_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.CategoryStruct.comp S.δ S.L₃.f = 0

noncomputable def CategoryTheory.ShortComplex.SnakeInput.L₁' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.ShortComplex C

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

Equations

• S.L₁' = CategoryTheory.ShortComplex.mk S.L₀.g S.δ ⋯

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.L₁'_X₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.L₁'.X₂ = S.L₀.X₃

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.L₁'_X₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.L₁'.X₁ = S.L₀.X₂

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.L₁'_g {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.L₁'.g = S.δ

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.L₁'_X₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.L₁'.X₃ = S.L₃.X₁

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.L₁'_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.L₁'.f = S.L₀.g

noncomputable def CategoryTheory.ShortComplex.SnakeInput.L₂' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.ShortComplex C

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

Equations

• S.L₂' = CategoryTheory.ShortComplex.mk S.δ S.L₃.f ⋯

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.L₂'_X₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.L₂'.X₃ = S.L₃.X₂

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.L₂'_X₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.L₂'.X₂ = S.L₃.X₁

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.L₂'_g {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.L₂'.g = S.L₃.f

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.L₂'_X₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.L₂'.X₁ = S.L₀.X₃

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.L₂'_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.L₂'.f = S.δ

theorem CategoryTheory.ShortComplex.SnakeInput.L₁'_exact {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.L₁'.Exact

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

noncomputable def CategoryTheory.ShortComplex.SnakeInput.PIsoUnopOpP' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.P ≅ Opposite.unop S.op.P'

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

Equations

• S.PIsoUnopOpP' = CategoryTheory.Limits.pullbackIsoUnopPushout S.L₁.g S.v₀₁.τ₃

noncomputable def CategoryTheory.ShortComplex.SnakeInput.P'IsoUnopOpP {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.P' ≅ Opposite.unop S.op.P

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

Equations

• S.P'IsoUnopOpP = CategoryTheory.Limits.pushoutIsoUnopPullback S.L₂.f S.v₂₃.τ₁

theorem CategoryTheory.ShortComplex.SnakeInput.op_δ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.op.δ = S.δ.op

noncomputable def CategoryTheory.ShortComplex.SnakeInput.L₂'OpIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.L₂'.op ≅ S.op.L₁'

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

Equations

• S.L₂'OpIso = CategoryTheory.ShortComplex.isoMk (CategoryTheory.Iso.refl S.L₂'.op.X₁) (CategoryTheory.Iso.refl S.L₂'.op.X₂) (CategoryTheory.Iso.refl S.L₂'.op.X₃) ⋯ ⋯

theorem CategoryTheory.ShortComplex.SnakeInput.L₂'_exact {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.L₂'.Exact

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.ShortComplex.SnakeInput.composableArrows {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.ComposableArrows C 5

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

• S.composableArrows = CategoryTheory.ComposableArrows.mk₅ S.L₀.f S.L₀.g S.δ S.L₃.f S.L₃.g

theorem CategoryTheory.ShortComplex.SnakeInput.snake_lemma {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.composableArrows.Exact

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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) {A : C} (x₃ : A ⟶ S.L₀.X₃) (x₂ : A ⟶ S.L₁.X₂) (x₁ : A ⟶ S.L₂.X₁) (h₂ : CategoryTheory.CategoryStruct.comp x₂ S.L₁.g = CategoryTheory.CategoryStruct.comp x₃ S.v₀₁.τ₃) (h₁ : CategoryTheory.CategoryStruct.comp x₁ S.L₂.f = CategoryTheory.CategoryStruct.comp x₂ S.v₁₂.τ₂) : CategoryTheory.CategoryStruct.comp x₃ S.δ = CategoryTheory.CategoryStruct.comp x₁ S.v₂₃.τ₁

structure CategoryTheory.ShortComplex.SnakeInput.Hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S₁ : CategoryTheory.ShortComplex.SnakeInput C) (S₂ : CategoryTheory.ShortComplex.SnakeInput C) : Type u_2

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

• f₀ : S₁.L₀ ⟶ S₂.L₀

  a morphism between the zeroth lines

• f₁ : S₁.L₁ ⟶ S₂.L₁

  a morphism between the first lines

• f₂ : S₁.L₂ ⟶ S₂.L₂

  a morphism between the second lines

• f₃ : S₁.L₃ ⟶ S₂.L₃

  a morphism between the third lines

• comm₀₁ : CategoryTheory.CategoryStruct.comp self.f₀ S₂.v₀₁ = CategoryTheory.CategoryStruct.comp S₁.v₀₁ self.f₁
• comm₁₂ : CategoryTheory.CategoryStruct.comp self.f₁ S₂.v₁₂ = CategoryTheory.CategoryStruct.comp S₁.v₁₂ self.f₂
• comm₂₃ : CategoryTheory.CategoryStruct.comp self.f₂ S₂.v₂₃ = CategoryTheory.CategoryStruct.comp S₁.v₂₃ self.f₃

theorem CategoryTheory.ShortComplex.SnakeInput.Hom.ext {C : Type u_1} : ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {inst_1 : CategoryTheory.Abelian C} {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} {x y : S₁.Hom S₂}, x.f₀ = y.f₀ → x.f₁ = y.f₁ → x.f₂ = y.f₂ → x.f₃ = y.f₃ → x = y

theorem CategoryTheory.ShortComplex.SnakeInput.Hom.comm₀₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} (self : S₁.Hom S₂) : CategoryTheory.CategoryStruct.comp self.f₀ S₂.v₀₁ = CategoryTheory.CategoryStruct.comp S₁.v₀₁ self.f₁

theorem CategoryTheory.ShortComplex.SnakeInput.Hom.comm₁₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} (self : S₁.Hom S₂) : CategoryTheory.CategoryStruct.comp self.f₁ S₂.v₁₂ = CategoryTheory.CategoryStruct.comp S₁.v₁₂ self.f₂

theorem CategoryTheory.ShortComplex.SnakeInput.Hom.comm₂₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} (self : S₁.Hom S₂) : CategoryTheory.CategoryStruct.comp self.f₂ S₂.v₂₃ = CategoryTheory.CategoryStruct.comp S₁.v₂₃ self.f₃

theorem CategoryTheory.ShortComplex.SnakeInput.Hom.comm₀₁_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} (self : S₁.Hom S₂) {Z : CategoryTheory.ShortComplex C} (h : S₂.L₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp self.f₀ (CategoryTheory.CategoryStruct.comp S₂.v₀₁ h) = CategoryTheory.CategoryStruct.comp S₁.v₀₁ (CategoryTheory.CategoryStruct.comp self.f₁ h)

theorem CategoryTheory.ShortComplex.SnakeInput.Hom.comm₂₃_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} (self : S₁.Hom S₂) {Z : CategoryTheory.ShortComplex C} (h : S₂.L₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp self.f₂ (CategoryTheory.CategoryStruct.comp S₂.v₂₃ h) = CategoryTheory.CategoryStruct.comp S₁.v₂₃ (CategoryTheory.CategoryStruct.comp self.f₃ h)

theorem CategoryTheory.ShortComplex.SnakeInput.Hom.comm₁₂_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} (self : S₁.Hom S₂) {Z : CategoryTheory.ShortComplex C} (h : S₂.L₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp self.f₁ (CategoryTheory.CategoryStruct.comp S₂.v₁₂ h) = CategoryTheory.CategoryStruct.comp S₁.v₁₂ (CategoryTheory.CategoryStruct.comp self.f₂ h)

def CategoryTheory.ShortComplex.SnakeInput.Hom.id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : S.Hom S

The identity morphism of a snake input.

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.Hom.id_f₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : (CategoryTheory.ShortComplex.SnakeInput.Hom.id S).f₃ = CategoryTheory.CategoryStruct.id S.L₃

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.Hom.id_f₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : (CategoryTheory.ShortComplex.SnakeInput.Hom.id S).f₁ = CategoryTheory.CategoryStruct.id S.L₁

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.Hom.id_f₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : (CategoryTheory.ShortComplex.SnakeInput.Hom.id S).f₀ = CategoryTheory.CategoryStruct.id S.L₀

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.Hom.id_f₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : (CategoryTheory.ShortComplex.SnakeInput.Hom.id S).f₂ = CategoryTheory.CategoryStruct.id S.L₂

def CategoryTheory.ShortComplex.SnakeInput.Hom.comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} {S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁.Hom S₂) (g : S₂.Hom S₃) : S₁.Hom S₃

The composition of morphisms of snake inputs.

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} {S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁.Hom S₂) (g : S₂.Hom S₃) : (f.comp g).f₁ = CategoryTheory.CategoryStruct.comp f.f₁ g.f₁

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} {S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁.Hom S₂) (g : S₂.Hom S₃) : (f.comp g).f₂ = CategoryTheory.CategoryStruct.comp f.f₂ g.f₂

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} {S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁.Hom S₂) (g : S₂.Hom S₃) : (f.comp g).f₃ = CategoryTheory.CategoryStruct.comp f.f₃ g.f₃

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} {S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁.Hom S₂) (g : S₂.Hom S₃) : (f.comp g).f₀ = CategoryTheory.CategoryStruct.comp f.f₀ g.f₀

instance CategoryTheory.ShortComplex.SnakeInput.instCategory {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.Category.{u_2, max u_2 u_1} (CategoryTheory.ShortComplex.SnakeInput C)

Equations

• CategoryTheory.ShortComplex.SnakeInput.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.id_f₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : (CategoryTheory.CategoryStruct.id S).f₀ = CategoryTheory.CategoryStruct.id S.L₀

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.id_f₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : (CategoryTheory.CategoryStruct.id S).f₁ = CategoryTheory.CategoryStruct.id S.L₁

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.id_f₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : (CategoryTheory.CategoryStruct.id S).f₂ = CategoryTheory.CategoryStruct.id S.L₂

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.id_f₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : (CategoryTheory.CategoryStruct.id S).f₃ = CategoryTheory.CategoryStruct.id S.L₃

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.comp_f₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} {S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃) : (CategoryTheory.CategoryStruct.comp f g).f₀ = CategoryTheory.CategoryStruct.comp f.f₀ g.f₀

theorem CategoryTheory.ShortComplex.SnakeInput.comp_f₀_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} {S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃) {Z : CategoryTheory.ShortComplex C} (h : S₃.L₀ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).f₀ h = CategoryTheory.CategoryStruct.comp f.f₀ (CategoryTheory.CategoryStruct.comp g.f₀ h)

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.comp_f₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} {S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃) : (CategoryTheory.CategoryStruct.comp f g).f₁ = CategoryTheory.CategoryStruct.comp f.f₁ g.f₁

theorem CategoryTheory.ShortComplex.SnakeInput.comp_f₁_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} {S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃) {Z : CategoryTheory.ShortComplex C} (h : S₃.L₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).f₁ h = CategoryTheory.CategoryStruct.comp f.f₁ (CategoryTheory.CategoryStruct.comp g.f₁ h)

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.comp_f₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} {S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃) : (CategoryTheory.CategoryStruct.comp f g).f₂ = CategoryTheory.CategoryStruct.comp f.f₂ g.f₂

theorem CategoryTheory.ShortComplex.SnakeInput.comp_f₂_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} {S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃) {Z : CategoryTheory.ShortComplex C} (h : S₃.L₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).f₂ h = CategoryTheory.CategoryStruct.comp f.f₂ (CategoryTheory.CategoryStruct.comp g.f₂ h)

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.comp_f₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} {S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃) : (CategoryTheory.CategoryStruct.comp f g).f₃ = CategoryTheory.CategoryStruct.comp f.f₃ g.f₃

theorem CategoryTheory.ShortComplex.SnakeInput.comp_f₃_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} {S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃) {Z : CategoryTheory.ShortComplex C} (h : S₃.L₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).f₃ h = CategoryTheory.CategoryStruct.comp f.f₃ (CategoryTheory.CategoryStruct.comp g.f₃ h)

def CategoryTheory.ShortComplex.SnakeInput.functorL₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.Functor (CategoryTheory.ShortComplex.SnakeInput C) (CategoryTheory.ShortComplex C)

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.

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.functorL₀_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), CategoryTheory.ShortComplex.SnakeInput.functorL₀.map f = f.f₀

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.functorL₀_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.ShortComplex.SnakeInput.functorL₀.obj S = S.L₀

def CategoryTheory.ShortComplex.SnakeInput.functorL₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.Functor (CategoryTheory.ShortComplex.SnakeInput C) (CategoryTheory.ShortComplex C)

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.

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.functorL₁_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), CategoryTheory.ShortComplex.SnakeInput.functorL₁.map f = f.f₁

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.functorL₁_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.ShortComplex.SnakeInput.functorL₁.obj S = S.L₁

def CategoryTheory.ShortComplex.SnakeInput.functorL₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.Functor (CategoryTheory.ShortComplex.SnakeInput C) (CategoryTheory.ShortComplex C)

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.

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.functorL₂_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.ShortComplex.SnakeInput.functorL₂.obj S = S.L₂

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.functorL₂_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), CategoryTheory.ShortComplex.SnakeInput.functorL₂.map f = f.f₂

def CategoryTheory.ShortComplex.SnakeInput.functorL₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.Functor (CategoryTheory.ShortComplex.SnakeInput C) (CategoryTheory.ShortComplex C)

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.

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.functorL₃_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), CategoryTheory.ShortComplex.SnakeInput.functorL₃.map f = f.f₃

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.functorL₃_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.ShortComplex.SnakeInput.functorL₃.obj S = S.L₃

noncomputable def CategoryTheory.ShortComplex.SnakeInput.functorP {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.Functor (CategoryTheory.ShortComplex.SnakeInput C) C

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.

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.functorP_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (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₁.τ₃ ⋯ ⋯

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.functorP_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.ShortComplex.SnakeInput.functorP.obj S = S.P

theorem CategoryTheory.ShortComplex.SnakeInput.naturality_φ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) : CategoryTheory.CategoryStruct.comp S₁.φ₂ f.f₂.τ₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.SnakeInput.functorP.map f) S₂.φ₂

theorem CategoryTheory.ShortComplex.SnakeInput.naturality_φ₂_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) {Z : C} (h : S₂.L₂.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp S₁.φ₂ (CategoryTheory.CategoryStruct.comp f.f₂.τ₂ h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.SnakeInput.functorP.map f) (CategoryTheory.CategoryStruct.comp S₂.φ₂ h)

theorem CategoryTheory.ShortComplex.SnakeInput.naturality_φ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) : CategoryTheory.CategoryStruct.comp S₁.φ₁ f.f₂.τ₁ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.SnakeInput.functorP.map f) S₂.φ₁

theorem CategoryTheory.ShortComplex.SnakeInput.naturality_φ₁_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) {Z : C} (h : S₂.L₂.X₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp S₁.φ₁ (CategoryTheory.CategoryStruct.comp f.f₂.τ₁ h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.SnakeInput.functorP.map f) (CategoryTheory.CategoryStruct.comp S₂.φ₁ h)

theorem CategoryTheory.ShortComplex.SnakeInput.naturality_δ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) : CategoryTheory.CategoryStruct.comp S₁.δ f.f₃.τ₁ = CategoryTheory.CategoryStruct.comp f.f₀.τ₃ S₂.δ

theorem CategoryTheory.ShortComplex.SnakeInput.naturality_δ_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex.SnakeInput C} {S₂ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) {Z : C} (h : S₂.L₃.X₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp S₁.δ (CategoryTheory.CategoryStruct.comp f.f₃.τ₁ h) = CategoryTheory.CategoryStruct.comp f.f₀.τ₃ (CategoryTheory.CategoryStruct.comp S₂.δ h)

noncomputable def CategoryTheory.ShortComplex.SnakeInput.functorL₁' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.Functor (CategoryTheory.ShortComplex.SnakeInput C) (CategoryTheory.ShortComplex C)

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.

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₁'.map f).τ₂ = f.f₀.τ₃

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.functorL₁'_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.ShortComplex.SnakeInput.functorL₁'.obj S = S.L₁'

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₁'.map f).τ₃ = f.f₃.τ₁

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₁'.map f).τ₁ = f.f₀.τ₂

noncomputable def CategoryTheory.ShortComplex.SnakeInput.functorL₂' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.Functor (CategoryTheory.ShortComplex.SnakeInput C) (CategoryTheory.ShortComplex C)

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.

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.functorL₂'_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.ShortComplex.SnakeInput.functorL₂'.obj S = S.L₂'

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₂'.map f).τ₁ = f.f₀.τ₃

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₂'.map f).τ₃ = f.f₃.τ₂

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₂'.map f).τ₂ = f.f₃.τ₁

noncomputable def CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : CategoryTheory.Functor (CategoryTheory.ShortComplex.SnakeInput C) (CategoryTheory.ComposableArrows C 5)

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.

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) : CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor.obj S = S.composableArrows

@[simp]

theorem CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] : ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X ⟶ Y), CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor.map f = CategoryTheory.ComposableArrows.homMk₅ f.f₀.τ₁ f.f₀.τ₂ f.f₀.τ₃ f.f₃.τ₁ f.f₃.τ₂ f.f₃.τ₃ ⋯ ⋯ ⋯ ⋯ ⋯