Documentation

TauCeti.CategoryTheory.Exact.Resolution.ChainComplex

The chain complex of a finite resolution #

A finite P-resolution of X in an exact category is a chain of conflations

K₁ ↪ Q₀ ↠ X,   K₂ ↪ Q₁ ↠ K₁,   …,   Kₙ ↪ Qₙ₋₁ ↠ Kₙ₋₁

ending at a syzygy Kₙ satisfying P. Splicing the conflations together gives the bounded chain complex

0 ⟶ Kₙ ⟶ Qₙ₋₁ ⟶ ⋯ ⟶ Q₁ ⟶ Q₀

augmented by the deflation Q₀ ↠ X: the differential Qₖ₊₁ ⟶ Qₖ is the composite Qₖ₊₁ ↠ Kₖ₊₁ ↪ Qₖ, and the terms beyond Kₙ are zero. This file constructs that complex from the recursive data, so that the comparison theory of resolutions can be phrased with Mathlib's chain maps and chain homotopies.

The construction commutes with conflation-exact functors: the complex of the image of a resolution under such a functor F is the image under F of its complex. This is what makes the comparison theory functorial, and in particular compatible with the grading shift of a graded exact category.

Main definitions #

Main results #

Implementation notes #

TauCeti.ExactStructure.FiniteResolution.term is exposed, for the same reason as TauCeti.ExactStructure.FiniteResolution.syzygy: it is the type index of the augmentation, of the differential, and of every family of morphisms between the complexes of two resolutions, and the recursive constructions of those families only typecheck when (step … r).term (n + 1) reduces to r.term n. It is moreover reducible, so that simp and rw unify a morphism typed with (step … r).term (n + 1) against one typed with r.term n; without this every lemma mixing the two would need an explicit rfl step. The price is that the equation lemmas of term are not simp lemmas: simp indexes left-hand sides at reducible transparency, so (base hX).term 0 is unfolded before it could be matched and the lemmas would never fire. They are stated for rw and term-mode use. The augmentation and the differential are sealed behind their equations. toChainComplex is an abbreviation, exactly as Mathlib's ChainComplex.of is, so that its terms are the terms of the resolution definitionally; simp therefore computes its differentials through ChainComplex.of_d, and toChainComplex_d is the rw form of that lemma.

References #

source
@[reducible]
noncomputable def TauCeti.ExactStructure.FiniteResolution.term {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} :
E.FiniteResolution P X → ℕ → C

The n-th term of the chain complex of a finite resolution: the resolving term Qₙ for n below the length, the last syzygy Kₙ in degree n equal to the length, and a zero object beyond.

