GradedTensorProduct.tmul_coe_mul_coe_tmul
theorem GradedTensorProduct.tmul_coe_mul_coe_tmul :
∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι]
[inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι] [inst_3 : CommRing R] [inst_4 : Ring A]
[inst_5 : Ring B] [inst_6 : Algebra R A] [inst_7 : Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B)
[inst_8 : GradedAlgebra 𝒜] [inst_9 : 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₂)
This theorem, called `GradedTensorProduct.tmul_coe_mul_coe_tmul`, describes the multiplication operation on partially homogenous elements in the context of graded tensor products. Specifically, for any commutative semiring `ι`, a module structure of `ι` over non-zero integers `ℤˣ`, and graded algebra structures induced by `ι` on rings `A` and `B` over a commutative ring `R`, the multiplication of two elements `a₁ ᵍ⊗ₜ[R] ↑b₁` and `↑a₂ ᵍ⊗ₜ[R] b₂` in the graded tensor product is equal to `(-1) ^ (j₁ * i₂)` times the tensor product of `a₁ * ↑a₂` and `↑b₁ * b₂`. Here `a₁` and `a₂` are elements of ring `A`, `b₁` is a homogenous element of the `j₁`th graded component of ring `B`, and `b₂` is an element of ring `B`, where `j₁` and `i₂` are elements of `ι`.
More concisely: Given commutative semirings ι, module structures of ι over ℤˣ, and graded algebra structures over a commutative ring R on rings A and B, the multiplication of homogenous elements a₁⊗ₜ[R] ua₁ in the graded tensor product of A and B is equal to (-1) ^ (j₁ * i₂) * (a₁ * ua₂)⊗ₜ[R] (ub₁ * b₂), where a₁ is in A, ub₁ is the homogeneous component of degree j₁ in B, and i₂ is in ι.
|
GradedTensorProduct.tmul_coe_mul_zero_coe_tmul
theorem GradedTensorProduct.tmul_coe_mul_zero_coe_tmul :
∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι]
[inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι] [inst_3 : CommRing R] [inst_4 : Ring A]
[inst_5 : Ring B] [inst_6 : Algebra R A] [inst_7 : Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B)
[inst_8 : GradedAlgebra 𝒜] [inst_9 : GradedAlgebra ℬ] {j₁ : ι} (a₁ : A) (b₁ : ↥(ℬ j₁)) (a₂ : ↥(𝒜 0)) (b₂ : B),
a₁ ᵍ⊗ₜ[R] ↑b₁ * ↑a₂ ᵍ⊗ₜ[R] b₂ = (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)
The theorem `GradedTensorProduct.tmul_coe_mul_zero_coe_tmul` states that for any commutative semiring over some type `ι`, a module over `ι` and the additive group of integers, a decidable equality on `ι`, and a commutative ring `R`. Given ring structures on types `A` and `B`, and `A` and `B` are algebras over `R`. Furthermore, given grade structures `𝒜` and `ℬ` on `A` and `B` respectively, if `a₁` is an element of `A`, `b₁` is an element of grade `j₁` in `ℬ`, `a₂` is an element of grade `0` in `𝒜`, and `b₂` is an element of `B`. Then, the tensor product of `a₁` and `b₁`, multiplied by the tensor product of `a₂` and `b₂`, is equal to the tensor product of the product of `a₁` and `a₂`, and the product of `b₁` and `b₂`.
More concisely: For commutative semirings ι, modules over ι and additive groups of integers, decideable equality on ι, commutative ring R, ringed algebras A and B over R with grade structures 𝒜 and ℬ respectively, if a₁ is of grade j₁ in ℬ, a₂ is of grade 0 in 𝒜, then a₁ ⊗ b₁ ⊗ a₂ ⊗ b₂ = (a₁ ⊗ a₂) ⊗ (b₁ ⊗ b₂).
|
GradedTensorProduct.tmul_zero_coe_mul_coe_tmul
theorem GradedTensorProduct.tmul_zero_coe_mul_coe_tmul :
∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι]
[inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι] [inst_3 : CommRing R] [inst_4 : Ring A]
[inst_5 : Ring B] [inst_6 : Algebra R A] [inst_7 : Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B)
[inst_8 : GradedAlgebra 𝒜] [inst_9 : GradedAlgebra ℬ] {i₂ : ι} (a₁ : A) (b₁ : ↥(ℬ 0)) (a₂ : ↥(𝒜 i₂)) (b₂ : B),
a₁ ᵍ⊗ₜ[R] ↑b₁ * ↑a₂ ᵍ⊗ₜ[R] b₂ = (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)
The theorem `GradedTensorProduct.tmul_zero_coe_mul_coe_tmul` states a specific case for graded tensor products in the context of graded algebras. Given that `R` is a Commutative Ring, `A` and `B` are Rings, `ι` is a Commutative Semiring, `ℤˣ` is the multiplicative group of integers that are units under multiplication, `𝒜` and `ℬ` are functions from `ι` to submodules of `A` and `B` respectively, and both `𝒜` and `ℬ` have the graded algebra structure, the theorem asserts that for any elements `a₁` from `A`, `b₁` from the 0-th grade of `ℬ`, `a₂` from the `i₂`-th grade of `𝒜`, and `b₂` from `B`, the graded tensor product of `a₁` with `b₁` times the graded tensor product of `a₂` with `b₂` equals the graded tensor product of the product of `a₁` and `a₂` with the product of `b₁` and `b₂`.
More concisely: For commutative rings R, graded algebras 𝒜 and ℬ over R with functions ι -> submodules, and elements a₁ from A, b₁ from the 0-th grade of ℬ, a₂ from the i₂-th grade of 𝒜, and b₂ from B, the graded tensor product of a₁ with b₁ ⊗₁ R a₂ with b₂ equals the graded tensor product of a₁ * a₂ with b₁ ⊗₁ R b₂.
|
GradedTensorProduct.hom_ext
theorem GradedTensorProduct.hom_ext :
∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
[inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
(𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
{M : Type u_5} [inst_9 : AddCommMonoid M] [inst_10 : Module R M] ⦃f g : GradedTensorProduct R 𝒜 ℬ →ₗ[R] M⦄,
f ∘ₗ ↑(GradedTensorProduct.of R 𝒜 ℬ) = g ∘ₗ ↑(GradedTensorProduct.of R 𝒜 ℬ) → f = g
This theorem, `GradedTensorProduct.hom_ext`, asserts that for any types `R`, `ι`, `A`, `B` and `M`, with `R` a commutative ring, `ι` a commutative semiring with decidable equality, `A` and `B` being rings and `R`-algebras, and `M` being an `R`-module, along with maps `𝒜` and `ℬ` from `ι` to the submodules of `A` and `B` respectively such that there are graded algebra structures on `𝒜` and `ℬ`, if we have two `R`-linear maps `f` and `g` from the graded tensor product of `R`, `𝒜` and `ℬ` to `M`, and these maps agree when composed with the inclusion of the underlying tensor product into the graded tensor product, then `f` and `g` are equal. Essentially, it's saying that two linear maps from the graded tensor product are the same if they coincide on the underlying tensor product.
More concisely: Given commutative rings R, ι, rings and R-algebras A, B over a commutative semiring ι with decidable equality, an R-module M, graded algebra structures on the maps 𝒜 from ι to the submodules of A and ℬ from ι to the submodules of B, and R-linear maps f and g from the graded tensor product of R, 𝒜, and ℬ to M that agree on the underlying tensor product, then f = g.
|
GradedTensorProduct.algHom_ext
theorem GradedTensorProduct.algHom_ext :
∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι]
[inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι] [inst_3 : CommRing R] [inst_4 : Ring A]
[inst_5 : Ring B] [inst_6 : Algebra R A] [inst_7 : Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B)
[inst_8 : GradedAlgebra 𝒜] [inst_9 : GradedAlgebra ℬ] {C : Type u_5} [inst_10 : Ring C] [inst_11 : Algebra R C]
⦃f g : GradedTensorProduct R 𝒜 ℬ →ₐ[R] C⦄,
f.comp (GradedTensorProduct.includeLeft 𝒜 ℬ) = g.comp (GradedTensorProduct.includeLeft 𝒜 ℬ) →
f.comp (GradedTensorProduct.includeRight 𝒜 ℬ) = g.comp (GradedTensorProduct.includeRight 𝒜 ℬ) → f = g
This theorem, named `GradedTensorProduct.algHom_ext`, states that given two algebra morphisms `f` and `g` from the graded tensor product of two graded algebras `𝒜` and `ℬ` to another algebra `C`, if the compositions of `f` and `g` with the left and right inclusions of the graded tensor product are equivalent respectively, then `f` and `g` must be the same. In other words, the theorem provides a condition under which two algebra morphisms from the graded tensor product of two graded algebras can be considered equal. Here, all involved algebraic structures are over a commutative ring `R`, and `ι` serves as the index set for the gradings, which itself is a commutative semiring and a module over the additive group of integers.
More concisely: Given two algebra homomorphisms from the graded tensor product of two graded R-algebras to an algebra, if their compositions with the left and right inclusions are equivalent, then they are equal.
|