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 ofAandBthat form a graded algebra, this is a type alias forA ⊗[R] Bwith 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 forGradedTensorProduct R 𝒜 ℬ.a ᵍ⊗ₜ bis notation forGradedTensorProduct.tmul _ a b.
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 #
- 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] ℬ.
Equations
- GradedTensorProduct R 𝒜 ℬ = TensorProduct R A B
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
- GradedTensorProduct.instAddCommGroupWithOne 𝒜 ℬ = Algebra.TensorProduct.instAddCommGroupWithOne
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 ℬ]
:
Module R (GradedTensorProduct R 𝒜 ℬ)
Equations
- GradedTensorProduct.instModule 𝒜 ℬ = TensorProduct.leftModule
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.
Equations
- GradedTensorProduct.of R 𝒜 ℬ = LinearEquiv.refl R (TensorProduct R A B)
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 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)
:
GradedTensorProduct R 𝒜 ℬ
The graded tensor product of two elements of graded rings.
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
- GradedTensorProduct.auxEquiv R 𝒜 ℬ = (GradedTensorProduct.of R 𝒜 ℬ).symm.trans (TensorProduct.congr (DirectSum.decomposeAlgEquiv 𝒜).toLinearEquiv (DirectSum.decomposeAlgEquiv ℬ).toLinearEquiv)
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)
:
(GradedTensorProduct.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 ℬ]
:
(GradedTensorProduct.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 ℬ]
:
(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 ι]
[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.
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 ι]
[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 𝒜 ℬ)
:
((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 ι]
[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.
Equations
- GradedTensorProduct.instMul 𝒜 ℬ = { mul := fun (x y : GradedTensorProduct R 𝒜 ℬ) => ((GradedTensorProduct.mulHom 𝒜 ℬ) x) y }
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 = ((GradedTensorProduct.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 𝒜 ℬ)
:
(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 ι]
[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 𝒜 ℬ)
Equations
- GradedTensorProduct.instMonoid 𝒜 ℬ = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯
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 𝒜 ℬ)
Equations
- GradedTensorProduct.instRing 𝒜 ℬ = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
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)
:
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 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 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)
:
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)
:
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)
:
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.
Equations
- GradedTensorProduct.includeLeftRingHom 𝒜 ℬ = { toFun := fun (a : A) => a ᵍ⊗ₜ[R] 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
@[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)
:
(GradedTensorProduct.includeLeftRingHom 𝒜 ℬ) a = a ᵍ⊗ₜ[R] 1
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 𝒜 ℬ)
Equations
- GradedTensorProduct.instAlgebra 𝒜 ℬ = Algebra.mk ((GradedTensorProduct.includeLeftRingHom 𝒜 ℬ).comp (algebraMap 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 = (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)
:
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)
:
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.
Equations
- GradedTensorProduct.includeLeft 𝒜 ℬ = { toRingHom := GradedTensorProduct.includeLeftRingHom 𝒜 ℬ, commutes' := ⋯ }
Instances For
@[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)
:
(GradedTensorProduct.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.
Equations
- GradedTensorProduct.includeRight 𝒜 ℬ = AlgHom.ofLinearMap { toFun := fun (b : B) => 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ } ⋯ ⋯
Instances For
@[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)
:
(GradedTensorProduct.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.
Equations
- GradedTensorProduct.lift 𝒜 ℬ f g h_anti_commutes = AlgHom.ofLinearMap (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(GradedTensorProduct.of R 𝒜 ℬ).symm) ⋯ ⋯
Instances For
@[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)
:
(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 ι]
[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]
:
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 ι]
[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 (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 ι]
[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)$.
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 ι]
[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 𝒜 ℬ)
:
(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 ι]
[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))
: