def
HasLinearlyIndependentDifferentials
(R : Type u)
(A : Type v)
(B : Type w)
[CommRing R]
[CommRing A]
[CommRing B]
[Algebra R A]
[Algebra A B]
[Algebra R B]
[IsScalarTower R A B]
:
Predicate asserting that the canonical map from the cotangent module of
the kernel I = ker(A → B) to B ⊗_A Ω[A/R] has a left inverse, i.e. that the
differentials of generators of I are linearly independent in B ⊗_A Ω[A/R].
Instances For
theorem
smooth_subvariety_criterion_formallySmooth
{R : Type u}
{A : Type v}
{B : Type w}
[CommRing R]
[CommRing A]
[CommRing B]
[Algebra R A]
[Algebra A B]
[Algebra R B]
[IsScalarTower R A B]
[Algebra.FormallySmooth R A]
(hf : Function.Surjective ⇑(algebraMap A B))
:
Formally-smooth version of the smooth subvariety criterion: assuming A
is formally smooth over R and A → B is surjective, B is formally smooth
over R iff the defining ideal has linearly independent differentials.
theorem
smooth_subvariety_criterion
{R : Type u}
{A : Type v}
{B : Type w}
[CommRing R]
[CommRing A]
[CommRing B]
[Algebra R A]
[Algebra A B]
[Algebra R B]
[IsScalarTower R A B]
[Algebra.Smooth R A]
(hf : Function.Surjective ⇑(algebraMap A B))
(hker : (RingHom.ker (algebraMap A B)).FG)
:
Smooth subvariety criterion (Cor 25, Lec 20): if A is smooth over R
and A → B is surjective with finitely generated kernel, then B is smooth
over R iff the kernel has linearly independent differentials, i.e. iff the
subvariety is locally defined by independent differentials.