Structures · Algebra

Algebra.FormallyUnramified

An R-algebra A is formally unramified if Ω[A⁄R] is trivial. This is equivalent to "for every R-algebra, every square-zero ideal I : Ideal B and f : A →ₐ[R] B ⧸ I, there exists at most one lift A →ₐ[R] B". See Algebra.FormallyUnramified.iff_comp_injective.

Defined in

Mathlib.RingTheory.Unramified.Basic

Shape

2 explicit arguments · adds subsingleton_kaehlerDifferential