of_surjective — Mathlib

English

If f: A →ₐ[R] B is surjective and A is unramified over R, then B is unramified over R.

Русский

Если алгебра-гомоморфизм f: A → B над R сюръективен и A неразветвлена над R, то B тоже неразвлена над R.

LaTeX

$$$[\text{Surjective } f] \land [\text{Unramified } R \; A] \Rightarrow [\text{Unramified } R \; B]$$$

Lean4

/-- This holds in general for epimorphisms. -/
theorem of_surjective [FormallyUnramified R A] (f : A →ₐ[R] B) (H : Function.Surjective f) : FormallyUnramified R B :=
  by
  rw [iff_comp_injective]
  intro Q _ _ I hI f₁ f₂ e
  ext x
  obtain ⟨x, rfl⟩ := H x
  rw [← AlgHom.comp_apply, ← AlgHom.comp_apply]
  congr 1
  apply FormallyUnramified.comp_injective I hI
  ext x; exact DFunLike.congr_fun e (f x)

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