English
For a monoid object M, the set of morphisms X → M carries a natural monoid structure with multiplication f * g := lift f g ≫ μ and unit given by toUnit X ≫ η; associativity and unit laws hold.
Русский
Для моноидного объекта M множество морфизмов X → M естественным образом образует моноид: умножение f * g = lift f g ≫ μ, единица = toUnit X ≫ η; выполняются ассоциативность и единичные законы.
LaTeX
$$$\\text{monoid}\colon (X \\to M) \\text{ with } (f * g) := \\mathrm{lift}\, f\\, g \\;\\gg\\; μ \\, , \\, 1 := \\; toUnit\, X \\;\\gg\\; η$$$
Lean4
/-- If `X` represents a presheaf of monoids, then `X` is a monoid object. -/
@[simps]
def ofRepresentableBy (F : Cᵒᵖ ⥤ MonCat.{w}) (α : (F ⋙ forget _).RepresentableBy X) : MonObj X
where
one := α.homEquiv.symm 1
mul := α.homEquiv.symm (α.homEquiv (fst X X) * α.homEquiv (snd X X))
one_mul := by
apply α.homEquiv.injective
simp only [α.homEquiv_comp, Equiv.apply_symm_apply]
simp only [Functor.comp_map, ConcreteCategory.forget_map_eq_coe, map_mul]
simp only [← ConcreteCategory.forget_map_eq_coe, ← Functor.comp_map, ← α.homEquiv_comp]
simp only [whiskerRight_fst, whiskerRight_snd]
simp only [α.homEquiv_comp, Equiv.apply_symm_apply]
simp [leftUnitor_hom]
mul_one := by
apply α.homEquiv.injective
simp only [α.homEquiv_comp, Equiv.apply_symm_apply]
simp only [Functor.comp_map, ConcreteCategory.forget_map_eq_coe, map_mul]
simp only [← ConcreteCategory.forget_map_eq_coe, ← Functor.comp_map, ← α.homEquiv_comp]
simp only [whiskerLeft_fst, whiskerLeft_snd]
simp only [α.homEquiv_comp, Equiv.apply_symm_apply]
simp [rightUnitor_hom]
mul_assoc := by
apply α.homEquiv.injective
simp only [α.homEquiv_comp, Equiv.apply_symm_apply]
simp only [Functor.comp_map, ConcreteCategory.forget_map_eq_coe, map_mul]
simp only [← ConcreteCategory.forget_map_eq_coe, ← Functor.comp_map, ← α.homEquiv_comp]
simp only [whiskerRight_fst, whiskerRight_snd, whiskerLeft_fst, associator_hom_fst, whiskerLeft_snd]
simp only [α.homEquiv_comp, Equiv.apply_symm_apply]
simp only [Functor.comp_map, ConcreteCategory.forget_map_eq_coe, map_mul, _root_.mul_assoc]
simp only [← ConcreteCategory.forget_map_eq_coe, ← Functor.comp_map, ← α.homEquiv_comp]
simp
