Documentation

TauCeti.LinearAlgebra.TensorProduct.Balanced.Unit

Unit identifications for balanced tensor products #

Tensoring a module with the regular bimodule over a noncommutative algebra returns the original module. The identifications send a ⊗ n to a • n and m ⊗ a to m a. Their inverses insert 1. These are the unit identifications for composition of bimodules, before introducing gradings or differentials. A semiring algebra over k can use these identifications by installing Algebra.semiringToRing k locally.

The construction follows the ordinary tensor product underlying Keller, Deriving DG categories, Section 6.1. Scalar actions use Mathlib's Algebra.lsmul.

source
noncomputable def TauCeti.BalancedTensorProduct.lid (k : Type u_1) (A : Type u_2) [CommRing k] [Ring A] [Algebra k A] (N : Type u_3) [AddCommGroup N] [Module k N] [Module A N] [IsScalarTower k A N] :
BalancedTensorProduct k A A N ≃ₗ[k] N

Tensoring the regular right module with a left module evaluates the left action.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.BalancedTensorProduct.lid_tmul (k : Type u_1) (A : Type u_2) [CommRing k] [Ring A] [Algebra k A] (N : Type u_3) [AddCommGroup N] [Module k N] [Module A N] [IsScalarTower k A N] (a : A) (n : N) :
    (lid k A N) (tmul k A a n) = a • n
    source
    @[simp]
    theorem TauCeti.BalancedTensorProduct.lid_symm_apply (k : Type u_1) (A : Type u_2) [CommRing k] [Ring A] [Algebra k A] (N : Type u_3) [AddCommGroup N] [Module k N] [Module A N] [IsScalarTower k A N] (n : N) :
    (lid k A N).symm n = tmul k A 1 n
    source
    noncomputable def TauCeti.BalancedTensorProduct.rid (k : Type u_1) (A : Type u_2) [CommRing k] [Ring A] [Algebra k A] (M : Type u_3) [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [IsScalarTower k Aᵐᵒᵖ M] :
    BalancedTensorProduct k A M A ≃ₗ[k] M

    Tensoring a right module with the regular left module evaluates the right action.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.BalancedTensorProduct.rid_tmul (k : Type u_1) (A : Type u_2) [CommRing k] [Ring A] [Algebra k A] (M : Type u_3) [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [IsScalarTower k Aᵐᵒᵖ M] (m : M) (a : A) :
      (rid k A M) (tmul k A m a) = MulOpposite.op a • m
      source
      @[simp]
      theorem TauCeti.BalancedTensorProduct.rid_symm_apply (k : Type u_1) (A : Type u_2) [CommRing k] [Ring A] [Algebra k A] (M : Type u_3) [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [IsScalarTower k Aᵐᵒᵖ M] (m : M) :
      (rid k A M).symm m = tmul k A m 1