forget_createsLimit — Mathlib

English

The forgetful functor from GrpCat to MonCat creates limits: limits in GrpCat can be obtained by taking limits in MonCat and then equipping with a group structure.

Русский

Функтор забывания из GrpCat в MonCat создаёт пределы: пределы в GrpCat получаются как пределы в MonCat с дополнительной структурой группы.

LaTeX

$$$ \text{forget GrpCat} \text{ createsLimit } F (\text{forget GrpCat}) $$$

Lean4

@[to_additive]
noncomputable instance forget_createsLimit : CreatesLimit F (forget GrpCat.{u}) :=
  by
  set e : forget₂ GrpCat.{u} MonCat.{u} ⋙ forget MonCat.{u} ≅ forget GrpCat.{u} := Iso.refl _
  exact createsLimitOfNatIso e

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