The Jacobi-Zariski exact sequence

Given R → S → T, the Jacobi-Zariski exact sequence is

H¹(L_{T/R}) → H¹(L_{T/S}) → T ⊗[S] Ω[S/R] → Ω[T/R] → Ω[T/S] → 0

The maps are

• Algebra.H1Cotangent.map
• Algebra.H1Cotangent.δ
• KaehlerDifferential.mapBaseChange
• KaehlerDifferential.map and the exactness lemmas are
• Algebra.H1Cotangent.exact_map_δ
• Algebra.H1Cotangent.exact_δ_mapBaseChange
• KaehlerDifferential.exact_mapBaseChange_map
• KaehlerDifferential.map_surjective

noncomputable def Algebra.Generators.kerCompPreimage {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) (x : ↥Q.ker) : ↥(Q.comp P).ker

Given R[X] → S and S[Y] → T, this is the lift of an element in ker(S[Y] → T) to ker(R[X][Y] → S[Y] → T) constructed from P.σ.

Equations

• Q.kerCompPreimage P x = ⟨Finsupp.sum ↑x fun (n : Q.vars →₀ ℕ) (r : S) => (MvPolynomial.rename Sum.inr) (P.σ r) * (MvPolynomial.monomial (Finsupp.mapDomain Sum.inl n)) 1, ⋯⟩

theorem Algebra.Generators.ofComp_kerCompPreimage {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) (x : ↥Q.ker) : (Q.ofComp P).toAlgHom ↑(Q.kerCompPreimage P x) = ↑x

theorem Algebra.Generators.Cotangent.map_ofComp_ker {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) : Submodule.map (Q.ofComp P).toAlgHom.toLinearMap (Submodule.restrictScalars R (Q.comp P).ker) = Submodule.restrictScalars R Q.ker

theorem Algebra.Generators.Cotangent.surjective_map_ofComp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) : Function.Surjective ⇑(Algebra.Extension.Cotangent.map (Q.ofComp P).toExtensionHom)

Given representations 0 → I → R[X] → S → 0 and 0 → K → S[Y] → T → 0, we may consider the induced representation 0 → J → R[X, Y] → T → 0, and the sequence T ⊗[S] (I/I²) → J/J² → K/K² is exact.

