English
The forget₂ functor CommMonCat ⥤ MonCat creates limits, i.e., limits in CommMonCat can be constructed by transporting to MonCat and using MonCat's limits.
Русский
Функтор forget₂ CommMonCat ⥤ MonCat создаёт пределы; пределы в CommMonCat можно построить через переход к MonCat и использования его пределов.
LaTeX
$$$\text{forget₂CreatesLimit } F$$$
Lean4
/-- We show that the forgetful functor `CommMonCat ⥤ MonCat` creates limits.
All we need to do is notice that the limit point has a `CommMonoid` instance available,
and then reuse the existing limit. -/
@[to_additive /-- We show that the forgetful functor `AddCommMonCat ⥤ AddMonCat` creates limits.
All we need to do is notice that the limit point has an `AddCommMonoid` instance available,
and then reuse the existing limit. -/
]
noncomputable instance forget₂CreatesLimit : CreatesLimit F (forget₂ CommMonCat MonCat.{u}) :=
createsLimitOfReflectsIso fun c' t =>
{ liftedCone :=
{ pt := CommMonCat.of (Types.Small.limitCone (F ⋙ forget CommMonCat)).pt
π :=
{ app j := ofHom (MonCat.limitπMonoidHom (F ⋙ forget₂ CommMonCat.{u} MonCat.{u}) j)
naturality _ _
j :=
ext <| fun x =>
congr_hom ((MonCat.HasLimits.limitCone (F ⋙ forget₂ CommMonCat MonCat.{u})).π.naturality j) x } }
validLift := by apply IsLimit.uniqueUpToIso (MonCat.HasLimits.limitConeIsLimit _) t
makesLimit :=
IsLimit.ofFaithful (forget₂ CommMonCat MonCat.{u}) (MonCat.HasLimits.limitConeIsLimit _) (fun _ => _) fun _ =>
rfl }
