Tensor products over a noncommutative algebra

For a right A-module M and a left A-module N, both modules over a commutative ring k, the balanced tensor product is the quotient of M ⊗[k] N by the relations (m a) ⊗ n - m ⊗ (a n). Right actions are represented by Module Aᵐᵒᵖ M.

The universal property identifies linear maps out of this quotient with balanced k-bilinear maps. Pure tensors, induction, extensionality, and functoriality let consumers work without unfolding the quotient. This is the underlying module construction for tensoring bimodules and differential graded modules. It is not a derived tensor product.

The quotient uses Mathlib's TensorProduct and Submodule.liftQ. The mathematical construction is the ordinary tensor product used in Keller, Deriving DG categories, Section 6.1.

def TauCeti.balancedTensorRelations (k : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] : Submodule k (TensorProduct k M N)

The submodule generated by the relations moving an A action across a tensor.

Equations

• TauCeti.balancedTensorRelations k A M N = Submodule.span k {z : TensorProduct k M N | ∃ (a : A) (m : M) (n : N), z = (MulOpposite.op a • m) ⊗ₜ[k] n - m ⊗ₜ[k] (a • n)}

def TauCeti.BalancedTensorProduct (k : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] : Type (max (max u_4 u_3) u_3 u_4)

The tensor product of a right A-module and a left A-module, balanced over A and linear over k. Compatible scalar actions give the usual algebra-relative tensor product.

Equations

• TauCeti.BalancedTensorProduct k A M N = (TensorProduct k M N ⧸ TauCeti.balancedTensorRelations k A M N)

@[instance_reducible]

instance TauCeti.BalancedTensorProduct.instAddCommGroup (k : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] : AddCommGroup (BalancedTensorProduct k A M N)

Equations

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

@[instance_reducible]

instance TauCeti.BalancedTensorProduct.instModule (k : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] : Module k (BalancedTensorProduct k A M N)

Equations

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

def TauCeti.BalancedTensorProduct.mkQ (k : Type u_1) (A : Type u_2) {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] : TensorProduct k M N →ₗ[k] BalancedTensorProduct k A M N

The quotient map from the tensor product over the ground ring.

Equations

• TauCeti.BalancedTensorProduct.mkQ k A = (TauCeti.balancedTensorRelations k A M N).mkQ

def TauCeti.BalancedTensorProduct.mk (k : Type u_1) (A : Type u_2) {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] : M →ₗ[k] N →ₗ[k] BalancedTensorProduct k A M N

The canonical bilinear map to the balanced tensor product.

Equations

• TauCeti.BalancedTensorProduct.mk k A = (TensorProduct.mk k M N).compr₂ (TauCeti.BalancedTensorProduct.mkQ k A)

def TauCeti.BalancedTensorProduct.tmul (k : Type u_1) (A : Type u_2) {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] (m : M) (n : N) : BalancedTensorProduct k A M N

A pure tensor in the balanced tensor product.

Equations

• TauCeti.BalancedTensorProduct.tmul k A m n = ((TauCeti.BalancedTensorProduct.mk k A) m) n

@[simp]

theorem TauCeti.BalancedTensorProduct.mk_apply (k : Type u_1) (A : Type u_2) {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] (m : M) (n : N) : ((mk k A) m) n = tmul k A m n

@[simp]

theorem TauCeti.BalancedTensorProduct.mkQ_tmul (k : Type u_1) (A : Type u_2) {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] (m : M) (n : N) : (mkQ k A) (m ⊗ₜ[k] n) = tmul k A m n

@[simp]

theorem TauCeti.BalancedTensorProduct.mkQ_eq_zero_iff (k : Type u_1) (A : Type u_2) {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] (z : TensorProduct k M N) : (mkQ k A) z = 0 ↔ z ∈ balancedTensorRelations k A M N

A ground-ring tensor vanishes in the quotient exactly when it lies in the span of balancing relations.

@[simp]

theorem TauCeti.BalancedTensorProduct.zero_tmul (k : Type u_1) (A : Type u_2) {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] (n : N) : tmul k A 0 n = 0

