quasiIso_πTruncGE_iff_isSupported

English

QuasiIso(truncGEMap φ e) is equivalent to a family of QuasiIsoAt φ i' for all i with e.f i = i'.

Русский

QuasiIso(truncGEMap φ e) эквивалентно семейству QuasiIsoAt φ i' для всех i с e.f i = i'.

LaTeX

$$$\mathrm{QuasiIso}\bigl(\mathrm{truncGEMap}(\phi,e)\bigr) \iff \forall i,i', (e.f i = i') \Rightarrow \mathrm{QuasiIsoAt}(\phi,i')$$$

Lean4

theorem quasiIso_πTruncGE_iff_isSupported : QuasiIso (K.πTruncGE e) ↔ K.IsSupported e :=
  by
  constructor
  · intro
    refine ⟨fun i' hi' => ?_⟩
    rw [exactAt_iff_of_quasiIsoAt (K.πTruncGE e) i']
    exact (K.truncGE e).exactAt_of_isSupported e i' hi'
  · intro
    rw [quasiIso_iff]
    intro i'
    by_cases hi' : ∃ i, e.f i = i'
    · obtain ⟨i, rfl⟩ := hi'
      infer_instance
    · rw [quasiIsoAt_iff_exactAt (K.πTruncGE e) i']
      all_goals exact exactAt_of_isSupported _ e i' (by simpa using hi')

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