has_over_limit_discrete_of_widePullback_limit

English

Given a wide pullback in C, for any discrete diagram F: Discrete J ⥤ Over B, there exists a limit in Over B.

Русский

При наличии широкого обратного (wide) pullback в C для дискретного диаграммы F: Discrete J ⥤ Over B существует предел в Over B.

LaTeX

$$$\forall F: \mathrm{Discrete}(J) \to \mathrm{Over}(B),\ HasLimit(F).$$$

Lean4

/-- Use the above equivalence to prove we have a limit. -/
theorem has_over_limit_discrete_of_widePullback_limit {B : C} (F : Discrete J ⥤ Over B)
    [HasLimit (widePullbackDiagramOfDiagramOver B F)] : HasLimit F :=
  HasLimit.mk
    { cone := _
      isLimit :=
        IsLimit.ofRightAdjoint (conesEquiv B F).symm.toAdjunction
          (limit.isLimit (widePullbackDiagramOfDiagramOver B F)) }

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