isSeparator_coproduct_separatingFamily

English

If X is a separator, then the coproduct over i of separatingFamily c (fun x => X) at index ⟨⟨⟩, i⟩ is a separator.

Русский

Если X является сепаратором, тоkopроductor над i-ми элементами separatingFamily c (fun x => X) образует сепаратор.

LaTeX

$$$\IsSeparator \left(\Sigma_{i} \mathrm{separatingFamily}\,c\, (\lambda\_, X)\, { fst := PUnit.unit, snd := i} \right)$$$

Lean4

theorem isSeparator_coproduct_separatingFamily {X : C} (hX : IsSeparator X) :
    IsSeparator (∐ (fun i ↦ separatingFamily c (fun (_ : Unit) ↦ X) ⟨⟨⟩, i⟩)) :=
  by
  let φ (i : ι) := separatingFamily c (fun (_ : Unit) ↦ X) ⟨⟨⟩, i⟩
  refine
    isSeparator_of_isColimit_cofan (isSeparating_separatingFamily c (X := fun (_ : Unit) ↦ X) (by simpa using hX)) (c :=
      Cofan.mk (∐ φ) (fun ⟨_, i⟩ ↦ Sigma.ι φ i)) ?_
  exact IsColimit.ofWhiskerEquivalence (Discrete.equivalence (Equiv.punitProd.{0} ι).symm) (coproductIsCoproduct φ)

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