limitConeIsLimit — Mathlib

English

Auxiliary lemma showing the forgetful functor from SemiRingCat to AddCommMonCat preserves limits when transported through the limit cone construction.

Русский

Вспомогательная лемма, показывающая, что функтор забывания из SemiRingCat в AddCommMonCat сохраняет пределы при переносе через построение предельного конуса.

LaTeX

$$$\text{forget₂AddCommMonPreservesLimitsAux} (F)$$$

Lean4

/-- Witness that the limit cone in `SemiRingCat` is a limit cone.
(Internal use only; use the limits API.)
-/
def limitConeIsLimit : IsLimit (limitCone F) :=
  by
  refine
    IsLimit.ofFaithful (forget SemiRingCat.{u}) (Types.Small.limitConeIsLimit.{v, u} _)
      (fun s => ofHom { toFun := _, map_one' := ?_, map_mul' := ?_, map_zero' := ?_, map_add' := ?_ }) (fun s => rfl)
  · simp only [Functor.mapCone_π_app, forget_map, map_one]
    rfl
  · intro x y
    simp only [Functor.comp_obj, Functor.mapCone_pt, Functor.mapCone_π_app, forget_map, map_mul, EquivLike.coe_apply]
    rw [← equivShrink_mul]
    rfl
  · simp only [Functor.mapCone_π_app, forget_map, map_zero]
    rfl
  · intro x y
    simp only [Functor.comp_obj, Functor.mapCone_pt, Functor.mapCone_π_app, forget_map, map_add, EquivLike.coe_apply]
    rw [← equivShrink_add]
    rfl

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