of_equiv — Mathlib

English

If A is unramified over R and e: A ≃ₐ[R] B is an algebra isomorphism, then B is unramified over R as well.

Русский

Если A неразветвлено над R и имеется алгебра-эквивалентность e: A ≃ₐ[R] B, то и B неразветвлено над R.

LaTeX

$$$\forall R,A,B\, (e: A \simeq_R B),\ Algebra.FormallyUnramified\, R\, B$$$

Lean4

theorem of_equiv [FormallyUnramified R A] (e : A ≃ₐ[R] B) : FormallyUnramified R B :=
  by
  rw [iff_comp_injective]
  intro C _ _ I hI f₁ f₂ e'
  rw [← f₁.comp_id, ← f₂.comp_id, ← e.comp_symm, ← AlgHom.comp_assoc, ← AlgHom.comp_assoc]
  congr 1
  refine FormallyUnramified.comp_injective I hI ?_
  rw [← AlgHom.comp_assoc, e', AlgHom.comp_assoc]

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