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 : 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.

noncomputable def Algebra.Extension.cotangentComplex {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : 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ⁿ).

@[simp]

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

noncomputable def KaehlerDifferential.cotangentComplexBaseChange (R : Type u) (S : Type v) [CommRing R] [CommRing S] (P : Type u_2) (A : Type u_3) [CommRing P] [CommRing A] [Algebra P S] [Algebra P A] [Algebra R P] [Algebra S A] [IsScalarTower P S A] : TensorProduct P A ↥(RingHom.ker (algebraMap P S)) →ₗ[A] TensorProduct P A Ω[P⁄R]

This is (isomorphic to) the base change of the cotangent complex to A, but the domain and codomains of this are more manageable.

theorem KaehlerDifferential.cotangentComplexBaseChange_tmul {R : Type u} {S : Type v} [CommRing R] [CommRing S] {P : Type u_2} {A : Type u_3} [CommRing P] [CommRing A] [Algebra P S] [Algebra P A] [Algebra R P] [Algebra S A] [IsScalarTower P S A] (a : A) (b : ↥(RingHom.ker (algebraMap P S))) : (cotangentComplexBaseChange R S P A) (a ⊗ₜ[P] b) = a • (kerToTensor R P A) ⟨↑b, ⋯⟩

theorem Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplex {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) (A : Type u_1) [CommRing A] [Algebra S A] [Algebra P.Ring A] [IsScalarTower P.Ring S A] : KaehlerDifferential.cotangentComplexBaseChange R S P.Ring A = ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R]) ∘ₗ LinearMap.baseChange A P.cotangentComplex ∘ₗ ↑((TensorProduct.AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker).symm ≪≫ₗ LinearEquiv.baseChange S A (TensorProduct P.Ring S ↥P.ker) P.Cotangent P.cotangentEquiv)

theorem Algebra.Extension.lTensor_cotangentComplex_eq_cotangentComplexBaseChange {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Extension R S) (A : Type u_1) [CommRing A] [Algebra S A] [Algebra P.Ring A] [IsScalarTower P.Ring S A] : LinearMap.baseChange A P.cotangentComplex = ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R]).symm ∘ₗ KaehlerDifferential.cotangentComplexBaseChange R S P.Ring A ∘ₗ ↑((TensorProduct.AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker).symm ≪≫ₗ LinearEquiv.baseChange S A (TensorProduct P.Ring S ↥P.ker) P.Cotangent P.cotangentEquiv).symm

noncomputable def Algebra.Extension.CotangentSpace.map {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : 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.

@[simp]

theorem Algebra.Extension.CotangentSpace.map_tmul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : 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) : (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)

theorem Algebra.Extension.CotangentSpace.map_tmul_eq_tmul_map {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : 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⁄R]) : (CotangentSpace.map f) (x ⊗ₜ[P.Ring] y) = (algebraMap S S') x ⊗ₜ[P'.Ring] (KaehlerDifferential.map R R' P.Ring P'.Ring) y

@[simp]

theorem Algebra.Extension.CotangentSpace.map_id {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} : CotangentSpace.map (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 : Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : 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'' : 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'') : CotangentSpace.map (g.comp f) = ↑S (CotangentSpace.map g) ∘ₗ CotangentSpace.map f

theorem Algebra.Extension.CotangentSpace.map_comp_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : 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'' : 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) : (CotangentSpace.map (g.comp f)) x = (CotangentSpace.map g) ((CotangentSpace.map f) x)

theorem Algebra.Extension.CotangentSpace.map_cotangentComplex {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') (x : P.Cotangent) : (CotangentSpace.map f) (P.cotangentComplex x) = P'.cotangentComplex ((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 : Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') : CotangentSpace.map f ∘ₗ P.cotangentComplex = ↑S P'.cotangentComplex ∘ₗ Cotangent.map f

theorem Algebra.Extension.Hom.sub_aux {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : 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 : Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : 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.

@[simp]

theorem Algebra.Extension.Hom.subToKer_apply_coe {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : 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 : Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : 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.

theorem Algebra.Extension.Hom.sub_one_tmul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : 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) = 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 : Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : 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 • 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 : Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : 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') : CotangentSpace.map f - 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 : Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : 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') : map f - 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 : Extension R S) : P.CotangentSpace →ₗ[S] Ω[S⁄R]

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

theorem Algebra.Extension.toKaehler_surjective {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : 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 : 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 : 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].

@[implicit_reducible]

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

@[implicit_reducible]

noncomputable instance Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : 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

@[simp]

theorem Algebra.Extension.H1Cotangent.val_add {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : 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 : 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 : 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 : 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 : Extension R S) : Subsingleton P.H1Cotangent ↔ Function.Injective ⇑P.cotangentComplex

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

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

@[simp]

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

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

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

theorem Algebra.Extension.h1Cotangentι_ext_iff {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} {x y : P.H1Cotangent} : x = y ↔ ↑x = ↑y

theorem Algebra.Extension.exact_hCotangentι_cotangentComplex {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} : Function.Exact ⇑h1Cotangentι ⇑P.cotangentComplex

The sequence H¹(L_{S/R}) → P.Cotangent → P.CotangentSpace is exact.

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' : Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] {P : Extension R S} (f : P.Hom P') : P.H1Cotangent →ₗ[S] P'.H1Cotangent

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

@[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' : Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] {P : Extension R S} (f : P.Hom P') (c : ↥P.cotangentComplex.ker) : ↑((map f) c) = (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' : Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] {P : Extension R S} (f g : P.Hom P') : map f = map g

@[simp]

theorem Algebra.Extension.H1Cotangent.map_id {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Extension R S} : map (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' : 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'' : 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 : Extension R S} (f : P.Hom P') (g : P'.Hom P'') : map (g.comp f) = ↑S (map g) ∘ₗ map f

noncomputable def Algebra.Extension.H1Cotangent.equiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P₁ : Extension R S} {P₂ : Extension R S} (f₁ : P₁.Hom P₂) (f₂ : P₂.Hom P₁) : P₁.H1Cotangent ≃ₗ[S] P₂.H1Cotangent

Maps P₁ → P₂ and P₂ → P₁ between extensions induce an isomorphism between H¹(L_P₁) and H¹(L_P₂).

@[simp]

theorem Algebra.Extension.H1Cotangent.equiv_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P₁ : Extension R S} {P₂ : Extension R S} (f₁ : P₁.Hom P₂) (f₂ : P₂.Hom P₁) (c : ↥P₁.cotangentComplex.ker) : (equiv f₁ f₂) c = ⟨(Cotangent.map f₁) ↑c, ⋯⟩

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

