English
Same form as previous quasiIso_truncGEMap_iff: QuasiIso(truncGEMap φ e) iff a family of QuasiIsoAt φ i'.
Русский
То же самое, что и предыдущее: QuasiIso(truncGEMap φ e) эквивалентно семейству QuasiIsoAt φ i'.
LaTeX
$$$\mathrm{QuasiIso}(\mathrm{truncGEMap}(\phi,e)) \iff \forall (i) (i') (e.f i = i') \to \mathrm{QuasiIsoAt}(\phi,i')$$$
Lean4
theorem quasiIso_truncGEMap_iff : QuasiIso (truncGEMap φ e) ↔ ∀ (i : ι) (i' : ι') (_ : e.f i = i'), QuasiIsoAt φ i' :=
by
have : ∀ (i : ι) (i' : ι') (_ : e.f i = i'), QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i' :=
by
rintro i _ rfl
rw [← quasiIsoAt_iff_comp_left (K.πTruncGE e), πTruncGE_naturality φ e, quasiIsoAt_iff_comp_right]
rw [quasiIso_iff]
constructor
· intro h i i' hi
simpa only [← this i i' hi] using h i'
· intro h i'
by_cases hi' : ∃ i, e.f i = i'
· obtain ⟨i, hi⟩ := hi'
simpa only [this i i' hi] using h i i' hi
· rw [quasiIsoAt_iff_exactAt]
all_goals exact exactAt_of_isSupported _ e i' (by simpa using hi')
