leftAdjoint_preservesColimits — Mathlib

English

If E is an equivalence and K has a colimit, then K has a colimit after composing with E.

Русский

Если E эквивалентность и K имеет колимит, то K имеет колимит после композиции с E.

LaTeX

$$$$\\text{If } E \\text{ is an equivalence and hasColimit } K, \\text{ then hasColimit } (K \\circ E).$$$$

Lean4

/-- A left adjoint preserves colimits. -/
@[stacks 0038]
theorem leftAdjoint_preservesColimits : PreservesColimitsOfSize.{v, u} F where
  preservesColimitsOfShape :=
    {
      preservesColimit :=
        {
          preserves := fun hc =>
            ⟨IsColimit.isoUniqueCoconeMorphism.inv fun _ =>
                @Equiv.unique _ _ (IsColimit.isoUniqueCoconeMorphism.hom hc _)
                  ((adj.functorialityAdjunction _).homEquiv _ _)⟩ } }

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