fg_top — Mathlib

English

The FG-ness of the top subalgebra over S is equivalent to the FG-ness of S itself.

Русский

Финитная генерация верхней подалгебры над S эквивалентна FG самой S.

LaTeX

$$$\\text{fg\_top}$$$

Lean4

theorem fg_top (S : Subalgebra R A) : (⊤ : Subalgebra R S).FG ↔ S.FG :=
  ⟨fun h ↦ by
    rw [← S.range_val, ← Algebra.map_top]
    exact FG.map _ h, fun h ↦
    fg_of_fg_map _ S.val Subtype.val_injective <|
      by
      rw [Algebra.map_top, range_val]
      exact h⟩

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