mathlib documentation

ring_theory.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} [comm_semiring R] [comm_semiring A] [algebra R A] {s t : set A} (h1 : (algebra.adjoin R s).to_submodule.fg) (h2 : (algebra.adjoin (algebra.adjoin R s) t).to_submodule.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.

Equations
theorem subalgebra.fg_adjoin_finset {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (s : finset A) :
theorem subalgebra.fg_def {R : Type u} {A : Type v} [comm_semiring 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} [comm_semiring R] [semiring A] [algebra 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} :
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_of_submodule_fg {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (h : .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) :
(S.prod 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) :
(S.map f).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 : (S.map f).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 SP (algebra.adjoin R (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] :