Documentation

TauCeti.RingTheory.GradedAlgebra.TensorProduct

The graded tensor product of two internally โ„ค-graded algebras is graded #

Mathlib's GradedTensorProduct R ๐’œ โ„ฌ, written ๐’œ แตโŠ—[R] โ„ฌ, is the tensor product A โŠ—[R] B with the Koszul-signed multiplication

(a แตโŠ—โ‚œ b) * (a' แตโŠ—โ‚œ b') = (-1) ^ (|b| * |a'|) โ€ข (a * a') แตโŠ—โ‚œ (b * b').

Mathlib stops at the ring and algebra structures. This file supplies the grading they are compatible with: the total-degree grading of the underlying tensor product of graded modules turns ๐’œ แตโŠ—[R] โ„ฌ into an internally โ„ค-graded algebra.

Main definitions #

Main results #

The grading of the underlying module is TauCeti.InternalGrading.tensorProduct and the Koszul multiplication is Mathlib's GradedTensorProduct; only their compatibility is proved here.

References #

source
noncomputable def TauCeti.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 โ„ฌ] (n : โ„ค) :
Submodule R (GradedTensorProduct R ๐’œ โ„ฌ)

The total-degree grading of the graded tensor product ๐’œ แตโŠ—[R] โ„ฌ: the degree-n piece is the sum of the images of ๐’œ p โŠ— โ„ฌ (n - p).

