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 : (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
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).FGS.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) :
    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) :
    .FG S.FG
    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] :
    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] :
    theorem is_noetherian_subring_closure {R : Type u} [CommRing R] (s : Set R) (hs : s.Finite) :