English
Let A, B, C be commutative rings and f: A →+* B, g: B →+* C. If the composite g ∘ f is finite as an A-algebra, then g is finite as a B-algebra (i.e., C is finite over B).
Русский
Пусть A, B, C – коммутативные кольца, f: A →+* B и g: B →+* C. Если композиция g ∘ f сконечна как A-алгебра, то и g сконечна как B-алгебра (то есть C сконечна над B).
LaTeX
$$$\\\\forall A B C \, [\\\\text{CommRing } A] \, [\\\\text{CommRing } B] \, [\\\\text{CommRing } C], \\\\ f:A \\to A +* B, \\\\ g:B \\to B +* C, \\\\ (g \\circ f).Finite \\\\Rightarrow \\\\ g.Finite.$$$
Lean4
theorem of_comp_finite {f : A →+* B} {g : B →+* C} (h : (g.comp f).Finite) : g.Finite :=
by
algebraize [f, g, g.comp f]
exact Module.Finite.of_restrictScalars_finite A B C
