stupidTruncMap_stupidTruncXIso_hom

English

For indices i, i' with e.f i = i', a compatibility condition holds between the stupidTruncMap and the XIsos.

Русский

Для индексов i, i' с e.f i = i' выполняется совместимость между stupidTruncMap и XIsos на компонентах.

LaTeX

$$$(stupidTruncMap(\phi,e)).f(i') \circ (L.\mathrm{stupidTruncXIso}(e, h)).hom = (K.\mathrm{stupidTruncXIso}(e,h)).hom \circ \phi.f(i')$$$

Lean4

@[reassoc (attr := simp)]
theorem stupidTruncMap_stupidTruncXIso_hom {i : ι} {i' : ι'} (hi : e.f i = i') :
    (stupidTruncMap φ e).f i' ≫ (L.stupidTruncXIso e hi).hom = (K.stupidTruncXIso e hi).hom ≫ φ.f i' :=
  by
  subst hi
  simp [stupidTruncMap, stupidTruncXIso, extendMap_f _ _ rfl]

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