truncLE'Map_f_eq — Mathlib

English

If i is not in BoundaryLE, then the i-th component of truncLE'Map φ e is given by conjugation with XXIso components and φ.f i'.

Русский

Если i не в BoundaryLE, то компонент i-ой части truncLE'Map φ e задан конъюгацией через XXIso и φ.f i'.

LaTeX

$$$(truncLE'Map\;\phi\;e).f i = (K.truncLE'XIso e h hi).hom \circ (\phi.f i') \circ (L.truncLE'XIso e h hi).inv$$$

Lean4

theorem truncLE'Map_f_eq {i : ι} (hi : ¬e.BoundaryLE i) {i' : ι'} (h : e.f i = i') :
    (truncLE'Map φ e).f i = (K.truncLE'XIso e h hi).hom ≫ φ.f i' ≫ (L.truncLE'XIso e h hi).inv :=
  Quiver.Hom.op_inj (by simpa using truncGE'Map_f_eq ((opFunctor C c').map φ.op) e.op (by simpa) h)

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