Equations
Instances For
    source
    theorem TauCeti.isInternal_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 โ„ฌ] :
    DirectSum.IsInternal (gradedTensorGrading ๐’œ โ„ฌ)

    The homogeneous pieces of the graded tensor product form an internal direct sum.

    source
    theorem TauCeti.tmul_mem_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 โ„ฌ] {p q : โ„ค} {a : A} {b : B} (ha : a โˆˆ ๐’œ p) (hb : b โˆˆ โ„ฌ q) :
    a แตโŠ—โ‚œ[R] b โˆˆ gradedTensorGrading ๐’œ โ„ฌ (p + q)

    A pure tensor of homogeneous elements is homogeneous, of the sum of their degrees.

    source
    theorem TauCeti.gradedTensorGrading_le {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 โ„ฌ] {n : โ„ค} {C : Submodule R (GradedTensorProduct R ๐’œ โ„ฌ)} (h : โˆ€ (p : โ„ค), โˆ€ a โˆˆ ๐’œ p, โˆ€ b โˆˆ โ„ฌ (n - p), a แตโŠ—โ‚œ[R] b โˆˆ C) :
    gradedTensorGrading ๐’œ โ„ฌ n โ‰ค C

    A submodule containing every homogeneous pure tensor of total degree n contains the whole degree-n piece of the graded tensor product.

    source
    theorem TauCeti.gradedTensor_eq_top_of_tmul_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 โ„ฌ] {C : Submodule R (GradedTensorProduct R ๐’œ โ„ฌ)} (h : โˆ€ (p q : โ„ค), โˆ€ a โˆˆ ๐’œ p, โˆ€ b โˆˆ โ„ฌ q, a แตโŠ—โ‚œ[R] b โˆˆ C) :
    C = โŠค

    A submodule containing every homogeneous pure tensor is the whole graded tensor product.

    source
    instance TauCeti.instGradedMonoidGradedTensorGrading {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 โ„ฌ] :
    SetLike.GradedMonoid (gradedTensorGrading ๐’œ โ„ฌ)

    The Koszul multiplication of the graded tensor product adds degrees.

    source
    @[instance_reducible]
    noncomputable instance TauCeti.instGradedAlgebraGradedTensorGrading {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 โ„ฌ] :
    GradedAlgebra (gradedTensorGrading ๐’œ โ„ฌ)

    The graded tensor product of two internally โ„ค-graded algebras is an internally โ„ค-graded algebra for the total-degree grading.

    Equations
    source
    noncomputable def TauCeti.gradedTensorLift {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 โ„ฌ] {C : Type uC} [Ring C] [Algebra R C] (๐’ž : โ„ค โ†’ Submodule R C) [GradedAlgebra ๐’ž] (f : ๐’œ โ†’โ‚แต[R] ๐’ž) (g : โ„ฌ โ†’โ‚แต[R] ๐’ž) (h : โˆ€ โฆƒi j : โ„คโฆ„ (a : โ†ฅ(๐’œ i)) (b : โ†ฅ(โ„ฌ j)), f โ†‘a * g โ†‘b = (-1) ^ (j * i) โ€ข (g โ†‘b * f โ†‘a)) :
    gradedTensorGrading ๐’œ โ„ฌ โ†’โ‚แต[R] ๐’ž

    The graded algebra map out of a graded tensor product induced by two graded algebra maps whose images satisfy the Koszul commutation rule.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.gradedTensorLift_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 โ„ฌ] {C : Type uC} [Ring C] [Algebra R C] (๐’ž : โ„ค โ†’ Submodule R C) [GradedAlgebra ๐’ž] (f : ๐’œ โ†’โ‚แต[R] ๐’ž) (g : โ„ฌ โ†’โ‚แต[R] ๐’ž) (h : โˆ€ โฆƒi j : โ„คโฆ„ (a : โ†ฅ(๐’œ i)) (b : โ†ฅ(โ„ฌ j)), f โ†‘a * g โ†‘b = (-1) ^ (j * i) โ€ข (g โ†‘b * f โ†‘a)) (a : A) (b : B) :
      (gradedTensorLift ๐’œ โ„ฌ ๐’ž f g h) (a แตโŠ—โ‚œ[R] b) = f a * g b

      The graded tensor lift sends a pure tensor to the product of the two factor maps.

      source
      @[simp]
      theorem TauCeti.gradedTensor_add_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 โ„ฌ] (aโ‚ aโ‚‚ : A) (b : B) :
      (aโ‚ + aโ‚‚) แตโŠ—โ‚œ[R] b = aโ‚ แตโŠ—โ‚œ[R] b + aโ‚‚ แตโŠ—โ‚œ[R] b

      A pure tensor of the graded tensor product is additive in its left factor.

      source
      @[simp]
      theorem TauCeti.gradedTensor_tmul_add {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 โ„ฌ] (a : A) (bโ‚ bโ‚‚ : B) :
      a แตโŠ—โ‚œ[R] (bโ‚ + bโ‚‚) = a แตโŠ—โ‚œ[R] bโ‚ + a แตโŠ—โ‚œ[R] bโ‚‚

      A pure tensor of the graded tensor product is additive in its right factor.

      source
      @[simp]
      theorem TauCeti.gradedTensor_smul_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 โ„ฌ] (r : R) (a : A) (b : B) :
      (r โ€ข a) แตโŠ—โ‚œ[R] b = r โ€ข a แตโŠ—โ‚œ[R] b

      Scalars pass from the left factor of a pure tensor to the tensor.

      source
      @[simp]
      theorem TauCeti.gradedTensor_tmul_smul {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 โ„ฌ] (r : R) (a : A) (b : B) :
      a แตโŠ—โ‚œ[R] (r โ€ข b) = r โ€ข a แตโŠ—โ‚œ[R] b

      Scalars pass from the right factor of a pure tensor to the tensor.

      source
      @[simp]
      theorem TauCeti.gradedTensor_zero_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 โ„ฌ] (b : B) :
      0 แตโŠ—โ‚œ[R] b = 0

      A pure tensor of the graded tensor product vanishes when its left factor does.

      source
      @[simp]
      theorem TauCeti.gradedTensor_tmul_zero {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 โ„ฌ] (a : A) :
      a แตโŠ—โ‚œ[R] 0 = 0

      A pure tensor of the graded tensor product vanishes when its right factor does.

      source
      theorem TauCeti.gradedTensor_linearMap_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 โ„ฌ] {M : Type u_1} [AddCommGroup M] [Module R M] {f g : GradedTensorProduct R ๐’œ โ„ฌ โ†’โ‚—[R] M} (h : โˆ€ (p q : โ„ค), โˆ€ a โˆˆ ๐’œ p, โˆ€ b โˆˆ โ„ฌ q, f (a แตโŠ—โ‚œ[R] b) = g (a แตโŠ—โ‚œ[R] b)) :
      f = g

      Two linear maps out of the graded tensor product agree as soon as they agree on the pure tensors of homogeneous elements.

      source
      noncomputable def TauCeti.gradedTensorIncludeLeft {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 โ„ฌ] :
      ๐’œ โ†’โ‚แต[R] gradedTensorGrading ๐’œ โ„ฌ

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

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.gradedTensorIncludeLeft_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 โ„ฌ] (a : A) :
        (gradedTensorIncludeLeft ๐’œ โ„ฌ) a = a แตโŠ—โ‚œ[R] 1
        source
        noncomputable def TauCeti.gradedTensorIncludeRight {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 โ„ฌ] :
        โ„ฌ โ†’โ‚แต[R] gradedTensorGrading ๐’œ โ„ฌ

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

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.gradedTensorIncludeRight_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 โ„ฌ] (b : B) :
          (gradedTensorIncludeRight ๐’œ โ„ฌ) b = 1 แตโŠ—โ‚œ[R] b
          source
          theorem TauCeti.gradedTensorAlgHom_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 โ„ฌ] {C : Type uC} [Ring C] [Algebra R C] (๐’ž : โ„ค โ†’ Submodule R C) [GradedAlgebra ๐’ž] โฆƒf g : gradedTensorGrading ๐’œ โ„ฌ โ†’โ‚แต[R] ๐’žโฆ„ (ha : f.comp (gradedTensorIncludeLeft ๐’œ โ„ฌ) = g.comp (gradedTensorIncludeLeft ๐’œ โ„ฌ)) (hb : f.comp (gradedTensorIncludeRight ๐’œ โ„ฌ) = g.comp (gradedTensorIncludeRight ๐’œ โ„ฌ)) :
          f = g

          Two graded algebra morphisms from the graded tensor product agree if their compositions with the left and right factor inclusions agree.

          source
          theorem TauCeti.gradedTensorAlgHom_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 โ„ฌ] {C : Type uC} [Ring C] [Algebra R C] {๐’ž : โ„ค โ†’ Submodule R C} [GradedAlgebra ๐’ž] {f g : gradedTensorGrading ๐’œ โ„ฌ โ†’โ‚แต[R] ๐’ž} :
          f = g โ†” f.comp (gradedTensorIncludeLeft ๐’œ โ„ฌ) = g.comp (gradedTensorIncludeLeft ๐’œ โ„ฌ) โˆง f.comp (gradedTensorIncludeRight ๐’œ โ„ฌ) = g.comp (gradedTensorIncludeRight ๐’œ โ„ฌ)