fg_of_fg_map

Mathlib.RingTheory.Finiteness.Basic

URI: https://scilib.ai/kg/mathlib#Submodule.fg_of_fg_map

← MathLib Explorer

English

If f is injective and (N.map f).FG holds, then N.FG holds.

Русский

Если f инъективно и (N.map f).FG, то N.FG.

LaTeX

$$hf : Function.Injective f → (N.map f).FG → N.FG$$

Lean4

theorem fg_of_fg_map {R M P : Type*} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P]
    (f : M →ₗ[R] P) (hf : LinearMap.ker f = ⊥) {N : Submodule R M} (hfn : (N.map f).FG) : N.FG :=
  fg_of_fg_map_injective f (LinearMap.ker_eq_bot.1 hf) hfn

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru