English
See item 74119 for the isomorphism between the limit and the Hom-set description via Coyoneda.
Русский
См. пункт 74119 для изоморфизма между пределом и описанием через Coyoneda.
LaTeX
$$$\\text{limitCompCoyonedaIsoCone}(F,X) : \\lim (F \\circ (\\text{coyoneda.obj} (op X))) \\cong (\\mathrm{Hom}((\\mathrm{const}\\ J).obj X, F))$$$
Lean4
@[reassoc (attr := simp)]
theorem add'_comp (f₁ f₂ : L.obj X ⟶ L.obj Y) (g : L.obj Y ⟶ L.obj Z) : add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g) :=
by
obtain ⟨α, h₁, h₂⟩ := exists_leftFraction₂ L W f₁ f₂
obtain ⟨β, hβ⟩ := exists_leftFraction L W g
obtain ⟨γ, hγ⟩ := (RightFraction.mk _ α.hs β.f).exists_leftFraction
dsimp at hγ
rw [add'_eq W f₁ f₂ α h₁ h₂,
add'_eq W (f₁ ≫ g) (f₂ ≫ g) (LeftFraction₂.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.s ≫ γ.s) (W.comp_mem _ _ β.hs γ.hs))];
rotate_left
· rw [h₁, hβ]
exact LeftFraction.map_comp_map_eq_map _ _ _ hγ _
· rw [h₂, hβ]
exact LeftFraction.map_comp_map_eq_map _ _ _ hγ _
rw [hβ, LeftFraction.map_comp_map_eq_map _ _ γ hγ]
dsimp [LeftFraction₂.add]
rw [add_comp]
