integralClosure_algebraMap_injective

English

More generally, the injectivity of the algebra map from the valuation subring to the integral closure persists when mapping through the integral closures along a scalar tower.

Русский

Более обобщенно, инъективность алгебраического отображения сохраняется при отображении через интегральные замыкания по цепочке скаляров.

LaTeX

$$$\\text{integralClosureAlgebraMapInjective} :\\; \\text{Injective } (\\mathrm{algebraMap}\\; v.valuationSubring \\; (\\mathrm{integralClosure}(v.valuationSubring L))).$$$

Lean4

theorem integralClosure_algebraMap_injective :
    Injective (algebraMap v.valuationSubring (integralClosure v.valuationSubring L)) :=
  FaithfulSMul.algebraMap_injective ↥v.valuationSubring ↥(integralClosure (↥v.valuationSubring) L)

Похожие утверждения