fg_of_fg_of_fg

theorem 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] [inst_6 : IsScalarTower A B C] [inst_7 : IsNoetherianRing A], ⊤.FG → ⊤.FG → Function.Injective ⇑(algebraMap B C) → ⊤.FG

**Artin-Tate lemma**: Given a chain of subrings A ⊆ B ⊆ C in commutative rings, and supposing that A is a Noetherian ring, and C is finitely generated as an algebra over A, and C is also finitely generated as a module over B, the theorem states that B is finitely generated as an algebra over A. In other words, if A is Noetherian and C is both algebra-finite over A and module-finite over B (with the algebra mapping from B to C being injective), then B is also algebra-finite over A. The theorem refers to several key concepts in algebra. A Noetherian ring is a ring such that all of its ideals are finitely generated. A ring (or module) is said to be finitely generated if there exist a finite number of elements such that any element in the ring (or module) can be expressed as a combination of these generating elements. The algebra mapping is a function that preserves the algebraic structure, and being injective implies that it maps distinct elements of B to distinct elements of C.

More concisely: Given a Noetherian subring A of B, and a finitely generated subring C of B that is also finitely generated as a module over B, if C is algebra-finite and module-finite over A with an injective algebra mapping from B to C, then B is algebra-finite over A.