English
If α = β, then the corresponding congruence on apps holds after taking opposite, mirroring congr_app with op arguments.
Русский
Если α=β, то соответствующее согласующее отображение сохраняется после взятия противоположного
LaTeX
$$$\forall \{X,Y:\mathrm{SheafedSpace}(C)\},\; \alpha,\beta:\, X\to Y,\; h:\alpha=\beta\Rightarrow \alpha.c.app(\mathrm{op}\,U) = (\beta.c.app(\mathrm{op}\,U))\circ (X.presheaf.map(\mathrm{eqToHom}(⋯)))$$$
Lean4
theorem epi_of_base_surjective_of_stalk_mono {X Y : SheafedSpace C} (f : X ⟶ Y) (h₁ : Function.Surjective f.base)
(h₂ : ∀ x, Mono (f.stalkMap x)) : Epi f := by
constructor
intro Z ⟨g, gc⟩ ⟨h, hc⟩ e
obtain rfl : g = h :=
ConcreteCategory.hom_ext _ _ fun y ↦ by
rw [← (h₁ y).choose_spec]
simpa using congr(($e).base.hom (h₁ y).choose)
refine SheafedSpace.hom_stalk_ext ⟨g, gc⟩ ⟨g, hc⟩ rfl fun y ↦ ?_
rw [← (h₁ y).choose_spec, ← cancel_mono (f.stalkMap (h₁ y).choose), stalkCongr_hom, stalkSpecializes_refl,
Category.id_comp, ← PresheafedSpace.stalkMap.comp f ⟨g, gc⟩, ← PresheafedSpace.stalkMap.comp f ⟨g, hc⟩]
congr 1
