Documentation

Mathlib.Algebra.Homology.CochainComplexMinus

Bounded above cochain complexes #

In this file, we consider the full subcategory CochainComplex.Minus C of CochainComplex C ℤ consisting of bounded above cochain complexes in a category C.

This file should be kept in sync with Mathlib/Algebra/Homology/CochainComplexPlus.lean.

source
def CochainComplex.minus (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] :
CategoryTheory.ObjectProperty (CochainComplex C ℤ)

The property of cochain complexes that are bounded above.

Equations
Instances For
    source
    theorem CochainComplex.minus_iff (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (K : CochainComplex C ℤ) :
    CochainComplex.minus C K ↔ ∃ (n : ℤ), K.IsStrictlyLE n
    source
    instance CochainComplex.instIsClosedUnderIsomorphismsIntMinus (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] :
    (CochainComplex.minus C).IsClosedUnderIsomorphisms
    source
    @[reducible, inline]
    abbrev CochainComplex.Minus (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] :
    Type (max u_1 v_1)

    The full subcategory of CochainComplex C ℤ consisting of bounded above complexes.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev CochainComplex.Minus.ι (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] :
      CategoryTheory.Functor (Minus C) (CochainComplex C ℤ)

      The inclusion of the full subcategory of bounded above cochain complexes.

      Equations
      Instances For
        source
        def CochainComplex.Minus.fullyFaithfulι (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] :
        (ι C).FullyFaithful

        The inclusion of the full subcategory of bounded above cochain complexes is fully faithful.

        Equations
        Instances For
          source
          instance CochainComplex.Minus.instIsClosedUnderLimitsOfShapeIntMinusOfFinCategoryOfHasLimitsOfShape (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (J : Type u_2) [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] [CategoryTheory.Limits.HasLimitsOfShape J C] :
          (CochainComplex.minus C).IsClosedUnderLimitsOfShape J
          source
          instance CochainComplex.Minus.instIsClosedUnderColimitsOfShapeIntMinusOfFinCategoryOfHasColimitsOfShape (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (J : Type u_2) [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] [CategoryTheory.Limits.HasColimitsOfShape J C] :
          (CochainComplex.minus C).IsClosedUnderColimitsOfShape J
          source
          instance CochainComplex.Minus.instHasFiniteLimits (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] :
          CategoryTheory.Limits.HasFiniteLimits (Minus C)
          source
          instance CochainComplex.Minus.instHasFiniteColimits (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] :
          CategoryTheory.Limits.HasFiniteColimits (Minus C)
          source
          theorem CochainComplex.Minus.mono_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingCospan C] {X Y : Minus C} (f : X ⟶ Y) :
          CategoryTheory.Mono f ↔ CategoryTheory.Mono f.hom
          source
          instance CochainComplex.Minus.instMonoIntHomFullSubcategoryMinusOfHasLimitsOfShapeWalkingCospan (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingCospan C] {X Y : Minus C} (f : X ⟶ Y) [CategoryTheory.Mono f] :
          CategoryTheory.Mono f.hom
          source
          theorem CochainComplex.Minus.epi_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Limits.WalkingSpan C] {X Y : Minus C} (f : X ⟶ Y) :
          CategoryTheory.Epi f ↔ CategoryTheory.Epi f.hom
          source
          instance CochainComplex.Minus.instEpiIntHomFullSubcategoryMinusOfHasColimitsOfShapeWalkingSpan (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Limits.WalkingSpan C] {X Y : Minus C} (f : X ⟶ Y) [CategoryTheory.Epi f] :
          CategoryTheory.Epi f.hom
          source
          def CochainComplex.Minus.quasiIso (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] :
          CategoryTheory.MorphismProperty (Minus C)

          The class of quasi-isomorphisms in the category of bounded above cochain complexes.

          Equations
          Instances For
            source
            theorem CochainComplex.Minus.quasiIso_iff (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] {X Y : Minus C} (f : X ⟶ Y) :
            quasiIso C f ↔ QuasiIso f.hom
            source
            instance CochainComplex.Minus.instHasTwoOutOfThreePropertyQuasiIso (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] :
            (quasiIso C).HasTwoOutOfThreeProperty
            source
            instance CochainComplex.Minus.instIsStableUnderRetractsQuasiIso (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.CategoryWithHomology C] :
            (quasiIso C).IsStableUnderRetracts
            source
            instance CochainComplex.Minus.instIsStableUnderShiftIntMinus (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] :
            (CochainComplex.minus C).IsStableUnderShift ℤ
            source
            instance CochainComplex.Minus.instIsCompatibleWithShiftQuasiIsoInt (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] :
            (quasiIso C).IsCompatibleWithShift ℤ
            source
            @[implicit_reducible]
            def CategoryTheory.Functor.mapCochainComplexMinus {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] [F.PreservesZeroMorphisms] :
            Functor (CochainComplex.Minus C) (CochainComplex.Minus D)

            The functor on categories of bounded above cochain complexes that is induced by a functor (which preserves zero morphisms).

            Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Functor.mapCochainComplexMinus_map_hom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] [F.PreservesZeroMorphisms] {X✝ Y✝ : CochainComplex.Minus C} (f : X✝ ⟶ Y✝) :
              (F.mapCochainComplexMinus.map f).hom = (F.mapHomologicalComplex (ComplexShape.up ℤ)).map f.hom
              source
              @[simp]
              theorem CategoryTheory.Functor.mapCochainComplexMinus_obj_obj {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] [F.PreservesZeroMorphisms] (X : CochainComplex.Minus C) :
              (F.mapCochainComplexMinus.obj X).obj = (F.mapHomologicalComplex (ComplexShape.up ℤ)).obj X.obj
              source
              def CategoryTheory.Functor.mapCochainComplexMinusCompι {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] [F.PreservesZeroMorphisms] :
              F.mapCochainComplexMinus.comp (CochainComplex.Minus.ι D) ≅ (CochainComplex.Minus.ι C).comp (F.mapHomologicalComplex (ComplexShape.up ℤ))

              The isomorphism between F.mapCochainComplexMinus ⋙ CochainComplex.Minus.ι D and CochainComplex.Minus.ι C ⋙ F.mapHomologicalComplex _ when F : C ⥤ D is a functor which preserves zero morphisms

              Equations
              Instances For
                source
                @[simp]
                theorem CategoryTheory.Functor.mapCochainComplexMinusCompι_hom_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] [F.PreservesZeroMorphisms] (X : CochainComplex.Minus C) :
                F.mapCochainComplexMinusCompι.hom.app X = CategoryStruct.id ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj X.obj)
                source
                @[simp]
                theorem CategoryTheory.Functor.mapCochainComplexMinusCompι_inv_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] [F.PreservesZeroMorphisms] (X : CochainComplex.Minus C) :
                F.mapCochainComplexMinusCompι.inv.app X = CategoryStruct.id ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj X.obj)
                source
                @[instance_reducible]
                noncomputable instance CategoryTheory.Functor.instCommShiftMinusMapCochainComplexMinusInt {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [Preadditive C] [Preadditive D] [F.Additive] :
                F.mapCochainComplexMinus.CommShift ℤ
                Equations
                source
                instance CategoryTheory.Functor.instCommShiftMinusCochainComplexIntHomMapCochainComplexMinusCompι {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [Preadditive C] [Preadditive D] [F.Additive] :
                NatTrans.CommShift F.mapCochainComplexMinusCompι.hom ℤ
                source
                theorem CategoryTheory.Functor.homotopyEquivalences_mapCochainComplexMinus_map {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [Preadditive C] [Preadditive D] [F.Additive] {K L : CochainComplex.Minus C} (f : K ⟶ L) (hf : HomologicalComplex.homotopyEquivalences C (ComplexShape.up ℤ) f.hom) :
                HomologicalComplex.homotopyEquivalences D (ComplexShape.up ℤ) (F.mapCochainComplexMinus.map f).hom
                source
                def CategoryTheory.NatTrans.mapCochainComplexMinus {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] {F₁ F₂ : Functor C D} [F₁.Additive] [F₂.Additive] (τ : F₁ ⟶ F₂) :
                F₁.mapCochainComplexMinus ⟶ F₂.mapCochainComplexMinus

                The natural transformation F₁.mapCochainComplexMinus ⟶ F₂.mapCochainComplexMinus induced by a natural transformation F₁ ⟶ F₂.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.NatTrans.mapCochainComplexMinus_app_hom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] {F₁ F₂ : Functor C D} [F₁.Additive] [F₂.Additive] (τ : F₁ ⟶ F₂) (K : CochainComplex.Minus C) :
                  ((mapCochainComplexMinus τ).app K).hom = (mapHomologicalComplex τ (ComplexShape.up ℤ)).app K.obj
                  source
                  @[simp]
                  theorem CategoryTheory.NatTrans.mapCochainComplexMinus_add {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] {F₁ F₂ : Functor C D} [F₁.Additive] [F₂.Additive] (τ τ' : F₁ ⟶ F₂) :
                  mapCochainComplexMinus (τ + τ') = mapCochainComplexMinus τ + mapCochainComplexMinus τ'
                  source
                  @[simp]
                  theorem CategoryTheory.NatTrans.mapCochainComplexMinus_id {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F₁ : Functor C D) [F₁.Additive] :
                  mapCochainComplexMinus (CategoryStruct.id F₁) = CategoryStruct.id F₁.mapCochainComplexMinus
                  source
                  theorem CategoryTheory.NatTrans.mapCochainComplexMinus_comp {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] {F₁ F₂ F₃ : Functor C D} [F₁.Additive] [F₂.Additive] [F₃.Additive] (τ : F₁ ⟶ F₂) (τ' : F₂ ⟶ F₃) :
                  mapCochainComplexMinus (CategoryStruct.comp τ τ') = CategoryStruct.comp (mapCochainComplexMinus τ) (mapCochainComplexMinus τ')
                  source
                  theorem CategoryTheory.NatTrans.mapCochainComplexMinus_comp_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] {F₁ F₂ F₃ : Functor C D} [F₁.Additive] [F₂.Additive] [F₃.Additive] (τ : F₁ ⟶ F₂) (τ' : F₂ ⟶ F₃) {Z : Functor (CochainComplex.Minus C) (CochainComplex.Minus D)} (h : F₃.mapCochainComplexMinus ⟶ Z) :
                  CategoryStruct.comp (mapCochainComplexMinus (CategoryStruct.comp τ τ')) h = CategoryStruct.comp (mapCochainComplexMinus τ) (CategoryStruct.comp (mapCochainComplexMinus τ') h)
                  source
                  instance CategoryTheory.NatTrans.instCommShiftMinusMapCochainComplexMinusInt {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] {F₁ F₂ : Functor C D} [F₁.Additive] [F₂.Additive] (τ : F₁ ⟶ F₂) :
                  CommShift (mapCochainComplexMinus τ) ℤ