Short complexes

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

TODO: A homology API for these objects shall be developed in the folder Algebra.Homology.ShortComplex and eventually the homology of objects in HomologicalComplex C c shall be redefined using this.

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

structure CategoryTheory.ShortComplex (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : 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

@[simp]

theorem CategoryTheory.ShortComplex.zero_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (self : CategoryTheory.ShortComplex C) {Z : C} (h : self.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp self.f (CategoryTheory.CategoryStruct.comp self.g h) = CategoryTheory.CategoryStruct.comp 0 h

theorem CategoryTheory.ShortComplex.Hom.ext {C : Type u_1} : ∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {S₁ S₂ : CategoryTheory.ShortComplex C} (x y : CategoryTheory.ShortComplex.Hom S₁ S₂), x.τ₁ = y.τ₁ → x.τ₂ = y.τ₂ → x.τ₃ = y.τ₃ → x = y

theorem CategoryTheory.ShortComplex.Hom.ext_iff {C : Type u_1} : ∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {S₁ S₂ : CategoryTheory.ShortComplex C} (x y : CategoryTheory.ShortComplex.Hom S₁ S₂), x = y ↔ x.τ₁ = y.τ₁ ∧ x.τ₂ = y.τ₂ ∧ x.τ₃ = y.τ₃

structure CategoryTheory.ShortComplex.Hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) : Type u_3

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

• τ₁ : S₁.X₁ ⟶ S₂.X₁

  the morphism on the left objects

• τ₂ : S₁.X₂ ⟶ S₂.X₂

  the morphism on the middle objects

• τ₃ : S₁.X₃ ⟶ S₂.X₃

  the morphism on the right objects

• comm₁₂ : CategoryTheory.CategoryStruct.comp self.τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f self.τ₂

  the left commutative square of a morphism in ShortComplex

• comm₂₃ : CategoryTheory.CategoryStruct.comp self.τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g self.τ₃

  the right commutative square of a morphism in ShortComplex

theorem CategoryTheory.ShortComplex.Hom.comm₂₃_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (self : CategoryTheory.ShortComplex.Hom S₁ S₂) {Z : C} (h : S₂.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp self.τ₂ (CategoryTheory.CategoryStruct.comp S₂.g h) = CategoryTheory.CategoryStruct.comp S₁.g (CategoryTheory.CategoryStruct.comp self.τ₃ h)

theorem CategoryTheory.ShortComplex.Hom.comm₁₂_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (self : CategoryTheory.ShortComplex.Hom S₁ S₂) {Z : C} (h : S₂.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp self.τ₁ (CategoryTheory.CategoryStruct.comp S₂.f h) = CategoryTheory.CategoryStruct.comp S₁.f (CategoryTheory.CategoryStruct.comp self.τ₂ h)

@[simp]

theorem CategoryTheory.ShortComplex.Hom.id_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.Hom.id S).τ₃ = CategoryTheory.CategoryStruct.id S.X₃

@[simp]

theorem CategoryTheory.ShortComplex.Hom.id_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.Hom.id S).τ₁ = CategoryTheory.CategoryStruct.id S.X₁

@[simp]

theorem CategoryTheory.ShortComplex.Hom.id_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.Hom.id S).τ₂ = CategoryTheory.CategoryStruct.id S.X₂

def CategoryTheory.ShortComplex.Hom.id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.ShortComplex.Hom S S

The identity morphism of a short complex.

Equations

• CategoryTheory.ShortComplex.Hom.id S = CategoryTheory.ShortComplex.Hom.mk (CategoryTheory.CategoryStruct.id S.X₁) (CategoryTheory.CategoryStruct.id S.X₂) (CategoryTheory.CategoryStruct.id S.X₃)

@[simp]

theorem CategoryTheory.ShortComplex.Hom.comp_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : CategoryTheory.ShortComplex.Hom S₁ S₂) (φ₂₃ : CategoryTheory.ShortComplex.Hom S₂ S₃) : (CategoryTheory.ShortComplex.Hom.comp φ₁₂ φ₂₃).τ₃ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₃ φ₂₃.τ₃

@[simp]

theorem CategoryTheory.ShortComplex.Hom.comp_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : CategoryTheory.ShortComplex.Hom S₁ S₂) (φ₂₃ : CategoryTheory.ShortComplex.Hom S₂ S₃) : (CategoryTheory.ShortComplex.Hom.comp φ₁₂ φ₂₃).τ₁ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₁ φ₂₃.τ₁

