of_equiv — Mathlib

English

If e: A ≃ₐ[R] B is an algebra isomorphism, and A is formally smooth over R, then B is formally smooth over R.

Русский

Если e: A ≃ₐ[R] B — алгебраический изоморфизм, и A формально гладко над R, то B также формально гладко над R.

LaTeX

$$of_equiv (e : A ≃ₐ[R] B) : FormallySmooth R B given FormallySmooth R A.$$

Lean4

theorem of_equiv [FormallySmooth R A] (e : A ≃ₐ[R] B) : FormallySmooth R B :=
  by
  constructor
  intro C _ _ I hI f
  use (FormallySmooth.lift I ⟨2, hI⟩ (f.comp e : A →ₐ[R] C ⧸ I)).comp e.symm
  rw [← AlgHom.comp_assoc, FormallySmooth.comp_lift, AlgHom.comp_assoc, AlgEquiv.comp_symm, AlgHom.comp_id]

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