Adjoining elements and being finitely generated in an algebra tower #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main results #
algebra.fg_trans': ifSis finitely generated asR-algebra andAasS-algebra, thenAis finitely generated asR-algebrafg_of_fg_of_fg: Artin--Tate lemma: if C/B/A is a tower of 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.
theorem
algebra.adjoin_algebra_map
(R : Type u)
(S : Type v)
(A : Type w)
[comm_semiring R]
[comm_semiring S]
[semiring A]
[algebra R S]
[algebra S A]
[algebra R A]
[is_scalar_tower R S A]
(s : set S) :
algebra.adjoin R (⇑(algebra_map S A) '' s) = subalgebra.map (is_scalar_tower.to_alg_hom R S A) (algebra.adjoin R s)
theorem
algebra.adjoin_restrict_scalars
(C : Type u_1)
(D : Type u_2)
(E : Type u_3)
[comm_semiring C]
[comm_semiring D]
[comm_semiring E]
[algebra C D]
[algebra C E]
[algebra D E]
[is_scalar_tower C D E]
(S : set E) :
theorem
algebra.adjoin_res_eq_adjoin_res
(C : Type u_1)
(D : Type u_2)
(E : Type u_3)
(F : Type u_4)
[comm_semiring C]
[comm_semiring D]
[comm_semiring E]
[comm_semiring F]
[algebra C D]
[algebra C E]
[algebra C F]
[algebra D F]
[algebra E F]
[is_scalar_tower C D F]
[is_scalar_tower C E F]
{S : set D}
{T : set E}
(hS : algebra.adjoin C S = ⊤)
(hT : algebra.adjoin C T = ⊤) :
subalgebra.restrict_scalars C (algebra.adjoin E (⇑(algebra_map D F) '' S)) = subalgebra.restrict_scalars C (algebra.adjoin D (⇑(algebra_map E F) '' T))
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) :
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.