iso_inv_app — Mathlib

English

In the quotient/lift setting, the inverse part of the iso lifts to a CommShift structure on A via the lifted functor.

Русский

В настройке квази-упрощения/лифта, обратная часть изоморфизма поднимается до структуры CommShift на A через поднятый функтор.

LaTeX

$$(\\mathrm{iso} F r hF a).inv.app ((\\mathrm{functor} r).obj X) = (F.commShiftIso a).inv.app X \\;\\gg\\; (lift r F hF).map (((\\mathrm{functor} r).commShiftIso a).hom.app X)$$

Lean4

@[simp]
theorem iso_inv_app (a : A) (X : C) :
    (iso F r hF a).inv.app ((functor r).obj X) =
      (F.commShiftIso a).inv.app X ≫ (lift r F hF).map (((functor r).commShiftIso a).hom.app X) :=
  by
  dsimp only [iso, natIsoLift]
  rw [natTransLift_app]
  dsimp
  erw [id_comp, comp_id, comp_id, comp_id, Functor.map_id, id_comp]

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