hasProduct_of_equiv_of_iso — Mathlib

English

Let f : α → C and g : β → C be functors with HasProduct f and an equivalence e : β ≃ α together with isomorphisms g j ≅ f (e j) for all j. Then HasProduct g.

Русский

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

LaTeX

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

Lean4

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

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