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} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : PreSubmersivePresentation R S ι σ) : P.toExtension.Cotangent →ₗ[S] σ → 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 : σ induced by the injection P.map : σ → ι.

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

Equations

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

theorem Algebra.PreSubmersivePresentation.cotangentComplexAux_apply {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : PreSubmersivePresentation R S ι σ) (x : ↥P.ker) (i : σ) : P.cotangentComplexAux (Extension.Cotangent.mk x) i = (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map i)) ↑x)

theorem Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] {P : PreSubmersivePresentation R S ι σ} (x : ↥P.ker) : P.cotangentComplexAux (Extension.Cotangent.mk x) = 0 ↔ ∀ (i : σ), (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (P.map i)) ↑x) = 0

theorem Algebra.SubmersivePresentation.cotangentComplexAux_injective {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) [Finite σ] : Function.Injective ⇑P.cotangentComplexAux

theorem Algebra.SubmersivePresentation.cotangentComplexAux_surjective {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) [Finite σ] : Function.Surjective ⇑P.cotangentComplexAux

noncomputable def Algebra.SubmersivePresentation.cotangentEquiv {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) : P.toExtension.Cotangent ≃ₗ[S] σ → S

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

Equations

• P.cotangentEquiv = LinearEquiv.ofBijective P.cotangentComplexAux ⋯

@[simp]

theorem Algebra.SubmersivePresentation.cotangentEquiv_apply {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) (a✝ : P.toExtension.Cotangent) (a✝¹ : σ) : P.cotangentEquiv a✝ a✝¹ = P.cotangentComplexAux a✝ a✝¹

theorem Algebra.SubmersivePresentation.cotangentComplex_injective {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) : Function.Injective ⇑P.toExtension.cotangentComplex

instance Algebra.SubmersivePresentation.subsingleton_h1Cotangent {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) : Subsingleton P.toExtension.H1Cotangent

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

noncomputable def Algebra.SubmersivePresentation.basisCotangent {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) : Module.Basis σ S P.toExtension.Cotangent

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

Equations

• P.basisCotangent = P.basisDeriv.map P.cotangentEquiv.symm

theorem Algebra.SubmersivePresentation.basisCotangent_apply {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) (r : σ) : P.basisCotangent r = Extension.Cotangent.mk ⟨P.relation r, ⋯⟩

instance Algebra.SubmersivePresentation.free_cotangent {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) : Module.Free S P.toExtension.Cotangent

Stacks Tag 00T7 ((3))

noncomputable def Algebra.SubmersivePresentation.sectionCotangent {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (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 σ 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 σ) ∘ₗ Finsupp.lcomapDomain P.map ⋯ ∘ₗ ↑P.cotangentSpaceBasis.repr

theorem Algebra.SubmersivePresentation.sectionCotangent_eq_iff {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) [Finite σ] (x : P.toExtension.CotangentSpace) (y : P.toExtension.Cotangent) : P.sectionCotangent x = y ↔ ∀ (i : σ), (P.cotangentSpaceBasis.repr x) (P.map i) = P.cotangentComplexAux y i

theorem Algebra.SubmersivePresentation.sectionCotangent_comp {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) : P.sectionCotangent ∘ₗ P.toExtension.cotangentComplex = LinearMap.id

theorem Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) (i : ι) (hi : i ∉ Set.range P.map) : P.sectionCotangent (P.cotangentSpaceBasis i) = 0

@[deprecated Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range (since := "2025-05-23")]

theorem Algebra.SubmersivePresentation.sectionCotangent_zero_of_not_mem_range {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) (i : ι) (hi : i ∉ Set.range P.map) : P.sectionCotangent (P.cotangentSpaceBasis i) = 0

Alias of Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range.

noncomputable def Algebra.SubmersivePresentation.basisKaehlerOfIsCompl {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) {κ : Type u_5} {f : κ → ι} (hf : Function.Injective f) (hcompl : IsCompl (Set.range f) (Set.range P.map)) : Module.Basis κ S Ω[S⁄R]

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

