English
Being integrally closed is preserved under injective algebra homomorphisms: if f : A → B is an injective R-algebra homomorphism and B is integrally closed over R, then A is integrally closed over R as well.
Русский
Интегральная замкнутость сохраняется при инъективных алгебраических гомоморфизмах: если f:A→B — инъективный R-алгебра-гомоморфизм и B интегрально замкнуто относительно R, то и A интегрально замкнуто относительно R.
LaTeX
$$$\forall f\,\big(\text{Injective}(f)\;\rightarrow\; IsIntegrallyClosedIn\,R\,B \rightarrow IsIntegrallyClosedIn\,R\,A\big)$$$
Lean4
/-- Being integrally closed is preserved under injective algebra homomorphisms. -/
theorem isIntegrallyClosedIn (f : A →ₐ[R] B) (hf : Function.Injective f) :
IsIntegrallyClosedIn R B → IsIntegrallyClosedIn R A :=
by
rintro ⟨inj, cl⟩
refine ⟨Function.Injective.of_comp (f := f) ?_, fun hx => ?_, ?_⟩
· convert inj
aesop
· obtain ⟨y, fx_eq⟩ := cl.mp ((isIntegral_algHom_iff f hf).mpr hx)
aesop
· rintro ⟨y, rfl⟩
apply (isIntegral_algHom_iff f hf).mp
simp_all
