limitCone — Mathlib

English

The limit cone for a functor into a complete lattice is given explicitly by pt = iInf F.obj with projection maps π_j = homOfLE( ... ).

Русский

Предел-конус для функторa в полную решетку задан явно: вершина pt = iInf F.obj, проекции π_j = homOfLE( ... ).

LaTeX

$$$\text{limitCone }(F) = \{\;\text{pt} = \inf_j F(j),\; \pi_j = \mathrm{homOfLE}(\dots)\;\}$$$

Lean4

/-- The limit cone over any functor into a complete lattice.
-/
@[simps]
def limitCone (F : J ⥤ α) : LimitCone F
    where
  cone :=
    { pt := iInf F.obj
      π := { app := fun _ => homOfLE (CompleteLattice.sInf_le _ _ (Set.mem_range_self _)) } }
  isLimit := { lift := fun s => homOfLE (CompleteLattice.le_sInf _ _ (by rintro _ ⟨j, rfl⟩; exact (s.π.app j).le)) }

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