map_add_inv_app — Mathlib

English

For shifts a, b and a fully faithful F, the inverse of the add-homomorphism is given by a composite formula involving the inverses of i-binders and the shiftAdd isomorphism.

Русский

При сдвигах a, b и полностьюFaithful F, обратная к гомоморфизму сложения задаётся через композицию, включающую обратные для i-обвязок и изоморфизм shiftAdd.

LaTeX

$$$ F.map ((add hF s i a b).inv.app X) = (i b).hom.app ((s a).obj X) ≫ ((i a).hom.app X)⟦b⟧' ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) ≫ (i (a + b)).inv.app X $$$

Lean4

@[simp]
theorem map_add_inv_app (a b : A) (X : C) :
    F.map ((add hF s i a b).inv.app X) =
      (i b).hom.app ((s a).obj X) ≫
        ((i a).hom.app X)⟦b⟧' ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) ≫ (i (a + b)).inv.app X :=
  by
  dsimp [add]
  simp

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