Theorems · Theorem · commutative algebra

fg_of_fg_of_fg

∀ (A : Type w) (B : Type u₁) (C : Type u_1) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  [inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C] [IsScalarTower A B C] [IsNoetherianRing A],
  ⊤.FG → ⊤.FG → 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; Altman--Kleiman 16.17.

Defined in

Mathlib.RingTheory.Adjoin.Tower

Cited by

0 results in Mathlib

Foundations

Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingCommRingAlgebraAlgebraAlgebraIsScalarTowerIsNoetherianRing