@[simp]

theorem TauCeti.BalancedTensorProduct.tmul_zero (k : Type u_1) (A : Type u_2) {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] (m : M) : tmul k A m 0 = 0

theorem TauCeti.BalancedTensorProduct.add_tmul (k : Type u_1) (A : Type u_2) {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] (m m' : M) (n : N) : tmul k A (m + m') n = tmul k A m n + tmul k A m' n

theorem TauCeti.BalancedTensorProduct.tmul_add (k : Type u_1) (A : Type u_2) {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] (m : M) (n n' : N) : tmul k A m (n + n') = tmul k A m n + tmul k A m n'

@[simp]

theorem TauCeti.BalancedTensorProduct.smul_tmul (k : Type u_1) (A : Type u_2) {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] (r : k) (m : M) (n : N) : tmul k A (r • m) n = r • tmul k A m n

@[simp]

theorem TauCeti.BalancedTensorProduct.tmul_smul (k : Type u_1) (A : Type u_2) {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] (r : k) (m : M) (n : N) : tmul k A m (r • n) = r • tmul k A m n

theorem TauCeti.BalancedTensorProduct.balance (k : Type u_1) (A : Type u_2) {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] (a : A) (m : M) (n : N) : tmul k A (MulOpposite.op a • m) n = tmul k A m (a • n)

An A action can be moved from the right module to the left module.

theorem TauCeti.BalancedTensorProduct.mkQ_surjective (k : Type u_1) (A : Type u_2) {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] : Function.Surjective ⇑(mkQ k A)

Every balanced tensor is represented by a ground-ring tensor.

theorem TauCeti.BalancedTensorProduct.induction_on (k : Type u_1) (A : Type u_2) {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] {P : BalancedTensorProduct k A M N → Prop} (x : BalancedTensorProduct k A M N) (ht : ∀ (m : M) (n : N), P (tmul k A m n)) (ha : ∀ (x y : BalancedTensorProduct k A M N), P x → P y → P (x + y)) : P x

Induction on balanced tensors by pure tensors and addition.

theorem TauCeti.BalancedTensorProduct.hom_ext {k : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] {P : Type u_5} [AddCommGroup P] [Module k P] {f g : BalancedTensorProduct k A M N →ₗ[k] P} (h : ∀ (m : M) (n : N), f (tmul k A m n) = g (tmul k A m n)) : f = g

Linear maps out of a balanced tensor product agree if they agree on pure tensors.

theorem TauCeti.BalancedTensorProduct.hom_ext_iff {k : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] {P : Type u_5} [AddCommGroup P] [Module k P] {f g : BalancedTensorProduct k A M N →ₗ[k] P} : f = g ↔ ∀ (m : M) (n : N), f (tmul k A m n) = g (tmul k A m n)

def TauCeti.BalancedTensorProduct.lift {k : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] {P : Type u_5} [AddCommGroup P] [Module k P] (f : M →ₗ[k] N →ₗ[k] P) (hf : ∀ (a : A) (m : M) (n : N), (f (MulOpposite.op a • m)) n = (f m) (a • n)) : BalancedTensorProduct k A M N →ₗ[k] P

Lift a balanced bilinear map through the tensor product.

Equations

• TauCeti.BalancedTensorProduct.lift f hf = (TauCeti.balancedTensorRelations k A M N).liftQ (TensorProduct.lift f) ⋯

@[simp]

theorem TauCeti.BalancedTensorProduct.lift_tmul {k : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] {P : Type u_5} [AddCommGroup P] [Module k P] (f : M →ₗ[k] N →ₗ[k] P) (hf : ∀ (a : A) (m : M) (n : N), (f (MulOpposite.op a • m)) n = (f m) (a • n)) (m : M) (n : N) : (lift f hf) (tmul k A m n) = (f m) n

