of_equiv — Mathlib

English

Smoothness transfers under algebra isomorphisms: if A is smooth over R and e: A ≃ₐ[R] B, then B is smooth over R.

Русский

Гладкость переносится через алгебраические изоморфизмы: если A гладко над R, то и B гладко над R.

LaTeX

$$$[\operatorname{Smooth} R A] \Rightarrow [\operatorname{Smooth} R B] \text{ for } e: A \cong_R B$$$

Lean4

/-- Being smooth is transported via algebra isomorphisms. -/
theorem of_equiv [Smooth R A] (e : A ≃ₐ[R] B) : Smooth R B
    where
  formallySmooth := FormallySmooth.of_equiv e
  finitePresentation := FinitePresentation.equiv e

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