English
If A is finite as an R-module, then A is algebraic over R (as an instance).
Русский
Если A является конечной как модуль над R, то A алгебраическая над R (инстанс).
LaTeX
$$[Module.Finite R A] ⇒ Algebra.IsAlgebraic R A$$
Lean4
theorem restrictScalars [Algebra.IsAlgebraic R S] {a : A} (h : IsAlgebraic S a) : IsAlgebraic R a :=
by
have ⟨p, hp, eval0⟩ := h
by_cases hRS : Function.Injective (algebraMap R S)
on_goal 2 =>
exact (Algebra.isAlgebraic_of_not_injective fun h ↦ hRS <| .of_comp (IsScalarTower.algebraMap_eq R S A ▸ h)).1 _
have := hRS.noZeroDivisors _ (map_zero _) (map_mul _)
classical
have ⟨r, hr, int⟩ := Algebra.IsAlgebraic.exists_integral_multiples R (p.support.image (coeff p))
let p :=
(r • p).toSubring (integralClosure R S).toSubring fun s hs ↦
by
obtain ⟨n, hn, rfl⟩ := mem_coeffs_iff.mp hs
exact int _ (Finset.mem_image_of_mem _ <| support_smul _ _ hn)
have : IsAlgebraic (integralClosure R S) a := by
refine ⟨p, ?_, ?_⟩
· have : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr hRS
simpa only [← Polynomial.map_ne_zero_iff (f := Subring.subtype _) Subtype.val_injective, p, map_toSubring,
smul_ne_zero_iff] using And.intro hr hp
rw [← eval_map_algebraMap, Subalgebra.algebraMap_eq, ← map_map, ← Subalgebra.toSubring_subtype, map_toSubring,
eval_map_algebraMap, ← AlgHom.restrictScalars_apply R, map_smul, AlgHom.restrictScalars_apply, eval0, smul_zero]
exact restrictScalars_of_isIntegral _ this
