lift_comp_conePointUniqueUpToIso_hom

English

For any r, the lift of r followed by the isomorphism hom equals the lift of r on the other cone: P.lift r ≫ (conePointUniqueUpToIso Q).hom = Q.lift r.

Русский

Для любых r подъём через P и изоморфия-ход равны подъёму через Q: P.lift r ≫ (conePointUniqueUpToIso Q).hom = Q.lift r.

LaTeX

$$$P.lift r \;\gg\ (conePointUniqueUpToIso Q).hom = Q.lift r$$$

Lean4

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

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