isoShift_inv_naturality — Mathlib

English

Inverse component of isoShift evaluated at X is given by the inv.app X of a base iso composed with the map part.

Русский

Обратный компонент isoShift на X равен inv.app X базового изоморфизма, композиции с картой.

LaTeX

$$$ (\mathrm{isoShift}(n)).inv.app X = (\mathrm{inv} \;\mathrm{F.shiftIso} n a a' ha').app X \circ (\mathrm{F.map} \ (shiftFunctor C n).map) $$$

Lean4

@[reassoc]
theorem isoShift_inv_naturality (n : M) {X Y : C} (f : X ⟶ Y) :
    (F.shift n).map f ≫ (F.isoShift n).inv.app Y = (F.isoShift n).inv.app X ≫ F.map (f⟦n⟧') :=
  (F.isoShift n).inv.naturality f

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