English
If L is algebraic over A, and C is the integral closure of A in L, then the fraction field of C is L.
Русский
Если L является алгебраическим над A, и C — интегральное замыкание A в L, то поле дробей C равно L.
LaTeX
$$$\operatorname{Frac}(\mathrm{integralClosure}(A,L)) \cong L$$$
Lean4
/-- If the field `L` is an algebraic extension of the integral domain `A`,
the integral closure `C` of `A` in `L` has fraction field `L`. -/
theorem isFractionRing_of_algebraic [Algebra.IsAlgebraic A L] (inj : ∀ x, algebraMap A L x = 0 → x = 0) :
IsFractionRing C L :=
{ map_units := fun ⟨y, hy⟩ =>
IsUnit.mk0 _
(show algebraMap C L y ≠ 0 from fun h =>
mem_nonZeroDivisors_iff_ne_zero.mp hy
((injective_iff_map_eq_zero (algebraMap C L)).mp (algebraMap_injective C A L) _ h))
surj := fun z =>
let ⟨x, hx, int⟩ := (Algebra.IsAlgebraic.isAlgebraic z).exists_integral_multiple
⟨⟨mk' C _ int, algebraMap _ _ x,
mem_nonZeroDivisors_of_ne_zero fun h ↦
hx (inj _ <| by rw [IsScalarTower.algebraMap_apply A C L, h, RingHom.map_zero])⟩,
by rw [algebraMap_mk', ← IsScalarTower.algebraMap_apply A C L, Algebra.smul_def, mul_comm]⟩
exists_of_eq := fun {x y} h => ⟨1, by simpa using algebraMap_injective C A L h⟩ }
