Exact sequences

A sequence of n composable arrows S : ComposableArrows C (i.e. a functor S : Fin (n + 1) ⥤ C) is said to be exact (S.Exact) if the composition of two consecutive arrows are zero (S.IsComplex) and the diagram is exact at each i for 1 ≤ i < n.

Together with the inductive construction of composable arrows ComposableArrows.precomp, this is useful in order to state that certain finite sequences of morphisms are exact (e.g the snake lemma), even though in the applications it would usually be more convenient to use individual lemmas expressing the exactness at a particular object.

This implementation is a refactor of exact_seq with appeared in the Liquid Tensor Experiment as a property of lists in Arrow C.

def CategoryTheory.ShortComplex.toComposableArrows {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) : ComposableArrows C 2

The composable arrows associated to a short complex.

@[simp]

theorem CategoryTheory.ShortComplex.toComposableArrows_map {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) {X✝ Y✝ : Fin (1 + 1 + 1)} (g : X✝ ⟶ Y✝) : S.toComposableArrows.map g = ComposableArrows.Precomp.map (ComposableArrows.mk₁ S.g) S.f X✝ Y✝ ⋯

@[simp]

theorem CategoryTheory.ShortComplex.toComposableArrows_obj {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) (a✝ : Fin (1 + 1 + 1)) : S.toComposableArrows.obj a✝ = ComposableArrows.Precomp.obj (ComposableArrows.mk₁ S.g) S.X₁ a✝

def CategoryTheory.ShortComplex.mapToComposableArrows {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) : S₁.toComposableArrows ⟶ S₂.toComposableArrows

A map of short complexes induces a map of composable arrows with the same data.

@[simp]

theorem CategoryTheory.ShortComplex.mapToComposableArrows_app_0 {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) : (mapToComposableArrows φ).app 0 = φ.τ₁

@[simp]

theorem CategoryTheory.ShortComplex.mapToComposableArrows_app_1 {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) : (mapToComposableArrows φ).app 1 = φ.τ₂

@[simp]

theorem CategoryTheory.ShortComplex.mapToComposableArrows_app_2 {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) : (mapToComposableArrows φ).app 2 = φ.τ₃

@[simp]

theorem CategoryTheory.ShortComplex.mapToComposableArrows_id {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ : ShortComplex C} : mapToComposableArrows (CategoryStruct.id S₁) = CategoryStruct.id S₁.toComposableArrows

@[simp]

theorem CategoryTheory.ShortComplex.mapToComposableArrows_comp {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} (φ : S₁ ⟶ S₂) (ψ : S₂ ⟶ S₃) : mapToComposableArrows (CategoryStruct.comp φ ψ) = CategoryStruct.comp (mapToComposableArrows φ) (mapToComposableArrows ψ)

structure CategoryTheory.ComposableArrows.IsComplex {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} (S : ComposableArrows C n) : Prop

F : ComposableArrows C n is a complex if all compositions of two consecutive arrows are zero.

• zero (i : ℕ) (hi : i + 2 ≤ n := by omega) : CategoryStruct.comp (S.map' i (i + 1) ⋯ ⋯) (S.map' (i + 1) (i + 2) ⋯ hi) = 0

  the composition of two consecutive arrows is zero

theorem CategoryTheory.ComposableArrows.IsComplex.zero_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S : ComposableArrows C n} (self : S.IsComplex) (i : ℕ) (hi : i + 2 ≤ n := by omega) {Z : C} (h : S.obj ⟨i + 2, ⋯⟩ ⟶ Z) : CategoryStruct.comp (S.map' i (i + 1) ⋯ ⋯) (CategoryStruct.comp (S.map' (i + 1) (i + 2) ⋯ hi) h) = CategoryStruct.comp 0 h

