Cotangent complex of a submersive presentation #

Let P be a submersive presentation of S as an R-algebra and denote by I the kernel R[X] → S. We show

SubmersivePresentation.free_cotangent: I ⧸ I ^ 2 is S-free on the classes of P.relation i.
SubmersivePresentation.subsingleton_h1Cotangent: H¹(L_{S/R}) = 0.
SubmersivePresentation.free_kaehlerDifferential: Ω[S⁄R] is S-free on the images of dxᵢ where i ∉ Set.range P.map.
SubmersivePresentation.rank_kaehlerDifferential: If S is non-trivial, the rank of Ω[S⁄R] is the dimension of P.

We also provide the corresponding instances for standard smooth algebras as corollaries.

We keep the notation I = ker(R[X] → S) in all docstrings of this file.

noncomputable def Algebra.PreSubmersivePresentation.cotangentComplexAux {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S) :

P.toExtension.Cotangent →ₗ[S] P.rels → S

Given a pre-submersive presentation, this is the composition I ⧸ I ^ 2 → ⊕ S dxᵢ → ⊕ S dxᵢ where the second direct sum runs over all i : P.rels induced by the injection P.map : P.rels → P.vars.

If P is submersive, this is an isomorphism. See SubmersivePresentation.cotangentEquiv.

Equations

P.cotangentComplexAux = ↑(Finsupp.linearEquivFunOnFinite S S P.rels) ∘ₗ Finsupp.lcomapDomain P.map ⋯ ∘ₗ ↑P.cotangentSpaceBasis.repr ∘ₗ P.toExtension.cotangentComplex

Instances For

source

theorem Algebra.PreSubmersivePresentation.cotangentComplexAux_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : PreSubmersivePresentation R S) (x : ↥P.ker) (i : P.rels) :

P.cotangentComplexAux (Extension.Cotangent.mk x) i = (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map i)) ↑x)

source

theorem Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P : PreSubmersivePresentation R S} (x : ↥P.ker) :

P.cotangentComplexAux (Extension.Cotangent.mk x) = 0 ↔ ∀ (i : P.rels), (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map i)) ↑x) = 0

source

theorem Algebra.SubmersivePresentation.cotangentComplexAux_injective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : SubmersivePresentation R S) :

Function.Injective ⇑P.cotangentComplexAux

source

theorem Algebra.SubmersivePresentation.cotangentComplexAux_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : SubmersivePresentation R S) :

Function.Surjective ⇑P.cotangentComplexAux

source

noncomputable def Algebra.SubmersivePresentation.cotangentEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : SubmersivePresentation R S) :

P.toExtension.Cotangent ≃ₗ[S] P.rels → S

The isomorphism of S-modules between I ⧸ I ^ 2 and P.rels → S given by P.relation i ↦ ∂ⱼ (P.relation i).

Equations

P.cotangentEquiv = LinearEquiv.ofBijective P.cotangentComplexAux ⋯

Instances For

source

@[simp]

theorem Algebra.SubmersivePresentation.cotangentEquiv_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : SubmersivePresentation R S) (a✝ : P.toExtension.Cotangent) (a✝¹ : P.rels) :

P.cotangentEquiv a✝ a✝¹ = P.cotangentComplexAux a✝ a✝¹

source

theorem Algebra.SubmersivePresentation.cotangentComplex_injective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : SubmersivePresentation R S) :

Function.Injective ⇑P.toExtension.cotangentComplex

source

instance Algebra.SubmersivePresentation.subsingleton_h1Cotangent {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : SubmersivePresentation R S) :

Subsingleton P.toExtension.H1Cotangent

If P is a submersive presentation, H¹ of the associated cotangent complex vanishes.

source

noncomputable def Algebra.SubmersivePresentation.basisCotangent {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : SubmersivePresentation R S) :

Basis P.rels S P.toExtension.Cotangent

The classes of P.relation i form a basis of I ⧸ I ^ 2.

Stacks Tag 00T7 ((3))

Equations

