limitConeIsLimit — Mathlib

English

The limit cone for any diagram F in AlgCat(R) satisfies the universal property, i.e., it is a limit cone.

Русский

Предел-конус для любой диаграммы F в AlgCat(R) удовлетворяет универсальному свойству, то есть является пределом.

LaTeX

$$$$\text{IsLimit}(\text{limitCone}(F)).$$$$

Lean4

/-- Witness that the limit cone in `AlgCat R` is a limit cone.
(Internal use only; use the limits API.)
-/
def limitConeIsLimit : IsLimit (limitCone.{v, w} F) :=
  by
  refine
    IsLimit.ofFaithful (forget (AlgCat R)) (Types.Small.limitConeIsLimit.{v, w} _)
      (fun s => ofHom { toFun := _, map_one' := ?_, map_mul' := ?_, map_zero' := ?_, map_add' := ?_, commutes' := ?_ })
      (fun s => rfl)
  · congr
    ext j
    simp only [Functor.mapCone_π_app, forget_map, map_one, Pi.one_apply]
  · intro x y
    ext j
    simp only [Functor.comp_obj, forget_obj, Functor.mapCone_pt, Functor.mapCone_π_app, forget_map,
      Equiv.symm_apply_apply, Types.Small.limitCone_pt, equivShrink_symm_mul, EquivLike.coe_apply]
    apply map_mul
  · ext j
    simp only [Functor.comp_obj, forget_obj, Functor.mapCone_pt, Functor.mapCone_π_app, forget_map,
      Equiv.symm_apply_apply, equivShrink_symm_zero, EquivLike.coe_apply]
    apply map_zero
  · intro x y
    ext j
    simp only [Functor.comp_obj, forget_obj, Functor.mapCone_pt, Functor.mapCone_π_app, forget_map,
      Equiv.symm_apply_apply, Types.Small.limitCone_pt, equivShrink_symm_add, EquivLike.coe_apply]
    apply map_add
  · intro r
    simp only [Equiv.algebraMap_def, Equiv.symm_symm]
    apply congrArg
    apply Subtype.ext
    ext j
    exact (s.π.app j).hom.commutes r

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