English
The class of formally unramified ring homomorphisms is closed under pre- and post-composition with ring isomorphisms; i.e., if f: R → S is formally unramified and e: S ≃ T is a ring isomorphism, then e ∘ f: R → T is formally unramified, and if g: S → T is formally unramified and e: R ≃ S is an isomorphism, then g ∘ e: R ≃ T is formally unramified.
Русский
Класс морфизмов колец, формально немрамированных, сохраняется под пред- и посткомпозицией с изоморфизмами колец; если f: R → S формально немрамирован и e: S ≃ T — изоморфизм, то e ∘ f: R → T формально немрамирован; аналогично для g: S → T и e: R ≃ S.
LaTeX
$$$\\forall R,S,T$ коммутативные кольца, $f:R\\to S$, $e:S\\simeq T$, $\\mathrm{FrmUnramified}(f) \\Rightarrow \\mathrm{FrmUnramified}(e\\circ f)$ и $\\forall f:S\\to T$, $e:R\\simeq S$, $\\mathrm{FrmUnramified}(f) \\Rightarrow \\mathrm{FrmUnramified}(f\\circ e)$$$
Lean4
theorem respectsIso : RespectsIso FormallyUnramified :=
by
refine stableUnderComposition.respectsIso ?_
intro R S _ _ e
letI := e.toRingHom.toAlgebra
exact Algebra.FormallyUnramified.of_surjective (Algebra.ofId R S) e.surjective
