mono_of_base_injective_of_stalk_epi

English

If a morphism f has a surjective base map and each stalk map is mono, then f is epi.

Русский

Если база сюръективна и каждый stalkMap моно, то f эпиморфизм

LaTeX

$$$\forall f:X\to Y,\; \mathrm{Surjective}(f.base)\land (\forall x,\mathrm{Mono}(f.stalkMap\,x))\Rightarrow \mathrm{Epi}(f)$$$

Lean4

theorem mono_of_base_injective_of_stalk_epi {X Y : SheafedSpace C} (f : X ⟶ Y) (h₁ : Function.Injective f.base)
    (h₂ : ∀ x, Epi (f.stalkMap x)) : Mono f := by
  constructor
  intro Z ⟨g, gc⟩ ⟨h, hc⟩ e
  obtain rfl : g = h := ConcreteCategory.hom_ext _ _ fun x ↦ h₁ congr(($e).base x)
  refine SheafedSpace.hom_stalk_ext ⟨g, gc⟩ ⟨g, hc⟩ rfl fun x ↦ ?_
  rw [← cancel_epi (f.stalkMap (g x)), stalkCongr_hom, stalkSpecializes_refl, Category.id_comp, ←
    PresheafedSpace.stalkMap.comp ⟨g, gc⟩ f, ← PresheafedSpace.stalkMap.comp ⟨g, hc⟩ f]
  congr 1

Похожие утверждения