P.basisCotangent = { repr := P.cotangentEquiv.trans (Finsupp.linearEquivFunOnFinite S S P.rels).symm }

Instances For

source

instance Algebra.SubmersivePresentation.free_cotangent {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : SubmersivePresentation R S) :

Module.Free S P.toExtension.Cotangent

Stacks Tag 00T7 ((3))

source

noncomputable def Algebra.SubmersivePresentation.sectionCotangent {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : SubmersivePresentation R S) :

P.toExtension.CotangentSpace →ₗ[S] P.toExtension.Cotangent

If P is a submersive presentation, this is the section of the map I ⧸ I ^ 2 → ⊕ S dxᵢ given by projecting to the summands indexed by P.rels and composing with the inverse of P.cotangentEquiv.

By SubmersivePresentation.sectionCotangent_comp this is indeed a section.

Equations

P.sectionCotangent = ↑P.cotangentEquiv.symm ∘ₗ ↑(Finsupp.linearEquivFunOnFinite S S P.rels) ∘ₗ Finsupp.lcomapDomain P.map ⋯ ∘ₗ ↑P.cotangentSpaceBasis.repr

Instances For

source

theorem Algebra.SubmersivePresentation.sectionCotangent_eq_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : SubmersivePresentation R S) (x : P.toExtension.CotangentSpace) (y : P.toExtension.Cotangent) :

P.sectionCotangent x = y ↔ ∀ (i : P.rels), (P.cotangentSpaceBasis.repr x) (P.map i) = P.cotangentComplexAux y i

source

theorem Algebra.SubmersivePresentation.sectionCotangent_comp {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : SubmersivePresentation R S) :

P.sectionCotangent ∘ₗ P.toExtension.cotangentComplex = LinearMap.id

source

theorem Algebra.SubmersivePresentation.sectionCotangent_zero_of_not_mem_range {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : SubmersivePresentation R S) (i : P.vars) (hi : i ∉ Set.range P.map) :

P.sectionCotangent (P.cotangentSpaceBasis i) = 0

source

noncomputable def Algebra.SubmersivePresentation.basisKaehlerOfIsCompl {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : SubmersivePresentation R S) {κ : Type u_3} {f : κ → P.vars} (hf : Function.Injective f) (hcompl : IsCompl (Set.range f) (Set.range P.map)) :

Basis κ S (Ω[S⁄R])

Given a submersive presentation of S as R-algebra, any indexing type κ complementary to the P.rels in P.vars indexes a basis of Ω[S⁄R]. See SubmersivePresentation.basisKaehler for the special case κ = (Set.range P.map)ᶜ.

Equations

P.basisKaehlerOfIsCompl hf hcompl = Basis.ofSplitExact ⋯ ⋯ ⋯ P.cotangentSpaceBasis hf ⋯ ⋯ ⋯

Instances For

source

noncomputable def Algebra.SubmersivePresentation.basisKaehler {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : SubmersivePresentation R S) :

Basis (↑(Set.range P.map)ᶜ) S (Ω[S⁄R])

Given a submersive presentation of S as R-algebra, the images of dxᵢ for i in the complement of P.rels in P.vars form a basis of Ω[S⁄R].

Stacks Tag 00T7 ((2))

Equations

P.basisKaehler = P.basisKaehlerOfIsCompl ⋯ ⋯

Instances For

source

theorem Algebra.SubmersivePresentation.free_kaehlerDifferential {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : SubmersivePresentation R S) :

Module.Free S (Ω[S⁄R])

If P is a submersive presentation of S as an R-algebra, Ω[S⁄R] is free.

Stacks Tag 00T7 ((2))

source

theorem Algebra.SubmersivePresentation.rank_kaehlerDifferential {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Nontrivial S] (P : SubmersivePresentation R S) :

Module.rank S (Ω[S⁄R]) = ↑P.dimension

If P is a submersive presentation of S as an R-algebra and S is nontrivial, Ω[S⁄R] is free of rank the dimension of P, i.e. the number of generators minus the number of relations.

source