Extracting outer factors from a balanced tensor product

For a right A-module M, a left A-module N, and ground-ring modules L, P, there is a canonical identification

(M ⊗[k] L) ⊗[A] (N ⊗[k] P) ≃ (M ⊗[A] N) ⊗[k] (L ⊗[k] P).

Here the displayed A-tensor products mean BalancedTensorProduct. The A actions on the ground-ring tensor products act on their first factors, as in Mathlib. The identification isolates the middle balanced factor in compositions of bimodules of the form L ⊗[k] M and N ⊗[k] P: first commute the factors of the first ground-ring tensor product. In particular, a vanishing middle factor makes the whole tensor product vanish.

We descend Mathlib's TensorProduct.tensorTensorTensorComm using the balanced universal property. This is an ordinary module identification, with no flatness assumption; it does not assert a derived tensor comparison. The tensor composition convention follows Keller, Deriving DG categories, Section 6.1.

def TauCeti.BalancedTensorProduct.outerFactors (k : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) (L : Type u_5) (P : Type u_6) [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [SMulCommClass k Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] [SMulCommClass k A N] [AddCommGroup L] [Module k L] [AddCommGroup P] [Module k P] : BalancedTensorProduct k A (TensorProduct k M L) (TensorProduct k N P) ≃ₗ[k] TensorProduct k (BalancedTensorProduct k A M N) (TensorProduct k L P)

Extract the two ground-ring factors on which the balancing algebra does not act. The actions on M ⊗ L and N ⊗ P are Mathlib's first-factor actions.

@[simp]

theorem TauCeti.BalancedTensorProduct.outerFactors_tmul (k : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) (L : Type u_5) (P : Type u_6) [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [SMulCommClass k Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] [SMulCommClass k A N] [AddCommGroup L] [Module k L] [AddCommGroup P] [Module k P] (m : M) (n : N) (l : L) (p : P) : (outerFactors k A M N L P) (tmul k A (m ⊗ₜ[k] l) (n ⊗ₜ[k] p)) = tmul k A m n ⊗ₜ[k] (l ⊗ₜ[k] p)

On pure tensors, outerFactors separates the balanced factors m, n from the ground-ring factors l, p.

@[simp]

theorem TauCeti.BalancedTensorProduct.outerFactors_symm_tmul (k : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) (L : Type u_5) (P : Type u_6) [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [SMulCommClass k Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] [SMulCommClass k A N] [AddCommGroup L] [Module k L] [AddCommGroup P] [Module k P] (m : M) (n : N) (l : L) (p : P) : (outerFactors k A M N L P).symm (tmul k A m n ⊗ₜ[k] (l ⊗ₜ[k] p)) = tmul k A (m ⊗ₜ[k] l) (n ⊗ₜ[k] p)

On pure tensors, the inverse of outerFactors reinserts the ground-ring factors l, p into the two arguments of the balanced tensor product.

theorem TauCeti.BalancedTensorProduct.outerFactors_map (k : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) (L : Type u_5) (P : Type u_6) [CommRing k] [Semiring A] [AddCommGroup M] [Module k M] [Module Aᵐᵒᵖ M] [SMulCommClass k Aᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module A N] [SMulCommClass k A N] [AddCommGroup L] [Module k L] [AddCommGroup P] [Module k P] {M' : Type u_7} {N' : Type u_8} {L' : Type u_9} {P' : Type u_10} [AddCommGroup M'] [Module k M'] [Module Aᵐᵒᵖ M'] [SMulCommClass k Aᵐᵒᵖ M'] [AddCommGroup N'] [Module k N'] [Module A N'] [SMulCommClass k A N'] [AddCommGroup L'] [Module k L'] [AddCommGroup P'] [Module k P'] (f : M →ₗ[k] M') (g : N →ₗ[k] N') (l : L →ₗ[k] L') (p : P →ₗ[k] P') (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) : ↑(outerFactors k A M' N' L' P') ∘ₗ map (TensorProduct.map f l) (TensorProduct.map g p) ⋯ ⋯ = TensorProduct.map (map f g hf hg) (TensorProduct.map l p) ∘ₗ ↑(outerFactors k A M N L P)

Extracting outer factors commutes with tensoring equivariant maps in the acted factors and arbitrary linear maps in the two ground-ring factors.