instPreservesLimitsOfSizeUliftFunctor

English

The functor uliftFunctor preserves limits of arbitrary size.

Русский

Функтор uliftFunctor сохраняет пределы произвольного размера.

LaTeX

$$$\mathrm{PreservesLimitsOfSize}(\mathrm{uliftFunctor})$$$

Lean4

/-- The functor `uliftFunctor : Type u ⥤ Type (max u v)` preserves limits of arbitrary size.
-/
noncomputable instance : PreservesLimitsOfSize.{w', w} uliftFunctor.{v, u} where
  preservesLimitsOfShape
    {J} :=
    {
      preservesLimit := fun {K} =>
        {
          preserves := fun {c} hc =>
            by
            rw [Types.isLimit_iff ((uliftFunctor.{v, u}).mapCone c)]
            intro s hs
            obtain ⟨x, hx₁, hx₂⟩ := (Types.isLimit_iff c).mp ⟨hc⟩ _ ((sectionsEquiv K).symm ⟨s, hs⟩).2
            exact
              ⟨⟨x⟩, fun i => ULift.ext _ _ (hx₁ i), fun y hy =>
                ULift.ext _ _ (hx₂ y.down fun i ↦ ULift.ext_iff.mp (hy i))⟩ } }

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