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 ofA
andB
that form a graded algebra, this is a type alias forA ⊗[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 forGradedTensorProduct R 𝒜 ℬ
.a ᵍ⊗ₜ b
is 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.
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
Equations
- GradedTensorProduct.instAddCommGroupWithOne 𝒜 ℬ = Algebra.TensorProduct.instAddCommGroupWithOne
Equations
- GradedTensorProduct.instModule 𝒜 ℬ = TensorProduct.leftModule
The casting equivalence to move between regular and graded tensor products.
Equations
- GradedTensorProduct.of R 𝒜 ℬ = LinearEquiv.refl R (TensorProduct R A B)
Instances For
Two linear maps from the graded tensor product agree if they agree on the underlying tensor product.
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
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
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
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 }
Equations
- GradedTensorProduct.instMonoid 𝒜 ℬ = Monoid.mk ⋯ ⋯ npowRec ⋯ ⋯
Equations
- GradedTensorProduct.instRing 𝒜 ℬ = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
The characterization of this multiplication on partially homogeneous elements.
A special case for when b₁
has grade 0.
A special case for when a₂
has grade 0.
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
Equations
- GradedTensorProduct.instAlgebra 𝒜 ℬ = Algebra.mk ((GradedTensorProduct.includeLeftRingHom 𝒜 ℬ).comp (algebraMap R A)) ⋯ ⋯
The algebra morphism A →ₐ[R] A ⊗[R] B
sending a
to a ⊗ₜ 1
.
Equations
- GradedTensorProduct.includeLeft 𝒜 ℬ = { toRingHom := GradedTensorProduct.includeLeftRingHom 𝒜 ℬ, commutes' := ⋯ }
Instances For
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
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
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
Two algebra morphism from the graded tensor product agree if their compositions with the left and right inclusions agree.
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.