eqvGen_of_π_eq — Mathlib

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

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