map

Mathlib.RingTheory.Finiteness.Basic

URI: https://scilib.ai/kg/mathlib#Submodule.FG.map

← MathLib Explorer

English

If f is injective and the image N.map f is finitely generated, then N is finitely generated.

Русский

Если f инъективно и образ N.map f конечно порожден, то N порожден как FG.

LaTeX

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

Lean4

theorem map {N : Submodule R M} (hs : N.FG) : (N.map f).FG :=
  let ⟨t, ht⟩ := fg_def.1 hs
  fg_def.2 ⟨f '' t, ht.1.image _, by rw [span_image, ht.2]⟩

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

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

Разделы

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

Аффилиация

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