English
The application of toPlus to x is computed by mk, i.e. toPlus P applied to x equals mk x.
Русский
Применение toPlus к x вычисляется через mk: toPlus P применяемый к x равен mk x.
LaTeX
$$$(J.toPlus P).app\ _ x = mk (Meq.mk S x)$$$
Lean4
theorem toPlus_apply {X : C} {P : Cᵒᵖ ⥤ D} (S : J.Cover X) (x : Meq P S) (I : S.Arrow) :
(J.toPlus P).app _ (x I) = (J.plusObj P).map I.f.op (mk x) :=
by
dsimp only [toPlus, plusObj]
delta Cover.toMultiequalizer
dsimp [mk]
rw [← ConcreteCategory.comp_apply, ι_colimMap_assoc, colimit.ι_pre, ConcreteCategory.comp_apply,
ConcreteCategory.comp_apply]
dsimp only [Functor.op]
let e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE (OrderTop.le_top _)
rw [← colimit.w _ e.op, ConcreteCategory.comp_apply]
apply congr_arg
apply Concrete.multiequalizer_ext (C := D)
intro i
dsimp
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply,
Multiequalizer.lift_ι, Multiequalizer.lift_ι, Multiequalizer.lift_ι]
erw [Meq.equiv_symm_eq_apply]
simpa using (x.condition (Cover.Relation.mk' (I.precompRelation i.f))).symm
