map — Mathlib

English

If S is finitely generated over R and f is an algebra hom, then the image subalgebra S.map f is finitely generated.

Русский

Если S FG, то образ через f подалгебры S.map f FG.

LaTeX

$$$S.FG \\rightarrow (\\operatorname{Subalgebra.map} f\\; S).FG$$$

Lean4

theorem map {S : Subalgebra R A} (f : A →ₐ[R] B) (hs : S.FG) : (S.map f).FG :=
  by
  let ⟨s, hs⟩ := hs
  classical exact ⟨s.image f, by rw [Finset.coe_image, Algebra.adjoin_image, hs]⟩

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