Documentation

Mathlib.RingTheory.Adjoin.Tower

Adjoining elements and being finitely generated in an algebra tower #

Main results #

theorem Algebra.adjoin_res_eq_adjoin_res (C : Type u_1) (D : Type u_2) (E : Type u_3) (F : Type u_4) [CommSemiring C] [CommSemiring D] [CommSemiring E] [CommSemiring F] [Algebra C D] [Algebra C E] [Algebra C F] [Algebra D F] [Algebra E F] [IsScalarTower C D F] [IsScalarTower C E F] {S : Set D} {T : Set E} (hS : Algebra.adjoin C S = ) (hT : Algebra.adjoin C T = ) :
theorem Algebra.fg_trans' {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] (hRS : .FG) (hSA : .FG) :
.FG
theorem exists_subalgebra_of_fg (A : Type w) (B : Type u₁) (C : Type u_1) [CommSemiring A] [CommSemiring B] [Semiring C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower 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) [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra B C] [Algebra A C] [IsScalarTower A B C] [IsNoetherianRing A] (hAC : .FG) (hBC : .FG) (hBCi : Function.Injective (algebraMap B C)) :
.FG

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.