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 : Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R s)))
(h2 : Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin (↥(Algebra.adjoin R s)) t)))
:
Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R (s ∪ t)))
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
- Subalgebra.FG S = ∃ (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)
:
Subalgebra.FG (Algebra.adjoin R ↑s)
theorem
Subalgebra.fg_def
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{S : Subalgebra R A}
:
Subalgebra.FG S ↔ ∃ (t : Set A), Set.Finite t ∧ Algebra.adjoin R t = S
theorem
Subalgebra.fg_of_fg_toSubmodule
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
{S : Subalgebra R A}
:
Submodule.FG (Subalgebra.toSubmodule S) → Subalgebra.FG S
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)
:
theorem
Subalgebra.fg_of_submodule_fg
{R : Type u}
{A : Type v}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(h : Submodule.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 : Subalgebra.FG S)
(hT : Subalgebra.FG T)
:
Subalgebra.FG (Subalgebra.prod S T)
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 : Subalgebra.FG S)
:
Subalgebra.FG (Subalgebra.map f S)
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.FG (Subalgebra.map f S))
:
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]
:
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 : Subalgebra.FG S)
[IsNoetherianRing R]
: