Documentation

Mathlib.Algebra.Homology.ShortComplex.Exact

Exact short complexes #

When S : ShortComplex C, this file defines a structure S.Exact which expresses the exactness of S, i.e. there exists a homology data h : S.HomologyData such that h.left.H is zero. When [S.HasHomology], it is equivalent to the assertion IsZero S.homology.

Almost by construction, this notion of exactness is self dual, see Exact.op and Exact.unop.

The assertion that the short complex S : ShortComplex C is exact.

  • condition : ∃ (h : S.HomologyData), CategoryTheory.Limits.IsZero h.left.H

    the condition that there exists an homology data whose left.H field is zero

Instances For

    the condition that there exists an homology data whose left.H field is zero

    theorem CategoryTheory.ShortComplex.exact_iff_i_p_zero {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [S.HasHomology] (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData) :
    S.Exact CategoryTheory.CategoryStruct.comp h₁.i h₂.p = 0
    theorem CategoryTheory.ShortComplex.RightHomologyData.exact_map_iff {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] {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] [(S.map F).HasHomology] :
    (S.map F).Exact CategoryTheory.Limits.IsZero (F.obj h.H)
    theorem CategoryTheory.ShortComplex.Exact.map_of_preservesLeftHomologyOf {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] {S : CategoryTheory.ShortComplex C} (h : S.Exact) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [(S.map F).HasHomology] :
    (S.map F).Exact
    theorem CategoryTheory.ShortComplex.Exact.map_of_preservesRightHomologyOf {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] {S : CategoryTheory.ShortComplex C} (h : S.Exact) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [F.PreservesRightHomologyOf S] [(S.map F).HasHomology] :
    (S.map F).Exact
    theorem CategoryTheory.ShortComplex.Exact.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] {S : CategoryTheory.ShortComplex C} (h : S.Exact) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] :
    (S.map F).Exact
    theorem CategoryTheory.ShortComplex.exact_map_iff_of_faithful {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] (S : CategoryTheory.ShortComplex C) [S.HasHomology] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] [F.Faithful] :
    (S.map F).Exact S.Exact

    Given an exact short complex S and a limit kernel fork kf for S.g, this is the left homology data for S with K := kf.pt and H := 0.

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

      Given an exact short complex S and a colimit cokernel cofork cc for S.f, this is the right homology data for S with Q := cc.pt and H := 0.

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

        A splitting for a short complex S consists of the data of a retraction r : X₂ ⟶ X₁ of S.f and section s : X₃ ⟶ X₂ of S.g which satisfy r ≫ S.f + S.g ≫ s = 𝟙 _

        Instances For

          Given a splitting of a short complex S, this shows that S.f is a split monomorphism.

          Equations
          • s.splitMono_f = { retraction := s.r, id := }
          Instances For

            Given a splitting of a short complex S, this shows that S.g is a split epimorphism.

            Equations
            • s.splitEpi_g = { section_ := s.s, id := }
            Instances For
              theorem CategoryTheory.ShortComplex.Splitting.ext_r {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (s : S.Splitting) (s' : S.Splitting) (h : s.r = s'.r) :
              s = s'
              theorem CategoryTheory.ShortComplex.Splitting.ext_s {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {S : CategoryTheory.ShortComplex C} (s : S.Splitting) (s' : S.Splitting) (h : s.s = s'.s) :
              s = s'

              The left homology data on a short complex equipped with a splitting.

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

                The right homology data on a short complex equipped with a splitting.

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

                  The homology data on a short complex equipped with a splitting.

                  Equations
                  • s.homologyData = { left := s.leftHomologyData, right := s.rightHomologyData, iso := CategoryTheory.Iso.refl 0, comm := }
                  Instances For

                    A short complex equipped with a splitting is exact.

                    If a short complex S is equipped with a splitting, then S.X₁ is the kernel of S.g.

                    Equations
                    • s.fIsKernel = s.homologyData.left.hi
                    Instances For

                      If a short complex S is equipped with a splitting, then S.X₃ is the cokernel of S.f.

                      Equations
                      • s.gIsCokernel = s.homologyData.right.hp
                      Instances For

                        If a short complex S has a splitting and F is an additive functor, then S.map F also has a splitting.

                        Equations
                        • s.map F = { r := F.map s.r, s := F.map s.s, f_r := , s_g := , id := }
                        Instances For

                          A splitting on a short complex induces splittings on isomorphic short complexes.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            noncomputable def CategoryTheory.ShortComplex.Splitting.ofHasBinaryBiproduct {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (X₁ : C) (X₂ : C) [CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂] :
                            (CategoryTheory.ShortComplex.mk CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.snd ).Splitting

                            The obvious splitting of the short complex X₁ ⟶ X₁ ⊞ X₂ ⟶ X₂.

                            Equations
                            Instances For

                              The obvious splitting of a short complex when S.X₁ is zero and S.g is an isomorphism.

                              Equations
                              Instances For

                                The obvious splitting of a short complex when S.f is an isomorphism and S.X₃ is zero.

                                Equations
                                Instances For

                                  The splitting of the short complex S.op deduced from a splitting of S.

                                  Equations
                                  • h.op = { r := h.s.op, s := h.r.op, f_r := , s_g := , id := }
                                  Instances For

                                    The splitting of the short complex S.unop deduced from a splitting of S.

                                    Equations
                                    • h.unop = { r := h.s.unop, s := h.r.unop, f_r := , s_g := , id := }
                                    Instances For

                                      The isomorphism S.X₂ ≅ S.X₁ ⊞ S.X₃ induced by a splitting of the short complex S.

                                      Equations
                                      Instances For

                                        In a balanced category, if a short complex S is exact and S.f is a mono, then S.X₁ is the kernel of S.g.

                                        Equations
                                        Instances For

                                          In a balanced category, if a short complex S is exact and S.g is an epi, then S.X₃ is the cokernel of S.g.

                                          Equations
                                          Instances For

                                            If a short complex S in a balanced category is exact and such that S.f is a mono, then a morphism k : A ⟶ S.X₂ such that k ≫ S.g = 0 lifts to a morphism A ⟶ S.X₁.

                                            Equations
                                            Instances For

                                              If a short complex S in a balanced category is exact and such that S.g is an epi, then a morphism k : S.X₂ ⟶ A such that S.f ≫ k = 0 descends to a morphism S.X₃ ⟶ A.

                                              Equations
                                              Instances For
                                                theorem CategoryTheory.ShortComplex.quasiIso_iff_of_zeros {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) :

                                                Given a morphism of short complexes φ : S₁ ⟶ S₂ in an abelian category, if S₁.f and S₁.g are zero (e.g. when S₁ is of the form 0 ⟶ S₁.X₂ ⟶ 0) and S₂.f = 0 (e.g when S₂ is of the form 0 ⟶ S₂.X₂ ⟶ S₂.X₃), then φ is a quasi-isomorphism iff the obvious short complex S₁.X₂ ⟶ S₂.X₂ ⟶ S₂.X₃ is exact and φ.τ₂ is a mono).

                                                theorem CategoryTheory.ShortComplex.quasiIso_iff_of_zeros' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) :

                                                Given a morphism of short complexes φ : S₁ ⟶ S₂ in an abelian category, if S₁.g = 0 (e.g when S₁ is of the form S₁.X₁ ⟶ S₁.X₂ ⟶ 0) and both S₂.f and S₂.g are zero (e.g when S₂ is of the form 0 ⟶ S₂.X₂ ⟶ 0), then φ is a quasi-isomorphism iff the obvious short complex S₁.X₂ ⟶ S₁.X₂ ⟶ S₂.X₂ is exact and φ.τ₂ is an epi).

                                                If S is an exact short complex and f : S.X₂ ⟶ J is a morphism to an injective object J such that S.f ≫ f = 0, this is a morphism φ : S.X₃ ⟶ J such that S.g ≫ φ = f.

                                                Equations
                                                Instances For

                                                  If S is an exact short complex and f : P ⟶ S.X₂ is a morphism from a projective object P such that f ≫ S.g = 0, this is a morphism φ : P ⟶ S.X₁ such that φ ≫ S.f = f.

                                                  Equations
                                                  Instances For
                                                    @[deprecated CategoryTheory.ShortComplex.Exact.liftFromProjective]

                                                    Alias of CategoryTheory.ShortComplex.Exact.liftFromProjective.


                                                    If S is an exact short complex and f : P ⟶ S.X₂ is a morphism from a projective object P such that f ≫ S.g = 0, this is a morphism φ : P ⟶ S.X₁ such that φ ≫ S.f = f.

                                                    Equations
                                                    Instances For
                                                      @[deprecated CategoryTheory.ShortComplex.Exact.liftFromProjective_comp]

                                                      Alias of CategoryTheory.ShortComplex.Exact.liftFromProjective_comp.

                                                      @[deprecated CategoryTheory.ShortComplex.Exact.descToInjective]

                                                      Alias of CategoryTheory.ShortComplex.Exact.descToInjective.


                                                      If S is an exact short complex and f : S.X₂ ⟶ J is a morphism to an injective object J such that S.f ≫ f = 0, this is a morphism φ : S.X₃ ⟶ J such that S.g ≫ φ = f.

                                                      Equations
                                                      Instances For
                                                        @[deprecated CategoryTheory.ShortComplex.Exact.comp_descToInjective]

                                                        Alias of CategoryTheory.ShortComplex.Exact.comp_descToInjective.

                                                        This is the splitting of a short complex S in a balanced category induced by a section of the morphism S.g : S.X₂ ⟶ S.X₃

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

                                                          This is the splitting of a short complex S in a balanced category induced by a retraction of the morphism S.f : S.X₁ ⟶ S.X₂

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