comp_coconePointUniqueUpToIso_inv

English

For colimits s,t and j in J, the leg t.ι.app j composed with the inverse of coconePointUniqueUpToIso P Q equals s.ι.app j under the inverse hom of the iso.

Русский

Для колимитов s,t и любого j ∈ J, композиция t.ι.app j с обратной стороной coconePointUniqueUpToIso(P,Q) равна inv аппликации j применённой к s.ι.app j.

LaTeX

$$$ t.\iota.app j \\! \, (P.coconePointUniqueUpToIso Q).inv = s.\iota.app j $$$

Lean4

@[reassoc (attr := simp)]
theorem comp_coconePointUniqueUpToIso_inv {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) (j : J) :
    t.ι.app j ≫ (coconePointUniqueUpToIso P Q).inv = s.ι.app j :=
  (uniqueUpToIso P Q).inv.w _

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