map_of_surjective — Mathlib

English

If M is FG over L and f:M→[L]N is surjective, then N is FG over L.

Русский

Если M порождается конечном образом и отображение f:M→[L]N сюръективно, то N также порождается конечном образом.

LaTeX

$$$\text{FG}(L,M) \land \operatorname{Surjective}(f) \Rightarrow \text{FG}(L,N)$$$

Lean4

theorem map_of_surjective {N : Type*} [L.Structure N] (h : FG L M) (f : M →[L] N) (hs : Function.Surjective f) :
    FG L N := by
  rw [← Hom.range_eq_top] at hs
  rw [fg_def, ← hs]
  exact h.range f

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