Documentation

Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Graded tensor products over graded algebras #

The graded tensor product $A \hat\otimes_R B$ is imbued with a multiplication defined on homogeneous tensors by:

$$(a \otimes b) \cdot (a' \otimes b') = (-1)^{\deg a' \deg b} (a \cdot a') \otimes (b \cdot b')$$

where $A$ and $B$ are algebras graded by , , or ι (or more generally, any index that satisfies Module ι (Additive ℤˣ)).

Main results #

Notation #

References #

Implementation notes #

We cannot put the multiplication on A ⊗[R] B directly as it would conflict with the existing multiplication defined without the $(-1)^{\deg a' \deg b}$ term. Furthermore, the ring A may not have a unique graduation, and so we need the chosen graduation 𝒜 to appear explicitly in the type.

TODO #

noncomputable def GradedTensorProduct (R : Type u_1) {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] :
Type (max u_4 u_3)

A Type synonym for A ⊗[R] B, but with multiplication as TensorProduct.gradedMul.

This has notation 𝒜 ᵍ⊗[R] ℬ.

Equations
Instances For

    A Type synonym for A ⊗[R] B, but with multiplication as TensorProduct.gradedMul.

    This has notation 𝒜 ᵍ⊗[R] ℬ.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      noncomputable instance GradedTensorProduct.instAddCommGroupWithOne {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] :
      Equations
      noncomputable instance GradedTensorProduct.instModule {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] :
      Equations
      noncomputable def GradedTensorProduct.of (R : Type u_1) {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] :

      The casting equivalence to move between regular and graded tensor products.

      Equations
      Instances For
        @[simp]
        theorem GradedTensorProduct.of_one {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] :
        (GradedTensorProduct.of R 𝒜 ) 1 = 1
        @[simp]
        theorem GradedTensorProduct.of_symm_one {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] :
        (GradedTensorProduct.of R 𝒜 ).symm 1 = 1
        @[simp]
        theorem GradedTensorProduct.of_symm_of {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] (x : TensorProduct R A B) :
        (GradedTensorProduct.of R 𝒜 ).symm ((GradedTensorProduct.of R 𝒜 ) x) = x
        @[simp]
        theorem GradedTensorProduct.symm_of_of {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] (x : GradedTensorProduct R 𝒜 ) :
        (GradedTensorProduct.of R 𝒜 ) ((GradedTensorProduct.of R 𝒜 ).symm x) = x
        theorem GradedTensorProduct.hom_ext {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] {M : Type u_5} [AddCommMonoid M] [Module R M] ⦃f : GradedTensorProduct R 𝒜 →ₗ[R] M ⦃g : GradedTensorProduct R 𝒜 →ₗ[R] M (h : f ∘ₗ (GradedTensorProduct.of R 𝒜 ) = g ∘ₗ (GradedTensorProduct.of R 𝒜 )) :
        f = g

        Two linear maps from the graded tensor product agree if they agree on the underlying tensor product.

        @[reducible, inline]
        noncomputable abbrev GradedTensorProduct.tmul (R : Type u_1) {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {𝒜 : ιSubmodule R A} {ℬ : ιSubmodule R B} [GradedAlgebra 𝒜] [GradedAlgebra ] (a : A) (b : B) :

        The graded tensor product of two elements of graded rings.

        Equations
        Instances For

          The graded tensor product of two elements of graded rings.

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

            The graded tensor product of two elements of graded rings.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              noncomputable def GradedTensorProduct.auxEquiv (R : Type u_1) {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] :
              GradedTensorProduct R 𝒜 ≃ₗ[R] TensorProduct R (DirectSum ι fun (i : ι) => (𝒜 i)) (DirectSum ι fun (i : ι) => ( i))

              An auxiliary construction to move between the graded tensor product of internally-graded objects and the tensor product of direct sums.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem GradedTensorProduct.auxEquiv_tmul {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] (a : A) (b : B) :
                theorem GradedTensorProduct.auxEquiv_one {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] :
                theorem GradedTensorProduct.auxEquiv_symm_one {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] :
                (GradedTensorProduct.auxEquiv R 𝒜 ).symm 1 = 1
                noncomputable def GradedTensorProduct.mulHom {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] :

                Auxiliary construction used to build the Mul instance and get distributivity of + and \smul.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem GradedTensorProduct.mulHom_apply {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] (x : GradedTensorProduct R 𝒜 ) (y : GradedTensorProduct R 𝒜 ) :
                  ((GradedTensorProduct.mulHom 𝒜 ) x) y = (GradedTensorProduct.auxEquiv R 𝒜 ).symm (((TensorProduct.gradedMul R (fun (x : ι) => (𝒜 x)) fun (x : ι) => ( x)) ((GradedTensorProduct.auxEquiv R 𝒜 ) x)) ((GradedTensorProduct.auxEquiv R 𝒜 ) y))
                  noncomputable instance GradedTensorProduct.instMul {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] :

                  The multipication on the graded tensor product.

                  See GradedTensorProduct.coe_mul_coe for a characterization on pure tensors.

                  Equations
                  theorem GradedTensorProduct.mul_def {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] (x : GradedTensorProduct R 𝒜 ) (y : GradedTensorProduct R 𝒜 ) :
                  x * y = ((GradedTensorProduct.mulHom 𝒜 ) x) y
                  theorem GradedTensorProduct.auxEquiv_mul {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] (x : GradedTensorProduct R 𝒜 ) (y : GradedTensorProduct R 𝒜 ) :
                  (GradedTensorProduct.auxEquiv R 𝒜 ) (x * y) = ((TensorProduct.gradedMul R (fun (x : ι) => (𝒜 x)) fun (x : ι) => ( x)) ((GradedTensorProduct.auxEquiv R 𝒜 ) x)) ((GradedTensorProduct.auxEquiv R 𝒜 ) y)
                  noncomputable instance GradedTensorProduct.instMonoid {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] :
                  Equations
                  noncomputable instance GradedTensorProduct.instRing {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] :
                  Equations
                  • One or more equations did not get rendered due to their size.
                  theorem GradedTensorProduct.tmul_coe_mul_coe_tmul {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] {j₁ : ι} {i₂ : ι} (a₁ : A) (b₁ : ( j₁)) (a₂ : (𝒜 i₂)) (b₂ : B) :
                  a₁ ᵍ⊗ₜ[R] b₁ * a₂ ᵍ⊗ₜ[R] b₂ = (-1) ^ (j₁ * i₂) (a₁ * a₂) ᵍ⊗ₜ[R] (b₁ * b₂)

                  The characterization of this multiplication on partially homogenous elements.

                  theorem GradedTensorProduct.tmul_zero_coe_mul_coe_tmul {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] {i₂ : ι} (a₁ : A) (b₁ : ( 0)) (a₂ : (𝒜 i₂)) (b₂ : B) :
                  a₁ ᵍ⊗ₜ[R] b₁ * a₂ ᵍ⊗ₜ[R] b₂ = (a₁ * a₂) ᵍ⊗ₜ[R] (b₁ * b₂)

                  A special case for when b₁ has grade 0.

                  theorem GradedTensorProduct.tmul_coe_mul_zero_coe_tmul {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] {j₁ : ι} (a₁ : A) (b₁ : ( j₁)) (a₂ : (𝒜 0)) (b₂ : B) :
                  a₁ ᵍ⊗ₜ[R] b₁ * a₂ ᵍ⊗ₜ[R] b₂ = (a₁ * a₂) ᵍ⊗ₜ[R] (b₁ * b₂)

                  A special case for when a₂ has grade 0.

                  theorem GradedTensorProduct.tmul_one_mul_coe_tmul {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] {i₂ : ι} (a₁ : A) (a₂ : (𝒜 i₂)) (b₂ : B) :
                  a₁ ᵍ⊗ₜ[R] 1 * a₂ ᵍ⊗ₜ[R] b₂ = (a₁ * a₂) ᵍ⊗ₜ[R] b₂
                  theorem GradedTensorProduct.tmul_coe_mul_one_tmul {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] {j₁ : ι} (a₁ : A) (b₁ : ( j₁)) (b₂ : B) :
                  a₁ ᵍ⊗ₜ[R] b₁ * 1 ᵍ⊗ₜ[R] b₂ = a₁ ᵍ⊗ₜ[R] (b₁ * b₂)
                  theorem GradedTensorProduct.tmul_one_mul_one_tmul {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] (a₁ : A) (b₂ : B) :
                  a₁ ᵍ⊗ₜ[R] 1 * 1 ᵍ⊗ₜ[R] b₂ = a₁ ᵍ⊗ₜ[R] b₂
                  noncomputable def GradedTensorProduct.includeLeftRingHom {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] :

                  The ring morphism A →+* A ⊗[R] B sending a to a ⊗ₜ 1.

                  Equations
                  Instances For
                    @[simp]
                    theorem GradedTensorProduct.includeLeftRingHom_apply {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] (a : A) :
                    noncomputable instance GradedTensorProduct.instAlgebra {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] :
                    Equations
                    theorem GradedTensorProduct.algebraMap_def {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] (r : R) :
                    (algebraMap R (GradedTensorProduct R 𝒜 )) r = (algebraMap R A) r ᵍ⊗ₜ[R] 1
                    theorem GradedTensorProduct.tmul_algebraMap_mul_coe_tmul {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] {i₂ : ι} (a₁ : A) (r : R) (a₂ : (𝒜 i₂)) (b₂ : B) :
                    a₁ ᵍ⊗ₜ[R] (algebraMap R B) r * a₂ ᵍ⊗ₜ[R] b₂ = (a₁ * a₂) ᵍ⊗ₜ[R] ((algebraMap R B) r * b₂)
                    theorem GradedTensorProduct.tmul_coe_mul_algebraMap_tmul {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] {j₁ : ι} (a₁ : A) (b₁ : ( j₁)) (r : R) (b₂ : B) :
                    a₁ ᵍ⊗ₜ[R] b₁ * (algebraMap R A) r ᵍ⊗ₜ[R] b₂ = (a₁ * (algebraMap R A) r) ᵍ⊗ₜ[R] (b₁ * b₂)
                    noncomputable def GradedTensorProduct.includeLeft {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] :

                    The algebra morphism A →ₐ[R] A ⊗[R] B sending a to a ⊗ₜ 1.

                    Equations
                    Instances For
                      @[simp]
                      theorem GradedTensorProduct.includeLeft_apply {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] (a : A) :
                      noncomputable def GradedTensorProduct.includeRight {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] :

                      The algebra morphism B →ₐ[R] A ⊗[R] B sending b to 1 ⊗ₜ b.

                      Equations
                      Instances For
                        @[simp]
                        theorem GradedTensorProduct.includeRight_apply {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] (a : B) :
                        theorem GradedTensorProduct.algebraMap_def' {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] (r : R) :
                        (algebraMap R (GradedTensorProduct R 𝒜 )) r = 1 ᵍ⊗ₜ[R] (algebraMap R B) r
                        noncomputable def GradedTensorProduct.lift {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] {C : Type u_5} [Ring C] [Algebra R C] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (h_anti_commutes : ∀ ⦃i j : ι⦄ (a : (𝒜 i)) (b : ( j)), f a * g b = (-1) ^ (j * i) (g b * f a)) :

                        The forwards direction of the universal property; an algebra morphism out of the graded tensor product can be assembed from maps on each component that (anti)commute on pure elements of the corresponding graded algebras.

                        Equations
                        Instances For
                          @[simp]
                          theorem GradedTensorProduct.lift_tmul {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] {C : Type u_5} [Ring C] [Algebra R C] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (h_anti_commutes : ∀ ⦃i j : ι⦄ (a : (𝒜 i)) (b : ( j)), f a * g b = (-1) ^ (j * i) (g b * f a)) (a : A) (b : B) :
                          (GradedTensorProduct.lift 𝒜 f g h_anti_commutes) (a ᵍ⊗ₜ[R] b) = f a * g b
                          noncomputable def GradedTensorProduct.liftEquiv {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] {C : Type u_5} [Ring C] [Algebra R C] :
                          { fg : (A →ₐ[R] C) × (B →ₐ[R] C) // ∀ ⦃i j : ι⦄ (a : (𝒜 i)) (b : ( j)), fg.1 a * fg.2 b = (-1) ^ (j * i) (fg.2 b * fg.1 a) } (GradedTensorProduct R 𝒜 →ₐ[R] C)

                          The universal property of the graded tensor product; every algebra morphism uniquely factors as a pair of algebra morphisms that anticommute with respect to the grading.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            theorem GradedTensorProduct.algHom_ext {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] {C : Type u_5} [Ring C] [Algebra R C] ⦃f : GradedTensorProduct R 𝒜 →ₐ[R] C ⦃g : GradedTensorProduct R 𝒜 →ₐ[R] C (ha : f.comp (GradedTensorProduct.includeLeft 𝒜 ) = g.comp (GradedTensorProduct.includeLeft 𝒜 )) (hb : f.comp (GradedTensorProduct.includeRight 𝒜 ) = g.comp (GradedTensorProduct.includeRight 𝒜 )) :
                            f = g

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

                            noncomputable def GradedTensorProduct.comm {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] :

                            The non-trivial symmetric braiding, sending $a \otimes b$ to $(-1)^{\deg a' \deg b} (b \otimes a)$.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              theorem GradedTensorProduct.auxEquiv_comm {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] (x : GradedTensorProduct R 𝒜 ) :
                              (GradedTensorProduct.auxEquiv R 𝒜) ((GradedTensorProduct.comm 𝒜 ) x) = (TensorProduct.gradedComm R (fun (x : ι) => (𝒜 x)) fun (x : ι) => ( x)) ((GradedTensorProduct.auxEquiv R 𝒜 ) x)
                              @[simp]
                              theorem GradedTensorProduct.comm_coe_tmul_coe {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring ι] [Module ι (Additive ˣ)] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ιSubmodule R A) (ℬ : ιSubmodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ] {i : ι} {j : ι} (a : (𝒜 i)) (b : ( j)) :
                              (GradedTensorProduct.comm 𝒜 ) (a ᵍ⊗ₜ[R] b) = (-1) ^ (j * i) b ᵍ⊗ₜ[R] a