of_equiv — Mathlib

English

If A ≃ₐ[R] B and A is formally étale over R, then B is formally étale over R.

Русский

Если A и B эквивалентны как A-билю, и A формально étale над R, то B тоже формально étale над R.

LaTeX

$$$\text{FormallyEtale}(R,A) \Rightarrow \text{FormallyEtale}(R,B)$ given an algebra equivalence $A \simeq_R B$$$

Lean4

theorem of_equiv [FormallyEtale R A] (e : A ≃ₐ[R] B) : FormallyEtale R B :=
  FormallyEtale.iff_unramified_and_smooth.mpr ⟨FormallyUnramified.of_equiv e, FormallySmooth.of_equiv e⟩

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