instPreservesColimitsOfSizeUliftFunctor

English

The universe-lift functor preserves colimits of arbitrary size: Ulift(Colim_J F) ≅ Colim_J (Ulift ∘ F).

Русский

Функтор подъёма вселенной сохраняет колимиты произвольного размера: Ulift(Colim_J F) ≅ Colim_J (Ulift ∘ F).

LaTeX

$$$\forall J,\; \mathrm{Ulift}(\mathrm{Colim}_J F) \cong \mathrm{Colim}_J (\mathrm{Ulift} \circ F)$$$

Lean4

/-- The functor `uliftFunctor : AddCommGrpCat.{u} ⥤ AddCommGrpCat.{max u v}` preserves colimits
of arbitrary size.
-/
noncomputable instance : PreservesColimitsOfSize.{w', w} uliftFunctor.{v, u} where
  preservesColimitsOfShape
    {J
      _} :=
    {
      preservesColimit := fun {F} ↦
        {
          preserves := fun {c} hc ↦ by
            classical
            rw [isColimit_iff_bijective_desc, ← Function.Bijective.of_comp_iff _ (quotQuotUliftAddEquiv F).bijective, ←
              AddEquiv.coe_toAddMonoidHom, ← AddMonoidHom.coe_comp, Quot.desc_quotQuotUliftAddEquiv]
            exact ULift.up_bijective.comp ((isColimit_iff_bijective_desc c).mp (Nonempty.intro hc)) } }

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