Theorems · Theorem · ring theory

TensorProduct.gradedMul_def

∀ (R : Type u_5) {ι : Type u_6} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_7) (ℬ : ι → Type u_8) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)]
  [inst_8 : DirectSum.GRing 𝒜] [inst_9 : DirectSum.GRing ℬ] [inst_10 : DirectSum.GAlgebra R 𝒜]
  [inst_11 : DirectSum.GAlgebra R ℬ],
  TensorProduct.gradedMul R 𝒜 ℬ =
    TensorProduct.curry
      (TensorProduct.map (LinearMap.mul' R (DirectSum ι fun i => 𝒜 i)) (LinearMap.mul' R (DirectSum ι fun i => ℬ i)) ∘ₗ
        ↑(TensorProduct.assoc R (DirectSum ι fun i => 𝒜 i) (DirectSum ι fun i => 𝒜 i)
                (TensorProduct R (DirectSum ι fun i => ℬ i) (DirectSum ι fun i => ℬ i))).symm ∘ₗ
          LinearMap.lTensor (DirectSum ι fun i => 𝒜 i)
              (↑(TensorProduct.assoc R (DirectSum ι fun i => 𝒜 i) (DirectSum ι fun i => ℬ i)
                    (DirectSum ι fun i => ℬ i)) ∘ₗ
                LinearMap.rTensor (DirectSum ι fun i => ℬ i) ↑(TensorProduct.gradedComm R ℬ 𝒜) ∘ₗ
                  ↑(TensorProduct.assoc R (DirectSum ι ℬ) (DirectSum ι 𝒜) (DirectSum ι ℬ)).symm) ∘ₗ
            ↑(TensorProduct.assoc R (DirectSum ι 𝒜) (DirectSum ι ℬ) (TensorProduct R (DirectSum ι 𝒜) (DirectSum ι ℬ))))

Defined in

Mathlib.LinearAlgebra.TensorProduct.Graded.External

Cited by

1 results in Mathlib

Foundations

Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringModuleDecidableEqCommRingAddCommGroupAddCommGroupModuleModuleDirectSum.GRingDirectSum.GRingDirectSum.GAlgebraDirectSum.GAlgebra