Adjoining elements to form subalgebras #
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}
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
{s : Set A}
{t : Set A}
(h1 : (Subalgebra.toSubmodule (Algebra.adjoin R s)).FG)
(h2 : (Subalgebra.toSubmodule (Algebra.adjoin (↥(Algebra.adjoin R s)) t)).FG)
:
(Subalgebra.toSubmodule (Algebra.adjoin R (s ∪ t))).FG
def
Subalgebra.FG
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S : Subalgebra R A)
:
A subalgebra S is finitely generated if there exists t : Finset A such that
Algebra.adjoin R t = S.
Equations
- S.FG = ∃ (t : Finset A), Algebra.adjoin R ↑t = S
Instances For
theorem
Subalgebra.fg_adjoin_finset
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(s : Finset A)
:
(Algebra.adjoin R ↑s).FG
theorem
Subalgebra.fg_def
{R : Type u}
{A : Type v}
[CommSemiring 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}
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
⊥.FG
theorem
Subalgebra.fg_of_fg_toSubmodule
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{S : Subalgebra R A}
:
(Subalgebra.toSubmodule S).FG → S.FG
theorem
Subalgebra.fg_of_noetherian
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
[IsNoetherian R A]
(S : Subalgebra R A)
:
S.FG
theorem
Subalgebra.fg_of_submodule_fg
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(h : ⊤.FG)
:
⊤.FG
theorem
Subalgebra.FG.prod
{R : Type u}
{A : Type v}
{B : Type w}
[CommSemiring 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}
[CommSemiring 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}
[CommSemiring 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}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(S : Subalgebra R A)
:
theorem
Subalgebra.induction_on_adjoin
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
[IsNoetherian R A]
(P : Subalgebra R A → Prop)
(base : P ⊥)
(ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S)))
(S : Subalgebra R A)
:
P S
instance
AlgHom.isNoetherianRing_range
{R : Type u}
{A : Type v}
{B : Type w}
[CommSemiring R]
[CommRing A]
[CommRing B]
[Algebra R A]
[Algebra R B]
(f : A →ₐ[R] B)
[IsNoetherianRing A]
:
IsNoetherianRing ↥f.range
The image of a Noetherian R-algebra under an R-algebra map is a Noetherian ring.
Equations
- ⋯ = ⋯
theorem
isNoetherianRing_of_fg
{R : Type u}
{A : Type v}
[CommRing R]
[CommRing A]
[Algebra R A]
{S : Subalgebra R A}
(HS : S.FG)
[IsNoetherianRing R]
: