coconesIsoComponentInv — Mathlib

English

An explicit construction giving the j-th component of the cocones isomorphism for a cocone t.

Русский

Явное описание j-й компоненты изоморфизма коконов для конуса t.

LaTeX

$$$$\\text{component}_j \\big(\\text{coconesIsoComponentHom}\\;\\cdot\\big)(Y) = (\\text{adj}.homEquiv (K.obj j) Y)\\big( t.app\\; j\\big).$$$$

Lean4

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

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