@[simp]

theorem CategoryTheory.ShortComplex.Hom.comp_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : CategoryTheory.ShortComplex.Hom S₁ S₂) (φ₂₃ : CategoryTheory.ShortComplex.Hom S₂ S₃) : (CategoryTheory.ShortComplex.Hom.comp φ₁₂ φ₂₃).τ₂ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₂ φ₂₃.τ₂

def CategoryTheory.ShortComplex.Hom.comp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : CategoryTheory.ShortComplex.Hom S₁ S₂) (φ₂₃ : CategoryTheory.ShortComplex.Hom S₂ S₃) : CategoryTheory.ShortComplex.Hom S₁ S₃

The composition of morphisms of short complexes.

Equations

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

instance CategoryTheory.ShortComplex.instCategoryShortComplex {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Category.{u_3, max u_3 u_1} (CategoryTheory.ShortComplex C)

Equations

• CategoryTheory.ShortComplex.instCategoryShortComplex = CategoryTheory.Category.mk

theorem CategoryTheory.ShortComplex.hom_ext {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (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} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (τ₁ : S₁.X₁ ⟶ S₂.X₁) (τ₂ : S₁.X₂ ⟶ S₂.X₂) (τ₃ : S₁.X₃ ⟶ S₂.X₃) (comm₁₂ : CategoryTheory.CategoryStruct.comp τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂) (comm₂₃ : CategoryTheory.CategoryStruct.comp τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃) : (CategoryTheory.ShortComplex.homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃).τ₂ = τ₂

@[simp]

theorem CategoryTheory.ShortComplex.homMk_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (τ₁ : S₁.X₁ ⟶ S₂.X₁) (τ₂ : S₁.X₂ ⟶ S₂.X₂) (τ₃ : S₁.X₃ ⟶ S₂.X₃) (comm₁₂ : CategoryTheory.CategoryStruct.comp τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂) (comm₂₃ : CategoryTheory.CategoryStruct.comp τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃) : (CategoryTheory.ShortComplex.homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃).τ₁ = τ₁

@[simp]

theorem CategoryTheory.ShortComplex.homMk_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (τ₁ : S₁.X₁ ⟶ S₂.X₁) (τ₂ : S₁.X₂ ⟶ S₂.X₂) (τ₃ : S₁.X₃ ⟶ S₂.X₃) (comm₁₂ : CategoryTheory.CategoryStruct.comp τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂) (comm₂₃ : CategoryTheory.CategoryStruct.comp τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃) : (CategoryTheory.ShortComplex.homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃).τ₃ = τ₃

def CategoryTheory.ShortComplex.homMk {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (τ₁ : S₁.X₁ ⟶ S₂.X₁) (τ₂ : S₁.X₂ ⟶ S₂.X₂) (τ₃ : S₁.X₃ ⟶ S₂.X₃) (comm₁₂ : CategoryTheory.CategoryStruct.comp τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂) (comm₂₃ : CategoryTheory.CategoryStruct.comp τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃) : S₁ ⟶ S₂

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

Equations

• CategoryTheory.ShortComplex.homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃ = CategoryTheory.ShortComplex.Hom.mk τ₁ τ₂ τ₃

@[simp]

theorem CategoryTheory.ShortComplex.id_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.CategoryStruct.id S).τ₁ = CategoryTheory.CategoryStruct.id S.X₁

@[simp]

theorem CategoryTheory.ShortComplex.id_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.CategoryStruct.id S).τ₂ = CategoryTheory.CategoryStruct.id S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.id_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.CategoryStruct.id S).τ₃ = CategoryTheory.CategoryStruct.id S.X₃

theorem CategoryTheory.ShortComplex.comp_τ₁_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : S₁ ⟶ S₂) (φ₂₃ : S₂ ⟶ S₃) {Z : C} (h : S₃.X₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp φ₁₂ φ₂₃).τ₁ h = CategoryTheory.CategoryStruct.comp φ₁₂.τ₁ (CategoryTheory.CategoryStruct.comp φ₂₃.τ₁ h)

@[simp]

theorem CategoryTheory.ShortComplex.comp_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : S₁ ⟶ S₂) (φ₂₃ : S₂ ⟶ S₃) : (CategoryTheory.CategoryStruct.comp φ₁₂ φ₂₃).τ₁ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₁ φ₂₃.τ₁