theorem CategoryTheory.ComposableArrows.IsComplex.zero' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S : ComposableArrows C n} (hS : S.IsComplex) (i j k : ℕ) (hij : i + 1 = j := by omega) (hjk : j + 1 = k := by omega) (hk : k ≤ n := by omega) : CategoryStruct.comp (S.map' i j ⋯ ⋯) (S.map' j k ⋯ hk) = 0

theorem CategoryTheory.ComposableArrows.IsComplex.zero'_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S : ComposableArrows C n} (hS : S.IsComplex) (i j k : ℕ) (hij : i + 1 = j := by omega) (hjk : j + 1 = k := by omega) (hk : k ≤ n := by omega) {Z : C} (h : S.obj ⟨k, ⋯⟩ ⟶ Z) : CategoryStruct.comp (S.map' i j ⋯ ⋯) (CategoryStruct.comp (S.map' j k ⋯ hk) h) = CategoryStruct.comp 0 h

theorem CategoryTheory.ComposableArrows.isComplex_of_iso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S₁ S₂ : ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : S₁.IsComplex) : S₂.IsComplex

theorem CategoryTheory.ComposableArrows.isComplex_iff_of_iso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S₁ S₂ : ComposableArrows C n} (e : S₁ ≅ S₂) : S₁.IsComplex ↔ S₂.IsComplex

theorem CategoryTheory.ComposableArrows.isComplex₀ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ComposableArrows C 0) : S.IsComplex

theorem CategoryTheory.ComposableArrows.isComplex₁ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ComposableArrows C 1) : S.IsComplex

@[reducible, inline]

abbrev CategoryTheory.ComposableArrows.sc' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} (S : ComposableArrows C n) (hS : S.IsComplex) (i j k : ℕ) (hij : i + 1 = j := by omega) (hjk : j + 1 = k := by omega) (hk : k ≤ n := by omega) : ShortComplex C

The short complex consisting of maps S.map' i j and S.map' j k when we know that S : ComposableArrows C n satisfies S.IsComplex.

@[reducible, inline]

abbrev CategoryTheory.ComposableArrows.sc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} (S : ComposableArrows C n) (hS : S.IsComplex) (i : ℕ) (hi : i + 2 ≤ n := by omega) : ShortComplex C

The short complex consisting of maps S.map' i (i + 1) and S.map' (i + 1) (i + 2) when we know that S : ComposableArrows C n satisfies S.IsComplex.

structure CategoryTheory.ComposableArrows.Exact {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} (S : ComposableArrows C n) extends S.IsComplex : Prop

F : ComposableArrows C n is exact if it is a complex and that all short complexes consisting of two consecutive arrows are exact.

• zero (i : ℕ) (hi : i + 2 ≤ n := by omega) : CategoryStruct.comp (S.map' i (i + 1) ⋯ ⋯) (S.map' (i + 1) (i + 2) ⋯ hi) = 0
• exact (i : ℕ) (hi : i + 2 ≤ n := by omega) : (S.sc ⋯ i hi).Exact

theorem CategoryTheory.ComposableArrows.Exact.exact' {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S : ComposableArrows C n} (hS : S.Exact) (i j k : ℕ) (hij : i + 1 = j := by omega) (hjk : j + 1 = k := by omega) (hk : k ≤ n := by omega) : (S.sc' ⋯ i j k hij hjk hk).Exact

def CategoryTheory.ComposableArrows.sc'Map {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S₁ S₂ : ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i j k : ℕ) (hij : i + 1 = j := by omega) (hjk : j + 1 = k := by omega) (hk : k ≤ n := by omega) : S₁.sc' h₁ i j k hij hjk hk ⟶ S₂.sc' h₂ i j k hij hjk hk

Functoriality maps for ComposableArrows.sc'.

@[simp]

theorem CategoryTheory.ComposableArrows.sc'Map_τ₂ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S₁ S₂ : ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i j k : ℕ) (hij : i + 1 = j := by omega) (hjk : j + 1 = k := by omega) (hk : k ≤ n := by omega) : (sc'Map φ h₁ h₂ i j k hij hjk hk).τ₂ = φ.app ⟨j, ⋯⟩

@[simp]

