homRestrict_f — Mathlib

English

For ψ : K ⟶ L.extend e and any i,i' with h : e.f i = i', the i-th component of the restricted morphism equals the composition of the restriction isomorphism, ψ.f i', and the extend isomorphism.

Русский

Для ψ: K ⟶ L.extend e и любых i, i' с h: e.f i = i', i-й компонент ограниченного морфизма равен композиции из изоморфизма ограничения, ψ.f i' и изоморфизма расширения.

LaTeX

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

Lean4

theorem homRestrict_f (ψ : 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 :=
  homRestrict.f_eq ψ h

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