mathlib documentation

ring_theory.adjoin.basic

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 #

Tags #

adjoin, algebra, finitely-generated algebra

theorem algebra.subset_adjoin {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s : set A} :
theorem algebra.adjoin_le {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s : set A} {S : subalgebra R A} (H : s S) :
theorem algebra.adjoin_le_iff {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s : set A} {S : subalgebra R A} :
theorem algebra.adjoin_mono {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s t : set A} (H : s t) :
@[simp]
theorem algebra.adjoin_empty (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] :
theorem algebra.adjoin_eq_span (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (s : set A) :
theorem algebra.adjoin_image (R : Type u) {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) (s : set A) :
@[simp]
theorem algebra.adjoin_insert_adjoin (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (s : set A) (x : A) :
theorem algebra.adjoin_union (R : Type u) {A : Type v} [comm_semiring R] [comm_semiring A] [algebra R A] (s t : set A) :
theorem algebra.adjoin_eq_range (R : Type u) {A : Type v} [comm_semiring R] [comm_semiring A] [algebra R A] (s : set A) :
theorem algebra.adjoin_singleton_eq_range (R : Type u) {A : Type v} [comm_semiring R] [comm_semiring A] [algebra R A] (x : A) :
theorem algebra.adjoin_singleton_one (R : Type u) {A : Type v} [comm_semiring R] [comm_semiring A] [algebra R A] :
theorem algebra.mem_adjoin_iff {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {s : set A} {x : A} :
theorem algebra.adjoin_eq_ring_closure {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (s : set A) :
theorem algebra.fg_trans {R : Type u} {A : Type v} [comm_ring R] [comm_ring A] [algebra R A] {s t : set A} (h1 : (algebra.adjoin R s).to_submodule.fg) (h2 : (algebra.adjoin (algebra.adjoin R s) t).to_submodule.fg) :
def subalgebra.fg {R : Type u} {A : Type v} [comm_semiring 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
theorem subalgebra.fg_adjoin_finset {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (s : finset A) :
theorem subalgebra.fg_def {R : Type u} {A : Type v} [comm_semiring 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} [comm_semiring R] [semiring A] [algebra R A] :
theorem subalgebra.fg_of_fg_to_submodule {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {S : subalgebra R A} :
theorem subalgebra.fg_of_noetherian {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] [is_noetherian R A] (S : subalgebra R A) :
S.fg
theorem subalgebra.fg_of_submodule_fg {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (h : .fg) :
theorem subalgebra.fg_map {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (S : subalgebra R 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} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (S : subalgebra R 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} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
theorem subalgebra.induction_on_adjoin {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] [is_noetherian R A] (P : subalgebra R A → Prop) (base : P ) (ih : ∀ (S : subalgebra R A) (x : A), P SP (algebra.adjoin R (insert x S))) (S : subalgebra R 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] [algebra R A] [algebra R B] (f : A →ₐ[R] B) [is_noetherian_ring A] :

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] [algebra R A] {S : subalgebra R A} (HS : S.fg) [is_noetherian_ring R] :
theorem is_noetherian_ring_closure {R : Type u} [comm_ring R] (s : set R) (hs : s.finite) :