theorem CategoryTheory.ShortComplex.comp_τ₂_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : S₁ ⟶ S₂) (φ₂₃ : S₂ ⟶ S₃) {Z : C} (h : S₃.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp φ₁₂ φ₂₃).τ₂ h = CategoryTheory.CategoryStruct.comp φ₁₂.τ₂ (CategoryTheory.CategoryStruct.comp φ₂₃.τ₂ h)

@[simp]

theorem CategoryTheory.ShortComplex.comp_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : S₁ ⟶ S₂) (φ₂₃ : S₂ ⟶ S₃) : (CategoryTheory.CategoryStruct.comp φ₁₂ φ₂₃).τ₂ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₂ φ₂₃.τ₂

theorem CategoryTheory.ShortComplex.comp_τ₃_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : S₁ ⟶ S₂) (φ₂₃ : S₂ ⟶ S₃) {Z : C} (h : S₃.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp φ₁₂ φ₂₃).τ₃ h = CategoryTheory.CategoryStruct.comp φ₁₂.τ₃ (CategoryTheory.CategoryStruct.comp φ₂₃.τ₃ h)

@[simp]

theorem CategoryTheory.ShortComplex.comp_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : S₁ ⟶ S₂) (φ₂₃ : S₂ ⟶ S₃) : (CategoryTheory.CategoryStruct.comp φ₁₂ φ₂₃).τ₃ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₃ φ₂₃.τ₃

instance CategoryTheory.ShortComplex.instZeroHomShortComplexToQuiverToCategoryStructInstCategoryShortComplex {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} : Zero (S₁ ⟶ S₂)

Equations

• CategoryTheory.ShortComplex.instZeroHomShortComplexToQuiverToCategoryStructInstCategoryShortComplex = { zero := CategoryTheory.ShortComplex.Hom.mk 0 0 0 }

@[simp]

theorem CategoryTheory.ShortComplex.zero_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) : 0.τ₁ = 0

@[simp]

theorem CategoryTheory.ShortComplex.zero_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) : 0.τ₂ = 0

@[simp]

theorem CategoryTheory.ShortComplex.zero_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) : 0.τ₃ = 0