theorem Algebra.Generators.Cotangent.exact {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) : Function.Exact ⇑(LinearMap.liftBaseChange T (Algebra.Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ⇑(Algebra.Extension.Cotangent.map (Q.ofComp P).toExtensionHom)

noncomputable def Algebra.Generators.CotangentSpace.compEquiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) : (Q.comp P).toExtension.CotangentSpace ≃ₗ[T] Q.toExtension.CotangentSpace × TensorProduct S T P.toExtension.CotangentSpace

Given R[X] → S and S[Y] → T, the cotangent space of R[X][Y] → T is isomorphic to the direct product of the cotangent space of S[Y] → T and R[X] → S (base changed to T).

Equations

• Algebra.Generators.CotangentSpace.compEquiv Q P = (Q.comp P).cotangentSpaceBasis.repr.trans (Q.cotangentSpaceBasis.prod (Basis.baseChange T P.cotangentSpaceBasis)).repr.symm

theorem Algebra.Generators.CotangentSpace.compEquiv_symm_inr {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) : ↑(Algebra.Generators.CotangentSpace.compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (TensorProduct S T P.toExtension.CotangentSpace) = LinearMap.liftBaseChange T (Algebra.Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)

theorem Algebra.Generators.CotangentSpace.compEquiv_symm_zero {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) (x : TensorProduct S T P.toExtension.CotangentSpace) : (Algebra.Generators.CotangentSpace.compEquiv Q P).symm (0, x) = (LinearMap.liftBaseChange T (Algebra.Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) x

theorem Algebra.Generators.CotangentSpace.fst_compEquiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) : LinearMap.fst T Q.toExtension.CotangentSpace (TensorProduct S T P.toExtension.CotangentSpace) ∘ₗ ↑(Algebra.Generators.CotangentSpace.compEquiv Q P) = Algebra.Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom

theorem Algebra.Generators.CotangentSpace.fst_compEquiv_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) (x : (Q.comp P).toExtension.CotangentSpace) : ((Algebra.Generators.CotangentSpace.compEquiv Q P) x).1 = (Algebra.Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) x

theorem Algebra.Generators.CotangentSpace.map_toComp_injective {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) : Function.Injective ⇑(LinearMap.liftBaseChange T (Algebra.Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))

theorem Algebra.Generators.CotangentSpace.map_ofComp_surjective {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) : Function.Surjective ⇑(Algebra.Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom)

Given representations R[X] → S and S[Y] → T, the sequence T ⊗[S] (⨁ₓ S dx) → (⨁ₓ T dx) ⊕ (⨁ᵧ T dy) → ⨁ᵧ T dy is exact.

theorem Algebra.Generators.CotangentSpace.exact {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) : Function.Exact ⇑(LinearMap.liftBaseChange T (Algebra.Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) ⇑(Algebra.Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom)

noncomputable def Algebra.Generators.H1Cotangent.δAux (R : Type u) {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) : Q.Ring →ₗ[R] TensorProduct S T (Ω[S⁄R])

Given 0 → I → S[Y] → T → 0, this is an auxiliary map from S[Y] to T ⊗[S] Ω[S⁄R] whose restriction to ker(I/I² → ⊕ S dyᵢ) is the connecting homomorphism in the Jacobi-Zariski sequence.

Equations

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

theorem Algebra.Generators.H1Cotangent.δAux_monomial {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (n : Q.vars →₀ ℕ) (r : S) : (Algebra.Generators.H1Cotangent.δAux R Q) ((MvPolynomial.monomial n) r) = (n.prod fun (x1 : Q.vars) (x2 : ℕ) => Q.val x1 ^ x2) ⊗ₜ[S] (KaehlerDifferential.D R S) r

@[simp]

theorem Algebra.Generators.H1Cotangent.δAux_X {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (i : Q.vars) : (Algebra.Generators.H1Cotangent.δAux R Q) (MvPolynomial.X i) = 0

theorem Algebra.Generators.H1Cotangent.δAux_mul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (x y : Q.Ring) : (Algebra.Generators.H1Cotangent.δAux R Q) (x * y) = x • (Algebra.Generators.H1Cotangent.δAux R Q) y + y • (Algebra.Generators.H1Cotangent.δAux R Q) x

theorem Algebra.Generators.H1Cotangent.δAux_C {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (r : S) : (Algebra.Generators.H1Cotangent.δAux R Q) (MvPolynomial.C r) = 1 ⊗ₜ[S] (KaehlerDifferential.D R S) r

theorem Algebra.Generators.H1Cotangent.δAux_toAlgHom {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {Q : Algebra.Generators S T} {Q' : Algebra.Generators S T} (f : Q.Hom Q') (x : Q.Ring) : (Algebra.Generators.H1Cotangent.δAux R Q') (f.toAlgHom x) = (Algebra.Generators.H1Cotangent.δAux R Q) x + (Finsupp.linearCombination T (⇑(Algebra.Generators.H1Cotangent.δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (KaehlerDifferential.D S Q.Ring) x))

theorem Algebra.Generators.H1Cotangent.δAux_ofComp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) (x : (Q.comp P).Ring) : (Algebra.Generators.H1Cotangent.δAux R Q) ((Q.ofComp P).toAlgHom x) = (LinearMap.baseChange T P.toExtension.toKaehler) ((Algebra.Generators.CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (KaehlerDifferential.D R (Q.comp P).Ring) x)).2

theorem Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChange {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) : LinearMap.liftBaseChange T (Algebra.Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) ∘ₗ LinearMap.baseChange T P.toExtension.cotangentComplex = (Q.comp P).toExtension.cotangentComplex ∘ₗ LinearMap.liftBaseChange T (Algebra.Extension.Cotangent.map (Q.toComp P).toExtensionHom)

noncomputable def Algebra.Generators.H1Cotangent.δ {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) : Q.toExtension.H1Cotangent →ₗ[T] TensorProduct S T (Ω[S⁄R])

The connecting homomorphism in the Jacobi-Zariski sequence for given presentations. Given representations 0 → I → R[X] → S → 0 and 0 → K → S[Y] → T → 0, we may consider the induced representation 0 → J → R[X, Y] → T → 0, and this map is obtained by applying snake lemma to the following diagram

    T ⊗[S] Ω[S/R]    →          Ω[T/R]        →   Ω[T/S]  → 0
        ↑                         ↑                 ↑
0 → T ⊗[S] (⨁ₓ S dx) → (⨁ₓ T dx) ⊕ (⨁ᵧ T dy) →  ⨁ᵧ T dy → 0
        ↑                         ↑                 ↑
    T ⊗[S] (I/I²)    →           J/J²         →    K/K²   → 0
                                  ↑                 ↑
                             H¹(L_{T/R})      → H¹(L_{T/S})

This is independent from the presentations chosen. See H1Cotangent.δ_comp_equiv.

Equations

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

theorem Algebra.Generators.H1Cotangent.exact_δ_map {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) : Function.Exact ⇑(Algebra.Generators.H1Cotangent.δ Q P) ⇑(KaehlerDifferential.mapBaseChange R S T)

theorem Algebra.Generators.H1Cotangent.δ_eq {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) (x : Q.toExtension.H1Cotangent) (y : (Q.comp P).toExtension.Cotangent) (hy : (Algebra.Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = ↑x) (z : TensorProduct S T P.toExtension.CotangentSpace) (hz : (LinearMap.liftBaseChange T (Algebra.Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) z = (Q.comp P).toExtension.cotangentComplex y) : (Algebra.Generators.H1Cotangent.δ Q P) x = (LinearMap.baseChange T P.toExtension.toKaehler) z

theorem Algebra.Generators.H1Cotangent.δ_eq_δAux {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) (x : ↥Q.ker) (hx : Algebra.Extension.Cotangent.mk x ∈ LinearMap.ker Q.toExtension.cotangentComplex) : (Algebra.Generators.H1Cotangent.δ Q P) ⟨Algebra.Extension.Cotangent.mk x, hx⟩ = (Algebra.Generators.H1Cotangent.δAux R Q) ↑x

theorem Algebra.Generators.H1Cotangent.δ_eq_δ {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) (P' : Algebra.Generators R S) : Algebra.Generators.H1Cotangent.δ Q P = Algebra.Generators.H1Cotangent.δ Q P'

theorem Algebra.Generators.H1Cotangent.exact_map_δ {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) : Function.Exact ⇑(Algebra.Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom) ⇑(Algebra.Generators.H1Cotangent.δ Q P)

theorem Algebra.Generators.H1Cotangent.δ_map {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) (Q' : Algebra.Generators S T) (P' : Algebra.Generators R S) (f : Q'.Hom Q) (x : Q'.toExtension.H1Cotangent) : (Algebra.Generators.H1Cotangent.δ Q P) ((Algebra.Extension.H1Cotangent.map f.toExtensionHom) x) = (Algebra.Generators.H1Cotangent.δ Q' P') x

theorem Algebra.Generators.H1Cotangent.δ_comp_equiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) (Q' : Algebra.Generators S T) (P' : Algebra.Generators R S) : Algebra.Generators.H1Cotangent.δ Q P ∘ₗ ↑(Algebra.Generators.H1Cotangent.equiv Q' Q) = Algebra.Generators.H1Cotangent.δ Q' P'

theorem Algebra.Generators.H1Cotangent.exact_map_δ' {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {T : Type uT} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (Q : Algebra.Generators S T) (P : Algebra.Generators R S) (P' : Algebra.Generators R T) (f : P'.Hom Q) : Function.Exact ⇑(Algebra.Extension.H1Cotangent.map f.toExtensionHom) ⇑(Algebra.Generators.H1Cotangent.δ Q P)

A variant of exact_map_δ that takes in an arbitrary map between generators.

noncomputable def Algebra.H1Cotangent.δ (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (T : Type w) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] : Algebra.H1Cotangent S T →ₗ[T] TensorProduct S T (Ω[S⁄R])

The connecting homomorphism in the Jacobi-Zariski sequence.

Equations

• Algebra.H1Cotangent.δ R S T = Algebra.Generators.H1Cotangent.δ (Algebra.Generators.self S T) (Algebra.Generators.self R S)

theorem Algebra.H1Cotangent.exact_map_δ (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (T : Type w) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] : Function.Exact ⇑(Algebra.H1Cotangent.map R S T T) ⇑(Algebra.H1Cotangent.δ R S T)

Given algebras R → S → T, H¹(L_{T/R}) → H¹(L_{T/S}) → T ⊗[S] Ω[S/R] is exact.

theorem Algebra.H1Cotangent.exact_δ_mapBaseChange (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (T : Type w) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] : Function.Exact ⇑(Algebra.H1Cotangent.δ R S T) ⇑(KaehlerDifferential.mapBaseChange R S T)

Given algebras R → S → T, H¹(L_{T/S}) → T ⊗[S] Ω[S/R] → Ω[T/R] is exact.