Formally étale morphisms #
An R
-algebra A
is formally étale (resp. unramified, smooth) if for every R
-algebra,
every square-zero ideal I : ideal B
and f : A →ₐ[R] B ⧸ I
, there exists
exactly (resp. at most, at least) one lift A →ₐ[R] B
.
We show that the property extends onto nilpotent ideals, and that these properties are stable
under R
-algebra homomorphisms and compositions.
- comp_injective : ∀ ⦃B : Type ?⦄ [_inst_6 : comm_ring B] [_inst_7 : algebra R B] (I : ideal B), I ^ 2 = ⊥ → function.injective (ideal.quotient.mkₐ R I).comp
An R
-algebra A
is formally unramified if 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
.
Instances of this typeclass
- comp_surjective : ∀ ⦃B : Type ?⦄ [_inst_6 : comm_ring B] [_inst_7 : algebra R B] (I : ideal B), I ^ 2 = ⊥ → function.surjective (ideal.quotient.mkₐ R I).comp
An R
algebra A
is formally smooth if for every R
-algebra, every square-zero ideal
I : ideal B
and f : A →ₐ[R] B ⧸ I
, there exists at least one lift A →ₐ[R] B
.
- comp_bijective : ∀ ⦃B : Type ?⦄ [_inst_6 : comm_ring B] [_inst_7 : algebra R B] (I : ideal B), I ^ 2 = ⊥ → function.bijective (ideal.quotient.mkₐ R I).comp
An R
algebra A
is formally étale if for every R
-algebra, every square-zero ideal
I : ideal B
and f : A →ₐ[R] B ⧸ I
, there exists exactly one lift A →ₐ[R] B
.
Instances of this typeclass
For a formally smooth R
-algebra A
and a map f : A →ₐ[R] B ⧸ I
with I
square-zero,
this is an arbitrary lift A →ₐ[R] B
.
Equations
- algebra.formally_smooth.lift I hI g = _.some
For a formally smooth R
-algebra A
and a map f : A →ₐ[R] B ⧸ I
with I
nilpotent,
this is an arbitrary lift A →ₐ[R] B
.
Equations
Let P →ₐ[R] A
be a surjection with kernel J
, and P
a formally smooth R
-algebra,
then A
is formally smooth over R
iff the surjection P ⧸ J ^ 2 →ₐ[R] A
has a section.
Geometric intuition: we require that a first-order thickening of Spec A
inside Spec P
admits
a retraction.
This holds in general for epimorphisms.
This actually does not need the localization instance, and is stated here again for
consistency. See algebra.formally_unramified.of_comp
instead.
The intended use is for copying proofs between formally_{unramified, smooth, etale}
without the need to change anything (including removing redundant arguments).