theorem CategoryTheory.ComposableArrows.sc'Map_τ₃ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S₁ S₂ : ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i j k : ℕ) (hij : i + 1 = j := by omega) (hjk : j + 1 = k := by omega) (hk : k ≤ n := by omega) : (sc'Map φ h₁ h₂ i j k hij hjk hk).τ₃ = φ.app ⟨k, ⋯⟩

@[simp]

theorem CategoryTheory.ComposableArrows.sc'Map_τ₁ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S₁ S₂ : ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i j k : ℕ) (hij : i + 1 = j := by omega) (hjk : j + 1 = k := by omega) (hk : k ≤ n := by omega) : (sc'Map φ h₁ h₂ i j k hij hjk hk).τ₁ = φ.app ⟨i, ⋯⟩

def CategoryTheory.ComposableArrows.scMap {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S₁ S₂ : ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i : ℕ) (hi : i + 2 ≤ n := by omega) : S₁.sc h₁ i hi ⟶ S₂.sc h₂ i hi

Functoriality maps for ComposableArrows.sc.

@[simp]

theorem CategoryTheory.ComposableArrows.scMap_τ₂ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S₁ S₂ : ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i : ℕ) (hi : i + 2 ≤ n := by omega) : (scMap φ h₁ h₂ i hi).τ₂ = φ.app ⟨i + 1, ⋯⟩

@[simp]

theorem CategoryTheory.ComposableArrows.scMap_τ₃ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S₁ S₂ : ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i : ℕ) (hi : i + 2 ≤ n := by omega) : (scMap φ h₁ h₂ i hi).τ₃ = φ.app ⟨i + 2, ⋯⟩

@[simp]

theorem CategoryTheory.ComposableArrows.scMap_τ₁ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S₁ S₂ : ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i : ℕ) (hi : i + 2 ≤ n := by omega) : (scMap φ h₁ h₂ i hi).τ₁ = φ.app ⟨i, ⋯⟩

def CategoryTheory.ComposableArrows.sc'MapIso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S₁ S₂ : ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i j k : ℕ) (hij : i + 1 = j := by omega) (hjk : j + 1 = k := by omega) (hk : k ≤ n := by omega) : S₁.sc' h₁ i j k hij hjk hk ≅ S₂.sc' h₂ i j k hij hjk hk

The isomorphism S₁.sc' _ i j k ≅ S₂.sc' _ i j k induced by an isomorphism S₁ ≅ S₂ in ComposableArrows C n.

@[simp]

theorem CategoryTheory.ComposableArrows.sc'MapIso_inv {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S₁ S₂ : ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i j k : ℕ) (hij : i + 1 = j := by omega) (hjk : j + 1 = k := by omega) (hk : k ≤ n := by omega) : (sc'MapIso e h₁ h₂ i j k hij hjk hk).inv = sc'Map e.inv h₂ h₁ i j k hij hjk hk

@[simp]

theorem CategoryTheory.ComposableArrows.sc'MapIso_hom {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S₁ S₂ : ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i j k : ℕ) (hij : i + 1 = j := by omega) (hjk : j + 1 = k := by omega) (hk : k ≤ n := by omega) : (sc'MapIso e h₁ h₂ i j k hij hjk hk).hom = sc'Map e.hom h₁ h₂ i j k hij hjk hk

def CategoryTheory.ComposableArrows.scMapIso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S₁ S₂ : ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i : ℕ) (hi : i + 2 ≤ n := by omega) : S₁.sc h₁ i hi ≅ S₂.sc h₂ i hi

The isomorphism S₁.sc _ i ≅ S₂.sc _ i induced by an isomorphism S₁ ≅ S₂ in ComposableArrows C n.

@[simp]

theorem CategoryTheory.ComposableArrows.scMapIso_inv {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S₁ S₂ : ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i : ℕ) (hi : i + 2 ≤ n := by omega) : (scMapIso e h₁ h₂ i hi).inv = scMap e.inv h₂ h₁ i hi

@[simp]

theorem CategoryTheory.ComposableArrows.scMapIso_hom {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S₁ S₂ : ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex) (i : ℕ) (hi : i + 2 ≤ n := by omega) : (scMapIso e h₁ h₂ i hi).hom = scMap e.hom h₁ h₂ i hi

