Theorems · Inductive type · commutative algebra

Algebra.FormallyUnramified

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

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

Cited by

75 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CommRingCommRingAlgebra