@[reducible, inline]

abbrev ProjectiveModules.IsProjectiveModule (R : Type u_1) [Semiring R] (P : Type u_2) [AddCommMonoid P] [Module R P] : Prop

Definition 22.2 (Projective module). An R-module P is projective if it satisfies the lifting property: every surjection f : M → N and every map g : P → N admit a lift h : P → M with f ∘ h = g. Equivalently, P is a direct summand of a free module. Thin wrapper around Mathlib's Module.Projective.

noncomputable def FundamentalHomologicalAlgebra.lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} (f : Y ⟶ Z) (P : CategoryTheory.ProjectiveResolution Y) (Q : FundamentalThm.Resolution Z) : P.complex ⟶ Q.complex

The chain map produced by the Fundamental Theorem of Homological Algebra (Theorem 22.1): any map f : Y → Z between objects of an abelian category lifts to a chain map between any projective resolution of Y and any resolution of Z covering f. See lift_commutes for the relation to the augmentations and liftUniqueUpToHomotopy for uniqueness.

theorem FundamentalHomologicalAlgebra.lift_commutes {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} (f : Y ⟶ Z) (P : CategoryTheory.ProjectiveResolution Y) (Q : FundamentalThm.Resolution Z) : CategoryTheory.CategoryStruct.comp (lift f P Q) Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)

The chain map lift f P Q covers f: composing it with the augmentation of Q agrees with composing the augmentation of P with the chain map associated to f. This is the commutativity clause in the Fundamental Theorem (Theorem 22.1).

noncomputable def FundamentalHomologicalAlgebra.liftUniqueUpToHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} (f : Y ⟶ Z) {P : CategoryTheory.ProjectiveResolution Y} {Q : FundamentalThm.Resolution Z} (g h : P.complex ⟶ Q.complex) (g_comm : CategoryTheory.CategoryStruct.comp g Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)) (h_comm : CategoryTheory.CategoryStruct.comp h Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)) : Homotopy g h

Uniqueness up to chain homotopy in Theorem 22.1: any two chain maps g, h : P.complex → Q.complex between a projective resolution P of Y and a resolution Q of Z, both covering the same map f : Y → Z, are chain homotopic. Combined with lift this produces a well-defined map on derived functors.

noncomputable def FundamentalHomologicalAlgebra.fundamentalTheorem {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} (f : Y ⟶ Z) (P : CategoryTheory.ProjectiveResolution Y) (Q : FundamentalThm.Resolution Z) : { g : P.complex ⟶ Q.complex // CategoryTheory.CategoryStruct.comp g Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f) ∧ ∀ (h : P.complex ⟶ Q.complex), CategoryTheory.CategoryStruct.comp h Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f) → Nonempty (Homotopy g h) }

Theorem 22.1 (Fundamental Theorem of Homological Algebra). Given a map f : Y → Z in an abelian category, a projective resolution P of Y, and any resolution Q of Z, there exists a chain map g : P.complex → Q.complex covering f (i.e. with g ≫ Q.π = P.π ≫ (single₀).map f); moreover any other chain map covering f is chain homotopic to g. This packaged form returns the lift, together with the commutativity equation and the uniqueness statement, all in a single bundled term.