instIsIsoπTruncGEOfIsStrictlySupported

English

If K is strictly supported along e, then K.πTruncGE e is an isomorphism.

Русский

Если K строго поддержан вдоль e, то отображение K.πTruncGE e является изоморфизмом.

LaTeX

$$$\text{IsIso}\bigl(K.\pi_{\mathrm{TruncGE}}(e)\bigr)$$$

Lean4

instance [K.IsStrictlySupported e] : IsIso (K.πTruncGE e) :=
  by
  suffices ∀ (i' : ι'), IsIso ((K.πTruncGE e).f i') by apply Hom.isIso_of_components
  intro i'
  by_cases hn : ∃ i, e.f i = i'
  · obtain ⟨i, hi⟩ := hn
    dsimp [πTruncGE]
    rw [e.isIso_liftExtend_f_iff _ _ hi]
    infer_instance
  · simp only [not_exists] at hn
    refine ⟨0, ?_, ?_⟩
    all_goals apply (isZero_X_of_isStrictlySupported _ e i' hn).eq_of_src

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