English
mk' is additive with respect to addition for integral elements.
Русский
mk' аддитивно по сложению для интегральных элементов.
LaTeX
$$mk'_add$$
Lean4
/-- If A is an R-algebra all of whose elements are integral over R,
and x is an element of an A-algebra that is integral over A, then x is integral over R. -/
theorem isIntegral_trans [Algebra.IsIntegral R A] (x : B) (hx : IsIntegral A x) : IsIntegral R x :=
by
rcases hx with ⟨p, pmonic, hp⟩
let S := adjoin R (p.coeffs : Set A)
have : Module.Finite R S :=
⟨(Subalgebra.toSubmodule S).fg_top.mpr <|
fg_adjoin_of_finite p.coeffs.finite_toSet fun a _ ↦ Algebra.IsIntegral.isIntegral a⟩
let p' : S[X] := p.toSubring S.toSubring subset_adjoin
have hSx : IsIntegral S x :=
⟨p', (p.monic_toSubring _ _).mpr pmonic,
by
rw [IsScalarTower.algebraMap_eq S A B, ← eval₂_map]
convert hp; apply p.map_toSubring S.toSubring⟩
let Sx := Subalgebra.toSubmodule (adjoin S { x })
let MSx : Module S Sx :=
SMulMemClass.toModule
_ -- the next line times out without this
have : Module.Finite S Sx := ⟨(Submodule.fg_top _).mpr hSx.fg_adjoin_singleton⟩
refine
.of_mem_of_fg ((adjoin S { x }).restrictScalars R) ?_ _
((Subalgebra.mem_restrictScalars R).mpr <| subset_adjoin rfl)
rw [← Submodule.fg_top, ← Module.finite_def]
letI : SMul S Sx :=
{ MSx with } -- need this even though MSx is there
have : IsScalarTower R S Sx := Submodule.isScalarTower Sx
exact Module.Finite.trans S Sx
