instIsIsoFRestrictionToTruncGE'OfIsStrictlySupported

English

Each component (K.πTruncGE e).f i' is epi.

Русский

Каждый компонент (K.πTruncGE e).f i' является эпиморфизмом.

LaTeX

$$For all i', Epi((K.πTruncGE e).f i')$$

Lean4

instance [K.IsStrictlySupported e] (i : ι) : IsIso ((K.restrictionToTruncGE' e).f i) :=
  by
  by_cases hi : e.BoundaryGE i
  · rw [K.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv e rfl hi]
    have : IsIso (K.pOpcycles (e.f i)) :=
      K.isIso_pOpcycles _ _ rfl
        (by
          obtain ⟨hi₁, hi₂⟩ := hi
          apply
            IsZero.eq_of_src (K.isZero_X_of_isStrictlySupported e _ (fun j hj ↦ hi₂ j (by simpa only [hj] using hi₁))))
    infer_instance
  · rw [K.restrictionToTruncGE'_f_eq_iso_hom_iso_inv e rfl hi]
    infer_instance

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