Documentation

TauCeti.CategoryTheory.Abelian.Projective.Resolution

Chain maps between projective resolutions over the identity #

Mathlib compares two projective resolutions P and Q of the same object X by the lift of the identity of X (CategoryTheory.ProjectiveResolution.homotopyEquiv), which it constructs abstractly from the projectivity of the terms. Often one has an explicit chain map f : P.complex ⟶ Q.complex instead, compatible with the augmentations. Such an f is itself a lift of the identity of X, so it is homotopic to Mathlib's comparison (CategoryTheory.ProjectiveResolution.homotopyOfComm) and is a homotopy equivalence (CategoryTheory.ProjectiveResolution.homotopyEquivOfComm).

source
noncomputable def CategoryTheory.ProjectiveResolution.homotopyOfComm {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X : C} (P Q : ProjectiveResolution X) (f : P.complex ⟶ Q.complex) (hf : CategoryStruct.comp f Q.π = P.π) :
Homotopy f (P.homotopyEquiv Q).hom

A chain map between projective resolutions of X compatible with the augmentations is homotopic to the comparison (homotopyEquiv P Q).hom, the lift of the identity of X.

Instances For
    source
    noncomputable def CategoryTheory.ProjectiveResolution.homotopyEquivOfComm {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X : C} (P Q : ProjectiveResolution X) (f : P.complex ⟶ Q.complex) (hf : CategoryStruct.comp f Q.π = P.π) :
    HomotopyEquiv P.complex Q.complex

    A chain map between projective resolutions of X compatible with the augmentations is a homotopy equivalence; its homotopy inverse is the lift of the identity of X.

    Instances For
      source
      @[simp]
      theorem CategoryTheory.ProjectiveResolution.homotopyEquivOfComm_hom {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X : C} (P Q : ProjectiveResolution X) (f : P.complex ⟶ Q.complex) (hf : CategoryStruct.comp f Q.π = P.π) :
      (P.homotopyEquivOfComm Q f hf).hom = f

      The forward map of the homotopy equivalence is the given chain map.

      source
      @[simp]
      theorem CategoryTheory.ProjectiveResolution.homotopyEquivOfComm_inv {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {X : C} (P Q : ProjectiveResolution X) (f : P.complex ⟶ Q.complex) (hf : CategoryStruct.comp f Q.π = P.π) :
      (P.homotopyEquivOfComm Q f hf).inv = lift (CategoryStruct.id X) Q P

      The homotopy inverse is the lift of the identity from Q to P.