hasLimit — Mathlib

English

The forgetful functor CommRingCat ⥤ RingCat creates limits, with compatibility data given by existing limit cones.

Русский

Функтор забывания CommRingCat ⥤ RingCat создаёт пределы, с данными совместимости через существующие пределы.

LaTeX

$$$\mathrm{Inst}\;\text{CreatesLimit}_{\text{forget}_2} \;\text{RingCat}$$$

Lean4

/-- If `(F ⋙ forget CommRingCat).sections` is `u`-small, `F` has a limit. -/
instance hasLimit : HasLimit F :=
  let _ : Small.{u} (Functor.sections ((F ⋙ forget₂ CommRingCat RingCat) ⋙ forget RingCat)) :=
    inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget _))
  hasLimit_of_created F (forget₂ CommRingCat.{u} RingCat.{u})

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