yonedaMonObj — Mathlib

Lean4
/-- If `M` is a monoid object, then `Hom(-, M)` is a presheaf of monoids. -/
@[simps]
def yonedaMonObj : Cᵒᵖ ⥤ MonCat.{v} where
  obj X := MonCat.of (unop X ⟶ M)
  map {X Y₂}
    φ :=
    MonCat.ofHom
      { toFun := (φ.unop ≫ ·)
        map_one' := by
          change φ.unop ≫ toUnit _ ≫ η = toUnit _ ≫ η
          rw [← Category.assoc, toUnit_unique (φ.unop ≫ toUnit _)]
        map_mul' f₁
          f₂ := by
          change φ.unop ≫ lift f₁ f₂ ≫ μ = lift (φ.unop ≫ f₁) (φ.unop ≫ f₂) ≫ μ
          rw [← Category.assoc]
          cat_disch }
  map_id _ := MonCat.hom_ext (MonoidHom.ext Category.id_comp)
  map_comp _ _ := MonCat.hom_ext (MonoidHom.ext (Category.assoc _ _))
Похожие утверждения