quasiIsoAt_restrictionToTruncGE' — Mathlib

English

If j is not in BoundaryGE, then certain restriction-to-truncGE maps are quasi-isomorphisms at j.

Русский

Если j не лежит на границе, то соответствующие отображения restrictionToTruncGE' являются частичными изоморфизмами в степени j.

LaTeX

$$$\text{QuasiIsoAt}\bigl(K.\mathrm{restrictionToTruncGE}'(e)\,,\;j\bigr)$$$

Lean4

/-- `K.restrictionToTruncGE' e` is a quasi-isomorphism in degrees that are not at the boundary. -/
theorem quasiIsoAt_restrictionToTruncGE' (hj : ¬e.BoundaryGE j) [(K.restriction e).HasHomology j]
    [(K.truncGE' e).HasHomology j] : QuasiIsoAt (K.restrictionToTruncGE' e) j :=
  by
  rw [quasiIsoAt_iff]
  let φ := (shortComplexFunctor C c j).map (K.restrictionToTruncGE' e)
  have : Epi φ.τ₁ := by dsimp [φ]; infer_instance
  have : IsIso φ.τ₂ := K.isIso_restrictionToTruncGE' e j hj
  have : IsIso φ.τ₃ := K.isIso_restrictionToTruncGE' e _ (e.not_boundaryGE_next' hj rfl)
  exact ShortComplex.quasiIso_of_epi_of_isIso_of_mono φ

Похожие утверждения