Presentation of the module of differentials

Given a presentation of a R-algebra S, we obtain a presentation of the S-module Ω[S⁄R].

Assume pres : Algebra.Presentation R S is a presentation of S as an R-algebra. We then have a type ι for the generators, a type σ for the relations, and for each r : σ we have the relation pres.relation r in pres.Ring (which is a ring of polynomials over R with variables indexed by ι). Then, Ω[pres.Ring⁄R] identifies to the free module on the type ι, and for each r : σ, we may consider the image of the differential of pres.relation r in this free module, and by using the (surjective) map pres.Ring → S, we obtain an element pres.differentialsRelations.relation r in the free S-module on ι. The main result in this file is that Ω[S⁄R] identifies to the quotient of the free S-module on ι by the submodule generated by these elements pres.differentialsRelations.relation r. We show this as a consequence of Algebra.Extension.exact_cotangentComplex_toKaehler from the file Mathlib/RingTheory/Kaehler/CotangentComplex.lean.

noncomputable def Algebra.Presentation.differentialsRelations {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (pres : Presentation R S ι σ) : Module.Relations S

The shape of the presentation by generators and relations of the S-module Ω[S⁄R] that is obtained from a presentation of S as an R-algebra.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebra.Presentation.differentialsRelations_R {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (pres : Presentation R S ι σ) : pres.differentialsRelations.R = σ

@[simp]

theorem Algebra.Presentation.differentialsRelations_G {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (pres : Presentation R S ι σ) : pres.differentialsRelations.G = ι

We obtain here a few compatibilities which allow to compare the two sequences (σ →₀ S) → (ι →₀ S) → Ω[S⁄R] and pres.toExtension.Cotangent →ₗ[S] pres.toExtension.CotangentSpace → Ω[S⁄R]. Indeed, there is commutative diagram with a surjective map hom₁ : (σ →₀ S) →ₗ[S] pres.toExtension.Cotangent on the left and bijections on the middle and on the right. Then, the exactness of the first sequence shall follow from the exactness of the second which is Algebra.Extension.exact_cotangentComplex_toKaehler.

theorem Algebra.Presentation.differentials.comm₂₃' {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (pres : Presentation R S ι σ) : pres.toExtension.toKaehler ∘ₗ ↑pres.cotangentSpaceBasis.repr.symm = Finsupp.linearCombination S fun (g : ι) => (KaehlerDifferential.D R S) (pres.val g)

Same as comm₂₃ below, but here we have not yet constructed differentialsSolution.

noncomputable def Algebra.Presentation.differentials.hom₁ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (pres : Presentation R S ι σ) : (σ →₀ S) →ₗ[S] pres.toExtension.Cotangent

The canonical map (σ →₀ S) →ₗ[S] pres.toExtension.Cotangent.

Equations

• Algebra.Presentation.differentials.hom₁ pres = Finsupp.linearCombination S fun (r : σ) => Algebra.Extension.Cotangent.mk ⟨pres.relation r, ⋯⟩

theorem Algebra.Presentation.differentials.hom₁_single {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (pres : Presentation R S ι σ) (r : σ) : (hom₁ pres) (Finsupp.single r 1) = Extension.Cotangent.mk ⟨pres.relation r, ⋯⟩

theorem Algebra.Presentation.differentials.surjective_hom₁ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (pres : Presentation R S ι σ) : Function.Surjective ⇑(hom₁ pres)

theorem Algebra.Presentation.differentials.comm₁₂_single {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (pres : Presentation R S ι σ) (r : σ) : pres.toExtension.cotangentComplex ((hom₁ pres) (Finsupp.single r 1)) = pres.cotangentSpaceBasis.repr.symm (pres.differentialsRelations.relation r)

theorem Algebra.Presentation.differentials.comm₁₂ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (pres : Presentation R S ι σ) : pres.toExtension.cotangentComplex ∘ₗ hom₁ pres = ↑pres.cotangentSpaceBasis.repr.symm ∘ₗ pres.differentialsRelations.map

noncomputable def Algebra.Presentation.differentialsSolution {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (pres : Presentation R S ι σ) : pres.differentialsRelations.Solution (Ω[S⁄R])

The S-module Ω[S⁄R] contains an obvious solution to the system of linear equations pres.differentialsRelations.Solution when pres is a presentation of S as an R-algebra.

Equations

• pres.differentialsSolution = { var := fun (g : pres.differentialsRelations.G) => (KaehlerDifferential.D R S) (pres.val g), linearCombination_var_relation := ⋯ }

theorem Algebra.Presentation.differentials.comm₂₃ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (pres : Presentation R S ι σ) : pres.toExtension.toKaehler ∘ₗ ↑pres.cotangentSpaceBasis.repr.symm = pres.differentialsSolution.π

theorem Algebra.Presentation.differentialsSolution_isPresentation {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (pres : Presentation R S ι σ) : pres.differentialsSolution.IsPresentation

noncomputable def Algebra.Presentation.differentials {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [CommRing R] [CommRing S] [Algebra R S] (pres : Presentation R S ι σ) : Module.Presentation S (Ω[S⁄R])

The presentation of the S-module Ω[S⁄R] deduced from a presentation of S as a R-algebra.

Equations

• One or more equations did not get rendered due to their size.