Documentation

Mathlib.Algebra.Homology.ShortComplex.Basic

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.

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 fg = 0.

Instances For
    @[simp]

    the composition of the two given morphisms is zero

    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 : S₁.Hom 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 : S₁.Hom S₂), x = y x.τ₁ = y.τ₁ x.τ₂ = y.τ₂ x.τ₃ = y.τ₃

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

    Instances For

      The identity morphism of a short complex.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem CategoryTheory.ShortComplex.Hom.comp_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : S₁.Hom S₂) (φ₂₃ : S₂.Hom S₃) :
        (φ₁₂.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} (φ₁₂ : S₁.Hom S₂) (φ₂₃ : S₂.Hom S₃) :
        (φ₁₂.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} (φ₁₂ : S₁.Hom S₂) (φ₂₃ : S₂.Hom S₃) :
        (φ₁₂.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} (φ₁₂ : S₁.Hom S₂) (φ₂₃ : S₂.Hom S₃) :
        S₁.Hom S₃

        The composition of morphisms of short complexes.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          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₂₃ = { τ₁ := τ₁, τ₂ := τ₂, τ₃ := τ₃, comm₁₂ := comm₁₂, comm₂₃ := comm₂₃ }
          Instances For
            Equations
            • CategoryTheory.ShortComplex.instZeroHom = { zero := { τ₁ := 0, τ₂ := 0, τ₃ := 0, comm₁₂ := , comm₂₃ := } }
            @[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.π₁.map f = f.τ₁

            The first projection functor ShortComplex C ⥤ C.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[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.π₂.map f = f.τ₂

              The second projection functor ShortComplex C ⥤ C.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[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.π₃.map f = f.τ₃

                The third projection functor ShortComplex C ⥤ C.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  instance CategoryTheory.ShortComplex.preservesZeroMorphisms_π₁ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] :
                  CategoryTheory.ShortComplex.π₁.PreservesZeroMorphisms
                  Equations
                  • =
                  instance CategoryTheory.ShortComplex.preservesZeroMorphisms_π₂ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] :
                  CategoryTheory.ShortComplex.π₂.PreservesZeroMorphisms
                  Equations
                  • =
                  instance CategoryTheory.ShortComplex.preservesZeroMorphisms_π₃ {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] :
                  CategoryTheory.ShortComplex.π₃.PreservesZeroMorphisms
                  Equations
                  • =
                  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
                  Instances For
                    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
                    Instances For
                      @[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

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

                      Equations
                      Instances For
                        @[simp]
                        theorem CategoryTheory.ShortComplex.mapNatTrans_τ₃ {C : Type u_1} {D : Type u_2} [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} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (τ : F G) :
                        (S.mapNatTrans τ).τ₃ = τ.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} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (τ : F G) :
                        (S.mapNatTrans τ).τ₁ = τ.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} [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (τ : F G) :
                        (S.mapNatTrans τ).τ₂ = τ.app S.X₂

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

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

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

                          Equations
                          • S.mapNatIso τ = { hom := S.mapNatTrans τ.hom, inv := S.mapNatTrans τ.inv, hom_inv_id := , inv_hom_id := }
                          Instances For
                            @[simp]
                            @[simp]
                            @[simp]

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

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[simp]
                              theorem CategoryTheory.ShortComplex.isoMk_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₃ comm₁₂ comm₂₃).inv = CategoryTheory.ShortComplex.homMk e₁.inv e₂.inv e₃.inv
                              @[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₃ comm₁₂ comm₂₃).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₃ comm₁₂ comm₂₃).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₃ comm₁₂ comm₂₃).hom.τ₁ = e₁.hom
                              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.
                              Instances For

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

                                Equations
                                Instances For

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

                                  Equations
                                  Instances For

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

                                    Equations
                                    Instances For

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

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

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

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

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

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

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

                                            Equations
                                            Instances For
                                              @[reducible, inline]

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

                                              Equations
                                              Instances For