Adjoining elements to form subalgebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file develops the basic theory of finitely-generated subalgebras.
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.fg_trans
{R : Type u}
{A : Type v}
[comm_semiring R]
[comm_semiring A]
[algebra R A]
{s t : set A}
(h1 : (⇑subalgebra.to_submodule (algebra.adjoin R s)).fg)
(h2 : (⇑subalgebra.to_submodule (algebra.adjoin ↥(algebra.adjoin R s) t)).fg) :
(⇑subalgebra.to_submodule (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_fg_to_submodule
{R : Type u}
{A : Type v}
[comm_semiring R]
[semiring A]
[algebra R A]
{S : subalgebra R A} :
(⇑subalgebra.to_submodule 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.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) :
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) :
(subalgebra.map f 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 : (subalgebra.map f S).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 S → P (algebra.adjoin R (has_insert.insert x ↑S)))
(S : subalgebra R A) :
P S
@[protected, instance]
def
alg_hom.is_noetherian_ring_range
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring 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] :