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
    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.τ₃

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

    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.

      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.τ₁
        @[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.τ₂
        @[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.τ₃
        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.

        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.

          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.

            Instances For
              @[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✝) :
              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

              Instances For
                @[inline, reducible]

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

                Instances For