# Adjoining elements to form subalgebras

This file develops the basic theory of subalgebras of an R-algebra generated by a set of elements. A basic interface for adjoin is set up, and various results about finitely-generated subalgebras and submodules are proved.

## Definitions

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

## Tags

theorem algebra.subset_adjoin {R : Type u} {A : Type v} [semiring A] [ A] {s : set A} :
s s)

theorem algebra.adjoin_le {R : Type u} {A : Type v} [semiring A] [ A] {s : set A} {S : A} (H : s S) :
S

theorem algebra.adjoin_le_iff {R : Type u} {A : Type v} [semiring A] [ A] {s : set A} {S : A} :
S s S

theorem algebra.adjoin_mono {R : Type u} {A : Type v} [semiring A] [ A] {s t : set A} (H : s t) :

@[simp]
theorem algebra.adjoin_empty (R : Type u) (A : Type v) [semiring A] [ A] :

theorem algebra.adjoin_eq_span (R : Type u) {A : Type v} [semiring A] [ A] (s : set A) :
s) =

theorem algebra.adjoin_image (R : Type u) {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] (f : A →ₐ[R] B) (s : set A) :
(f '' s) = s).map f

@[simp]
theorem algebra.adjoin_insert_adjoin (R : Type u) {A : Type v} [semiring A] [ A] (s : set A) (x : A) :
(insert x s)) = (insert x s)

theorem algebra.adjoin_union (R : Type u) {A : Type v} [ A] (s t : set A) :
(s t) = s).under t)

theorem algebra.adjoin_eq_range (R : Type u) {A : Type v} [ A] (s : set A) :

theorem algebra.adjoin_singleton_eq_range (R : Type u) {A : Type v} [ A] (x : A) :
{x} =

theorem algebra.adjoin_singleton_one (R : Type u) {A : Type v} [ A] :
{1} =

theorem algebra.adjoin_union_coe_submodule (R : Type u) {A : Type v} [ A] (s t : set A) :
(s t)) = ( s)) * t)

theorem algebra.adjoin_int {R : Type u} [comm_ring R] (s : set R) :

theorem algebra.mem_adjoin_iff {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] {s : set A} {x : A} :

theorem algebra.adjoin_eq_ring_closure {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] (s : set A) :

theorem algebra.fg_trans {R : Type u} {A : Type v} [comm_ring R] [comm_ring A] [ A] {s t : set A} (h1 : s).fg) (h2 : t).fg) :
(s t)).fg

def subalgebra.fg {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :
Prop

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

Equations
theorem subalgebra.fg_adjoin_finset {R : Type u} {A : Type v} [semiring A] [ A] (s : finset A) :
s).fg

theorem subalgebra.fg_def {R : Type u} {A : Type v} [semiring A] [ A] {S : A} :
S.fg ∃ (t : set A), t.finite = S

theorem subalgebra.fg_bot {R : Type u} {A : Type v} [semiring A] [ A] :

theorem subalgebra.fg_of_fg_to_submodule {R : Type u} {A : Type v} [semiring A] [ A] {S : A} :
S.fg → S.fg

theorem subalgebra.fg_of_noetherian {R : Type u} {A : Type v} [semiring A] [ A] [ A] (S : A) :
S.fg

theorem subalgebra.fg_of_submodule_fg {R : Type u} {A : Type v} [semiring A] [ A] (h : .fg) :

theorem subalgebra.fg_map {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (S : A) (f : A →ₐ[R] B) (hs : S.fg) :
(S.map f).fg

theorem subalgebra.fg_of_fg_map {R : Type u} {A : Type v} {B : Type w} [semiring A] [ A] [semiring B] [ B] (S : A) (f : A →ₐ[R] B) (hf : function.injective f) (hs : (S.map f).fg) :
S.fg

theorem subalgebra.fg_top {R : Type u} {A : Type v} [semiring A] [ A] (S : A) :

theorem subalgebra.induction_on_adjoin {R : Type u} {A : Type v} [semiring A] [ A] [ A] (P : A → Prop) (base : P ) (ih : ∀ (S : A) (x : A), P SP (insert x S))) (S : A) :
P S

@[instance]
def alg_hom.is_noetherian_ring_range {R : Type u} {A : Type v} {B : Type w} [comm_ring R] [comm_ring A] [comm_ring B] [ A] [ B] (f : A →ₐ[R] B)  :

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

theorem is_noetherian_ring_of_fg {R : Type u} {A : Type v} [comm_ring R] [comm_ring A] [ A] {S : A} (HS : S.fg)  :

theorem is_noetherian_ring_closure {R : Type u} [comm_ring R] (s : set R) (hs : s.finite) :