Documentation

TauCeti.LinearAlgebra.TensorProduct.Balanced.Associator

Associativity of balanced tensor products #

For a right B-module M, a (B,C)-bimodule N, and a left C-module P, the two balanced tensor products (M tensor_B N) tensor_C P and M tensor_B (N tensor_C P) are canonically identified. The map sends a nested pure tensor to the other parenthesization and preserves the two outer actions. It uses the balanced quotient universal property at both stages, rather than assuming that either balancing algebra is commutative. This supplies the carrier associator needed for graded triple braid products and transfer through supplied bimodules.

source
def TauCeti.BalancedTensorProduct.assoc {k : Type u_1} {B : Type u_2} {C : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [CommRing k] [Semiring B] [Semiring C] [AddCommGroup M] [Module k M] [Module Bᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module B N] [Module Cᵐᵒᵖ N] [AddCommGroup P] [Module k P] [Module C P] [SMulCommClass B k N] [SMulCommClass Cᵐᵒᵖ k N] [SMulCommClass B Cᵐᵒᵖ N] :
BalancedTensorProduct k C (BalancedTensorProduct k B M N) P ≃ₗ[k] BalancedTensorProduct k B M (BalancedTensorProduct k C N P)

Reassociate a pair of balanced tensor products through the middle bimodule.

Instances For
    source
    @[simp]
    theorem TauCeti.BalancedTensorProduct.assoc_tmul {k : Type u_1} {B : Type u_2} {C : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [CommRing k] [Semiring B] [Semiring C] [AddCommGroup M] [Module k M] [Module Bᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module B N] [Module Cᵐᵒᵖ N] [AddCommGroup P] [Module k P] [Module C P] [SMulCommClass B k N] [SMulCommClass Cᵐᵒᵖ k N] [SMulCommClass B Cᵐᵒᵖ N] (m : M) (n : N) (p : P) :
    assoc (tmul k C (tmul k B m n) p) = tmul k B m (tmul k C n p)

    The balanced associator changes only the parentheses of a pure tensor.

    source
    @[simp]
    theorem TauCeti.BalancedTensorProduct.assoc_symm_tmul {k : Type u_1} {B : Type u_2} {C : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [CommRing k] [Semiring B] [Semiring C] [AddCommGroup M] [Module k M] [Module Bᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module B N] [Module Cᵐᵒᵖ N] [AddCommGroup P] [Module k P] [Module C P] [SMulCommClass B k N] [SMulCommClass Cᵐᵒᵖ k N] [SMulCommClass B Cᵐᵒᵖ N] (m : M) (n : N) (p : P) :
    assoc.symm (tmul k B m (tmul k C n p)) = tmul k C (tmul k B m n) p

    The inverse balanced associator restores the original parentheses.

    source
    theorem TauCeti.BalancedTensorProduct.assoc_smul_left {k : Type u_1} {B : Type u_2} {C : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [CommRing k] [Semiring B] [Semiring C] [AddCommGroup M] [Module k M] [Module Bᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module B N] [Module Cᵐᵒᵖ N] [AddCommGroup P] [Module k P] [Module C P] [SMulCommClass B k N] [SMulCommClass Cᵐᵒᵖ k N] [SMulCommClass B Cᵐᵒᵖ N] (S : Type u_7) [Semiring S] [Module S M] [SMulCommClass S k M] [SMulCommClass S Bᵐᵒᵖ M] (s : S) (x : BalancedTensorProduct k C (BalancedTensorProduct k B M N) P) :
    let x_1 := leftModule S; have x_2 := ⋯; have x_3 := ⋯; have x_4 := leftModule S; have x_5 := leftModule S; assoc (s • x) = s • assoc x

    The balanced associator preserves any commuting action on its first factor.

    source
    theorem TauCeti.BalancedTensorProduct.assoc_smul_right {k : Type u_1} {B : Type u_2} {C : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [CommRing k] [Semiring B] [Semiring C] [AddCommGroup M] [Module k M] [Module Bᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module B N] [Module Cᵐᵒᵖ N] [AddCommGroup P] [Module k P] [Module C P] [SMulCommClass B k N] [SMulCommClass Cᵐᵒᵖ k N] [SMulCommClass B Cᵐᵒᵖ N] (T : Type u_7) [Semiring T] [Module T P] [SMulCommClass T k P] [SMulCommClass C T P] (s : T) (x : BalancedTensorProduct k C (BalancedTensorProduct k B M N) P) :
    let x_1 := rightModule T; have x_2 := ⋯; have x_3 := ⋯; have x_4 := rightModule T; have x_5 := rightModule T; assoc (s • x) = s • assoc x

    The balanced associator preserves any commuting action on its last factor.

    source
    theorem TauCeti.BalancedTensorProduct.map_map_comp_assoc_eq {k : Type u_1} {B : Type u_2} {C : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [CommRing k] [Semiring B] [Semiring C] [AddCommGroup M] [Module k M] [Module Bᵐᵒᵖ M] [AddCommGroup N] [Module k N] [Module B N] [Module Cᵐᵒᵖ N] [AddCommGroup P] [Module k P] [Module C P] [SMulCommClass B k N] [SMulCommClass Cᵐᵒᵖ k N] [SMulCommClass B Cᵐᵒᵖ N] {M' : Type u_7} {N' : Type u_8} {P' : Type u_9} [AddCommGroup M'] [Module k M'] [Module Bᵐᵒᵖ M'] [AddCommGroup N'] [Module k N'] [Module B N'] [Module Cᵐᵒᵖ N'] [AddCommGroup P'] [Module k P'] [Module C P'] [SMulCommClass B k N'] [SMulCommClass Cᵐᵒᵖ k N'] [SMulCommClass B Cᵐᵒᵖ N'] (f : M →ₗ[k] M') (g : N →ₗ[k] N') (h : P →ₗ[k] P') (hf : ∀ (b : B) (m : M), f (MulOpposite.op b • m) = MulOpposite.op b • f m) (hgB : ∀ (b : B) (n : N), g (b • n) = b • g n) (hgC : ∀ (c : C) (n : N), g (MulOpposite.op c • n) = MulOpposite.op c • g n) (hh : ∀ (c : C) (p : P), h (c • p) = c • h p) :
    map f (map g h hgC hh) hf ⋯ ∘ₗ ↑assoc = ↑assoc ∘ₗ map (map f g hf hgB) h ⋯ hh

    Mapping the three factors commutes with balanced reassociation.