English
A key equality showing the compatibility of res_mk with pullback via the isomorphisms in the Plus construction.
Русский
Ключевое равенство, показывающее совместимость res_mk с вытяжкой через изоморфизмы в конструкции Plus.
LaTeX
$$$(J.plusObj P).map f.op (mk x) = mk (x.pullback f)$$$
Lean4
theorem res_mk_eq_mk_pullback {Y X : C} {P : Cᵒᵖ ⥤ D} {S : J.Cover X} (x : Meq P S) (f : Y ⟶ X) :
(J.plusObj P).map f.op (mk x) = mk (x.pullback f) :=
by
dsimp [mk, plusObj]
rw [← comp_apply (x := (Meq.equiv P S).symm x), ι_colimMap_assoc, colimit.ι_pre,
comp_apply (x := (Meq.equiv P S).symm x)]
apply congr_arg
apply (Meq.equiv P _).injective
dsimp only [Functor.op_obj, pullback_obj]
rw [Equiv.apply_symm_apply]
ext i
simp only [Functor.op_obj, unop_op, pullback_obj, diagram_obj, Functor.comp_obj, diagramPullback_app, Meq.equiv_apply,
Meq.pullback_apply]
rw [← ConcreteCategory.comp_apply, Multiequalizer.lift_ι]
erw [Meq.equiv_symm_eq_apply]
cases i; rfl
