structure FundamentalThm.Resolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (Z : C) : Type (max u v)

A resolution of an object Z in an abelian category: a chain complex equipped with a quasi-isomorphism to the chain complex concentrated in degree zero on Z.

• complex : ChainComplex C ℕ
• hasHomology (i : ℕ) : HomologicalComplex.HasHomology self.complex i
• π : self.complex ⟶ (ChainComplex.single₀ C).obj Z
• quasiIso : QuasiIso self.π

instance FundamentalThm.Resolution.instHasHomologyNatComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Z : C} (Q : Resolution Z) (i : ℕ) : HomologicalComplex.HasHomology Q.complex i

The underlying complex of a resolution has homology objects in every degree.

instance FundamentalThm.Resolution.instQuasiIsoNatπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Z : C} (Q : Resolution Z) : QuasiIso Q.π

The augmentation map of a resolution is a quasi-isomorphism.

@[simp]

theorem FundamentalThm.Resolution.complex_d_comp_π_f_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Z : C} (Q : Resolution Z) : CategoryTheory.CategoryStruct.comp (Q.complex.d 1 0) (Q.π.f 0) = 0

The composite of the differential d : E₁ ⟶ E₀ followed by the augmentation E₀ ⟶ Z vanishes, since the augmentation is a chain map into the complex concentrated in degree zero.

theorem FundamentalThm.Resolution.π_f_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Z : C} (Q : Resolution Z) (n : ℕ) : Q.π.f (n + 1) = 0

In positive degree the augmentation map of a resolution is zero, since the target chain complex is concentrated in degree zero.

noncomputable def FundamentalThm.Resolution.cokernelCofork {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Z : C} (Q : Resolution Z) : CategoryTheory.Limits.CokernelCofork (Q.complex.d 1 0)

The cokernel cofork on d : E₁ ⟶ E₀ given by the augmentation π : E₀ ⟶ Z.

noncomputable def FundamentalThm.Resolution.isColimitCokernelCofork {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Z : C} (Q : Resolution Z) : CategoryTheory.Limits.IsColimit Q.cokernelCofork

The augmentation π : E₀ ⟶ Z exhibits Z as the cokernel of d : E₁ ⟶ E₀, since the underlying complex is exact in degree zero as a consequence of π being a quasi-isomorphism.

theorem FundamentalThm.Resolution.exact₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Z : C} (Q : Resolution Z) : { X₁ := Q.complex.X 1, X₂ := Q.complex.X 0, X₃ := ((ChainComplex.single₀ C).obj Z).X 0, f := Q.complex.d 1 0, g := Q.π.f 0, zero := ⋯ }.Exact

The short complex E₁ ⟶ E₀ ⟶ Z formed by the differential and the augmentation is exact.

instance FundamentalThm.Resolution.epi_π_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Z : C} (Q : Resolution Z) (n : ℕ) : CategoryTheory.Epi (Q.π.f n)

Every component of the augmentation of a resolution is an epimorphism.

theorem FundamentalThm.Resolution.complex_exactAt_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Z : C} (Q : Resolution Z) (n : ℕ) : HomologicalComplex.ExactAt Q.complex (n + 1)

The underlying chain complex of a resolution is exact in every positive degree.

theorem FundamentalThm.Resolution.exact_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Z : C} (Q : Resolution Z) (n : ℕ) : { X₁ := Q.complex.X (n + 2), X₂ := Q.complex.X (n + 1), X₃ := Q.complex.X n, f := Q.complex.d (n + 2) (n + 1), g := Q.complex.d (n + 1) n, zero := ⋯ }.Exact

The short complex E_{n+2} ⟶ E_{n+1} ⟶ E_n formed by consecutive differentials is exact, expressing exactness of the resolution in positive degrees.

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

The degree-zero component of the lift of f : Y ⟶ Z to a chain map between resolutions: factor P.π.f 0 ≫ f through the epi Q.π.f 0, using projectivity of P.complex.X 0.

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

The degree-one component of the lift of f to a chain map: use exactness of Q at degree zero together with projectivity of P.complex.X 1 to lift d ≫ liftFZero f P Q along d.

@[simp]

