English
If two points in the glued diagram have the same π-image, they are related by the equivalence generated by the coequalizer relations.
Русский
Если два элемента слитого диаграммного контура имеют одинаковый образ π, они связаны отношением эквивалентности, порождённом отношениями коэквалентности.
LaTeX
$$$\forall x,y,\ πx = πy \Rightarrow \text{EqvGen}(\text{Function.Coequalizer.Rel } \,\, x,y)$$$
Lean4
theorem eqvGen_of_π_eq {x y : ↑(∐ D.U)} (h : 𝖣.π x = 𝖣.π y) :
Relation.EqvGen (Function.Coequalizer.Rel 𝖣.diagram.fstSigmaMap 𝖣.diagram.sndSigmaMap) x y :=
by
delta GlueData.π Multicoequalizer.sigmaπ at h
replace h :
coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap x =
coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap y :=
(TopCat.mono_iff_injective (Multicoequalizer.isoCoequalizer 𝖣.diagram).inv).mp inferInstance h
let diagram := parallelPair 𝖣.diagram.fstSigmaMap 𝖣.diagram.sndSigmaMap ⋙ forget _
have : colimit.ι diagram one x = colimit.ι diagram one y :=
by
dsimp only [coequalizer.π] at h
rw [← ι_preservesColimitIso_hom, ConcreteCategory.forget_map_eq_coe, types_comp_apply]
simp_all
have :
(colimit.ι diagram _ ≫ colim.map _ ≫ (colimit.isoColimitCocone _).hom) _ =
(colimit.ι diagram _ ≫ colim.map _ ≫ (colimit.isoColimitCocone _).hom) _ :=
(congr_arg
(colim.map (diagramIsoParallelPair diagram).hom ≫ (colimit.isoColimitCocone (Types.coequalizerColimit _ _)).hom)
this :
_)
simp only [eqToHom_refl, colimit.ι_map_assoc, diagramIsoParallelPair_hom_app, colimit.isoColimitCocone_ι_hom,
Category.id_comp] at this
exact Quot.eq.1 this