English
An auxiliary equivalence between a certain endomorphism quotient and a kerSquareLift composition holds, bridging cotangent quotients and linear lifts.
Русский
Справочная эквалентность между квантизированным эндоморфизмом и композициями сохраняет структуру котангента и линейного подъема.
LaTeX
$$End_equiv_aux (f : S →ₐ[R] S ⊗ S ⧸ KaehlerDifferential.ideal R S ^ 2) : (Ideal.Quotient.mkₐ R (KaehlerDifferential.ideal R S).cotangentIdeal).comp f = IsScalarTower.toAlgHom R S _ ↔ (TensorProduct.lmul' R : S ⊗[R] S →ₐ[R] S).kerSquareLift.comp f = AlgHom.id R S$$
Lean4
/-- `Ω[S⁄R]` is trivial if `R → S` is surjective.
Also see `Algebra.FormallyUnramified.iff_subsingleton_kaehlerDifferential`. -/
theorem subsingleton_of_surjective (h : Function.Surjective (algebraMap R S)) : Subsingleton Ω[S⁄R] :=
by
suffices (⊤ : Submodule S Ω[S⁄R]) ≤ ⊥ from (subsingleton_iff_forall_eq 0).mpr fun y ↦ this trivial
rw [← KaehlerDifferential.span_range_derivation, Submodule.span_le]
rintro _ ⟨x, rfl⟩; obtain ⟨x, rfl⟩ := h x; simp
