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 space I/I². (Defined in Generators/Basic)
• Algebra.Extension.CotangentSpace: The cotangent space ⨁ᵢ S dxᵢ.
• Algebra.Generators.cotangentSpaceBasis: The canonical basis on ⨁ᵢ S dxᵢ.
• Algebra.Extension.CotangentComplex: The map I/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: If f and g are two maps between presentations, f - g induces a map ⨁ᵢ S dxᵢ → I/I² that makes f and g homotopic.
• Algebra.Extension.H1Cotangent: The first homology of the (naive) cotangent complex of S over R, induced by a given presentation.
• Algebra.H1Cotangent: H¹(L_{S/R}), the first homology of the (naive) cotangent complex of S over R.

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.

@[reducible, inline]

abbrev Algebra.Extension.CotangentSpace {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Extension R S) : Type (max w v)

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])

noncomputable def Algebra.Extension.cotangentComplex {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Extension R S) : P.Cotangent →ₗ[S] P.CotangentSpace

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.

@[simp]

theorem Algebra.Extension.cotangentComplex_mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Extension R S) (x : ↥P.ker) : P.cotangentComplex (Algebra.Extension.Cotangent.mk x) = 1 ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) ↑x

noncomputable def Algebra.Extension.CotangentSpace.map {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') : P.CotangentSpace →ₗ[S] P'.CotangentSpace

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)

@[simp]

