map_isStrictlySupported — Mathlib

English

For ψ : K ⟶ L.extend e and i,i' with h : e.f i = i', the equality (e.homRestrict ψ).f i = (K.restrictionXIso e h).hom ≫ ψ.f i' ≫ (L.extendXIso e h).hom holds.

Русский

Для ψ: K ⟶ L.extend e и i, i' с h: e.f i = i', верно равенство (e.homRestrict ψ).f i = (K.restrictionXIso e h).hom ≫ ψ.f i' ≫ (L.extendXIso e h).hom.

LaTeX

$$$$ (e.homRestrict ψ).f i = (K.restrictionXIso e h).hom \circ ψ.f i' \circ (L.extendXIso e h).hom $$$$

Lean4

instance map_isStrictlySupported [K.IsStrictlySupported e] : ((F.mapHomologicalComplex c').obj K).IsStrictlySupported e
    where
  isZero i'
    hi' := by
    rw [IsZero.iff_id_eq_zero]
    dsimp
    rw [← F.map_id, (K.isZero_X_of_isStrictlySupported e i' hi').eq_of_src (𝟙 _) 0, F.map_zero]

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