unramifiedLocus_eq_univ_iff — Mathlib

English

The unramified locus is the whole spectrum if and only if A is formally unramified over R.

Русский

Неразветвленная локация есть вся спектральная схема Spec(R) тогда и только тогда, когда A формально неразветвлена над R.

LaTeX

$$$\\mathrm{unramifiedLocus}(R,A) = \\mathrm{Spec}(R) \\quad\\Longleftrightarrow\\quad \\mathrm{Algebra.FormallyUnramified}\\; R\\; A.$$$

Lean4

theorem unramifiedLocus_eq_univ_iff : unramifiedLocus R A = Set.univ ↔ Algebra.FormallyUnramified R A := by
  rw [unramifiedLocus_eq_compl_support, compl_eq_comm, Set.compl_univ, eq_comm, Module.support_eq_empty_iff,
    Algebra.formallyUnramified_iff]

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