Documentation

TauCeti.Algebra.Homology.DG.Algebra.TensorProduct

Tensor products of differential graded algebras #

The tensor product of two differential graded algebras (A, d_A) and (B, d_B) is Mathlib's Koszul-signed graded tensor product ๐’œ แตโŠ—[R] โ„ฌ, graded by total degree, with the differential

d (a แตโŠ—โ‚œ b) = d_A a แตโŠ—โ‚œ b + (-1) ^ |a| โ€ข (a แตโŠ—โ‚œ d_B b).

The sign is the one forced by the Koszul rule (f โŠ— g) (x โŠ— y) = (-1) ^ (|g| |x|) f x โŠ— g y for tensor products of homogeneous maps: the differential is d_A โŠ— 1 plus 1 โŠ— d_B, and since d_B has degree one the second summand carries the twist a โ†ฆ (-1) ^ |a| a on the left factor.

Main definitions #

Main results #

Only the left factor of a pure tensor has to be homogeneous for the sign rule, and only the left factor of a product has to be homogeneous for the Leibniz rule, exactly as in the one-factor Leibniz axiom TauCeti.IsDGAlgebra.leibniz.

References #

source
noncomputable def TauCeti.dgTensorDifferential {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (๐’œ : โ„ค โ†’ Submodule R A) (โ„ฌ : โ„ค โ†’ Submodule R B) [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] (dA : A โ†’โ‚—[R] A) (dB : B โ†’โ‚—[R] B) :
GradedTensorProduct R ๐’œ โ„ฌ โ†’โ‚—[R] GradedTensorProduct R ๐’œ โ„ฌ

The differential of the tensor product of two differential graded algebras: the sum of d_A โŠ— 1 and of d_B preceded, on the left factor, by the Koszul twist a โ†ฆ (-1) ^ |a| a.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.dgTensorDifferential_tmul {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} (a : A) (b : B) :
    (dgTensorDifferential ๐’œ โ„ฌ dA dB) (a แตโŠ—โ‚œ[R] b) = dA a แตโŠ—โ‚œ[R] b + ((InternalGrading.ofDecomposition ๐’œ).koszulTwist 1) a แตโŠ—โ‚œ[R] dB b

    The differential of a tensor product, evaluated on a pure tensor.

    source
    theorem TauCeti.dgTensorDifferential_tmul_of_mem {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {p : โ„ค} {a : A} (ha : a โˆˆ ๐’œ p) (b : B) :
    (dgTensorDifferential ๐’œ โ„ฌ dA dB) (a แตโŠ—โ‚œ[R] b) = dA a แตโŠ—โ‚œ[R] b + p.negOnePow โ€ข a แตโŠ—โ‚œ[R] dB b

    The sign rule for the differential of a tensor product on a pure tensor with homogeneous left factor: d (a แตโŠ—โ‚œ b) = d_A a แตโŠ—โ‚œ b + (-1) ^ |a| โ€ข (a แตโŠ—โ‚œ d_B b).

    source
    theorem TauCeti.isDGAlgebra_gradedTensorGrading {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} (hA : IsDGAlgebra ๐’œ dA) (hB : IsDGAlgebra โ„ฌ dB) :
    IsDGAlgebra (gradedTensorGrading ๐’œ โ„ฌ) (dgTensorDifferential ๐’œ โ„ฌ dA dB)

    The tensor product of two differential graded algebras is a differential graded algebra: the total-degree grading of ๐’œ แตโŠ—[R] โ„ฌ and the differential d (a แตโŠ—โ‚œ b) = d_A a แตโŠ—โ‚œ b + (-1) ^ |a| โ€ข (a แตโŠ—โ‚œ d_B b) satisfy the degree, square-zero, and graded Leibniz axioms.

    source
    noncomputable def TauCeti.dgTensorIncludeLeft {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} (hA : IsDGAlgebra ๐’œ dA) (hB : IsDGAlgebra โ„ฌ dB) :
    DGAlgHom hA โ‹ฏ

    The inclusion a โ†ฆ a แตโŠ—โ‚œ 1 of the left factor, as a morphism of differential graded algebras.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.dgTensorIncludeLeft_apply {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} (hA : IsDGAlgebra ๐’œ dA) (hB : IsDGAlgebra โ„ฌ dB) (a : A) :
      (dgTensorIncludeLeft hA hB) a = a แตโŠ—โ‚œ[R] 1
      source
      noncomputable def TauCeti.dgTensorIncludeRight {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} (hA : IsDGAlgebra ๐’œ dA) (hB : IsDGAlgebra โ„ฌ dB) :
      DGAlgHom hB โ‹ฏ

      The inclusion b โ†ฆ 1 แตโŠ—โ‚œ b of the right factor, as a morphism of differential graded algebras.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.dgTensorIncludeRight_apply {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} (hA : IsDGAlgebra ๐’œ dA) (hB : IsDGAlgebra โ„ฌ dB) (b : B) :
        (dgTensorIncludeRight hA hB) b = 1 แตโŠ—โ‚œ[R] b
        source
        noncomputable def TauCeti.dgTensorLift {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {C : Type uC} [Ring C] [Algebra R C] {๐’ž : โ„ค โ†’ Submodule R C} [GradedAlgebra ๐’ž] {dC : C โ†’โ‚—[R] C} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {hC : IsDGAlgebra ๐’ž dC} (f : DGAlgHom hA hC) (g : DGAlgHom hB hC) (h : โˆ€ โฆƒi j : โ„คโฆ„ (a : โ†ฅ(๐’œ i)) (b : โ†ฅ(โ„ฌ j)), f โ†‘a * g โ†‘b = (-1) ^ (j * i) โ€ข (g โ†‘b * f โ†‘a)) :
        DGAlgHom โ‹ฏ hC

        The morphism of differential graded algebras out of a tensor product induced by two morphisms of differential graded algebras whose images satisfy the Koszul commutation rule.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.dgTensorLift_tmul {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {C : Type uC} [Ring C] [Algebra R C] {๐’ž : โ„ค โ†’ Submodule R C} [GradedAlgebra ๐’ž] {dC : C โ†’โ‚—[R] C} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {hC : IsDGAlgebra ๐’ž dC} (f : DGAlgHom hA hC) (g : DGAlgHom hB hC) (h : โˆ€ โฆƒi j : โ„คโฆ„ (a : โ†ฅ(๐’œ i)) (b : โ†ฅ(โ„ฌ j)), f โ†‘a * g โ†‘b = (-1) ^ (j * i) โ€ข (g โ†‘b * f โ†‘a)) (a : A) (b : B) :
          (dgTensorLift f g h) (a แตโŠ—โ‚œ[R] b) = f a * g b

          The lift of two morphisms of differential graded algebras sends a pure tensor to the product of their values.

          source
          theorem TauCeti.dgTensorAlgHom_ext {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {C : Type uC} [Ring C] [Algebra R C] {๐’ž : โ„ค โ†’ Submodule R C} [GradedAlgebra ๐’ž] {dC : C โ†’โ‚—[R] C} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {hC : IsDGAlgebra ๐’ž dC} โฆƒf g : DGAlgHom โ‹ฏ hCโฆ„ (ha : f.comp (dgTensorIncludeLeft hA hB) = g.comp (dgTensorIncludeLeft hA hB)) (hb : f.comp (dgTensorIncludeRight hA hB) = g.comp (dgTensorIncludeRight hA hB)) :
          f = g

          Two morphisms of differential graded algebras out of a tensor product agree if their compositions with the left and right factor inclusions agree.

          source
          theorem TauCeti.dgTensorAlgHom_ext_iff {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {C : Type uC} [Ring C] [Algebra R C] {๐’ž : โ„ค โ†’ Submodule R C} [GradedAlgebra ๐’ž] {dC : C โ†’โ‚—[R] C} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {hC : IsDGAlgebra ๐’ž dC} {f g : DGAlgHom โ‹ฏ hC} :
          f = g โ†” f.comp (dgTensorIncludeLeft hA hB) = g.comp (dgTensorIncludeLeft hA hB) โˆง f.comp (dgTensorIncludeRight hA hB) = g.comp (dgTensorIncludeRight hA hB)