Documentation

Mathlib.RingTheory.Kaehler.JacobiZariski

The Jacobi-Zariski exact sequence #

Given algebras $R \to S \to T$, the Jacobi-Zariski exact sequence is a long exact sequence relating the first homology of the naive cotangent complexes and the Kähler differentials of the respective algebras. It takes the form: $$ H_1(L_{T/R}) \to H_1(L_{T/S}) \to T \otimes_S \Omega_{S/R} \to \Omega_{T/R} \to \Omega_{T/S} \to 0 $$ The maps in the sequence are

The exactness lemmas are

When $T$ is flat over $S$, the left bottom part of the snake lemma diagram used in the construction of the connecting homomorphism Algebra.Generators.H1Cotangent.δ naturally extends via a base change map. The exactness lemma is Algebra.Generators.H1Cotangent.exact_liftBaseChange_map_of_flat. Globally, this extends the Jacobi-Zariski exact sequence to the left via a natural base change map, taking the form $$ T \otimes_S H_1(L_{S/R}) \to H_1(L_{T/R}) \to H_1(L_{T/S}) $$ The exactness lemma is Algebra.H1Cotangent.exact_liftBaseChange_map_of_flat.

TODO #

The flatness assumption in Algebra.H1Cotangent.exact_liftBaseChange_map_of_flat is stronger than the Tor-vanishing conditions required in the full statement of [Stacks Project, 00S2], this should be refactored and generalized once more API for Tor modules is available.

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

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.

source
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
Instances For
    source
    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)
    source
    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
    source
    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
    source
    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
    source
    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))
    source
    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.

    source
    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)
    source
    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
    Instances For
      source
      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
      source
      @[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
      source
      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
      source
      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
      source
      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))
      source
      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
      source
      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)
      source
      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.
      Instances For
        source
        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)
        source
        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
        source
        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 ∈ Q.toExtension.cotangentComplex.ker) :
        (δ Q P) ⟨Extension.Cotangent.mk x, hx⟩ = (δAux R Q) ↑x
        source
        theorem Algebra.Generators.H1Cotangent.δ_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₁} {σ : Type w₂} (Q : Generators S T ι) (P : Generators R S σ) {r : S} (hr : MvPolynomial.C r ∈ Q.ker) :
        (δ Q P) ⟨Extension.Cotangent.mk ⟨MvPolynomial.C r, hr⟩, ⋯⟩ = 1 ⊗ₜ[S] (KaehlerDifferential.D R S) r
        source
        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'
        source
        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)
        source
        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
        source
        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'
        source
        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.

        source
        theorem Algebra.Generators.H1Cotangent.liftBaseChange_range_le {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.H1Cotangent.map (Q.toComp P).toExtensionHom)).range ≤ (Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom).ker
        source
        theorem Algebra.Generators.H1Cotangent.exact_liftBaseChange_map_of_flat {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 σ) [Module.Flat S T] :
        Function.Exact ⇑(LinearMap.liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)) ⇑(Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom)

        When $T$ is flat over $S$, the left bottom part of the snake lemma diagram used in the construction of the connecting homomorphism Algebra.Generators.H1Cotangent.δ naturally extends via a base change map.

        source
        theorem Algebra.Generators.H1Cotangent.exact_liftBaseChange_map_of_flat' {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 τ) [Module.Flat S T] (f : W.Hom Q) (g : P.Hom W) :
        Function.Exact ⇑(LinearMap.liftBaseChange T (Extension.H1Cotangent.map g.toExtensionHom)) ⇑(Extension.H1Cotangent.map f.toExtensionHom)

        A variant of exact_liftBaseChange_map_of_flat that takes in arbitrary maps between generators.

        source
        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
        Instances For
          source
          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 \to S \to T$, the sequence $H_1(L_{T/R}) \to H_1(L_{T/S}) \to T \otimes_S \Omega_{S/R}$ is exact.

          source
          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 \to S \to T$, the sequence $H_1(L_{T/S}) \to T \otimes_S \Omega_{S/R} \to \Omega_{T/R}$ is exact.

          source
          theorem Algebra.H1Cotangent.exact_liftBaseChange_map_of_flat (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] [Module.Flat S T] :
          Function.Exact ⇑(LinearMap.liftBaseChange T (map R R S T)) ⇑(map R S T T)

          Given algebras $R \to S \to T$ and $T$ flat over $S$, the sequence $T \otimes_S H_1(L_{S/R}) \to H_1(L_{T/R}) \to H_1(L_{T/S})$ is exact.