yonedaMon — Mathlib

Lean4
/-- The yoneda embedding of `Mon_C` into presheaves of monoids. -/
@[simps]
def yonedaMon : Mon C ⥤ Cᵒᵖ ⥤ MonCat.{v} where
  obj M := yonedaMonObj M.X
  map {M N}
    ψ :=
    { app
        Y :=
        MonCat.ofHom
          { toFun := (· ≫ ψ.hom)
            map_one' := by simp [Hom.one_def, Hom.one_def]
            map_mul' φ₁ φ₂ := by simp [Hom.mul_def] }
      naturality {M N} φ := MonCat.hom_ext <| MonoidHom.ext fun f ↦ Category.assoc φ.unop f ψ.hom }
  map_id M := NatTrans.ext <| funext fun _ ↦ MonCat.hom_ext <| MonoidHom.ext Category.comp_id
  map_comp _ _ := NatTrans.ext <| funext fun _ ↦ MonCat.hom_ext <| MonoidHom.ext (.symm <| Category.assoc · _ _)
Похожие утверждения