of_epi — Mathlib

English

If G is generated by x, then for any morphism f, (G.image f) is generated by the images f.app (X i) (x i).

Русский

Если G порожден через x, то образ подпрешефа по f порожден образом f.app (X_i)(x_i).

LaTeX

$$$G\text{ IsGeneratedBy } x \Rightarrow \forall {F'} (f: F \to F'),\ (G.image f).IsGeneratedBy (\lambda i => f.app (X i) (x i))$$$

Lean4

theorem of_epi [Epi f] : PresheafIsGeneratedBy F' (fun i ↦ f.app _ (x i)) := by
  simpa only [Subpresheaf.range_eq_top f] using h.range f

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