fg_of_fg_map — Mathlib

English

If S.map f is finitely generated and f is injective, then S is finitely generated.

Русский

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

LaTeX

$$Given f injective and (S.map f).FG, then S.FG.$$

Lean4

theorem fg_of_fg_map (S : Subalgebra R A) (f : A →ₐ[R] B) (hf : Function.Injective f) (hs : (S.map f).FG) : S.FG :=
  let ⟨s, hs⟩ := hs
  ⟨s.preimage f fun _ _ _ _ h ↦ hf h,
    map_injective hf <|
      by
      rw [← Algebra.adjoin_image, Finset.coe_preimage, Set.image_preimage_eq_of_subset, hs]
      rw [← AlgHom.coe_range, ← Algebra.adjoin_le_iff, hs, ← Algebra.map_top]
      exact map_mono le_top⟩

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