instance CategoryTheory.ShortComplex.instHasZeroMorphismsShortComplexInstCategoryShortComplex {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Limits.HasZeroMorphisms (CategoryTheory.ShortComplex C)

Equations

• CategoryTheory.ShortComplex.instHasZeroMorphismsShortComplexInstCategoryShortComplex = CategoryTheory.Limits.HasZeroMorphisms.mk

@[simp]

theorem CategoryTheory.ShortComplex.π₁_obj {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.ShortComplex.π₁.toPrefunctor.obj S = S.X₁

@[simp]

theorem CategoryTheory.ShortComplex.π₁_map {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : ∀ {X Y : CategoryTheory.ShortComplex C} (f : X ⟶ Y), CategoryTheory.ShortComplex.π₁.toPrefunctor.map f = f.τ₁

def CategoryTheory.ShortComplex.π₁ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Functor (CategoryTheory.ShortComplex C) C

The first projection functor ShortComplex C ⥤ C.

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.π₂_map {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : ∀ {X Y : CategoryTheory.ShortComplex C} (f : X ⟶ Y), CategoryTheory.ShortComplex.π₂.toPrefunctor.map f = f.τ₂

@[simp]

theorem CategoryTheory.ShortComplex.π₂_obj {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.ShortComplex.π₂.toPrefunctor.obj S = S.X₂

def CategoryTheory.ShortComplex.π₂ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Functor (CategoryTheory.ShortComplex C) C

The second projection functor ShortComplex C ⥤ C.

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.π₃_obj {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.ShortComplex.π₃.toPrefunctor.obj S = S.X₃

@[simp]

theorem CategoryTheory.ShortComplex.π₃_map {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : ∀ {X Y : CategoryTheory.ShortComplex C} (f : X ⟶ Y), CategoryTheory.ShortComplex.π₃.toPrefunctor.map f = f.τ₃

def CategoryTheory.ShortComplex.π₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Functor (CategoryTheory.ShortComplex C) C

The third projection functor ShortComplex C ⥤ C.

Equations

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

instance CategoryTheory.ShortComplex.preservesZeroMorphisms_π₁ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.ShortComplex.π₁

Equations

• (_ : CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.ShortComplex.π₁) = (_ : CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.ShortComplex.π₁)

instance CategoryTheory.ShortComplex.preservesZeroMorphisms_π₂ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.ShortComplex.π₂

Equations

• (_ : CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.ShortComplex.π₂) = (_ : CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.ShortComplex.π₂)

instance CategoryTheory.ShortComplex.preservesZeroMorphisms_π₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.ShortComplex.π₃

Equations

• (_ : CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.ShortComplex.π₃) = (_ : CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.ShortComplex.π₃)

instance CategoryTheory.ShortComplex.instIsIsoX₁τ₁ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (f : S₁ ⟶ S₂) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.τ₁

Equations

• (_ : CategoryTheory.IsIso f.τ₁) = (_ : CategoryTheory.IsIso (CategoryTheory.ShortComplex.π₁.mapIso (CategoryTheory.asIso f)).hom)

instance CategoryTheory.ShortComplex.instIsIsoX₂τ₂ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (f : S₁ ⟶ S₂) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.τ₂

Equations

• (_ : CategoryTheory.IsIso f.τ₂) = (_ : CategoryTheory.IsIso (CategoryTheory.ShortComplex.π₂.mapIso (CategoryTheory.asIso f)).hom)

instance CategoryTheory.ShortComplex.instIsIsoX₃τ₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (f : S₁ ⟶ S₂) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.τ₃

Equations

• (_ : CategoryTheory.IsIso f.τ₃) = (_ : CategoryTheory.IsIso (CategoryTheory.ShortComplex.π₃.mapIso (CategoryTheory.asIso f)).hom)

@[simp]

theorem CategoryTheory.ShortComplex.π₁Toπ₂_app {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.ShortComplex.π₁Toπ₂.app S = S.f

def CategoryTheory.ShortComplex.π₁Toπ₂ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.ShortComplex.π₁ ⟶ CategoryTheory.ShortComplex.π₂

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

Equations

• CategoryTheory.ShortComplex.π₁Toπ₂ = CategoryTheory.NatTrans.mk fun (S : CategoryTheory.ShortComplex C) => S.f

@[simp]

theorem CategoryTheory.ShortComplex.π₂Toπ₃_app {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.ShortComplex.π₂Toπ₃.app S = S.g

def CategoryTheory.ShortComplex.π₂Toπ₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.ShortComplex.π₂ ⟶ CategoryTheory.ShortComplex.π₃

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

Equations

• CategoryTheory.ShortComplex.π₂Toπ₃ = CategoryTheory.NatTrans.mk fun (S : CategoryTheory.ShortComplex C) => S.g

@[simp]

theorem CategoryTheory.ShortComplex.π₁Toπ₂_comp_π₂Toπ₃_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {Z : CategoryTheory.Functor (CategoryTheory.ShortComplex C) C} (h : CategoryTheory.ShortComplex.π₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex.π₁Toπ₂ (CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex.π₂Toπ₃ h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.ShortComplex.π₁Toπ₂_comp_π₂Toπ₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex.π₁Toπ₂ CategoryTheory.ShortComplex.π₂Toπ₃ = 0

@[simp]

theorem CategoryTheory.ShortComplex.map_g {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] : (CategoryTheory.ShortComplex.map S F).g = F.toPrefunctor.map S.g

@[simp]

theorem CategoryTheory.ShortComplex.map_X₁ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] : (CategoryTheory.ShortComplex.map S F).X₁ = F.toPrefunctor.obj S.X₁

@[simp]

theorem CategoryTheory.ShortComplex.map_X₃ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] : (CategoryTheory.ShortComplex.map S F).X₃ = F.toPrefunctor.obj S.X₃

@[simp]

theorem CategoryTheory.ShortComplex.map_f {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] : (CategoryTheory.ShortComplex.map S F).f = F.toPrefunctor.map S.f

@[simp]

theorem CategoryTheory.ShortComplex.map_X₂ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] : (CategoryTheory.ShortComplex.map S F).X₂ = F.toPrefunctor.obj S.X₂

def CategoryTheory.ShortComplex.map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] : CategoryTheory.ShortComplex D

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

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

@[simp]

theorem CategoryTheory.ShortComplex.mapNatTrans_τ₃ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms G] (τ : F ⟶ G) : (CategoryTheory.ShortComplex.mapNatTrans S τ).τ₃ = τ.app S.X₃

@[simp]

theorem CategoryTheory.ShortComplex.mapNatTrans_τ₂ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms G] (τ : F ⟶ G) : (CategoryTheory.ShortComplex.mapNatTrans S τ).τ₂ = τ.app S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.mapNatTrans_τ₁ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms G] (τ : F ⟶ G) : (CategoryTheory.ShortComplex.mapNatTrans S τ).τ₁ = τ.app S.X₁

def CategoryTheory.ShortComplex.mapNatTrans {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms G] (τ : F ⟶ G) : CategoryTheory.ShortComplex.map S F ⟶ CategoryTheory.ShortComplex.map S G

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

Equations

• CategoryTheory.ShortComplex.mapNatTrans S τ = CategoryTheory.ShortComplex.Hom.mk (τ.app S.X₁) (τ.app S.X₂) (τ.app S.X₃)

@[simp]

theorem CategoryTheory.ShortComplex.mapNatIso_hom {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms G] (τ : F ≅ G) : (CategoryTheory.ShortComplex.mapNatIso S τ).hom = CategoryTheory.ShortComplex.mapNatTrans S τ.hom

@[simp]

theorem CategoryTheory.ShortComplex.mapNatIso_inv {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms G] (τ : F ≅ G) : (CategoryTheory.ShortComplex.mapNatIso S τ).inv = CategoryTheory.ShortComplex.mapNatTrans S τ.inv

def CategoryTheory.ShortComplex.mapNatIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [CategoryTheory.Functor.PreservesZeroMorphisms F] [CategoryTheory.Functor.PreservesZeroMorphisms G] (τ : F ≅ G) : CategoryTheory.ShortComplex.map S F ≅ CategoryTheory.ShortComplex.map S G

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

Equations

• CategoryTheory.ShortComplex.mapNatIso S τ = CategoryTheory.Iso.mk (CategoryTheory.ShortComplex.mapNatTrans S τ.hom) (CategoryTheory.ShortComplex.mapNatTrans S τ.inv)

@[simp]

theorem CategoryTheory.Functor.mapShortComplex_map_τ₂ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] : ∀ {X Y : CategoryTheory.ShortComplex C} (φ : X ⟶ Y), ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ).τ₂ = F.toPrefunctor.map φ.τ₂

@[simp]

theorem CategoryTheory.Functor.mapShortComplex_map_τ₃ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] : ∀ {X Y : CategoryTheory.ShortComplex C} (φ : X ⟶ Y), ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ).τ₃ = F.toPrefunctor.map φ.τ₃