theorem FundamentalThm.liftFOne_zero_comm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} (f : Y ⟶ Z) (P : CategoryTheory.ProjectiveResolution Y) (Q : Resolution Z) : CategoryTheory.CategoryStruct.comp (liftFOne f P Q) (Q.complex.d 1 0) = CategoryTheory.CategoryStruct.comp (P.complex.d 1 0) (liftFZero f P Q)

Commutativity of the lifted square in degree 1 ↔ 0: liftFOne and liftFZero form a commuting square against the differentials.

noncomputable def FundamentalThm.liftFSucc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} (P : CategoryTheory.ProjectiveResolution Y) (Q : Resolution Z) (n : ℕ) (g : P.complex.X n ⟶ Q.complex.X n) (g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 1)) (w : CategoryTheory.CategoryStruct.comp g' (Q.complex.d (n + 1) n) = CategoryTheory.CategoryStruct.comp (P.complex.d (n + 1) n) g) : (g'' : P.complex.X (n + 2) ⟶ Q.complex.X (n + 2)) ×' CategoryTheory.CategoryStruct.comp g'' (Q.complex.d (n + 2) (n + 1)) = CategoryTheory.CategoryStruct.comp (P.complex.d (n + 2) (n + 1)) g'

Inductive step in constructing the lift: given commuting squares in degrees n and n+1, produce a degree-n+2 lift that fits into the next commuting square. This uses exactness of Q together with projectivity in degree n+2.

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

Existence half of Theorem 22.1 (Fundamental Theorem of Homological Algebra): given f : Y ⟶ Z, a projective resolution of Y, and a resolution of Z, we obtain a chain map P.complex ⟶ Q.complex lifting f, by assembling the degree-zero, degree-one, and inductive degree-n+2 components.

@[simp]

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

The lift lift f P Q is compatible with the augmentations: composing it with Q.π recovers P.π followed by the chain map induced by f.

@[simp]

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

The lift lift f P Q is compatible with the augmentations: composing it with Q.π recovers P.π followed by the chain map induced by f.

noncomputable def FundamentalThm.liftHomotopyZeroZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : Resolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0) : P.complex.X 0 ⟶ Q.complex.X 1

Degree-zero component of the chain homotopy to zero: if a chain map f : P → Q becomes zero after composing with Q.π, lift f.f 0 along the differential d : Q₁ ⟶ Q₀ using exactness of Q at degree zero and projectivity of P.complex.X 0.

@[simp]

theorem FundamentalThm.liftHomotopyZeroZero_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : Resolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0) : CategoryTheory.CategoryStruct.comp (liftHomotopyZeroZero f comm) (Q.complex.d 1 0) = f.f 0

The defining identity of liftHomotopyZeroZero: composing with the differential d : Q₁ ⟶ Q₀ recovers f.f 0.

@[simp]

theorem FundamentalThm.liftHomotopyZeroZero_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : Resolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0) {Z✝ : C} (h : Q.complex.X 0 ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (liftHomotopyZeroZero f comm) (CategoryTheory.CategoryStruct.comp (Q.complex.d 1 0) h) = CategoryTheory.CategoryStruct.comp (f.f 0) h

The defining identity of liftHomotopyZeroZero: composing with the differential d : Q₁ ⟶ Q₀ recovers f.f 0.

noncomputable def FundamentalThm.liftHomotopyZeroOne {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : Resolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0) : P.complex.X 1 ⟶ Q.complex.X 2

Degree-one component of the chain homotopy to zero: lift the corrected morphism f.f 1 - d ≫ liftHomotopyZeroZero f comm along d : Q₂ ⟶ Q₁ using exactness of Q in positive degree and projectivity of P.complex.X 1.

@[simp]

theorem FundamentalThm.liftHomotopyZeroOne_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : Resolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0) : CategoryTheory.CategoryStruct.comp (liftHomotopyZeroOne f comm) (Q.complex.d 2 1) = f.f 1 - CategoryTheory.CategoryStruct.comp (P.complex.d 1 0) (liftHomotopyZeroZero f comm)

The defining identity of liftHomotopyZeroOne: composing with d : Q₂ ⟶ Q₁ recovers the corrected morphism f.f 1 - d ≫ liftHomotopyZeroZero f comm.