theorem CategoryTheory.ComposableArrows.exact_of_iso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S₁ S₂ : ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : S₁.Exact) : S₂.Exact

theorem CategoryTheory.ComposableArrows.exact_iff_of_iso {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S₁ S₂ : ComposableArrows C n} (e : S₁ ≅ S₂) : S₁.Exact ↔ S₂.Exact

theorem CategoryTheory.ComposableArrows.exact₀ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ComposableArrows C 0) : S.Exact

theorem CategoryTheory.ComposableArrows.exact₁ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ComposableArrows C 1) : S.Exact

theorem CategoryTheory.ComposableArrows.isComplex₂_iff {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ComposableArrows C 2) : S.IsComplex ↔ CategoryStruct.comp (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯) = 0

theorem CategoryTheory.ComposableArrows.isComplex₂_mk {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ComposableArrows C 2) (w : CategoryStruct.comp (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯) = 0) : S.IsComplex

theorem CategoryTheory.ShortComplex.isComplex_toComposableArrows {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) : S.toComposableArrows.IsComplex

theorem CategoryTheory.ComposableArrows.exact₂_iff {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ComposableArrows C 2) (hS : S.IsComplex) : S.Exact ↔ (S.sc' hS 0 1 2 ⋯ ⋯ ⋯).Exact

theorem CategoryTheory.ComposableArrows.exact₂_mk {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ComposableArrows C 2) (w : CategoryStruct.comp (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯) = 0) (h : { X₁ := S.obj ⟨0, ⋯⟩, X₂ := S.obj ⟨1, ⋯⟩, X₃ := S.obj ⟨2, ⋯⟩, f := S.map' 0 1 ⋯ ⋯, g := S.map' 1 2 ⋯ ⋯, zero := w }.Exact) : S.Exact

theorem CategoryTheory.ShortComplex.Exact.exact_toComposableArrows {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (hS : S.Exact) : S.toComposableArrows.Exact

theorem CategoryTheory.ShortComplex.exact_iff_exact_toComposableArrows {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) : S.Exact ↔ S.toComposableArrows.Exact

theorem CategoryTheory.ComposableArrows.exact_iff_δ₀ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} (S : ComposableArrows C (n + 2)) : S.Exact ↔ (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact ∧ S.δ₀.Exact

theorem CategoryTheory.ComposableArrows.Exact.δ₀ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S : ComposableArrows C (n + 2)} (hS : S.Exact) : S.δ₀.Exact

theorem CategoryTheory.ComposableArrows.exact_of_δ₀ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S : ComposableArrows C (n + 2)} (h : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact) (h₀ : S.δ₀.Exact) : S.Exact

If S : ComposableArrows C (n + 2) is such that the first two arrows form an exact sequence and that the tail S.δ₀ is exact, then S is also exact. See ShortComplex.SnakeInput.snake_lemma in Algebra.Homology.ShortComplex.SnakeLemma for a use of this lemma.

theorem CategoryTheory.ComposableArrows.exact_iff_δlast {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} (S : ComposableArrows C (n + 2)) : S.Exact ↔ S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact

theorem CategoryTheory.ComposableArrows.Exact.δlast {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} {S : ComposableArrows C (n + 2)} (hS : S.Exact) : S.δlast.Exact

theorem CategoryTheory.ComposableArrows.exact_of_δlast {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {n : ℕ} (S : ComposableArrows C (n + 2)) (h₁ : S.δlast.Exact) (h₂ : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact) : S.Exact

theorem CategoryTheory.ComposableArrows.Exact.isIso_map' {C : Type u_2} [Category.{u_3, u_2} C] [Preadditive C] [Balanced C] {n : ℕ} {S : ComposableArrows C n} (hS : S.Exact) (k : ℕ) (hk : k + 3 ≤ n) (h₀ : S.map' k (k + 1) ⋯ ⋯ = 0) (h₁ : S.map' (k + 2) (k + 3) ⋯ hk = 0) : IsIso (S.map' (k + 1) (k + 2) ⋯ ⋯)