quasiIsoAt_truncLE'ToRestriction — Mathlib

English

For j with non-boundary, QuasiIsoAt(K.truncLE'ToRestriction e) j holds, given homology conditions.

Русский

При некраевом j выполняется QuasiIsoAt(K.truncLE'ToRestriction e) j при заданных условиях гомологии.

LaTeX

$$$ QuasiIsoAt\big(K.truncLE'ToRestriction e\big)\ j $$$

Lean4

/-- `K.truncLE'ToRestriction e` is a quasi-isomorphism in degrees that are not at the boundary. -/
theorem quasiIsoAt_truncLE'ToRestriction (j : ι) (hj : ¬e.BoundaryLE j) [(K.restriction e).HasHomology j]
    [(K.truncLE' e).HasHomology j] : QuasiIsoAt (K.truncLE'ToRestriction e) j :=
  by
  dsimp only [truncLE'ToRestriction]
  have : (K.op.restriction e.op).HasHomology j := inferInstanceAs ((K.restriction e).op.HasHomology j)
  rw [quasiIsoAt_unopFunctor_map_iff]
  exact truncGE'.quasiIsoAt_restrictionToTruncGE' K.op e.op j (by simpa)

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