Equations

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

noncomputable def Algebra.SubmersivePresentation.basisKaehler {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (P : SubmersivePresentation R S ι σ) : Module.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 σ in ι form a basis of Ω[S⁄R].

Equations

• P.basisKaehler = P.basisKaehlerOfIsCompl ⋯ ⋯

theorem Algebra.SubmersivePresentation.free_kaehlerDifferential {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] (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.

theorem Algebra.SubmersivePresentation.rank_kaehlerDifferential {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Finite σ] [Nontrivial S] [Finite ι] (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.

instance Algebra.instFreeCotangentToExtensionUnitLocalizationAway {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : Module.Free S (Generators.localizationAway S r).toExtension.Cotangent

@[reducible, inline]

noncomputable abbrev Algebra.Generators.cMulXSubOneCotangent {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : (localizationAway S r).toExtension.Cotangent

The image of g * X - 1 in I/I² if I is the kernel of the canonical presentation of the localization of S away from g.

Equations

• Algebra.Generators.cMulXSubOneCotangent S r = Algebra.Extension.Cotangent.mk ⟨MvPolynomial.C r * MvPolynomial.X () - 1, ⋯⟩

theorem Algebra.Generators.cMulXSubOneCotangent_eq {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : cMulXSubOneCotangent S r = Extension.Cotangent.mk ⟨MvPolynomial.C r * MvPolynomial.X () - 1, ⋯⟩

theorem Algebra.SubmersivePresentation.basisCotangent_localizationAway_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] (x : Unit) : (localizationAway S r).basisCotangent x = Generators.cMulXSubOneCotangent S r

noncomputable def Algebra.Generators.basisCotangentAway {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] : Module.Basis Unit S (localizationAway S r).toExtension.Cotangent

The basis of (g * X - 1) / (g * X - 1)² given by the image of g * X - 1.

This is def-eq to (SubmersivePresentation.localizationAway T g).basisCotangent, but

(SubmersivePresentation.localizationAway T g).toExtension =
  (Generators.localizationAway T g).toExtension

is not reducibly def-eq. Hence using the general SubmersivePresentation.basisCotangent leads to erw hell.

Equations

• Algebra.Generators.basisCotangentAway S r = (Algebra.SubmersivePresentation.localizationAway S r).basisCotangent

theorem Algebra.Generators.basisCotangentAway_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (r : R) [IsLocalization.Away r S] (x : Unit) : (basisCotangentAway S r) x = cMulXSubOneCotangent S r

instance Algebra.IsStandardSmooth.free_kaehlerDifferential {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsStandardSmooth R S] : Module.Free S Ω[S⁄R]

If S is R-standard smooth, Ω[S⁄R] is a free S-module.

instance Algebra.IsStandardSmooth.subsingleton_h1Cotangent {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsStandardSmooth R S] : Subsingleton (H1Cotangent R S)

theorem Algebra.IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Nontrivial S] (n : ℕ) [IsStandardSmoothOfRelativeDimension n R S] : Module.rank S Ω[S⁄R] = ↑n

If S is non-trivial and R-standard smooth of relative dimension, Ω[S⁄R] is a free S-module of rank n.

instance Algebra.IsStandardSmoothOfRelationDimension.subsingleton_kaehlerDifferential {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsStandardSmoothOfRelativeDimension 0 R S] : Subsingleton Ω[S⁄R]

@[instance 900]

instance Algebra.instSmoothOfIsStandardSmooth {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] [IsStandardSmooth R S] : Smooth R S

@[instance 900]

instance Algebra.instEtaleOfIsStandardSmoothOfRelativeDimensionOfNatNat {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] [IsStandardSmoothOfRelativeDimension 0 R S] : Etale R S

If S is R-standard smooth of relative dimension zero, it is étale.