Equations
Instances For
    source
    theorem TauCeti.ExactStructure.FiniteResolution.term_base_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (hX : P X) :
    (base hX).term 0 = X
    source
    theorem TauCeti.ExactStructure.FiniteResolution.term_base_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (hX : P X) (n : ℕ) :
    (base hX).term (n + 1) = 0
    source
    theorem TauCeti.ExactStructure.FiniteResolution.term_step_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {K Q X : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) :
    (step hQ i p zero hp r).term 0 = Q
    source
    theorem TauCeti.ExactStructure.FiniteResolution.term_step_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {K Q X : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) (n : ℕ) :
    (step hQ i p zero hp r).term (n + 1) = r.term n
    source
    theorem TauCeti.ExactStructure.FiniteResolution.prop_term_of_le_length {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (r : E.FiniteResolution P X) {n : ℕ} (hn : n ≤ r.length) :
    P (r.term n)

    Every term of index at most the length satisfies P.

    source
    theorem TauCeti.ExactStructure.FiniteResolution.isZero_term_of_length_lt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (r : E.FiniteResolution P X) {n : ℕ} (hn : r.length < n) :
    CategoryTheory.Limits.IsZero (r.term n)

    Every term of index beyond the length is a zero object.

    source
    noncomputable def TauCeti.ExactStructure.FiniteResolution.aug {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (r : E.FiniteResolution P X) :
    r.term 0 ⟶ X

    The augmentation of the complex of a resolution: the deflation Q₀ ↠ X of its first conflation, or the identity of X for the empty chain.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.ExactStructure.FiniteResolution.aug_base {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (hX : P X) :
      (base hX).aug = CategoryTheory.CategoryStruct.id X
      source
      @[simp]
      theorem TauCeti.ExactStructure.FiniteResolution.aug_step {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {K Q X : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) :
      (step hQ i p zero hp r).aug = p
      source
      theorem TauCeti.ExactStructure.FiniteResolution.isDeflation_aug {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (r : E.FiniteResolution P X) :
      E.IsDeflation r.aug

      The augmentation is a deflation.

      source
      noncomputable def TauCeti.ExactStructure.FiniteResolution.d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (r : E.FiniteResolution P X) (n : ℕ) :
      r.term (n + 1) ⟶ r.term n

      The differential Qₙ₊₁ ⟶ Qₙ of the complex of a resolution: the composite of the deflation Qₙ₊₁ ↠ Kₙ₊₁ with the inflation Kₙ₊₁ ↪ Qₙ.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.ExactStructure.FiniteResolution.d_base {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (hX : P X) (n : ℕ) :
        (base hX).d n = 0
        source
        @[simp]
        theorem TauCeti.ExactStructure.FiniteResolution.d_step_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {K Q X : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) :
        (step hQ i p zero hp r).d 0 = CategoryTheory.CategoryStruct.comp r.aug i
        source
        @[simp]
        theorem TauCeti.ExactStructure.FiniteResolution.d_step_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {K Q X : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) (n : ℕ) :
        (step hQ i p zero hp r).d (n + 1) = r.d n
        source
        @[simp]
        theorem TauCeti.ExactStructure.FiniteResolution.d_comp_aug {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (r : E.FiniteResolution P X) :
        CategoryTheory.CategoryStruct.comp (r.d 0) r.aug = 0

        The augmentation kills the first differential.

        source
        @[simp]
        theorem TauCeti.ExactStructure.FiniteResolution.d_comp_aug_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (r : E.FiniteResolution P X) {Z : C} (h : X ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (r.d 0) (CategoryTheory.CategoryStruct.comp r.aug h) = CategoryTheory.CategoryStruct.comp 0 h

        The augmentation kills the first differential.

        source
        @[simp]
        theorem TauCeti.ExactStructure.FiniteResolution.d_comp_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (r : E.FiniteResolution P X) (n : ℕ) :
        CategoryTheory.CategoryStruct.comp (r.d (n + 1)) (r.d n) = 0

        The differentials square to zero.

        source
        @[simp]
        theorem TauCeti.ExactStructure.FiniteResolution.d_comp_d_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (r : E.FiniteResolution P X) (n : ℕ) {Z : C} (h : r.term n ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (r.d (n + 1)) (CategoryTheory.CategoryStruct.comp (r.d n) h) = CategoryTheory.CategoryStruct.comp 0 h

        The differentials square to zero.

        source
        @[reducible, inline]
        noncomputable abbrev TauCeti.ExactStructure.FiniteResolution.toChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (r : E.FiniteResolution P X) :
        ChainComplex C ℕ

        The chain complex of a finite resolution: the resolving terms with the spliced differentials, Kₙ in degree n equal to the length, and zero beyond.

        Equations
        Instances For
          source
          theorem TauCeti.ExactStructure.FiniteResolution.toChainComplex_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {X : C} (r : E.FiniteResolution P X) (n : ℕ) :
          r.toChainComplex.d (n + 1) n = r.d n

          The differential of the complex in consecutive degrees. Not a simp lemma, since simp proves it from ChainComplex.of_d through the abbreviation; it is the form rw can use, which does not see ChainComplex.of.d through the abbreviation, and unifies with offset degrees such as r.toChainComplex.d (n + 2) (n + 1).

          source
          noncomputable def TauCeti.ExactStructure.FiniteResolution.termMapIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (hPP' : P ≤ P'.inverseImage F) {X : C} (r : E.FiniteResolution P X) (n : ℕ) :
          (map hF hPP' r).term n ≅ F.obj (r.term n)

          The terms of the image of a resolution under a conflation-exact functor F are the images of its terms: the identity in degrees up to the length, and the isomorphism 0 ≅ F 0 beyond it.

          Equations
          Instances For
            source
            @[simp]
            theorem TauCeti.ExactStructure.FiniteResolution.termMapIso_base_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (hPP' : P ≤ P'.inverseImage F) {X : C} (hX : P X) :
            termMapIso hF hPP' (base hX) 0 = CategoryTheory.Iso.refl (F.obj X)
            source
            @[simp]
            theorem TauCeti.ExactStructure.FiniteResolution.termMapIso_base_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (hPP' : P ≤ P'.inverseImage F) {X : C} (hX : P X) (n : ℕ) :
            termMapIso hF hPP' (base hX) (n + 1) = F.mapZeroObject.symm
            source
            @[simp]
            theorem TauCeti.ExactStructure.FiniteResolution.termMapIso_step_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (hPP' : P ≤ P'.inverseImage F) {K Q X : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) :
            termMapIso hF hPP' (step hQ i p zero hp r) 0 = CategoryTheory.Iso.refl (F.obj Q)
            source
            @[simp]
            theorem TauCeti.ExactStructure.FiniteResolution.termMapIso_step_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (hPP' : P ≤ P'.inverseImage F) {K Q X : C} (hQ : P Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution P K) (n : ℕ) :
            termMapIso hF hPP' (step hQ i p zero hp r) (n + 1) = termMapIso hF hPP' r n
            source
            @[simp]
            theorem TauCeti.ExactStructure.FiniteResolution.aug_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (hPP' : P ≤ P'.inverseImage F) {X : C} (r : E.FiniteResolution P X) :
            (map hF hPP' r).aug = CategoryTheory.CategoryStruct.comp (termMapIso hF hPP' r 0).hom (F.map r.aug)

            The augmentation of the image of a resolution is the image of its augmentation.

            source
            @[simp]
            theorem TauCeti.ExactStructure.FiniteResolution.d_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (hPP' : P ≤ P'.inverseImage F) {X : C} (r : E.FiniteResolution P X) (n : ℕ) :
            (map hF hPP' r).d n = CategoryTheory.CategoryStruct.comp (termMapIso hF hPP' r (n + 1)).hom (CategoryTheory.CategoryStruct.comp (F.map (r.d n)) (termMapIso hF hPP' r n).inv)

            The differentials of the image of a resolution are the images of its differentials.

            source
            noncomputable def TauCeti.ExactStructure.FiniteResolution.toChainComplexMapIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (hPP' : P ≤ P'.inverseImage F) {X : C} (r : E.FiniteResolution P X) :
            (map hF hPP' r).toChainComplex ≅ (F.mapHomologicalComplex (ComplexShape.down ℕ)).obj r.toChainComplex

            The complex of the image of a resolution under a conflation-exact functor F is the image of its complex under F.

            Equations
            Instances For
              source
              @[simp]
              theorem TauCeti.ExactStructure.FiniteResolution.toChainComplexMapIso_hom_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (hPP' : P ≤ P'.inverseImage F) {X : C} (r : E.FiniteResolution P X) (n : ℕ) :
              (toChainComplexMapIso hF hPP' r).hom.f n = (termMapIso hF hPP' r n).hom
              source
              @[simp]
              theorem TauCeti.ExactStructure.FiniteResolution.toChainComplexMapIso_inv_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {P' : CategoryTheory.ObjectProperty D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (hPP' : P ≤ P'.inverseImage F) {X : C} (r : E.FiniteResolution P X) (n : ℕ) :
              (toChainComplexMapIso hF hPP' r).inv.f n = (termMapIso hF hPP' r n).inv