@[simp]

theorem CategoryTheory.Functor.mapShortComplex_obj {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.Functor.mapShortComplex F).toPrefunctor.obj S = CategoryTheory.ShortComplex.map S F

@[simp]

theorem CategoryTheory.Functor.mapShortComplex_map_τ₁ {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] : ∀ {X Y : CategoryTheory.ShortComplex C} (φ : X ⟶ Y), ((CategoryTheory.Functor.mapShortComplex F).toPrefunctor.map φ).τ₁ = F.toPrefunctor.map φ.τ₁

def CategoryTheory.Functor.mapShortComplex {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.PreservesZeroMorphisms F] : CategoryTheory.Functor (CategoryTheory.ShortComplex C) (CategoryTheory.ShortComplex D)

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.

@[simp]

theorem CategoryTheory.ShortComplex.isoMk_hom_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e₁ : S₁.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₃).hom.τ₂ = e₂.hom

@[simp]

theorem CategoryTheory.ShortComplex.isoMk_hom_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e₁ : S₁.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₃).hom.τ₃ = e₃.hom

@[simp]

theorem CategoryTheory.ShortComplex.isoMk_hom_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e₁ : S₁.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₃).hom.τ₁ = e₁.hom

@[simp]

theorem CategoryTheory.ShortComplex.isoMk_inv {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e₁ : S₁.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₃).inv = CategoryTheory.ShortComplex.homMk e₁.inv e₂.inv e₃.inv (_ : CategoryTheory.CategoryStruct.comp e₁.inv S₁.f = CategoryTheory.CategoryStruct.comp S₂.f e₂.inv) (_ : CategoryTheory.CategoryStruct.comp e₂.inv S₁.g = CategoryTheory.CategoryStruct.comp S₂.g e₃.inv)

