forget_createsLimit — Mathlib

English

For every diagram F: J ⥤ CommMonCat, the forgetful functor forget CommMonCat creates limits of shape J.

Русский

Для каждого диаграммы F: J ⥤ CommMonCat забывающий функтор forget CommMonCat создаёт предел формы J.

LaTeX

$$$\text{CreatesLimit}\ F\ (\mathrm{forget}\ \mathrm{CommMonCat})$$$

Lean4

@[to_additive]
noncomputable instance forget_createsLimit : CreatesLimit F (forget CommMonCat.{u}) :=
  by
  set e : forget CommMonCat.{u} ≅ forget₂ CommMonCat.{u} MonCat.{u} ⋙ forget MonCat.{u} :=
    NatIso.ofComponents (fun _ ↦ Iso.refl _) (fun _ ↦ rfl)
  exact createsLimitOfNatIso e.symm

Похожие утверждения