closedUnderLimitsOfShape_discrete_empty

English

If L is faithful and full and P contains identities and respects isomorphisms, then the discrete PEmpty-indexed costructured arrow object is closed under limits.

Русский

Если L —Faithful и Full, и P содержит тождественные, и сохраняет изоморфизмы, то дискретный CostructuredArrow PEmpty имеет замкнутость по пределам.

LaTeX

$$$$ \\operatorname{ClosedUnderLimitsOfShape}\\Bigl( \\operatorname{Discrete}(PEmpty), \\; P.\\mathrm{costructuredArrowObj}(L, X) \\Bigr) $$$$

Lean4

theorem closedUnderLimitsOfShape_discrete_empty [L.Faithful] [L.Full] {Y : A} [P.ContainsIdentities] [P.RespectsIso] :
    ClosedUnderLimitsOfShape (Discrete PEmpty.{1}) (P.costructuredArrowObj L (X := L.obj Y)) :=
  by
  rintro D c hc -
  have : D = Functor.empty _ := Functor.empty_ext' _ _
  subst this
  let e : c.pt ≅ CostructuredArrow.mk (𝟙 (L.obj Y)) := hc.conePointUniqueUpToIso CostructuredArrow.mkIdTerminal
  rw [P.costructuredArrowObj_iff, P.costructuredArrow_iso_iff e]
  simpa using P.id_mem (L.obj Y)

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