Tensor product of graded algebra

In this file we show that if 𝒜 is a graded R-algebra, and S is any R-algebra, then S ⊗[R] 𝒜 is a graded S-algebra with the grading fun i ↦ (𝒜 i).baseChange S.

Implementation notes

We need to provide the shortcut instances afterwards for the grade zero because it is expensive to deduce via unification the function fun i ↦ (𝒜 i).baseChange S.

@[implicit_reducible]

instance GradedAlgebra.baseChange {ι : Type u_1} {R : Type u_2} {A : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] [Algebra R S] [DecidableEq ι] [AddMonoid ι] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] : GradedAlgebra fun (i : ι) => Submodule.baseChange S (𝒜 i)

Equations

• GradedAlgebra.baseChange 𝒜 = { toGradedMonoid := ⋯, toDecomposition := DirectSum.Decomposition.baseChange 𝒜 }

@[implicit_reducible]

instance GradedAlgebra.instSemiringSubtypeTensorProductMemSubmoduleBaseChangeOfNat {ι : Type u_1} {R : Type u_2} {A : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] [Algebra R S] [DecidableEq ι] [AddMonoid ι] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] : Semiring ↥(Submodule.baseChange S (𝒜 0))

Equations

• GradedAlgebra.instSemiringSubtypeTensorProductMemSubmoduleBaseChangeOfNat 𝒜 = SetLike.GradeZero.instSemiring fun (i : ι) => Submodule.baseChange S (𝒜 i)

@[implicit_reducible]

instance GradedAlgebra.instAlgebraSubtypeTensorProductMemSubmoduleBaseChangeOfNat {ι : Type u_1} {R : Type u_2} {A : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] [Algebra R S] [DecidableEq ι] [AddMonoid ι] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] : Algebra S ↥(Submodule.baseChange S (𝒜 0))

Equations

• GradedAlgebra.instAlgebraSubtypeTensorProductMemSubmoduleBaseChangeOfNat 𝒜 = SetLike.GradeZero.instAlgebra fun (i : ι) => Submodule.baseChange S (𝒜 i)

@[simp]

theorem GradedAlgebra.coe_algebraMap_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] [Algebra R S] [DecidableEq ι] [AddMonoid ι] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (s : S) : ↑((algebraMap S ↥(Submodule.baseChange S (𝒜 0))) s) = s ⊗ₜ[R] 1

@[implicit_reducible]

instance GradedAlgebra.instCommSemiringSubtypeTensorProductMemSubmoduleBaseChangeOfNat {ι : Type u_1} {R : Type u_2} {A : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] [Algebra R S] [DecidableEq ι] [AddMonoid ι] [CommSemiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] : CommSemiring ↥(Submodule.baseChange S (𝒜 0))

Equations

• GradedAlgebra.instCommSemiringSubtypeTensorProductMemSubmoduleBaseChangeOfNat 𝒜 = SetLike.GradeZero.instCommSemiring fun (i : ι) => Submodule.baseChange S (𝒜 i)

@[implicit_reducible]

instance GradedAlgebra.instAlgebraSubtypeTensorProductMemSubmoduleBaseChangeOfNat_1 {ι : Type u_1} {R : Type u_2} {A : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] [Algebra R S] [DecidableEq ι] [AddCommMonoid ι] [CommSemiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] : Algebra (↥(Submodule.baseChange S (𝒜 0))) (TensorProduct R S A)

Equations

• GradedAlgebra.instAlgebraSubtypeTensorProductMemSubmoduleBaseChangeOfNat_1 𝒜 = SetLike.GradeZero.instAlgebraSubtypeMemOfNat fun (i : ι) => Submodule.baseChange S (𝒜 i)

@[simp]

theorem GradedAlgebra.algebraMap_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] [Algebra R S] [DecidableEq ι] [AddCommMonoid ι] [CommSemiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] (x : ↥(Submodule.baseChange S (𝒜 0))) : (algebraMap (↥(Submodule.baseChange S (𝒜 0))) (TensorProduct R S A)) x = ↑x

@[implicit_reducible]