def TauCeti.BalancedTensorProduct.liftEquiv {k : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] {P : Type u_5} [AddCommGroup P] [Module k P] : { f : M →ₗ[k] N →ₗ[k] P // ∀ (a : A) (m : M) (n : N), (f (MulOpposite.op a • m)) n = (f m) (a • n) } ≃ (BalancedTensorProduct k A M N →ₗ[k] P)

The universal property: balanced bilinear maps are precisely linear maps out of the balanced tensor product.

Equations

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

@[simp]

theorem TauCeti.BalancedTensorProduct.liftEquiv_apply {k : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] {P : Type u_5} [AddCommGroup P] [Module k P] (f : { f : M →ₗ[k] N →ₗ[k] P // ∀ (a : A) (m : M) (n : N), (f (MulOpposite.op a • m)) n = (f m) (a • n) }) : liftEquiv f = lift ↑f ⋯

@[simp]

theorem TauCeti.BalancedTensorProduct.liftEquiv_symm_apply {k : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] {P : Type u_5} [AddCommGroup P] [Module k P] (g : BalancedTensorProduct k A M N →ₗ[k] P) (m : M) (n : N) : (↑(liftEquiv.symm g) m) n = g (tmul k A m n)

def TauCeti.BalancedTensorProduct.map {k : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] {M' : Type u_6} {N' : Type u_7} [AddCommGroup M'] [Module k M'] [Module Aᵐᵒᵖ M'] [AddCommGroup N'] [Module k N'] [Module A N'] (f : M →ₗ[k] M') (g : N →ₗ[k] N') (hf : ∀ (a : A) (m : M), f (MulOpposite.op a • m) = MulOpposite.op a • f m) (hg : ∀ (a : A) (n : N), g (a • n) = a • g n) : BalancedTensorProduct k A M N →ₗ[k] BalancedTensorProduct k A M' N'

The map induced by equivariant ground-ring linear maps in both factors.

Equations

• TauCeti.BalancedTensorProduct.map f g hf hg = TauCeti.BalancedTensorProduct.lift ((TauCeti.BalancedTensorProduct.mk k A ∘ₗ f).compl₂ g) ⋯

@[simp]

theorem TauCeti.BalancedTensorProduct.map_tmul {k : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] {M' : Type u_6} {N' : Type u_7} [AddCommGroup M'] [Module k M'] [Module Aᵐᵒᵖ M'] [AddCommGroup N'] [Module k N'] [Module A N'] (f : M →ₗ[k] M') (g : N →ₗ[k] N') (hf : ∀ (a : A) (m : M), f (MulOpposite.op a • m) = MulOpposite.op a • f m) (hg : ∀ (a : A) (n : N), g (a • n) = a • g n) (m : M) (n : N) : (map f g hf hg) (tmul k A m n) = tmul k A (f m) (g n)

@[simp]

theorem TauCeti.BalancedTensorProduct.map_id {k : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] : map LinearMap.id LinearMap.id ⋯ ⋯ = LinearMap.id

theorem TauCeti.BalancedTensorProduct.map_comp {k : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] {M' : Type u_6} {N' : Type u_7} {M'' : Type u_8} {N'' : Type u_9} [AddCommGroup M'] [Module k M'] [Module Aᵐᵒᵖ M'] [AddCommGroup N'] [Module k N'] [Module A N'] [AddCommGroup M''] [Module k M''] [Module Aᵐᵒᵖ M''] [AddCommGroup N''] [Module k N''] [Module A N''] (f : M →ₗ[k] M') (g : N →ₗ[k] N') (f' : M' →ₗ[k] M'') (g' : N' →ₗ[k] N'') (hf : ∀ (a : A) (m : M), f (MulOpposite.op a • m) = MulOpposite.op a • f m) (hg : ∀ (a : A) (n : N), g (a • n) = a • g n) (hf' : ∀ (a : A) (m : M'), f' (MulOpposite.op a • m) = MulOpposite.op a • f' m) (hg' : ∀ (a : A) (n : N'), g' (a • n) = a • g' n) : map (f' ∘ₗ f) (g' ∘ₗ g) ⋯ ⋯ = map f' g' hf' hg' ∘ₗ map f g hf hg

Tensoring respects composition of equivariant maps.