English
A cocone in Type is a multicoequalizer precisely when two compatibility conditions hold: (i) for all indices i1,i2 and elements x1,x2 with compatible images, the corresponding colimit identities agree; (ii) every element of the cocone's apex is hit by some i and some element of the corresponding right-side set.
Русский
Кокон в Type является мультиэквалайзером тогда и только тогда, когда выполняются две условия совместимости: (i) для любых индексов и элементов равенства образов гарантируют согласованность; (ii) каждый элемент апекса достигается некоторым индексовым элементом и элементом правой части.
LaTeX
$$$c.IsColimit \;\iff\; (\forall i_1,i_2:\!J.R)(x_1:\!d.right i_1)(x_2:\!d.right i_2),\; c.ι(.right i_1) x_1 = c.ι(.right i_2) x_2 \Rightarrow d.multispan.ιColimitType(.right i_1) x_1 = d.multispan.ιColimitType(.right i_2) x_2) \wedge\ (\forall x:\; c.pt), \exists i:\!J.R, \exists a:\!d.right i, c.ι(.right i) a = x.$$$
Lean4
theorem isMulticoequalizer_iff {J : MultispanShape.{w, w'}} {d : MultispanIndex J (Type u)}
(c : d.multispan.CoconeTypes) :
c.IsColimit ↔
(∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
c.ι (.right i₁) x₁ = c.ι (.right i₂) x₂ →
d.multispan.ιColimitType (.right i₁) x₁ = d.multispan.ιColimitType (.right i₂) x₂) ∧
(∀ (x : c.pt), ∃ (i : J.R) (a : d.right i), c.ι (.right i) a = x) :=
by
have (x : d.multispan.ColimitType) : ∃ (i : J.R) (a : d.right i), d.multispan.ιColimitType (.right i) a = x :=
by
obtain ⟨(l | r), z, rfl⟩ := d.multispan.ιColimitType_jointly_surjective x
· exact ⟨J.fst l, d.multispan.map (WalkingMultispan.Hom.fst l) z, by rw [ιColimitType_map]⟩
· exact ⟨r, z, by simp⟩
constructor
· intro hc
refine ⟨fun i₁ i₂ x₁ x₂ h ↦ ?_, ?_⟩
· simp only [← descColimitType_ιColimitType_apply] at h
exact hc.bijective.1 h
· intro x
obtain ⟨y, rfl⟩ := hc.bijective.2 x
obtain ⟨i, z, rfl⟩ := this y
exact ⟨i, z, by simp⟩
· rintro ⟨h₁, h₂⟩
refine ⟨fun x₁ x₂ h ↦ ?_, fun x ↦ ?_⟩
· obtain ⟨i₁, a₁, rfl⟩ := this x₁
obtain ⟨i₂, a₂, rfl⟩ := this x₂
exact h₁ _ _ _ _ h
· obtain ⟨i, y, rfl⟩ := h₂ x
exact ⟨d.multispan.ιColimitType (.right i) y, rfl⟩
