English
Let S be a finite-type algebra over R. Then S is formally unramified over R if and only if there exists an element t in S ⊗_R S such that t annihilates all elements of the form 1 ⊗ s − s ⊗ 1 for s ∈ S, and the image of t under the natural S-algebra map S ⊗_R S → S is 1.
Русский
Пусть S является алгеброй конечного типа над R. Тогда S формально неразветвлена над R if и only if существует элемент t в S ⊗_R S, такой что t убивает все элементы вида 1 ⊗ s − s ⊗ 1 для всех s ∈ S, и образ t под естественной картой S ⊗_R S → S равен 1.
LaTeX
$$$\\operatorname{FormallyUnramified}(R,S) \\iff \\exists t \\in S \\otimes_R S, \\left( \\forall s \\in S, (1 \\otimes s - s \\otimes 1) \\cdot t = 0 \\right) \\land \\operatorname{lmul}'(R,t) = 1$$$
Lean4
/-- Proposition I.2.3 + I.2.6 of [iversen]
A finite-type `R`-algebra `S` is (formally) unramified iff there exists a `t : S ⊗[R] S` satisfying
1. `t` annihilates every `1 ⊗ s - s ⊗ 1`.
2. the image of `t` is `1` under the map `S ⊗[R] S → S`.
-/
theorem iff_exists_tensorProduct [EssFiniteType R S] :
FormallyUnramified R S ↔
∃ t : S ⊗[R] S, (∀ s, ((1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S)) * t = 0) ∧ TensorProduct.lmul' R t = 1 :=
by
rw [formallyUnramified_iff, KaehlerDifferential, Ideal.cotangent_subsingleton_iff,
Ideal.isIdempotentElem_iff_of_fg _ (KaehlerDifferential.ideal_fg R S)]
have : ∀ t : S ⊗[R] S, TensorProduct.lmul' R t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S :=
by
intro t
simp only [KaehlerDifferential.ideal, RingHom.mem_ker, map_sub, map_one, sub_eq_zero, @eq_comm S 1]
simp_rw [this, ← KaehlerDifferential.span_range_eq_ideal]
constructor
· rintro ⟨e, he₁, he₂ : _ = Ideal.span _⟩
refine ⟨1 - e, ?_, ?_⟩
· intro s
obtain ⟨x, hx⟩ : e ∣ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1 :=
by
rw [← Ideal.mem_span_singleton, ← he₂]
exact Ideal.subset_span ⟨s, rfl⟩
rw [hx, mul_comm, ← mul_assoc, sub_mul, one_mul, he₁.eq, sub_self, zero_mul]
· rw [sub_sub_cancel, he₂, Ideal.mem_span_singleton]
· rintro ⟨t, ht₁, ht₂⟩
use 1 - t
rw [← sub_sub_self 1 t] at ht₁; generalize 1 - t = e at *
constructor
· suffices e ∈ (Submodule.span (S ⊗[R] S) {1 - e}).annihilator by
simpa [IsIdempotentElem, mul_sub, sub_eq_zero, eq_comm, -Ideal.submodule_span_eq,
Submodule.mem_annihilator_span_singleton] using this
exact
(show Ideal.span _ ≤ _ by
simpa only [Ideal.span_le, Set.range_subset_iff, Submodule.mem_annihilator_span_singleton, SetLike.mem_coe])
ht₂
· apply le_antisymm <;>
simp only [Ideal.submodule_span_eq, Ideal.mem_span_singleton, ht₂, Ideal.span_le, Set.singleton_subset_iff,
SetLike.mem_coe, Set.range_subset_iff]
intro s
use 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1
linear_combination ht₁ s
