Adjoining elements to form subalgebras

This file develops the basic theory of finitely-generated subalgebras.

Definitions

• FG (S : Subalgebra R A) : A predicate saying that the subalgebra is finitely-generated as an A-algebra

Tags

adjoin, algebra, finitely-generated algebra

theorem Algebra.fg_trans {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] {s t : Set A} (h1 : (Subalgebra.toSubmodule (adjoin R s)).FG) (h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG) : (Subalgebra.toSubmodule (adjoin R (s ∪ t))).FG

def Subalgebra.FG {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : Prop

A subalgebra S is finitely generated if there exists t : Finset A such that Algebra.adjoin R t = S.

Equations

• S.FG = ∃ (t : Finset A), Algebra.adjoin R ↑t = S

theorem Subalgebra.fg_adjoin_finset {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (s : Finset A) : (Algebra.adjoin R ↑s).FG

theorem Subalgebra.fg_def {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} : S.FG ↔ ∃ (t : Set A), t.Finite ∧ Algebra.adjoin R t = S

theorem Subalgebra.fg_bot {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : ⊥.FG

theorem Subalgebra.fg_of_fg_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} : (toSubmodule S).FG → S.FG

theorem Subalgebra.fg_of_noetherian {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] [IsNoetherian R A] (S : Subalgebra R A) : S.FG

theorem Subalgebra.fg_of_submodule_fg {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (h : ⊤.FG) : ⊤.FG

theorem Subalgebra.FG.prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {S : Subalgebra R A} {T : Subalgebra R B} (hS : S.FG) (hT : T.FG) : (S.prod T).FG

theorem Subalgebra.FG.map {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {S : Subalgebra R A} (f : A →ₐ[R] B) (hs : S.FG) : (Subalgebra.map f S).FG

theorem Subalgebra.fg_of_fg_map {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (S : Subalgebra R A) (f : A →ₐ[R] B) (hf : Function.Injective ⇑f) (hs : (map f S).FG) : S.FG

theorem Subalgebra.fg_top {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : ⊤.FG ↔ S.FG

theorem Subalgebra.induction_on_adjoin {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] [IsNoetherian R A] (P : Subalgebra R A → Prop) (base : P ⊥) (ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))) (S : Subalgebra R A) : P S

theorem Subalgebra.FG.sup {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S S' : Subalgebra R A} (hS : S.FG) (hS' : S'.FG) : (S ⊔ S').FG

instance AlgHom.isNoetherianRing_range {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) [IsNoetherianRing A] : IsNoetherianRing ↥f.range

The image of a Noetherian R-algebra under an R-algebra map is a Noetherian ring.

theorem isNoetherianRing_of_fg {R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A] {S : Subalgebra R A} (HS : S.FG) [IsNoetherianRing R] : IsNoetherianRing ↥S

theorem is_noetherian_subring_closure {R : Type u} [CommRing R] (s : Set R) (hs : s.Finite) : IsNoetherianRing ↥(Subring.closure s)