The canonical basis on the CotangentSpace.

@[simp]

theorem Algebra.Generators.cotangentSpaceBasis_repr_tmul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {ι : Type w} (P : Generators R S ι) (r : S) (x : P.Ring) (i : ι) : (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] {ι : Type w} (P : Generators R S ι) (x : P.toExtension.Ring) (i : ι) : (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] {ι : Type w} (P : Generators R S ι) (i : ι) : P.cotangentSpaceBasis i = 1 ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) (MvPolynomial.X i)

instance Algebra.Generators.instFreeCotangentSpaceToExtension {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {ι : Type w} (P : Generators R S ι) : Module.Free S P.toExtension.CotangentSpace

noncomputable def Algebra.Generators.cotangentRestrict {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {ι : Type w} (P : Generators R S ι) {σ : Type u_1} {u : σ → ι} (hu : Function.Injective u) : P.toExtension.Cotangent →ₗ[S] σ →₀ S

Given generators R[xᵢ] → S and an injective map σ → ι, this is the composition I/I² → ⊕ S dxᵢ → ⊕ S dxᵢ where the second i only runs over σ.

theorem Algebra.Generators.cotangentRestrict_mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {ι : Type w} (P : Generators R S ι) {σ : Type u_1} {u : σ → ι} (hu : Function.Injective u) (x : ↥P.ker) : ⇑((P.cotangentRestrict hu) (Extension.Cotangent.mk x)) = fun (j : σ) => (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (u j)) ↑x)

@[simp]

theorem Algebra.Generators.repr_CotangentSpaceMap {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {ι : Type w} {P : Generators R S ι} {R' : Type u'} {S' : Type v'} {ι' : Type w'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : 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 : ι) (j : ι') : (P'.cotangentSpaceBasis.repr ((Extension.CotangentSpace.map f.toExtensionHom) (P.cotangentSpaceBasis i))) j = (MvPolynomial.aeval P'.val) ((MvPolynomial.pderiv j) (f.val i))

theorem Algebra.Generators.toKaehler_tmul_D {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {ι : Type w} {P : Generators R S ι} (i : ι) : P.toExtension.toKaehler (1 ⊗ₜ[P.toExtension.Ring] (KaehlerDifferential.D R P.Ring) (MvPolynomial.X i)) = (KaehlerDifferential.D R S) (P.val i)

@[simp]

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

instance Algebra.instFinitePresentationKaehlerDifferentialOfFinitePresentation {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [FinitePresentation R S] : Module.FinitePresentation S Ω[S⁄R]

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

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

@[simp]

theorem Algebra.Generators.H1Cotangent.equiv_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {ι : Type w} {ι' : Type u_1} (P : Generators R S ι) (P' : Generators R S ι') (c : ↥P.toExtension.cotangentComplex.ker) : (equiv P P') c = ⟨(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.

noncomputable def Algebra.H1Cotangent.map (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (S' : Type u_2) [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] : H1Cotangent R S' →ₗ[S'] H1Cotangent S T

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

noncomputable def Algebra.H1Cotangent.mapEquiv (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (S' : Type u_2) [CommRing S'] [Algebra R S'] (e : S ≃ₐ[R] S') : H1Cotangent R S ≃ₗ[R] H1Cotangent R S'

Isomorphic algebras induce isomorphic H¹(L_{S/R}).

@[reducible, inline]

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

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

instance Algebra.instFiniteH1CotangentOfFinitePresentationOfProjectiveKaehlerDifferential {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [FinitePresentation R S] [Module.Projective S Ω[S⁄R]] : Module.Finite S (H1Cotangent R S)