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

• GradedTensorProduct R 𝒜 ℬ: for families of submodules of A and B that form a graded algebra, this is a type alias for A ⊗[R] B with the appropriate multiplication.
• GradedTensorProduct.instAlgebra: the ring structure induced by this multiplication.
• GradedTensorProduct.liftEquiv: a universal property for graded tensor products

Notation

• 𝒜 ᵍ⊗[R] ℬ is notation for GradedTensorProduct R 𝒜 ℬ.
• a ᵍ⊗ₜ b is notation for GradedTensorProduct.tmul _ a b.

References

• https://math.stackexchange.com/q/202718/1896
• [Algebra I, Bourbaki : Chapter III, §4.7, example (2)][bourbaki1989]

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

• Show that the tensor product of graded algebras is itself a graded algebra.
• Determine if replacing the synonym with a single-field structure improves performance.

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] ℬ.

@[implicit_reducible]

instance instAddCommGroupWithOneGradedTensorProduct (R : Type u_3) {ι : Type u_4} {A : Type u_1} {B : Type u_2} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] : AddCommGroupWithOne (GradedTensorProduct R 𝒜 ℬ)

@[implicit_reducible]

instance instModuleGradedTensorProduct (R : Type u_1) {ι : Type u_4} {A : Type u_2} {B : Type u_3} [CommSemiring ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] : Module R (GradedTensorProduct R 𝒜 ℬ)

def TensorProduct.«term_ᵍ⊗[_]_» : Lean.TrailingParserDescr

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

This has notation 𝒜 ᵍ⊗[R] ℬ.

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 ℬ] : TensorProduct R A B ≃ₗ[R] GradedTensorProduct R 𝒜 ℬ

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

@[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 ℬ] : (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 ℬ] : (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) : (of R 𝒜 ℬ).symm ((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 𝒜 ℬ) : (of R 𝒜 ℬ) ((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 g : GradedTensorProduct R 𝒜 ℬ →ₗ[R] M⦄ (h : f ∘ₗ ↑(of R 𝒜 ℬ) = g ∘ₗ ↑(of R 𝒜 ℬ)) : f = g

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

theorem GradedTensorProduct.hom_ext_iff {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 g : GradedTensorProduct R 𝒜 ℬ →ₗ[R] M} : f = g ↔ f ∘ₗ ↑(of R 𝒜 ℬ) = g ∘ₗ ↑(of R 𝒜 ℬ)

@[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) : GradedTensorProduct R 𝒜 ℬ

The graded tensor product of two elements of graded rings.

def GradedTensorProduct.«term_ᵍ⊗ₜ_» : Lean.TrailingParserDescr

The graded tensor product of two elements of graded rings.

def GradedTensorProduct.«term_ᵍ⊗ₜ[_]_» : Lean.TrailingParserDescr

The graded tensor product of two elements of graded rings.

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.

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) : (auxEquiv R 𝒜 ℬ) (a ᵍ⊗ₜ[R] b) = (DirectSum.decompose 𝒜) a ⊗ₜ[R] (DirectSum.decompose ℬ) 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 ℬ] : (auxEquiv R 𝒜 ℬ) 1 = 1

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 ℬ] : (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 ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Module ι (Additive ℤˣ)] : GradedTensorProduct R 𝒜 ℬ →ₗ[R] GradedTensorProduct R 𝒜 ℬ →ₗ[R] GradedTensorProduct R 𝒜 ℬ

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

theorem GradedTensorProduct.mulHom_apply {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 ℬ] [Module ι (Additive ℤˣ)] (x y : GradedTensorProduct R 𝒜 ℬ) : ((mulHom 𝒜 ℬ) x) y = (auxEquiv R 𝒜 ℬ).symm (((TensorProduct.gradedMul R (fun (x : ι) => ↥(𝒜 x)) fun (x : ι) => ↥(ℬ x)) ((auxEquiv R 𝒜 ℬ) x)) ((auxEquiv R 𝒜 ℬ) y))

@[implicit_reducible]

noncomputable instance GradedTensorProduct.instMul {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 ℬ] [Module ι (Additive ℤˣ)] : Mul (GradedTensorProduct R 𝒜 ℬ)

The multiplication on the graded tensor product.

See GradedTensorProduct.coe_mul_coe for a characterization on pure tensors.

theorem GradedTensorProduct.mul_def {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 ℬ] [Module ι (Additive ℤˣ)] (x y : GradedTensorProduct R 𝒜 ℬ) : x * y = ((mulHom 𝒜 ℬ) x) y

theorem GradedTensorProduct.auxEquiv_mul {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 ℬ] [Module ι (Additive ℤˣ)] (x y : GradedTensorProduct R 𝒜 ℬ) : (auxEquiv R 𝒜 ℬ) (x * y) = ((TensorProduct.gradedMul R (fun (x : ι) => ↥(𝒜 x)) fun (x : ι) => ↥(ℬ x)) ((auxEquiv R 𝒜 ℬ) x)) ((auxEquiv R 𝒜 ℬ) y)

