English
If X represents a presheaf of commutative monoids, then X is a commutative monoid object.
Русский
Если X представляет прешфеасовую коммутативную моноиду, то X является объектом коммутативной моноиды.
LaTeX
$$$$\text{IsCommMonObj}(X)$$, i.e., X carries a commutative monoid structure in C.$$
Lean4
/-- If `X` represents a presheaf of commutative monoids, then `X` is a commutative monoid object. -/
theorem ofRepresentableBy (F : Cᵒᵖ ⥤ CommMonCat) (α : (F ⋙ forget _).RepresentableBy X) :
letI : MonObj X := .ofRepresentableBy X (F ⋙ forget₂ CommMonCat MonCat) α
IsCommMonObj X :=
by
letI : MonObj X := .ofRepresentableBy X (F ⋙ forget₂ CommMonCat MonCat) α
have : μ = α.homEquiv.symm (α.homEquiv (fst X X) * α.homEquiv (snd X X)) := rfl
constructor
simp_rw [this, ← α.homEquiv.apply_eq_iff_eq, α.homEquiv_comp, Functor.comp_map, ConcreteCategory.forget_map_eq_coe,
Equiv.apply_symm_apply, map_mul, ← ConcreteCategory.forget_map_eq_coe, ← Functor.comp_map, ← α.homEquiv_comp,
op_tensorObj, Functor.comp_obj, braiding_hom_fst, braiding_hom_snd, _root_.mul_comm]
