acyclic_truncGE_iff_isSupportedOutside

English

(K.truncGE e) is acyclic if and only if K is supported outside e.

Русский

(K.truncGE e) акцикличен тогда и только тогда, когда K поддержан вне области e.

LaTeX

$$$(K.\mathrm{truncGE} e).\mathrm{Acyclic} \iff K.\mathrm{IsSupportedOutside}(e)$$$

Lean4

theorem acyclic_truncGE_iff_isSupportedOutside : (K.truncGE e).Acyclic ↔ K.IsSupportedOutside e :=
  by
  constructor
  · intro hK
    exact ⟨fun i => by simpa only [exactAt_iff_of_quasiIsoAt (K.πTruncGE e)] using hK (e.f i)⟩
  · intro hK i'
    by_cases hi' : ∃ i, e.f i = i'
    · obtain ⟨i, rfl⟩ := hi'
      simpa only [← exactAt_iff_of_quasiIsoAt (K.πTruncGE e)] using hK.exactAt i
    · exact exactAt_of_isSupported _ e i' (by simpa using hi')

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