Naive cotangent complex associated to a presentation. #
Given a presentation 0 → I → R[x₁,...,xₙ] → S → 0
(or equivalently a closed embedding S ↪ Aⁿ
defined by I
), we may define the (naive) cotangent complex I/I² → ⨁ᵢ S dxᵢ → Ω[S/R] → 0
.
Main results #
Algebra.Extension.Cotangent
: The conormal spaceI/I²
. (Defined inGenerators/Basic
)Algebra.Extension.CotangentSpace
: The cotangent space⨁ᵢ S dxᵢ
.Algebra.Generators.cotangentSpaceBasis
: The canonical basis on⨁ᵢ S dxᵢ
.Algebra.Extension.CotangentComplex
: The mapI/I² → ⨁ᵢ S dxᵢ
.Algebra.Extension.toKaehler
: The projection⨁ᵢ S dxᵢ → Ω[S/R]
.Algebra.Extension.toKaehler_surjective
: The map⨁ᵢ S dxᵢ → Ω[S/R]
is surjective.Algebra.Extension.exact_cotangentComplex_toKaehler
:I/I² → ⨁ᵢ S dxᵢ → Ω[S/R]
is exact.Algebra.Extension.Hom.Sub
: Iff
andg
are two maps between presentations,f - g
induces a map⨁ᵢ S dxᵢ → I/I²
that makesf
andg
homotopic.Algebra.Extension.H1Cotangent
: The first homology of the (naive) cotangent complex ofS
overR
, induced by a given presentation.Algebra.H1Cotangent
:H¹(L_{S/R})
, the first homology of the (naive) cotangent complex ofS
overR
.
Implementation detail #
We actually develop these material for general extensions (i.e. surjection P → S
) so that we can
apply them to infinitesimal smooth (or versal) extensions later.
The cotangent space on P = R[X]
.
This is isomorphic to Sⁿ
with n
being the number of variables of P
.
Equations
- P.CotangentSpace = TensorProduct P.Ring S (Ω[P.Ring⁄R])
Instances For
The cotangent complex given by a presentation R[X] → S
(i.e. a closed embedding S ↪ Aⁿ
).
Equations
- One or more equations did not get rendered due to their size.
Instances For
This is the map on the cotangent space associated to a map of presentation.
The matrix associated to this map is the Jacobian matrix. See CotangentSpace.repr_map
.
Equations
- Algebra.Extension.CotangentSpace.map f = LinearMap.liftBaseChange S (↑P.Ring ((TensorProduct.mk P'.Ring S' (Ω[P'.Ring⁄R'])) 1) ∘ₗ KaehlerDifferential.map R R' P.Ring P'.Ring)
Instances For
If f
and g
are two maps P → P'
between presentations,
then the image of f - g
is in the kernel of P' → S
.
Equations
- f.subToKer g = LinearMap.codRestrict (Submodule.restrictScalars R P'.ker) (f.toAlgHom.toLinearMap - g.toAlgHom.toLinearMap) ⋯
Instances For
If f
and g
are two maps P → P'
between presentations,
their difference induces a map P.CotangentSpace →ₗ[S] P'.Cotangent
that makes two maps
between the cotangent complexes homotopic.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The projection map from the relative cotangent space to the module of differentials.
Equations
- P.toKaehler = KaehlerDifferential.mapBaseChange R P.Ring S
Instances For
The first homology of the (naive) cotangent complex of S
over R
,
induced by a given presentation 0 → I → P → R → 0
,
defined as the kernel of I/I² → S ⊗[P] Ω[P⁄R]
.
Equations
- P.H1Cotangent = ↥(LinearMap.ker P.cotangentComplex)
Instances For
Equations
- ⋯ = ⋯
The inclusion of H¹(L_{S/R})
into the conormal space of a presentation.
Equations
- Algebra.Extension.h1Cotangentι = (LinearMap.ker P.cotangentComplex).subtype
Instances For
The induced map on the first homology of the (naive) cotangent complex.
Equations
- Algebra.Extension.H1Cotangent.map f = (Algebra.Extension.Cotangent.map f).restrict ⋯
Instances For
The canonical basis on the CotangentSpace
.
Equations
- P.cotangentSpaceBasis = Basis.baseChange S (KaehlerDifferential.mvPolynomialBasis R P.vars)
Instances For
H¹(L_{S/R})
is independent of the presentation chosen.
Equations
- One or more equations did not get rendered due to their size.
Instances For
H¹(L_{S/R})
, the first homology of the (naive) cotangent complex of S
over R
.
Equations
- Algebra.H1Cotangent R S = (Algebra.Generators.self R S).toExtension.H1Cotangent
Instances For
The induced map on the first homology of the (naive) cotangent complex of S
over R
.
Equations
- Algebra.H1Cotangent.map R S S' T = Algebra.Extension.H1Cotangent.map ((Algebra.Generators.self R S').defaultHom (Algebra.Generators.self S T)).toExtensionHom
Instances For
H¹(L_{S/R})
is independent of the presentation chosen.
Equations
- P.equivH1Cotangent = Algebra.Generators.H1Cotangent.equiv P (Algebra.Generators.self R S)