theorem Algebra.Extension.CotangentSpace.map_tmul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') (x : S) (y : P.Ring) : (Algebra.Extension.CotangentSpace.map f) (x ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) y) = (algebraMap S S') x ⊗ₜ[P'.Ring] (KaehlerDifferential.D R' P'.Ring) (f.toAlgHom y)

@[simp]

theorem Algebra.Extension.CotangentSpace.map_id {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} : Algebra.Extension.CotangentSpace.map (Algebra.Extension.Hom.id P) = LinearMap.id

theorem Algebra.Extension.CotangentSpace.map_comp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] {R'' : Type u''} {S'' : Type v''} [CommRing R''] [CommRing S''] [Algebra R'' S''] {P'' : Algebra.Extension R'' S''} [Algebra R R''] [Algebra S S''] [Algebra R S''] [IsScalarTower R R'' S''] [Algebra R' R''] [Algebra S' S''] [Algebra R' S''] [IsScalarTower R' R'' S''] [IsScalarTower R R' R''] [IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P'') : Algebra.Extension.CotangentSpace.map (g.comp f) = ↑S (Algebra.Extension.CotangentSpace.map g) ∘ₗ Algebra.Extension.CotangentSpace.map f

theorem Algebra.Extension.CotangentSpace.map_comp_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] {R'' : Type u''} {S'' : Type v''} [CommRing R''] [CommRing S''] [Algebra R'' S''] {P'' : Algebra.Extension R'' S''} [Algebra R R''] [Algebra S S''] [Algebra R S''] [IsScalarTower R R'' S''] [Algebra R' R''] [Algebra S' S''] [Algebra R' S''] [IsScalarTower R' R'' S''] [IsScalarTower R R' R''] [IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P'') (x : P.CotangentSpace) : (Algebra.Extension.CotangentSpace.map (g.comp f)) x = (Algebra.Extension.CotangentSpace.map g) ((Algebra.Extension.CotangentSpace.map f) x)

theorem Algebra.Extension.CotangentSpace.map_cotangentComplex {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') (x : P.Cotangent) : (Algebra.Extension.CotangentSpace.map f) (P.cotangentComplex x) = P'.cotangentComplex ((Algebra.Extension.Cotangent.map f) x)

theorem Algebra.Extension.CotangentSpace.map_comp_cotangentComplex {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') : Algebra.Extension.CotangentSpace.map f ∘ₗ P.cotangentComplex = ↑S P'.cotangentComplex ∘ₗ Algebra.Extension.Cotangent.map f

theorem Algebra.Extension.Hom.sub_aux {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f g : P.Hom P') (x y : P.Ring) : f.toAlgHom (x * y) - g.toAlgHom (x * y) - (P'.σ ((algebraMap P.Ring S') x) * (f.toAlgHom y - g.toAlgHom y) + P'.σ ((algebraMap P.Ring S') y) * (f.toAlgHom x - g.toAlgHom x)) ∈ P'.ker ^ 2

noncomputable def Algebra.Extension.Hom.subToKer {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f g : P.Hom P') : P.Ring →ₗ[R] ↥P'.ker

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) ⋯

@[simp]

theorem Algebra.Extension.Hom.subToKer_apply_coe {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f g : P.Hom P') (c : P.Ring) : ↑((f.subToKer g) c) = f.toRingHom c - g.toRingHom c

noncomputable def Algebra.Extension.Hom.sub {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f g : P.Hom P') : P.CotangentSpace →ₗ[S] P'.Cotangent

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.

theorem Algebra.Extension.Hom.sub_one_tmul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f g : P.Hom P') (x : P.Ring) : (f.sub g) (1 ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) x) = Algebra.Extension.Cotangent.mk ((f.subToKer g) x)

@[simp]

theorem Algebra.Extension.Hom.sub_tmul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f g : P.Hom P') (r : S) (x : P.Ring) : (f.sub g) (r ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) x) = r • Algebra.Extension.Cotangent.mk ((f.subToKer g) x)

theorem Algebra.Extension.CotangentSpace.map_sub_map {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f g : P.Hom P') : Algebra.Extension.CotangentSpace.map f - Algebra.Extension.CotangentSpace.map g = ↑S P'.cotangentComplex ∘ₗ f.sub g

theorem Algebra.Extension.Cotangent.map_sub_map {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f g : P.Hom P') : Algebra.Extension.Cotangent.map f - Algebra.Extension.Cotangent.map g = f.sub g ∘ₗ P.cotangentComplex

@[reducible, inline]

noncomputable abbrev Algebra.Extension.toKaehler {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Extension R S) : P.CotangentSpace →ₗ[S] Ω[S⁄R]

The projection map from the relative cotangent space to the module of differentials.

Equations

• P.toKaehler = KaehlerDifferential.mapBaseChange R P.Ring S

theorem Algebra.Extension.toKaehler_surjective {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} : Function.Surjective ⇑P.toKaehler

theorem Algebra.Extension.exact_cotangentComplex_toKaehler {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} : Function.Exact ⇑P.cotangentComplex ⇑P.toKaehler

noncomputable def Algebra.Extension.H1Cotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Extension R S) : Type w

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)

noncomputable instance Algebra.Extension.instAddCommGroupH1Cotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} : AddCommGroup P.H1Cotangent

Equations

• Algebra.Extension.instAddCommGroupH1Cotangent = id inferInstance

noncomputable instance Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R₀ : Type u_2} [CommRing R₀] [Algebra R₀ S] [Module R₀ P.Cotangent] [IsScalarTower R₀ S P.Cotangent] : Module R₀ P.H1Cotangent

Equations

• Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent = id inferInstance

@[simp]

theorem Algebra.Extension.H1Cotangent.val_add {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} (x y : P.H1Cotangent) : ↑(x + y) = ↑x + ↑y

@[simp]

theorem Algebra.Extension.H1Cotangent.val_zero {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} : ↑0 = 0

@[simp]

theorem Algebra.Extension.H1Cotangent.val_smul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R₀ : Type u_1} [CommRing R₀] [Algebra R₀ S] [Module R₀ P.Cotangent] [IsScalarTower R₀ S P.Cotangent] (r : R₀) (x : P.H1Cotangent) : ↑(r • x) = r • ↑x

instance Algebra.Extension.instIsScalarTowerH1CotangentOfCotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R₁ : Type u_1} {R₂ : Type u_2} [CommRing R₁] [CommRing R₂] [Algebra R₁ R₂] [Algebra R₁ S] [Algebra R₂ S] [Module R₁ P.Cotangent] [IsScalarTower R₁ S P.Cotangent] [Module R₂ P.Cotangent] [IsScalarTower R₂ S P.Cotangent] [IsScalarTower R₁ R₂ P.Cotangent] : IsScalarTower R₁ R₂ P.H1Cotangent

theorem Algebra.Extension.subsingleton_h1Cotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Extension R S) : Subsingleton P.H1Cotangent ↔ Function.Injective ⇑P.cotangentComplex

def Algebra.Extension.h1Cotangentι {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} : P.H1Cotangent →ₗ[S] P.Cotangent

The inclusion of H¹(L_{S/R}) into the conormal space of a presentation.

Equations

• Algebra.Extension.h1Cotangentι = (LinearMap.ker P.cotangentComplex).subtype

@[simp]

theorem Algebra.Extension.h1Cotangentι_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} (self : ↥(LinearMap.ker P.cotangentComplex)) : Algebra.Extension.h1Cotangentι self = ↑self

theorem Algebra.Extension.h1Cotangentι_injective {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} : Function.Injective ⇑Algebra.Extension.h1Cotangentι

theorem Algebra.Extension.h1Cotangentι_ext {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} (x y : P.H1Cotangent) (e : ↑x = ↑y) : x = y

noncomputable def Algebra.Extension.H1Cotangent.map {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] {P : Algebra.Extension R S} (f : P.Hom P') : P.H1Cotangent →ₗ[S] P'.H1Cotangent

The induced map on the first homology of the (naive) cotangent complex.

Equations

• Algebra.Extension.H1Cotangent.map f = (Algebra.Extension.Cotangent.map f).restrict ⋯

@[simp]

theorem Algebra.Extension.H1Cotangent.map_apply_coe {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] {P : Algebra.Extension R S} (f : P.Hom P') (c : ↥(LinearMap.ker P.cotangentComplex)) : ↑((Algebra.Extension.H1Cotangent.map f) c) = (Algebra.Extension.Cotangent.map f) ↑c

theorem Algebra.Extension.H1Cotangent.map_eq {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] {P : Algebra.Extension R S} (f g : P.Hom P') : Algebra.Extension.H1Cotangent.map f = Algebra.Extension.H1Cotangent.map g

@[simp]

theorem Algebra.Extension.H1Cotangent.map_id {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} : Algebra.Extension.H1Cotangent.map (Algebra.Extension.Hom.id P) = LinearMap.id

theorem Algebra.Extension.H1Cotangent.map_comp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] {R'' : Type u''} {S'' : Type v''} [CommRing R''] [CommRing S''] [Algebra R'' S''] {P'' : Algebra.Extension R'' S''} [Algebra R R''] [Algebra S S''] [Algebra R S''] [IsScalarTower R R'' S''] [Algebra R' R''] [Algebra S' S''] [Algebra R' S''] [IsScalarTower R' R'' S''] [IsScalarTower R R' R''] [IsScalarTower S S' S''] {P : Algebra.Extension R S} (f : P.Hom P') (g : P'.Hom P'') : Algebra.Extension.H1Cotangent.map (g.comp f) = ↑S (Algebra.Extension.H1Cotangent.map g) ∘ₗ Algebra.Extension.H1Cotangent.map f

noncomputable def Algebra.Generators.cotangentSpaceBasis {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) : Basis P.vars S P.toExtension.CotangentSpace

The canonical basis on the CotangentSpace.

Equations

• P.cotangentSpaceBasis = Basis.baseChange S (KaehlerDifferential.mvPolynomialBasis R P.vars)

@[simp]

theorem Algebra.Generators.cotangentSpaceBasis_repr_tmul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) (r : S) (x : P.Ring) (i : P.vars) : (P.cotangentSpaceBasis.repr (r ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) x)) i = r * (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv i) x)

theorem Algebra.Generators.cotangentSpaceBasis_repr_one_tmul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) (x : P.toExtension.Ring) (i : P.vars) : (P.cotangentSpaceBasis.repr (1 ⊗ₜ[P.toExtension.Ring] (KaehlerDifferential.D R P.toExtension.Ring) x)) i = (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv i) x)

theorem Algebra.Generators.cotangentSpaceBasis_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) (i : P.vars) : P.cotangentSpaceBasis i = 1 ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) (MvPolynomial.X i)

