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) :
theorem algebra.adjoin_eq_of_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) (h₂ : S algebra.adjoin R s) :
theorem algebra.adjoin_eq {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
theorem algebra.adjoin_induction {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s : set A} {p : A → Prop} {x : A} (h : x algebra.adjoin R s) (Hs : ∀ (x : A), x sp x) (Halg : ∀ (r : R), p ((algebra_map R A) r)) (Hadd : ∀ (x y : A), p xp yp (x + y)) (Hmul : ∀ (x y : A), p xp yp (x * y)) :
p x
theorem algebra.adjoin_union {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.span_le_adjoin (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (s : set A) :
theorem algebra.adjoin_to_submodule_le (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s : set A} {t : submodule R A} :
theorem algebra.adjoin_eq_span_of_subset (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] {s : set A} (hs : (submonoid.closure s) (submodule.span R s)) :
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.adjoint_prod_le (R : Type u) {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (s : set A) (t : set B) :
theorem algebra.adjoin_inl_union_inr_le_prod (R : Type u) {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (s : set A) (t : set B) :
theorem algebra.mem_adjoin_of_map_mul (R : Type u) {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {s : set A} {x : A} {f : A →ₗ[R] B} (hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = (f a₁) * f a₂) (h : x algebra.adjoin R s) :
f x algebra.adjoin R (f '' (s {1}))
theorem algebra.adjoin_inl_union_inr_eq_prod (R : Type u) {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (s : set A) (t : set B) :
theorem algebra.adjoin_union_eq_under (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_prod {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} {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} [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) :