ι_colimitIsoOfIsLeftKanExtension_inv

English

For i in C, colimit.ι F i corresponds to the colimit map through the isomorphism (F'.colimitIsoOfIsLeftKanExtension α).inv when comparing F and F' along L.

Русский

Для каждого i ∈ C, колимит-множитель через F и через F' согласован через изоморфизм (F'.colimitIsoOfIsLeftKanExtension α).inv при сопоставлении F и F' вдоль L.

LaTeX

$$$\\text{ι_colimitIsoOfIsLeftKanExtension_hom}$: Eq$$\\alpha.app i \\cdot \\text{colimit.ι}_F'(L.obj i)\\cdot (F'.colimitIsoOfIsLeftKanExtension α).hom = \\text{colimit.ι}_F i$$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_colimitIsoOfIsLeftKanExtension_inv (i : C) :
    colimit.ι F i ≫ (F'.colimitIsoOfIsLeftKanExtension α).inv = α.app i ≫ colimit.ι F' (L.obj i) := by
  rw [Iso.comp_inv_eq, assoc, ι_colimitIsoOfIsLeftKanExtension_hom]

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