@[simp]

theorem FundamentalThm.liftHomotopyZeroOne_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : Resolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0) {Z✝ : C} (h : Q.complex.X 1 ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (liftHomotopyZeroOne f comm) (CategoryTheory.CategoryStruct.comp (Q.complex.d 2 1) h) = CategoryTheory.CategoryStruct.comp (f.f 1 - CategoryTheory.CategoryStruct.comp (P.complex.d 1 0) (liftHomotopyZeroZero f comm)) h

The defining identity of liftHomotopyZeroOne: composing with d : Q₂ ⟶ Q₁ recovers the corrected morphism f.f 1 - d ≫ liftHomotopyZeroZero f comm.

noncomputable def FundamentalThm.liftHomotopyZeroSucc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : Resolution Z} (f : P.complex ⟶ Q.complex) (n : ℕ) (g : P.complex.X n ⟶ Q.complex.X (n + 1)) (g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) (w : f.f (n + 1) = CategoryTheory.CategoryStruct.comp (P.complex.d (n + 1) n) g + CategoryTheory.CategoryStruct.comp g' (Q.complex.d (n + 2) (n + 1))) : P.complex.X (n + 2) ⟶ Q.complex.X (n + 3)

Inductive step in building the chain homotopy to zero: given chain homotopy data in degrees n and n+1, produce the next degree-n+2 piece via exactness of Q in positive degree and projectivity of P.complex.X (n+2).

@[simp]

theorem FundamentalThm.liftHomotopyZeroSucc_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : Resolution Z} (f : P.complex ⟶ Q.complex) (n : ℕ) (g : P.complex.X n ⟶ Q.complex.X (n + 1)) (g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) (w : f.f (n + 1) = CategoryTheory.CategoryStruct.comp (P.complex.d (n + 1) n) g + CategoryTheory.CategoryStruct.comp g' (Q.complex.d (n + 2) (n + 1))) : CategoryTheory.CategoryStruct.comp (liftHomotopyZeroSucc f n g g' w) (Q.complex.d (n + 3) (n + 2)) = f.f (n + 2) - CategoryTheory.CategoryStruct.comp (P.complex.d (n + 2) (n + 1)) g'

The defining identity of liftHomotopyZeroSucc: composing with the differential recovers the corrected morphism f.f (n+2) - d ≫ g'.

@[simp]

theorem FundamentalThm.liftHomotopyZeroSucc_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : Resolution Z} (f : P.complex ⟶ Q.complex) (n : ℕ) (g : P.complex.X n ⟶ Q.complex.X (n + 1)) (g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) (w : f.f (n + 1) = CategoryTheory.CategoryStruct.comp (P.complex.d (n + 1) n) g + CategoryTheory.CategoryStruct.comp g' (Q.complex.d (n + 2) (n + 1))) {Z✝ : C} (h : Q.complex.X (n + 2) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (liftHomotopyZeroSucc f n g g' w) (CategoryTheory.CategoryStruct.comp (Q.complex.d (n + 3) (n + 2)) h) = CategoryTheory.CategoryStruct.comp (f.f (n + 2) - CategoryTheory.CategoryStruct.comp (P.complex.d (n + 2) (n + 1)) g') h

The defining identity of liftHomotopyZeroSucc: composing with the differential recovers the corrected morphism f.f (n+2) - d ≫ g'.

noncomputable def FundamentalThm.liftHomotopyZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} {P : CategoryTheory.ProjectiveResolution Y} {Q : Resolution Z} (f : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0) : Homotopy f 0

Any chain map f : P → Q from a projective resolution to a resolution that becomes zero after composing with the augmentation Q.π is chain-homotopic to zero, by assembling the degree-zero, degree-one, and inductive degree-n+2 components.

noncomputable def FundamentalThm.liftHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y Z : C} (f : Y ⟶ Z) {P : CategoryTheory.ProjectiveResolution Y} {Q : 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 half of Theorem 22.1 (Fundamental Theorem of Homological Algebra): any two chain maps g, h : P.complex ⟶ Q.complex lifting the same f : Y ⟶ Z are chain homotopic.