@[implicit_reducible]

noncomputable instance GradedTensorProduct.instMonoid {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 ℬ] [Module ι (Additive ℤˣ)] : Monoid (GradedTensorProduct R 𝒜 ℬ)

@[implicit_reducible]

noncomputable instance GradedTensorProduct.instRing {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 ℬ] [Module ι (Additive ℤˣ)] : Ring (GradedTensorProduct R 𝒜 ℬ)

theorem GradedTensorProduct.tmul_coe_mul_coe_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 ℬ] [Module ι (Additive ℤˣ)] {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 homogeneous 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 ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Module ι (Additive ℤˣ)] {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 ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Module ι (Additive ℤˣ)] {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 ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Module ι (Additive ℤˣ)] {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 ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Module ι (Additive ℤˣ)] {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 ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Module ι (Additive ℤˣ)] (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 ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Module ι (Additive ℤˣ)] : A →+* GradedTensorProduct R 𝒜 ℬ

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

@[simp]

theorem GradedTensorProduct.includeLeftRingHom_apply {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 ℬ] [Module ι (Additive ℤˣ)] (a : A) : (includeLeftRingHom 𝒜 ℬ) a = a ᵍ⊗ₜ[R] 1

@[implicit_reducible]

noncomputable instance GradedTensorProduct.instAlgebra {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 ℬ] [Module ι (Additive ℤˣ)] : Algebra R (GradedTensorProduct R 𝒜 ℬ)

theorem GradedTensorProduct.algebraMap_def {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 ℬ] [Module ι (Additive ℤˣ)] (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 ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Module ι (Additive ℤˣ)] {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 ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Module ι (Additive ℤˣ)] {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 ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Module ι (Additive ℤˣ)] : A →ₐ[R] GradedTensorProduct R 𝒜 ℬ

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

@[simp]

theorem GradedTensorProduct.includeLeft_apply {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 ℬ] [Module ι (Additive ℤˣ)] (a : A) : (includeLeft 𝒜 ℬ) a = a ᵍ⊗ₜ[R] 1

noncomputable def GradedTensorProduct.includeRight {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 ℬ] [Module ι (Additive ℤˣ)] : B →ₐ[R] GradedTensorProduct R 𝒜 ℬ

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

@[simp]

theorem GradedTensorProduct.includeRight_apply {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 ℬ] [Module ι (Additive ℤˣ)] (a : B) : (includeRight 𝒜 ℬ) a = 1 ᵍ⊗ₜ[R] a

theorem GradedTensorProduct.algebraMap_def' {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 ℬ] [Module ι (Additive ℤˣ)] (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 ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Module ι (Additive ℤˣ)] {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)) : GradedTensorProduct R 𝒜 ℬ →ₐ[R] C

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

@[simp]

theorem GradedTensorProduct.lift_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 ℬ] [Module ι (Additive ℤˣ)] {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) : (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 ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Module ι (Additive ℤˣ)] {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.

theorem GradedTensorProduct.algHom_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 ℬ] [Module ι (Additive ℤˣ)] {C : Type u_5} [Ring C] [Algebra R C] ⦃f g : GradedTensorProduct R 𝒜 ℬ →ₐ[R] C⦄ (ha : f.comp (includeLeft 𝒜 ℬ) = g.comp (includeLeft 𝒜 ℬ)) (hb : f.comp (includeRight 𝒜 ℬ) = g.comp (includeRight 𝒜 ℬ)) : f = g

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

theorem GradedTensorProduct.algHom_ext_iff {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 ℬ] [Module ι (Additive ℤˣ)] {C : Type u_5} [Ring C] [Algebra R C] {f g : GradedTensorProduct R 𝒜 ℬ →ₐ[R] C} : f = g ↔ f.comp (includeLeft 𝒜 ℬ) = g.comp (includeLeft 𝒜 ℬ) ∧ f.comp (includeRight 𝒜 ℬ) = g.comp (includeRight 𝒜 ℬ)

noncomputable def GradedTensorProduct.comm {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 ℬ] [Module ι (Additive ℤˣ)] : GradedTensorProduct R 𝒜 ℬ ≃ₐ[R] GradedTensorProduct R ℬ 𝒜

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

theorem GradedTensorProduct.auxEquiv_comm {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 ℬ] [Module ι (Additive ℤˣ)] (x : GradedTensorProduct R 𝒜 ℬ) : (auxEquiv R ℬ 𝒜) ((comm 𝒜 ℬ) x) = (TensorProduct.gradedComm R (fun (x : ι) => ↥(𝒜 x)) fun (x : ι) => ↥(ℬ x)) ((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 ι] [DecidableEq ι] [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Module ι (Additive ℤˣ)] {i j : ι} (a : ↥(𝒜 i)) (b : ↥(ℬ j)) : (comm 𝒜 ℬ) (↑a ᵍ⊗ₜ[R] ↑b) = (-1) ^ (j * i) • ↑b ᵍ⊗ₜ[R] ↑a