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

theorem Algebra.Generators.Cotangent.surjective_map_ofComp {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Generators S T ι) (P : Generators R S σ) : Function.Surjective ⇑(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 u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Generators S T ι) (P : Generators R S σ) : Function.Exact ⇑(LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)) ⇑(Extension.Cotangent.map (Q.ofComp P).toExtensionHom)

noncomputable def Algebra.Generators.CotangentSpace.compEquiv {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Generators S T ι) (P : 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 (Module.Basis.baseChange T P.cotangentSpaceBasis)).repr.symm

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

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

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

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

theorem Algebra.Generators.CotangentSpace.map_toComp_injective {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Generators S T ι) (P : Generators R S σ) : Function.Injective ⇑(LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))

theorem Algebra.Generators.CotangentSpace.map_ofComp_surjective {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Generators S T ι) (P : Generators R S σ) : Function.Surjective ⇑(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 u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Generators S T ι) (P : Generators R S σ) : Function.Exact ⇑(LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) ⇑(Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom)

noncomputable def Algebra.Generators.H1Cotangent.δAux (R : Type u₁) {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} (Q : 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

• Algebra.Generators.H1Cotangent.δAux R Q = (Finsupp.lsum R) fun (f : ι →₀ ℕ) => ↑R ((TensorProduct.mk S T Ω[S⁄R]) (f.prod fun (x1 : ι) (x2 : ℕ) => Q.val x1 ^ x2)) ∘ₗ ↑(KaehlerDifferential.D R S)

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

@[simp]

theorem Algebra.Generators.H1Cotangent.δAux_X {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} (Q : Generators S T ι) (i : ι) : (δAux R Q) (MvPolynomial.X i) = 0

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

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

theorem Algebra.Generators.H1Cotangent.δAux_toAlgHom {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {ι' : Type w₃} {Q : Generators S T ι} {Q' : Generators S T ι'} (f : Q.Hom Q') (x : Q.Ring) : (δAux R Q') (f.toAlgHom x) = (δAux R Q) x + (Finsupp.linearCombination T (⇑(δ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 u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Generators S T ι) (P : Generators R S σ) (x : (Q.comp P).Ring) : (δAux R Q) ((Q.ofComp P).toAlgHom x) = (LinearMap.baseChange T P.toExtension.toKaehler) ((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 u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Generators S T ι) (P : Generators R S σ) : LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) ∘ₗ LinearMap.baseChange T P.toExtension.cotangentComplex = (Q.comp P).toExtension.cotangentComplex ∘ₗ LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)

noncomputable def Algebra.Generators.H1Cotangent.δ {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Generators S T ι) (P : 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 u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Generators S T ι) (P : Generators R S σ) : Function.Exact ⇑(δ Q P) ⇑(KaehlerDifferential.mapBaseChange R S T)

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

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

theorem Algebra.Generators.H1Cotangent.δ_eq_δ {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} {σ' : Type w₄} (Q : Generators S T ι) (P : Generators R S σ) (P' : Generators R S σ') : δ Q P = δ Q P'

theorem Algebra.Generators.H1Cotangent.exact_map_δ {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Generators S T ι) (P : Generators R S σ) : Function.Exact ⇑(Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom) ⇑(δ Q P)

theorem Algebra.Generators.H1Cotangent.δ_map {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {ι' : Type w₃} {σ : Type w₂} {σ' : Type w₄} (Q : Generators S T ι) (P : Generators R S σ) (Q' : Generators S T ι') (P' : Generators R S σ') (f : Q'.Hom Q) (x : Q'.toExtension.H1Cotangent) : (δ Q P) ((Extension.H1Cotangent.map f.toExtensionHom) x) = (δ Q' P') x

theorem Algebra.Generators.H1Cotangent.δ_comp_equiv {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {ι' : Type w₃} {σ : Type w₂} {σ' : Type w₄} (Q : Generators S T ι) (P : Generators R S σ) (Q' : Generators S T ι') (P' : Generators R S σ') : δ Q P ∘ₗ ↑(equiv Q' Q) = δ Q' P'

theorem Algebra.Generators.H1Cotangent.exact_map_δ' {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} {τ : Type w₅} (Q : Generators S T ι) (P : Generators R S σ) (W : Generators R T τ) (f : W.Hom Q) : Function.Exact ⇑(Extension.H1Cotangent.map f.toExtensionHom) ⇑(δ Q P)

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

noncomputable def Algebra.H1Cotangent.δ (R : Type u₁) (S : Type u₂) [CommRing R] [CommRing S] [Algebra R S] (T : Type u₃) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] : 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 u₂) [CommRing R] [CommRing S] [Algebra R S] (T : Type u₃) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] : Function.Exact ⇑(map R S T T) ⇑(δ 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 u₂) [CommRing R] [CommRing S] [Algebra R S] (T : Type u₃) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] : Function.Exact ⇑(δ 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.