RectificationAcyclic.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.RectificationAcyclic.cone_acyclic line 13
Source documentation
The ordinary cone of a quasi-isomorphism is acyclic.
```
theorem cone_acyclic {K L : CochainComplex C ℤ} (f : K ⟶ L) [QuasiIso f] :
    (mappingCone f).Acyclic := by
…
```
theorem OAI.LittleFinitistic.RectificationAcyclic.short_exact_total_acyclic line 26
Source documentation
The total of a strict short exact sequence of complexes is acyclic. This is applied to the associated graded source-index pieces in rectification.
```
theorem short_exact_total_acyclic (S : ShortComplex (CochainComplex C ℤ))
    (hS : S.ShortExact) :
    (RectificationTotal.total S.g S.f (Homotopy.ofEq S.zero)).Acyclic := by
…
```
Mentions: OAI.LittleFinitistic.RectificationTotal.total

def OAI.LittleFinitistic.RectificationAcyclic.contractBoundedProjective line 39

Source documentation

Bounded-above acyclic complexes of projectives admit an actual contraction.

noncomputable def contractBoundedProjective (K : CochainComplex C ℤ) (hi : ℤ)
    [K.IsStrictlyLE hi] [∀ i, Projective (K.X i)] (hK : K.Acyclic) :
    Homotopy (𝟙 K) 0 := by
…

theorem OAI.LittleFinitistic.RectificationAcyclic.bounded_projective_homotopy_inverse line 47

Source documentation

A quasi-isomorphism between bounded-above projective complexes has an actual chain-map inverse up to specified homotopies, retaining the given forward map.

theorem bounded_projective_homotopy_inverse {K L : CochainComplex C ℤ}
    (f : K ⟶ L) [QuasiIso f] (hi : ℤ) [K.IsStrictlyLE hi] [L.IsStrictlyLE hi]
    [∀ i, Projective (K.X i)] [∀ i, Projective (L.X i)] :
    ∃ g : L ⟶ K, Nonempty (Homotopy (f ≫ g) (𝟙 K)) ∧
      Nonempty (Homotopy (g ≫ f) (𝟙 L)) := by
…

theorem OAI.LittleFinitistic.RectificationAcyclic.finite_exact_filtration_acyclic line 79

Source documentation

A finite decreasing filtration with acyclic successive quotients is acyclic. The hypotheses are actual short exact sequences of complexes.

theorem finite_exact_filtration_acyclic (n : ℕ)
    (F G : ℕ → CochainComplex C ℤ)
    (u : ∀ i, F (i+1) ⟶ F i) (v : ∀ i, F i ⟶ G i)
    (huv : ∀ i, u i ≫ v i = 0)
    (hseq : ∀ i, i < n → (ShortComplex.mk (u i) (v i) (huv i)).ShortExact)
    (hG : ∀ i, i < n → (G i).Acyclic) (hn : (F n).Acyclic) :
    (F 0).Acyclic := by
…

theorem OAI.LittleFinitistic.RectificationAcyclic.quasiIso_of_acyclic_quotient line 91
Source documentation
A short exact inclusion with acyclic quotient is a quasi-isomorphism.
```
theorem quasiIso_of_acyclic_quotient (S : ShortComplex (CochainComplex C ℤ))
    (hS : S.ShortExact) (hQ : S.X₃.Acyclic) : QuasiIso S.f := by
…
```

theorem OAI.LittleFinitistic.RectificationAcyclic.inclusion_homotopy_inverse line 105

Source documentation

The given inclusion, rather than an unspecified replacement, has an actual homotopy inverse once its quotient is proved acyclic by the finite filtration.

theorem inclusion_homotopy_inverse (S : ShortComplex (CochainComplex C ℤ))
    (hS : S.ShortExact) (hQ : S.X₃.Acyclic) (hi : ℤ)
    [S.X₁.IsStrictlyLE hi] [S.X₂.IsStrictlyLE hi]
    [∀ i, Projective (S.X₁.X i)] [∀ i, Projective (S.X₂.X i)] :
    ∃ g : S.X₂ ⟶ S.X₁, Nonempty (Homotopy (S.f ≫ g) (𝟙 S.X₁)) ∧
      Nonempty (Homotopy (g ≫ S.f) (𝟙 S.X₂)) := by
…