English
For any functor F, the action on morphisms respects composition: F.map g (F.map f a) = F.map (f ∘ g) a.
Русский
Действие F на морфизмы сохраняет композицию: F.map g (F.map f a) = F.map (f ∘ g) a.
LaTeX
$$$\forall X,Y,Z, f: X\to Y, g: Y\to Z, a,\ F: (F\,)\; (F.map g (F.map f\; a)) = F.map (f \circ g) a$$$
Lean4
/-- The two parallel maps in the equalizer diagram for the sheaf condition corresponding to the
inclusion maps in a disjoint coproduct are equal.
-/
theorem firstMap_eq_secondMap :
Equalizer.Presieve.Arrows.firstMap F X c.inj = Equalizer.Presieve.Arrows.secondMap F X c.inj :=
by
ext a ⟨i, j⟩
simp only [Equalizer.Presieve.Arrows.firstMap, Types.pi_lift_π_apply, types_comp_apply,
Equalizer.Presieve.Arrows.secondMap]
by_cases hi : i = j
· rw [hi, Mono.right_cancellation _ _ pullback.condition]
· have := preservesTerminal_of_isSheaf_for_empty F hF hI
apply_fun
(F.mapIso ((hd hi).isoPullback).op ≪≫
F.mapIso (terminalIsoIsTerminal (terminalOpOfInitial initialIsInitial)).symm ≪≫
(PreservesTerminal.iso F)).hom using
injective_of_mono _
ext ⟨i⟩
exact i.elim
