limitConeOfEqualizerAndProduct — Mathlib

English

There exists a limit cone for F built from the given data of products and equalizers.

Русский

Существует предел-коно́м F, построенный из данных о произведениях и равноселителях.

LaTeX

$$$\text{limitConeOfEqualizerAndProduct}(F)$ is a LimitCone for F$$

Lean4

/-- Given the existence of the appropriate (possibly finite) products and equalizers,
we can construct a limit cone for `F`.
(This assumes the existence of all equalizers, which is technically stronger than needed.)
-/
noncomputable def limitConeOfEqualizerAndProduct (F : J ⥤ C) [HasLimit (Discrete.functor F.obj)]
    [HasLimit (Discrete.functor fun f : Σ p : J × J, p.1 ⟶ p.2 => F.obj f.1.2)] [HasEqualizers C] : LimitCone F
    where
  cone := _
  isLimit :=
    buildIsLimit (Pi.lift fun f => limit.π (Discrete.functor F.obj) ⟨_⟩ ≫ F.map f.2)
      (Pi.lift fun f => limit.π (Discrete.functor F.obj) ⟨f.1.2⟩) (by simp) (by simp) (limit.isLimit _)
      (limit.isLimit _) (limit.isLimit _)

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