English
Let R → A be a morphism of commutative rings with A an R-algebra. The unramified locus of A over R consists precisely of those primes p of R for which the Kähler differentials Ω_{A/R} vanish after localization at p; equivalently, the unramified locus is the complement of the support of Ω_{A/R} in Spec(R).
Русский
Пусть R → A — гомоморфизм коммутативных колец, причём A является R-алгеброй. Неразветвленная локация A над R состоит ровно из таких простых идеалов p в Spec(R), для которых локализация Ω_{A/R} в p равна нулю; эквивалентно, это дополнение поддержки Ω_{A/R} в Spec(R).
LaTeX
$$$\\operatorname{unramifiedLocus}(R,A) = \\bigl( \\operatorname{Module.support} A \\Omega[A\\,/\\,R] \\bigr)^{c}$$$
Lean4
theorem unramifiedLocus_eq_compl_support : unramifiedLocus R A = (Module.support A Ω[A⁄R])ᶜ :=
by
ext p
simp only [Set.mem_compl_iff, Module.notMem_support_iff]
have := IsLocalizedModule.iso p.asIdeal.primeCompl (KaehlerDifferential.map R R A (Localization.AtPrime p.asIdeal))
exact (Algebra.formallyUnramified_iff _ _).trans this.subsingleton_congr.symm
