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
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} :
s ⊆ ↑(algebra.adjoin R s)
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) :
algebra.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} :
algebra.adjoin R s ≤ S ↔ s ⊆ ↑S
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) :
algebra.adjoin R s ≤ algebra.adjoin R t
@[simp]
theorem
algebra.adjoin_empty
(R : Type u)
(A : Type v)
[comm_semiring R]
[semiring A]
[algebra R A] :
algebra.adjoin R ∅ = ⊥
theorem
algebra.adjoin_eq_span
(R : Type u)
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(s : set A) :
↑(algebra.adjoin R s) = submodule.span R (monoid.closure 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) :
algebra.adjoin R (⇑f '' s) = (algebra.adjoin R s).map f
theorem
algebra.adjoin_union
(R : Type u)
{A : Type v}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
(s t : set A) :
algebra.adjoin R (s ∪ t) = (algebra.adjoin R s).under (algebra.adjoin ↥(algebra.adjoin R s) t)
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) :
algebra.adjoin R {x} = (polynomial.aeval x).range
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) :
↑(algebra.adjoin R (s ∪ t)) = (↑(algebra.adjoin R s)) * ↑(algebra.adjoin R t)
theorem
algebra.mem_adjoin_iff
{R : Type u}
{A : Type v}
[comm_ring R]
[ring A]
[algebra R A]
{s : set A}
{x : A} :
x ∈ algebra.adjoin R s ↔ x ∈ ring.closure (set.range ⇑(algebra_map R A) ∪ s)
theorem
algebra.adjoin_eq_ring_closure
{R : Type u}
{A : Type v}
[comm_ring R]
[ring A]
[algebra R A]
(s : set A) :
↑(algebra.adjoin R s) = ring.closure (set.range ⇑(algebra_map R A) ∪ s)
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).fg)
(h2 : ↑(algebra.adjoin ↥(algebra.adjoin R s) t).fg) :
↑(algebra.adjoin R (s ∪ t)).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.
theorem
subalgebra.fg_adjoin_finset
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
(s : finset A) :
(algebra.adjoin R ↑s).fg
theorem
subalgebra.fg_def
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{S : subalgebra R A} :
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) :
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) :
@[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] :