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.Generators.Cotangent: The conormal space I/I². (Defined in Generators/Basic)
• Algebra.Generators.CotangentSpace: The cotangent space ⨁ᵢ S dxᵢ.
• Algebra.Generators.CotangentComplex: The map I/I² → ⨁ᵢ S dxᵢ.
• Algebra.Generators.toKaehler: The projection ⨁ᵢ S dxᵢ → Ω[S/R].
• Algebra.Generators.toKaehler_surjective: The map ⨁ᵢ S dxᵢ → Ω[S/R] is surjective.
• Algebra.Generators.exact_cotangentComplex_toKaehler: I/I² → ⨁ᵢ S dxᵢ → Ω[S/R] is exact.
• Algebra.Generators.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.

@[reducible, inline]

abbrev Algebra.Generators.CotangentSpace {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) : Type (max (max u 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.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.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.Ring) (i : P.vars) : (P.cotangentSpaceBasis.repr (1 ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.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)

noncomputable def Algebra.Generators.cotangentComplex {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators 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.Generators.cotangentComplex_mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) (x : { x : P.Ring // x ∈ P.ker }) : P.cotangentComplex (Algebra.Generators.Cotangent.mk x) = 1 ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) ↑x

noncomputable def Algebra.Generators.CotangentSpace.map {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') : 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.Generators.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.Generators.CotangentSpace.map_tmul {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') (x : S) (y : P.Ring) : (Algebra.Generators.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.Generators.CotangentSpace.repr_map {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.Generators.CotangentSpace.map f) (P.cotangentSpaceBasis i))) j = (MvPolynomial.aeval P'.val) ((MvPolynomial.pderiv j) (f.val i))

@[simp]

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

theorem Algebra.Generators.CotangentSpace.map_comp {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'] {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''] [Algebra R' R''] [Algebra S' S''] [Algebra R' S''] [IsScalarTower R' R'' S''] [IsScalarTower R' S' S''] [IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P'') : Algebra.Generators.CotangentSpace.map (g.comp f) = ↑S (Algebra.Generators.CotangentSpace.map g) ∘ₗ Algebra.Generators.CotangentSpace.map f

theorem Algebra.Generators.CotangentSpace.map_comp_apply {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'] {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''] [Algebra R' R''] [Algebra S' S''] [Algebra R' S''] [IsScalarTower R' R'' S''] [IsScalarTower R' S' S''] [IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P'') (x : P.CotangentSpace) : (Algebra.Generators.CotangentSpace.map (g.comp f)) x = (Algebra.Generators.CotangentSpace.map g) ((Algebra.Generators.CotangentSpace.map f) x)

theorem Algebra.Generators.CotangentSpace.map_cotangentComplex {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') (x : P.Cotangent) : (Algebra.Generators.CotangentSpace.map f) (P.cotangentComplex x) = P'.cotangentComplex ((Algebra.Generators.Cotangent.map f) x)

theorem Algebra.Generators.CotangentSpace.map_comp_cotangentComplex {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') : Algebra.Generators.CotangentSpace.map f ∘ₗ P.cotangentComplex = ↑S P'.cotangentComplex ∘ₗ Algebra.Generators.Cotangent.map f

theorem Algebra.Generators.Hom.sub_aux {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') (g : P.Hom P') (x : P.Ring) (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

@[simp]

theorem Algebra.Generators.Hom.subToKer_apply_coe {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') (g : P.Hom P') (c : P.Ring) : ↑((f.subToKer g) c) = f.toAlgHom c - g.toAlgHom c

noncomputable def Algebra.Generators.Hom.subToKer {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') (g : P.Hom P') : P.Ring →ₗ[R] { x : P'.Ring // x ∈ 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) ⋯

noncomputable def Algebra.Generators.Hom.sub {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') (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.Generators.Hom.sub_one_tmul {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') (g : P.Hom P') (x : P.Ring) : (f.sub g) (1 ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) x) = Algebra.Generators.Cotangent.mk ((f.subToKer g) x)

@[simp]

theorem Algebra.Generators.Hom.sub_tmul {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') (g : P.Hom P') (r : S) (x : P.Ring) : (f.sub g) (r ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) x) = r • Algebra.Generators.Cotangent.mk ((f.subToKer g) x)

theorem Algebra.Generators.CotangentSpace.map_sub_map {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') (g : P.Hom P') : Algebra.Generators.CotangentSpace.map f - Algebra.Generators.CotangentSpace.map g = ↑S P'.cotangentComplex ∘ₗ f.sub g

theorem Algebra.Generators.Cotangent.map_sub_map {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') (g : P.Hom P') : Algebra.Generators.Cotangent.map f - Algebra.Generators.Cotangent.map g = f.sub g ∘ₗ P.cotangentComplex

@[reducible, inline]

noncomputable abbrev Algebra.Generators.toKaehler {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators 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

@[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.toKaehler (P.cotangentSpaceBasis i) = (KaehlerDifferential.D R S) (P.val i)

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

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