coconesIsoComponentHom — Mathlib

English

There is a natural isomorphism between the cocones over K ⋙ F with cone point Y and the cocones over K with cone point G.obj Y.

Русский

Существует естественное изоморождение конусов над K ⋙ F с вершиной Y и конусов над K с вершиной G(Y).

LaTeX

$$$$(\\mathrm{cocones}\\ J\\ D)\\!\\big(\\operatorname{op}(K\\circ F)\\big) \\cong G\\;\\big(\\mathrm{cocones}\\ J\\ C\\big(\\operatorname{op}K\\big)\\big).$$$$

Lean4

/-- auxiliary construction for `coconesIso` -/
@[simp]
def coconesIsoComponentHom {J : Type u} [Category.{v} J] {K : J ⥤ C} (Y : D)
    (t : ((cocones J D).obj (op (K ⋙ F))).obj Y) : (G ⋙ (cocones J C).obj (op K)).obj Y
    where
  app j := (adj.homEquiv (K.obj j) Y) (t.app j)
  naturality j j'
    f := by
    rw [← adj.homEquiv_naturality_left, ← Functor.comp_map, t.naturality]
    simp

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