Documentation

Mathlib.RingTheory.GradedAlgebra.TensorProduct

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.

source
๐Ÿ”ธ coverage
@[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)
source
๐Ÿ”ธ coverage
@[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))
source
๐Ÿ”ธ coverage
@[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))
source
๐Ÿ“ coverage
@[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
source
๐Ÿ”ธ coverage
@[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))
source
๐Ÿ”ธ coverage
@[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)
source
๐Ÿ“ coverage
@[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
source
๐Ÿ”ธ coverage
@[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))
source
๐Ÿ”ธ coverage
@[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))
source
๐Ÿ”ธ coverage
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.
Instances For
    source
    ๐Ÿ“ coverage
    @[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
    source
    ๐Ÿ“ coverage
    @[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)
    source
    ๐Ÿ”ธ coverage
    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.

    Instances For
      source
      ๐Ÿ“ coverage
      @[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