def CategoryTheory.ShortComplex.isoMk {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e₁ : S₁.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.

theorem CategoryTheory.ShortComplex.isIso_of_isIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (f : S₁ ⟶ S₂) [CategoryTheory.IsIso f.τ₁] [CategoryTheory.IsIso f.τ₂] [CategoryTheory.IsIso f.τ₃] : CategoryTheory.IsIso f

@[simp]

theorem CategoryTheory.ShortComplex.op_X₂ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.op S).X₂ = Opposite.op S.X₂

@[simp]

theorem CategoryTheory.ShortComplex.op_X₁ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.op S).X₁ = Opposite.op S.X₃

@[simp]

theorem CategoryTheory.ShortComplex.op_X₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.op S).X₃ = Opposite.op S.X₁

@[simp]

theorem CategoryTheory.ShortComplex.op_g {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.op S).g = S.f.op

@[simp]

theorem CategoryTheory.ShortComplex.op_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : (CategoryTheory.ShortComplex.op S).f = S.g.op

def CategoryTheory.ShortComplex.op {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.ShortComplex Cᵒᵖ

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

Equations

• CategoryTheory.ShortComplex.op S = CategoryTheory.ShortComplex.mk S.g.op S.f.op (_ : CategoryTheory.CategoryStruct.comp S.g.op S.f.op = 0)

@[simp]

theorem CategoryTheory.ShortComplex.opMap_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) : (CategoryTheory.ShortComplex.opMap φ).τ₁ = φ.τ₃.op

@[simp]

theorem CategoryTheory.ShortComplex.opMap_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) : (CategoryTheory.ShortComplex.opMap φ).τ₂ = φ.τ₂.op

@[simp]

theorem CategoryTheory.ShortComplex.opMap_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) : (CategoryTheory.ShortComplex.opMap φ).τ₃ = φ.τ₁.op

def CategoryTheory.ShortComplex.opMap {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) : CategoryTheory.ShortComplex.op S₂ ⟶ CategoryTheory.ShortComplex.op S₁

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

Equations

• CategoryTheory.ShortComplex.opMap φ = CategoryTheory.ShortComplex.Hom.mk φ.τ₃.op φ.τ₂.op φ.τ₁.op

@[simp]

theorem CategoryTheory.ShortComplex.opMap_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.ShortComplex.opMap (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.op S)

@[simp]

theorem CategoryTheory.ShortComplex.unop_X₁ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex Cᵒᵖ) : (CategoryTheory.ShortComplex.unop S).X₁ = S.X₃.unop

@[simp]

theorem CategoryTheory.ShortComplex.unop_X₂ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex Cᵒᵖ) : (CategoryTheory.ShortComplex.unop S).X₂ = S.X₂.unop

@[simp]

theorem CategoryTheory.ShortComplex.unop_X₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex Cᵒᵖ) : (CategoryTheory.ShortComplex.unop S).X₃ = S.X₁.unop

@[simp]

theorem CategoryTheory.ShortComplex.unop_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex Cᵒᵖ) : (CategoryTheory.ShortComplex.unop S).f = S.g.unop

@[simp]

theorem CategoryTheory.ShortComplex.unop_g {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex Cᵒᵖ) : (CategoryTheory.ShortComplex.unop S).g = S.f.unop

def CategoryTheory.ShortComplex.unop {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex Cᵒᵖ) : CategoryTheory.ShortComplex C

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

Equations

• CategoryTheory.ShortComplex.unop S = CategoryTheory.ShortComplex.mk S.g.unop S.f.unop (_ : CategoryTheory.CategoryStruct.comp S.g.unop S.f.unop = 0)

@[simp]

theorem CategoryTheory.ShortComplex.unopMap_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex Cᵒᵖ} {S₂ : CategoryTheory.ShortComplex Cᵒᵖ} (φ : S₁ ⟶ S₂) : (CategoryTheory.ShortComplex.unopMap φ).τ₁ = φ.τ₃.unop

@[simp]

theorem CategoryTheory.ShortComplex.unopMap_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex Cᵒᵖ} {S₂ : CategoryTheory.ShortComplex Cᵒᵖ} (φ : S₁ ⟶ S₂) : (CategoryTheory.ShortComplex.unopMap φ).τ₂ = φ.τ₂.unop

@[simp]

