Theorems · Theorem · commutative algebra

Algebra.FormallySmooth.iff_split_injection

∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {P : Type u_2}
  [inst_3 : CommRing P] [inst_4 : Algebra R P] [Algebra.FormallySmooth R P] [inst_6 : Algebra P A]
  [IsScalarTower R P A],
  Function.Surjective ⇑(algebraMap P A) →
    (Algebra.FormallySmooth R A ↔ ∃ l, l ∘ₗ KaehlerDifferential.kerCotangentToTensor R P A = LinearMap.id)

Given a formally smooth R-algebra P and a surjective algebra homomorphism f : P →ₐ[R] A with kernel I (typically a presentation R[X] → A), A is formally smooth iff the P-linear map I/I² → A ⊗[P] Ω[P⁄R] is split injective. Also see Algebra.Extension.formallySmooth_iff_split_injection for the version in terms of Extension.

Defined in

Mathlib.RingTheory.Smooth.Basic

Cited by

3 results in Mathlib

Foundations

Depth 127 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraCommRingAlgebraAlgebra.FormallySmoothAlgebraIsScalarTower