English
Algebraicity over R is preserved when passing to a fraction ring: S is algebraic over R iff K is algebraic over R, under appropriate towers.
Русский
Алгебраичность над R сохраняется при переходе к дробному кольцу: S алгебраичен над R тогда и только тогда, когда K алгебраичен над R, при надлежащих торовых условиях.
LaTeX
$$$\text{Algebra.IsAlgebraic}_R S \iff \text{Algebra.IsAlgebraic}_R K$$$
Lean4
/-- `S` is algebraic over `R` iff a fraction ring of `S` is algebraic over `R` -/
theorem isAlgebraic_iff' [Field K] [IsDomain R] [Algebra R K] [Algebra S K] [NoZeroSMulDivisors R K]
[IsFractionRing S K] [IsScalarTower R S K] : Algebra.IsAlgebraic R S ↔ Algebra.IsAlgebraic R K :=
by
simp only [Algebra.isAlgebraic_def]
constructor
· intro h x
letI := MulActionWithZero.nontrivial S K
letI := FractionRing.liftAlgebra R K
have := FractionRing.isScalarTower_liftAlgebra R K
rw [IsFractionRing.isAlgebraic_iff R (FractionRing R) K, isAlgebraic_iff_isIntegral]
obtain ⟨a : S, b, ha, rfl⟩ := div_surjective (A := S) x
obtain ⟨f, hf₁, hf₂⟩ := h b
rw [div_eq_mul_inv]
refine .mul ?_ (.inv ?_) <;>
exact isAlgebraic_iff_isIntegral.mp <| (h _).algebraMap.extendScalars (FaithfulSMul.algebraMap_injective R _)
· intro h x
obtain ⟨f, hf₁, hf₂⟩ := h (algebraMap S K x)
use f, hf₁
rw [Polynomial.aeval_algebraMap_apply] at hf₂
exact (injective_iff_map_eq_zero (algebraMap S K)).1 (FaithfulSMul.algebraMap_injective _ _) _ hf₂
