mathlib documentation

ring_theory.adjoin.tower

Adjoining elements and being finitely generated in an algebra tower #

Main results #

theorem algebra.fg_trans' {R : Type u_1} {S : Type u_2} {A : Type u_3} [comm_semiring R] [comm_semiring S] [comm_semiring A] [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A] (hRS : .fg) (hSA : .fg) :
theorem exists_subalgebra_of_fg (A : Type w) (B : Type u₁) (C : Type u_1) [comm_semiring A] [comm_semiring B] [semiring C] [algebra A B] [algebra B C] [algebra A C] [is_scalar_tower A B C] (hAC : .fg) (hBC : .fg) :
(B₀ : subalgebra A B), B₀.fg .fg
theorem fg_of_fg_of_fg (A : Type w) (B : Type u₁) (C : Type u_1) [comm_ring A] [comm_ring B] [comm_ring C] [algebra A B] [algebra B C] [algebra A C] [is_scalar_tower A B C] [is_noetherian_ring A] (hAC : .fg) (hBC : .fg) (hBCi : function.injective (algebra_map B C)) :

Artin--Tate lemma: if A ⊆ B ⊆ C is a chain of subrings of commutative rings, and A is noetherian, and C is algebra-finite over A, and C is module-finite over B, then B is algebra-finite over A.

References: Atiyah--Macdonald Proposition 7.8; Stacks 00IS; Altman--Kleiman 16.17.