English
Two representatives x and y, living on covers S and T of X, yield equal mk-images precisely when there is a common refinement W of S and T and the refinements of x and y agree after pulling back along the maps to W.
Русский
Две представления x и y над покрытиями S и T дают равные изображения mk тогда и только тогда существует общий Refinement W над S и T и соответствия x и y после переноса на W согласованы.
LaTeX
$$$mk x = mk y \\iff \\exists W\\in J.Cover X\\; \\exists h_1: W\\to S\\; \\exists h_2: W\\to T,\\; x.refine h_1 = y.refine h_2$$$
Lean4
theorem eq_mk_iff_exists {X : C} {P : Cᵒᵖ ⥤ D} {S T : J.Cover X} (x : Meq P S) (y : Meq P T) :
mk x = mk y ↔ ∃ (W : J.Cover X) (h1 : W ⟶ S) (h2 : W ⟶ T), x.refine h1 = y.refine h2 :=
by
constructor
· intro h
obtain ⟨W, h1, h2, hh⟩ := Concrete.colimit_exists_of_rep_eq (C := D) _ _ _ h
use W.unop, h1.unop, h2.unop
ext I
apply_fun Multiequalizer.ι (W.unop.index P) I at hh
convert hh
all_goals
dsimp [diagram]
rw [← ConcreteCategory.comp_apply, Multiequalizer.lift_ι]
erw [Meq.equiv_symm_eq_apply]
cases I; rfl
· rintro ⟨S, h1, h2, e⟩
apply Concrete.colimit_rep_eq_of_exists (C := D)
use op S, h1.op, h2.op
apply Concrete.multiequalizer_ext
intro i
apply_fun fun ee => ee i at e
convert e using 1
all_goals
dsimp [diagram]
rw [← ConcreteCategory.comp_apply, Multiequalizer.lift_ι]
erw [Meq.equiv_symm_eq_apply]
cases i; rfl
