English
For any Finset s ⊂ A, there exists y ≠ 0 in R such that ∀ z ∈ s, IsIntegral R (y • z).
Русский
Для любого конечного множества s ⊂ A существует y ≠ 0 в R, такое что ∀ z ∈ s, IsIntegral R (y • z).
LaTeX
$$∀ (s : Finset A), ∃ y ≠ (0 : R), ∀ z ∈ s, IsIntegral R (y • z)$$
Lean4
theorem restrictScalars_of_isIntegral [int : Algebra.IsIntegral R S] {a : A} (h : IsAlgebraic S a) : IsAlgebraic R a :=
by
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 _)
have ⟨s, hs, int_s⟩ := h.exists_integral_multiple
cases subsingleton_or_nontrivial R
· have := Module.subsingleton R S
exact (is_transcendental_of_subsingleton _ _ h).elim
have ⟨r, hr, _, e⟩ := (int.1 s).isAlgebraic.exists_nonzero_dvd (mem_nonZeroDivisors_of_ne_zero hs)
refine .of_smul_isIntegral (y := r) (by rwa [isNilpotent_iff_eq_zero]) ?_
rw [Algebra.smul_def, IsScalarTower.algebraMap_apply R S, e, ← Algebra.smul_def, mul_comm, mul_smul]
exact isIntegral_trans _ (int_s.smul _)
