mathlib documentation

ring_theory.adjoin

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} :
s Salgebra.adjoin R 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} :

@[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.adjoin_union_coe_submodule (R : Type u) {A : Type v} [comm_semiring R] [comm_semiring A] [algebra R A] (s t : set 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} :

def subalgebra.fg {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] :
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} :
S.fg → S.fg

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] :
.fg.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) :
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) :
function.injective f(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] :