lift_comp_conePointUniqueUpToIso_inv

English

Let s and t be cones over F with s and t being limiting cones. For any cone r, the two lift maps satisfy Q.lift r ≫ (conePointUniqueUpToIso P Q).inv = P.lift r, where P and Q are IsLimit cones on s and t respectively and conePointUniqueUpToIso is the canonical isomorphism between the cone points.

Русский

Пусть s и t — конусы над F; пусть они являются пределами. Для любого конуса r композиция Q.lift r с обратным отображением конусного точки из P в Q равна P.lift r, где P и Q — IsLimit-конусы над s и t, а conePointUniqueUpToIso — каноническая изоморфия между их точками конуса.

LaTeX

$$$ Q.lift(r) \\circ (conePointUniqueUpToIso(P,Q))^{-1} = P.lift(r) $$$

Lean4

@[reassoc (attr := simp)]
theorem lift_comp_conePointUniqueUpToIso_inv {r s t : Cone F} (P : IsLimit s) (Q : IsLimit t) :
    Q.lift r ≫ (conePointUniqueUpToIso P Q).inv = P.lift r :=
  P.uniq _ _ (by simp)

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