theorem CategoryTheory.ShortComplex.unopMap_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex Cᵒᵖ} {S₂ : CategoryTheory.ShortComplex Cᵒᵖ} (φ : S₁ ⟶ S₂) : (CategoryTheory.ShortComplex.unopMap φ).τ₃ = φ.τ₁.unop

def CategoryTheory.ShortComplex.unopMap {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex Cᵒᵖ} {S₂ : CategoryTheory.ShortComplex Cᵒᵖ} (φ : S₁ ⟶ S₂) : CategoryTheory.ShortComplex.unop S₂ ⟶ CategoryTheory.ShortComplex.unop S₁

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

Equations

• CategoryTheory.ShortComplex.unopMap φ = CategoryTheory.ShortComplex.Hom.mk φ.τ₃.unop φ.τ₂.unop φ.τ₁.unop

@[simp]

theorem CategoryTheory.ShortComplex.unopMap_id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex Cᵒᵖ) : CategoryTheory.ShortComplex.unopMap (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.unop S)

@[simp]

theorem CategoryTheory.ShortComplex.opFunctor_map (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : ∀ {X Y : (CategoryTheory.ShortComplex C)ᵒᵖ} (φ : X ⟶ Y), (CategoryTheory.ShortComplex.opFunctor C).toPrefunctor.map φ = CategoryTheory.ShortComplex.opMap φ.unop

@[simp]

theorem CategoryTheory.ShortComplex.opFunctor_obj (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : (CategoryTheory.ShortComplex C)ᵒᵖ) : (CategoryTheory.ShortComplex.opFunctor C).toPrefunctor.obj S = CategoryTheory.ShortComplex.op S.unop

def CategoryTheory.ShortComplex.opFunctor (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Functor (CategoryTheory.ShortComplex C)ᵒᵖ (CategoryTheory.ShortComplex Cᵒᵖ)

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

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.unopFunctor_obj (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex Cᵒᵖ) : (CategoryTheory.ShortComplex.unopFunctor C).toPrefunctor.obj S = Opposite.op (CategoryTheory.ShortComplex.unop S)

@[simp]

theorem CategoryTheory.ShortComplex.unopFunctor_map (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : ∀ {X Y : CategoryTheory.ShortComplex Cᵒᵖ} (φ : X ⟶ Y), (CategoryTheory.ShortComplex.unopFunctor C).toPrefunctor.map φ = (CategoryTheory.ShortComplex.unopMap φ).op

def CategoryTheory.ShortComplex.unopFunctor (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Functor (CategoryTheory.ShortComplex Cᵒᵖ) (CategoryTheory.ShortComplex C)ᵒᵖ

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

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.opEquiv_inverse (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : (CategoryTheory.ShortComplex.opEquiv C).inverse = CategoryTheory.ShortComplex.unopFunctor C

@[simp]

theorem CategoryTheory.ShortComplex.opEquiv_unitIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : (CategoryTheory.ShortComplex.opEquiv C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.ShortComplex C)ᵒᵖ)

@[simp]

theorem CategoryTheory.ShortComplex.opEquiv_counitIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : (CategoryTheory.ShortComplex.opEquiv C).counitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.comp (CategoryTheory.ShortComplex.unopFunctor C) (CategoryTheory.ShortComplex.opFunctor C))

@[simp]

theorem CategoryTheory.ShortComplex.opEquiv_functor (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : (CategoryTheory.ShortComplex.opEquiv C).functor = CategoryTheory.ShortComplex.opFunctor C

def CategoryTheory.ShortComplex.opEquiv (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : (CategoryTheory.ShortComplex C)ᵒᵖ ≌ CategoryTheory.ShortComplex Cᵒᵖ

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

Equations

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

@[inline, reducible]

abbrev CategoryTheory.ShortComplex.unopOp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex Cᵒᵖ) : CategoryTheory.ShortComplex.op (CategoryTheory.ShortComplex.unop S) ≅ S

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

Equations

• CategoryTheory.ShortComplex.unopOp S = (CategoryTheory.ShortComplex.opEquiv C).counitIso.app S

@[inline, reducible]

abbrev CategoryTheory.ShortComplex.opUnop {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : CategoryTheory.ShortComplex.unop (CategoryTheory.ShortComplex.op S) ≅ S

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

Equations

• CategoryTheory.ShortComplex.opUnop S = CategoryTheory.Iso.unop ((CategoryTheory.ShortComplex.opEquiv C).unitIso.app (Opposite.op S))