of_submodule_quotient — Mathlib

English

If N ≤ M is a submodule with N FG and the quotient M/N FG, then M is FG.

Русский

Если N — подмодуль M c FG и M/N FG, то M FG.

LaTeX

$$N FG ∧ (M/N) FG ⇒ M FG$$

Lean4

theorem _root_.Module.Finite.of_submodule_quotient (N : Submodule R M) [Module.Finite R N] [Module.Finite R (M ⧸ N)] :
    Module.Finite R M where
  fg_top :=
    fg_of_fg_map_of_fg_inf_ker N.mkQ (by simpa only [map_top, range_mkQ] using Module.finite_def.mp ‹_›) <| by
      simpa only [top_inf_eq, ker_mkQ] using Module.Finite.iff_fg.mp ‹_›

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