|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Joël Riou. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Joël Riou |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +public import Mathlib.Algebra.Homology.HomotopyCategory.KInjective |
| 9 | +public import Mathlib.Algebra.Homology.CochainComplexOpposite |
| 10 | + |
| 11 | +/-! |
| 12 | +# K-projective cochain complexes |
| 13 | +
|
| 14 | +We define the notion of K-projective cochain complex in an abelian category, |
| 15 | +and show that bounded above complexes of projective objects are K-projective. |
| 16 | +
|
| 17 | +## TODO (@joelriou) |
| 18 | +* Provide an API for computing `Ext`-groups using a projective resolution |
| 19 | +
|
| 20 | +## References |
| 21 | +* [N. Spaltenstein, *Resolutions of unbounded complexes*][spaltenstein1998] |
| 22 | +
|
| 23 | +-/ |
| 24 | + |
| 25 | +@[expose] public section |
| 26 | + |
| 27 | +namespace CochainComplex |
| 28 | + |
| 29 | +open CategoryTheory Limits HomComplex Preadditive Opposite |
| 30 | + |
| 31 | +variable {C : Type*} [Category C] [Abelian C] |
| 32 | + |
| 33 | +-- TODO (@joelriou): show that this definition is equivalent to the |
| 34 | +-- original definition by Spaltenstein saying that whenever `L` |
| 35 | +-- is acyclic, then `HomComplex K L` is acyclic. (The condition below |
| 36 | +-- is equivalent to the acyclicity of `HomComplex K L` in degree |
| 37 | +-- `0`, and the general case follows by shifting `L`.) |
| 38 | +/-- A cochain complex `K` is K-projective if any morphism `K ⟶ L` |
| 39 | +with `L` acyclic is homotopic to zero. -/ |
| 40 | +class IsKProjective (K : CochainComplex C ℤ) : Prop where |
| 41 | + nonempty_homotopy_zero {L : CochainComplex C ℤ} (f : K ⟶ L) : |
| 42 | + L.Acyclic → Nonempty (Homotopy f 0) |
| 43 | + |
| 44 | +/-- A choice of homotopy to zero for a morphism from a |
| 45 | +K-projective cochain complex to an acyclic cochain complex. -/ |
| 46 | +noncomputable irreducible_def IsKProjective.homotopyZero |
| 47 | + {K L : CochainComplex C ℤ} (f : K ⟶ L) |
| 48 | + (hL : L.Acyclic) [K.IsKProjective] : |
| 49 | + Homotopy f 0 := |
| 50 | + (IsKProjective.nonempty_homotopy_zero f hL).some |
| 51 | + |
| 52 | +lemma _root_.HomotopyEquiv.isKProjective {K₁ K₂ : CochainComplex C ℤ} |
| 53 | + (e : HomotopyEquiv K₁ K₂) |
| 54 | + [K₁.IsKProjective] : K₂.IsKProjective where |
| 55 | + nonempty_homotopy_zero {L} f hL := |
| 56 | + ⟨Homotopy.trans (Homotopy.trans (.ofEq (by simp)) |
| 57 | + ((e.homotopyInvHomId.symm.compRight f).trans (.ofEq (by simp)))) |
| 58 | + (((IsKProjective.homotopyZero (e.hom ≫ f) hL).compLeft e.inv).trans (.ofEq (by simp)))⟩ |
| 59 | + |
| 60 | +lemma isKProjective_of_iso {K₁ K₂ : CochainComplex C ℤ} (e : K₁ ≅ K₂) |
| 61 | + [K₁.IsKProjective] : |
| 62 | + K₂.IsKProjective := |
| 63 | + (HomotopyEquiv.ofIso e).isKProjective |
| 64 | + |
| 65 | +lemma isKProjective_iff_of_iso {K₁ K₂ : CochainComplex C ℤ} (e : K₁ ≅ K₂) : |
| 66 | + K₁.IsKProjective ↔ K₂.IsKProjective := |
| 67 | + ⟨fun _ ↦ isKProjective_of_iso e, fun _ ↦ isKProjective_of_iso e.symm⟩ |
| 68 | + |
| 69 | +lemma isKProjective_iff_leftOrthogonal (K : CochainComplex C ℤ) : |
| 70 | + K.IsKProjective ↔ |
| 71 | + (HomotopyCategory.subcategoryAcyclic C).leftOrthogonal |
| 72 | + ((HomotopyCategory.quotient _ _).obj K) := by |
| 73 | + refine ⟨fun _ L f hL ↦ ?_, |
| 74 | + fun hK ↦ ⟨fun {L} f hL ↦ ⟨HomotopyCategory.homotopyOfEq _ _ ?_⟩⟩⟩ |
| 75 | + · obtain ⟨L, rfl⟩ := HomotopyCategory.quotient_obj_surjective L |
| 76 | + obtain ⟨f, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective f |
| 77 | + rw [HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic] at hL |
| 78 | + rw [HomotopyCategory.eq_of_homotopy f 0 (IsKProjective.homotopyZero f hL), Functor.map_zero] |
| 79 | + · rw [← HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic] at hL |
| 80 | + rw [hK ((HomotopyCategory.quotient _ _).map f) hL, Functor.map_zero] |
| 81 | + |
| 82 | +lemma IsKProjective.leftOrthogonal (K : CochainComplex C ℤ) [K.IsKProjective] : |
| 83 | + (HomotopyCategory.subcategoryAcyclic C).leftOrthogonal |
| 84 | + ((HomotopyCategory.quotient _ _).obj K) := by |
| 85 | + rwa [← isKProjective_iff_leftOrthogonal] |
| 86 | + |
| 87 | +instance (K : CochainComplex C ℤ) [hK : K.IsKProjective] (n : ℤ) : |
| 88 | + (K⟦n⟧).IsKProjective := by |
| 89 | + rw [isKProjective_iff_leftOrthogonal] at hK ⊢ |
| 90 | + exact ObjectProperty.prop_of_iso _ |
| 91 | + (((HomotopyCategory.quotient C (.up ℤ)).commShiftIso n).symm.app K) |
| 92 | + ((HomotopyCategory.subcategoryAcyclic C).leftOrthogonal.le_shift n _ hK) |
| 93 | + |
| 94 | +lemma isKProjective_shift_iff (K : CochainComplex C ℤ) (n : ℤ) : |
| 95 | + (K⟦n⟧).IsKProjective ↔ K.IsKProjective := |
| 96 | + ⟨fun _ ↦ isKProjective_of_iso (show K⟦n⟧⟦-n⟧ ≅ K from (shiftEquiv _ n).unitIso.symm.app K), |
| 97 | + fun _ ↦ inferInstance⟩ |
| 98 | + |
| 99 | +lemma isKProjective_of_op {K : CochainComplex C ℤ} |
| 100 | + (hK : IsKInjective ((opEquivalence C).functor.obj (op K))) : |
| 101 | + K.IsKProjective where |
| 102 | + nonempty_homotopy_zero {L} f hL := |
| 103 | + ⟨homotopyUnop ((IsKInjective.homotopyZero |
| 104 | + ((opEquivalence C).functor.map f.op) (acyclic_op hL)).trans |
| 105 | + (.ofEq (by simp)))⟩ |
| 106 | + |
| 107 | +attribute [local simp] opEquivalence ChainComplex.cochainComplexEquivalence in |
| 108 | +open Cochain.InductionUp in |
| 109 | +lemma isKProjective_of_projective (K : CochainComplex C ℤ) (d : ℤ) |
| 110 | + [K.IsStrictlyLE d] [∀ (n : ℤ), Projective (K.X n)] : |
| 111 | + K.IsKProjective := by |
| 112 | + let L := ((opEquivalence C).functor.obj (op K)) |
| 113 | + have (n : ℤ) : Injective (L.X n) := by |
| 114 | + dsimp [L] |
| 115 | + infer_instance |
| 116 | + have : L.IsStrictlyGE (-d) := by |
| 117 | + rw [isStrictlyGE_iff] |
| 118 | + intro i hi |
| 119 | + exact (K.isZero_of_isStrictlyLE d _ (by dsimp; lia)).op |
| 120 | + exact isKProjective_of_op (isKInjective_of_injective L (-d)) |
| 121 | + |
| 122 | +end CochainComplex |
0 commit comments