mathlib3 documentation

ring_theory.adjoin.fg

Adjoining elements to form subalgebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Definitions #

Tags #

adjoin, algebra, finitely-generated algebra

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_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) :
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 : (subalgebra.map f S).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 S P (algebra.adjoin R (has_insert.insert x S))) (S : subalgebra R A) :
P S
@[protected, instance]

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] :