toCostructuredArrow — Mathlib

English

Another instance of the same CompProj relation for toCostructuredArrow.

Русский

Еще один экземпляр того же отношения CompProj для toCostructuredArrow.

LaTeX

$$$ (G.toCostructuredArrow F X f h) \;\; \; \; \; \; = G $$$

Lean4

/-- For a functor `F : C ⥤ D` and an object `d : D`, we obtain a contravariant functor from the
category of structured arrows `d ⟶ F.obj c` to the category of costructured arrows
`F.op.obj c ⟶ (op d)`.
-/
@[simps]
def toCostructuredArrow (F : C ⥤ D) (d : D) : (StructuredArrow d F)ᵒᵖ ⥤ CostructuredArrow F.op (op d)
    where
  obj X := @CostructuredArrow.mk _ _ _ _ _ (op X.unop.right) F.op X.unop.hom.op
  map f := CostructuredArrow.homMk f.unop.right.op (by simp [← op_comp])

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