restriction_d_eq — Mathlib

English

The lifted extension of the restricted morphism equals the original morphism: e.liftExtend (e.homRestrict ψ) (e.homRestrict_hasLift ψ) = ψ.

Русский

Поднятие ограниченного морфизма возвращает исходный морфизм: e.liftExtend (e.homRestrict ψ) (e.homRestrict_hasLift ψ) = ψ.

LaTeX

$$$$ e.liftExtend (e.homRestrict ψ) (e.homRestrict_hasLift ψ) = ψ $$$$

Lean4

@[reassoc]
theorem restriction_d_eq {i j : ι} {i' j' : ι'} (hi : e.f i = i') (hj : e.f j = j') :
    (K.restriction e).d i j = (K.restrictionXIso e hi).hom ≫ K.d i' j' ≫ (K.restrictionXIso e hj).inv :=
  by
  subst hi hj
  simp [restrictionXIso]

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