quotient — Mathlib

English

If A is unramified over R and I is an ideal in A, then the quotient A/I is unramified over R.

Русский

Если A неразветвлено над R, то фактор-кольцо A/I также неразветвлено над R.

LaTeX

$$$[\text{Unramified } R \; A] \Rightarrow [\text{Unramified } R \; A/I]$$$

Lean4

instance quotient {A} [CommRing A] [Algebra R A] [FormallyUnramified R A] (I : Ideal A) :
    FormallyUnramified R (A ⧸ I) :=
  FormallyUnramified.of_surjective (IsScalarTower.toAlgHom R A (A ⧸ I)) Ideal.Quotient.mk_surjective

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