hasCoproduct_of_equiv_of_iso — Mathlib

English

Let f : α → C and g : β → C be functorial families with HasCoproduct f, and e : β ≃ α an equivalence together with isomorphisms g j ≅ f (e j). Then HasCoproduct g.

Русский

Пусть f : α → C и g : β → C задают семейства объектов с существованием их копроизведений. Если имеется эквивелентность e : β ≃ α и изоморфизмы g j ≅ f (e j) для всех j, то копроизведение g существует.

LaTeX

$$$\\text{HasCoproduct} f \\Rightarrow \\text{HasCoproduct} g$ given $e : β \\simeq α$ and $\\forall j,\, g j \\cong f (e j)$.$$

Lean4

theorem hasCoproduct_of_equiv_of_iso (f : α → C) (g : β → C) [HasCoproduct f] (e : β ≃ α) (iso : ∀ j, g j ≅ f (e j)) :
    HasCoproduct g :=
  by
  have α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f :=
    Discrete.natIso (fun ⟨j⟩ => iso j)
  exact hasColimit_of_iso α

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