Documentation

Mathlib.RingTheory.Adjoin.FG

Adjoining elements to form subalgebras #

This file develops the basic theory of finitely-generated subalgebras.

Definitions #

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
Instances For
    theorem Subalgebra.fg_def {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} :
    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.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) :
    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) :
    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.induction_on_adjoin {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] [IsNoetherian R A] (P : Subalgebra R AProp) (base : P ) (ih : ∀ (S : Subalgebra R A) (x : A), P SP (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] :