English
The algebra map from the valuation subring to the integral closure of L is injective, hence the inclusion of the subring into the integral closure is faithful.
Русский
Алгебраическое отображение от valuationSubring к интегральному замыканию в L является инъективным, следовательно включение подкольца в интегральное замыкание верно сохраняет различие.
LaTeX
$$$\\text{Injective } (\\mathrm{algebraMap}\\, v.valuationSubring\\, (\\mathrm{integralClosure}(v.valuationSubring L))).$$$
Lean4
/-- A ring equivalence between the integral closure of the valuation subring of `K` in `L`
and a ring `R` satisfying `isIntegralClosure R v.valuationSubring L`. -/
protected noncomputable def equiv (R : Type*) [CommRing R] [Algebra v.valuationSubring R] [Algebra R L]
[IsScalarTower v.valuationSubring R L] [IsIntegralClosure R v.valuationSubring L] :
integralClosure v.valuationSubring L ≃+* R :=
by
have := IsScalarTower.subalgebra' (valuationSubring v) L L (integralClosure (valuationSubring v) L)
exact (IsIntegralClosure.equiv v.valuationSubring R L (integralClosure v.valuationSubring L)).symm.toRingEquiv
