English
Given a multicoequalizer diagram in Type with sets A ⊆ X and families U,V of subsets, the induced multicofork map is a colimit in Type. In other words, in Type, A is the multicoequalizer of the family U along V.
Русский
Дано диаграмма мультиэквалайзера в категорийных типах с A ⊆ X и семействами U,V; индуцированная multicofork карта образует колимит в Type. Иначе говоря, A является мультиэквалайзерной подмножеством U вдоль V.
LaTeX
$$$\text{isColimitOfMulticoequalizerDiagram}(c) : \mathrm{IsColimit}(c.multicofork.map(\mathrm{Set}.functorToTypes)).$$$
Lean4
/-- Given `X : Type u`, `A : Set X`, `U : ι → Set X` and `V : ι → ι → Set X` such
that `MulticoequalizerDiagram A U V` holds, then in the category of types,
`A` is the multicoequalizer of the `U i`s along the `V i j`s. -/
noncomputable def isColimitOfMulticoequalizerDiagram (c : MulticoequalizerDiagram A U V) :
IsColimit (c.multicofork.map Set.functorToTypes) :=
by
let e := (c.multispanIndex.map Set.functorToTypes).multispan
apply _root_.Nonempty.some
rw [Types.isColimit_iff_coconeTypesIsColimit, Functor.CoconeTypes.isMulticoequalizer_iff]
refine ⟨fun i₁ i₂ ⟨x₁, h₁⟩ ⟨x₂, h₂⟩ h ↦ ?_, fun ⟨x, hx⟩ ↦ ?_⟩
· dsimp at i₁ i₂ h₁ h₂
obtain rfl : x₁ = x₂ := by simpa using h
have eq₁ :=
e.ιColimitType_map (WalkingMultispan.Hom.fst (J := .prod ι) ⟨i₁, i₂⟩)
⟨x₁, by dsimp; rw [c.min_eq]; exact ⟨h₁, h₂⟩⟩
have eq₂ :=
e.ιColimitType_map (WalkingMultispan.Hom.snd (J := .prod ι) ⟨i₁, i₂⟩)
⟨x₁, by dsimp; rw [c.min_eq]; exact ⟨h₁, h₂⟩⟩
dsimp [e] at eq₁ eq₂
rw [eq₁, eq₂]
· simp only [MulticoequalizerDiagram.multicofork_pt, ← c.iSup_eq, Set.iSup_eq_iUnion, Set.mem_iUnion] at hx
obtain ⟨i, hi⟩ := hx
exact ⟨i, ⟨x, hi⟩, rfl⟩
