forget_createsLimit — Mathlib

English

The forgetful functor forget MonCat creates limits for diagrams F: J ⥤ MonCat, i.e., limits in MonCat can be computed by lifting from the forgetful image.

Русский

Забывающая функция forget MonCat создаёт пределы для диаграмм F: J ⥤ MonCat, то есть пределы в MonCat можно вычислить через образ под забыванием.

LaTeX

$$$\text{CreatesLimit } F\big(\text{forget MonCat}\big)$$$

Lean4

@[to_additive]
noncomputable instance forget_createsLimit : CreatesLimit F (forget MonCat.{u}) :=
  by
  apply createsLimitOfReflectsIso
  intro c t
  have : Small.{u} (Functor.sections (F ⋙ forget MonCat)) :=
    (Types.hasLimit_iff_small_sections _).mp (HasLimit.mk { cone := c, isLimit := t })
  refine
    LiftsToLimit.mk
      (LiftableCone.mk
        { pt := MonCat.of (Types.Small.limitCone (F ⋙ forget MonCat)).pt,
          π := NatTrans.mk (fun j => ofHom (limitπMonoidHom F j)) (MonCat.HasLimits.limitCone F).π.naturality }
        (Cones.ext ((Types.isLimitEquivSections t).trans (equivShrink _)).symm.toIso
          (fun _ ↦ funext (fun _ ↦ by simp; rfl))))
      ?_
  refine IsLimit.ofFaithful (forget MonCat.{u}) (Types.Small.limitConeIsLimit.{v, u} _) ?_ ?_
  · intro _
    refine
      ofHom
        { toFun := (Types.Small.limitConeIsLimit.{v, u} _).lift ((forget MonCat).mapCone _), map_one' := by simp; rfl,
          map_mul' := ?_ }
    · intro x y
      simp only [Types.Small.limitConeIsLimit_lift, Functor.comp_obj, Functor.mapCone_pt, Functor.mapCone_π_app,
        forget_map, map_mul]
      congr
      simp only [Functor.comp_obj, Equiv.symm_apply_apply]
      rfl
  · exact fun _ ↦ rfl

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