Theorems · Inductive type · commutative algebra

Algebra.FormallySmooth

(R : Type u) → (A : Type v) → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → Prop

An R-algebra A is formally smooth if Ω[A⁄R] is A-projective and H¹(L_{A/R}) = 0. For the infinitesimal lifting definition, see FormallySmooth.lift and FormallySmooth.iff_comp_surjective.

Defined in

Mathlib.RingTheory.Smooth.Basic

Cited by

60 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CommRingCommRingAlgebra