@[simp]

theorem Algebra.Generators.repr_CotangentSpaceMap {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Generators R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f : P.Hom P') (i : P.vars) (j : P'.vars) : (P'.cotangentSpaceBasis.repr ((Algebra.Extension.CotangentSpace.map f.toExtensionHom) (P.cotangentSpaceBasis i))) j = (MvPolynomial.aeval P'.val) ((MvPolynomial.pderiv j) (f.val i))

@[simp]

theorem Algebra.Generators.toKaehler_cotangentSpaceBasis {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} (i : P.vars) : P.toExtension.toKaehler (P.cotangentSpaceBasis i) = (KaehlerDifferential.D R S) (P.val i)

noncomputable def Algebra.Generators.H1Cotangent.equiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) (P' : Algebra.Generators R S) : P.toExtension.H1Cotangent ≃ₗ[S] P'.toExtension.H1Cotangent

H¹(L_{S/R}) is independent of the presentation chosen.

Equations

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

@[simp]

theorem Algebra.Generators.H1Cotangent.equiv_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) (P' : Algebra.Generators R S) (c : ↥(LinearMap.ker P.toExtension.cotangentComplex)) : (Algebra.Generators.H1Cotangent.equiv P P') c = ⟨(Algebra.Extension.Cotangent.map (P.defaultHom P').toExtensionHom) ↑c, ⋯⟩

@[reducible, inline]

abbrev Algebra.H1Cotangent (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Type (max u v)

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

noncomputable def Algebra.H1Cotangent.map (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (S' : Type u_1) [CommRing S'] [Algebra R S'] (T : Type w) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra S' T] [IsScalarTower R S' T] : Algebra.H1Cotangent R S' →ₗ[S'] Algebra.H1Cotangent S T

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

@[reducible, inline]

noncomputable abbrev Algebra.Generators.equivH1Cotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) : P.toExtension.H1Cotangent ≃ₗ[S] Algebra.H1Cotangent R S

H¹(L_{S/R}) is independent of the presentation chosen.

Equations

• P.equivH1Cotangent = Algebra.Generators.H1Cotangent.equiv P (Algebra.Generators.self R S)