surjective_of_epi — Mathlib

English

If f is an epi morphism in PresheafOfModules, then for every X in C^op the map f.app X is surjective.

Русский

Если f является эпиморфизмом в PresheafOfModules, то для каждого объекта X в C^op отображение f.app X сюръективно.

LaTeX

$$$[Epi\ f] \\Rightarrow \\forall X, \\ Function.Surjective (f.app X)$$$

Lean4

theorem surjective_of_epi [Epi f] (X : Cᵒᵖ) : Function.Surjective (f.app X) :=
  by
  rw [← ModuleCat.epi_iff_surjective]
  infer_instance

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