instance GradedAlgebra.instRingSubtypeTensorProductMemSubmoduleBaseChangeOfNat {ι : Type u_1} {R : Type u_2} {A : Type u_3} {S : Type u_4} [CommSemiring R] [CommRing S] [Algebra R S] [DecidableEq ι] [AddMonoid ι] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] : Ring ↥(Submodule.baseChange S (𝒜 0))

Equations

• GradedAlgebra.instRingSubtypeTensorProductMemSubmoduleBaseChangeOfNat 𝒜 = SetLike.GradeZero.instRing fun (i : ι) => Submodule.baseChange S (𝒜 i)

@[implicit_reducible]

instance GradedAlgebra.instCommRingSubtypeTensorProductMemSubmoduleBaseChangeOfNat {ι : Type u_1} {R : Type u_2} {A : Type u_3} {S : Type u_4} [CommSemiring R] [CommRing S] [Algebra R S] [DecidableEq ι] [AddCommMonoid ι] [CommSemiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] : CommRing ↥(Submodule.baseChange S (𝒜 0))

Equations

• GradedAlgebra.instCommRingSubtypeTensorProductMemSubmoduleBaseChangeOfNat 𝒜 = SetLike.GradeZero.instCommRing fun (i : ι) => Submodule.baseChange S (𝒜 i)

def GradedAlgHom.liftEquiv {ι : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R A] [Algebra S B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule S B) [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Algebra R S] [Algebra R B] [IsScalarTower R S B] : (𝒜 →ₐᵍ[R] fun (x : ι) => Submodule.restrictScalars R (ℬ x)) ≃ ((fun (x : ι) => Submodule.baseChange S (𝒜 x)) →ₐᵍ[S] ℬ)

A map from the base change of a graded algebra is the same as a map to the scalar restriction.

In category-theoretical terms, this is an adjunction between:

1. 𝒜 ↦ (𝒜 · |>.baseChange S), a functor from Graded R-Algebra to Graded S-Algebra; and:
2. ℬ ↦ (ℬ · |>.restrictScalars R), a functor from Graded S-Algebra to Graded R-Algebra.

Equations

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

@[simp]

theorem GradedAlgHom.liftEquiv_tmul {ι : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R A] [Algebra S B] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule S B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Algebra R S] [Algebra R B] [IsScalarTower R S B] (f : 𝒜 →ₐᵍ[R] fun (x : ι) => Submodule.restrictScalars R (ℬ x)) (r : S) (x : A) : ((liftEquiv 𝒜 ℬ) f) (r ⊗ₜ[R] x) = r • f x

@[simp]

theorem GradedAlgHom.liftEquiv_symm_apply {ι : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R A] [Algebra S B] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule S B} [GradedAlgebra 𝒜] [GradedAlgebra ℬ] [Algebra R S] [Algebra R B] [IsScalarTower R S B] (f : (fun (x : ι) => Submodule.baseChange S (𝒜 x)) →ₐᵍ[S] ℬ) (x : A) : ((liftEquiv 𝒜 ℬ).symm f) x = f (1 ⊗ₜ[R] x)

def GradedAlgHom.includeRight {ι : Type u_1} {R : Type u_2} (S : Type u_3) {A : Type u_4} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜] [Algebra R S] : 𝒜 →ₐᵍ[R] fun (x : ι) => Submodule.restrictScalars R (Submodule.baseChange S (𝒜 x))

Graded version of Algebra.TensorProduct.includeRight, i.e. the inclusion from a graded R-algebra 𝒜 to its base change to S and then restricted back to R. (The restriction does not change the actual sets).

In categorical terms, this is the unit of the adjunction GradedAlgHom.liftEquiv.

Equations

• GradedAlgHom.includeRight S 𝒜 = { toAlgHom := Algebra.TensorProduct.includeRight, map_mem := ⋯ }

@[simp]

theorem GradedAlgHom.includeRight_apply {ι : Type u_1} {R : Type u_2} (S : Type u_3) {A : Type u_4} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R A] {𝒜 : ι → Submodule R A} [GradedAlgebra 𝒜] [Algebra R S] (x : A) : (includeRight S 𝒜) x = 1 ⊗ₜ[R] x