English
Localization of integral closure in an algebraic setting coincides with localization in the target field.
Русский
Локализация интегрального замыкания в алгебраическом контексте совпадает с локализацией в целевом поле.
LaTeX
$$$\text IsLocalization (Algebra.algebraMapSubmonoid C (nonZeroDivisors A)) L$$$
Lean4
/-- If `L` is an algebraic extension of `K = Frac(A)` and `L` has no zero smul divisors by `A`,
then `L` is the localization of the integral closure `C` of `A` in `L` at `A⁰`. -/
theorem isLocalization [IsDomain A] [Algebra.IsAlgebraic K L] : IsLocalization (Algebra.algebraMapSubmonoid C A⁰) L :=
by
haveI : IsDomain C := (IsIntegralClosure.equiv A C L (integralClosure A L)).toMulEquiv.isDomain (integralClosure A L)
haveI : NoZeroSMulDivisors A L := NoZeroSMulDivisors.trans_faithfulSMul A K L
haveI : NoZeroSMulDivisors A C := IsIntegralClosure.noZeroSMulDivisors A L
refine ⟨?_, fun z => ?_, fun {x y} h => ⟨1, ?_⟩⟩
· rintro ⟨_, x, hx, rfl⟩
rw [isUnit_iff_ne_zero, map_ne_zero_iff _ (IsIntegralClosure.algebraMap_injective C A L), Subtype.coe_mk,
map_ne_zero_iff _ (FaithfulSMul.algebraMap_injective A C)]
exact mem_nonZeroDivisors_iff_ne_zero.mp hx
· obtain ⟨m, hm⟩ :=
IsIntegral.exists_multiple_integral_of_isLocalization A⁰ z (Algebra.IsIntegral.isIntegral (R := K) z)
obtain ⟨x, hx⟩ : ∃ x, algebraMap C L x = m • z := IsIntegralClosure.isIntegral_iff.mp hm
refine ⟨⟨x, algebraMap A C m, m, SetLike.coe_mem m, rfl⟩, ?_⟩
rw [Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, hx, mul_comm, Submonoid.smul_def, smul_def]
· simp only [IsIntegralClosure.algebraMap_injective C A L h]
