Outer actions on balanced tensor products

An action on either factor which commutes with the balancing action descends to the balanced tensor product. Actions on opposite factors commute. These are the outer actions on the tensor product of bimodules. They carry no Koszul sign: the left action acts on the first factor and the right action on the second factor without crossing a tensor factor.

The module structures are explicit definitions rather than global instances, since a scalar ring acting on both factors can give two different actions on the quotient.

References

• B. Keller, Deriving DG categories, Section 6.1.

@[instance_reducible]

def TauCeti.BalancedTensorProduct.leftModule {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] (S : Type u_5) [Semiring S] [Module S M] [SMulCommClass S k M] [SMulCommClass S Aᵐᵒᵖ M] : Module S (BalancedTensorProduct k A M N)

The module structure induced by the outer action on the first factor.

@[simp]

theorem TauCeti.BalancedTensorProduct.smul_tmul_left {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] (S : Type u_5) [Semiring S] [Module S M] [SMulCommClass S k M] [SMulCommClass S Aᵐᵒᵖ M] (s : S) (m : M) (n : N) : s • tmul k A m n = tmul k A (s • m) n

An outer left action applies to the first factor of a pure tensor.

theorem TauCeti.BalancedTensorProduct.leftSMulCommClass {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] (S : Type u_5) [Semiring S] [Module S M] [SMulCommClass S k M] [SMulCommClass S Aᵐᵒᵖ M] : SMulCommClass S k (BalancedTensorProduct k A M N)

The outer left action commutes with the ground-ring action.

theorem TauCeti.BalancedTensorProduct.leftIsScalarTower {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] (S : Type u_5) [Semiring S] [Module S M] [SMulCommClass S k M] [SMulCommClass S Aᵐᵒᵖ M] [SMul k S] [IsScalarTower k S M] : IsScalarTower k S (BalancedTensorProduct k A M N)

Compatibility of the outer left action with restriction to the ground ring.

theorem TauCeti.BalancedTensorProduct.map_smul_left {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] (S : Type u_5) [Semiring S] [Module S M] [SMulCommClass S k M] [SMulCommClass S Aᵐᵒᵖ M] {M' : Type u_6} {N' : Type u_7} [AddCommGroup M'] [Module k M'] [Module Aᵐᵒᵖ M'] [Module S M'] [SMulCommClass S k M'] [SMulCommClass S 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) (hfs : ∀ (s : S) (m : M), f (s • m) = s • f m) (s : S) (z : BalancedTensorProduct k A M N) : (map f g hf hg) (s • z) = s • (map f g hf hg) z

Tensoring a map equivariant for the outer left action remains equivariant.

theorem TauCeti.BalancedTensorProduct.congr_smul_left {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] (S : Type u_5) [Semiring S] [Module S M] [SMulCommClass S k M] [SMulCommClass S Aᵐᵒᵖ M] {M' : Type u_6} {N' : Type u_7} [AddCommGroup M'] [Module k M'] [Module Aᵐᵒᵖ M'] [Module S M'] [SMulCommClass S k M'] [SMulCommClass S 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) (hfs : ∀ (s : S) (m : M), f (s • m) = s • f m) (s : S) (z : BalancedTensorProduct k A M N) : (congr f g hf hg) (s • z) = s • (congr f g hf hg) z

Tensor congruence respects an outer left action when the first equivalence does.

@[simp]

theorem TauCeti.BalancedTensorProduct.lift_smul_left {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] (S : Type u_5) [Semiring S] [Module S M] [SMulCommClass S k M] [SMulCommClass S Aᵐᵒᵖ M] {P : Type u_6} [AddCommGroup P] [Module k P] [Module S P] (f : M →ₗ[k] N →ₗ[k] P) (hf : ∀ (a : A) (m : M) (n : N), (f (MulOpposite.op a • m)) n = (f m) (a • n)) (hfs : ∀ (s : S) (m : M) (n : N), (f (s • m)) n = s • (f m) n) (s : S) (z : BalancedTensorProduct k A M N) : (lift f hf) (s • z) = s • (lift f hf) z

A balanced bilinear map equivariant in the first factor induces a left-equivariant map.

@[instance_reducible]

def TauCeti.BalancedTensorProduct.rightModule {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] (T : Type u_5) [Semiring T] [Module T N] [SMulCommClass T k N] [SMulCommClass A T N] : Module T (BalancedTensorProduct k A M N)

The module structure induced by the outer action on the second factor.

@[simp]

theorem TauCeti.BalancedTensorProduct.smul_tmul_right {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] (T : Type u_5) [Semiring T] [Module T N] [SMulCommClass T k N] [SMulCommClass A T N] (t : T) (m : M) (n : N) : t • tmul k A m n = tmul k A m (t • n)

An outer right action applies to the second factor of a pure tensor.

theorem TauCeti.BalancedTensorProduct.rightSMulCommClass {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] (T : Type u_5) [Semiring T] [Module T N] [SMulCommClass T k N] [SMulCommClass A T N] : SMulCommClass T k (BalancedTensorProduct k A M N)

The outer right action commutes with the ground-ring action.

theorem TauCeti.BalancedTensorProduct.rightIsScalarTower {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] (T : Type u_5) [Semiring T] [Module T N] [SMulCommClass T k N] [SMulCommClass A T N] [SMul k T] [IsScalarTower k T N] : IsScalarTower k T (BalancedTensorProduct k A M N)

Compatibility of the outer right action with restriction to the ground ring.

theorem TauCeti.BalancedTensorProduct.map_smul_right {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] (T : Type u_5) [Semiring T] [Module T N] [SMulCommClass T k N] [SMulCommClass A T 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'] [Module T N'] [SMulCommClass T k N'] [SMulCommClass A T 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) (hgt : ∀ (t : T) (n : N), g (t • n) = t • g n) (t : T) (z : BalancedTensorProduct k A M N) : (map f g hf hg) (t • z) = t • (map f g hf hg) z

Tensoring a map equivariant for the outer right action remains equivariant.

theorem TauCeti.BalancedTensorProduct.congr_smul_right {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] (T : Type u_5) [Semiring T] [Module T N] [SMulCommClass T k N] [SMulCommClass A T 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'] [Module T N'] [SMulCommClass T k N'] [SMulCommClass A T 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) (hgt : ∀ (t : T) (n : N), g (t • n) = t • g n) (t : T) (z : BalancedTensorProduct k A M N) : (congr f g hf hg) (t • z) = t • (congr f g hf hg) z

Tensor congruence respects an outer right action when the second equivalence does.

@[simp]

theorem TauCeti.BalancedTensorProduct.lift_smul_right {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] (T : Type u_5) [Semiring T] [Module T N] [SMulCommClass T k N] [SMulCommClass A T N] {P : Type u_6} [AddCommGroup P] [Module k P] [Module T P] (f : M →ₗ[k] N →ₗ[k] P) (hf : ∀ (a : A) (m : M) (n : N), (f (MulOpposite.op a • m)) n = (f m) (a • n)) (hfs : ∀ (s : T) (m : M) (n : N), (f m) (s • n) = s • (f m) n) (s : T) (z : BalancedTensorProduct k A M N) : (lift f hf) (s • z) = s • (lift f hf) z

A balanced bilinear map equivariant in the second factor induces a right-equivariant map.

theorem TauCeti.BalancedTensorProduct.outerSMulCommClass {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] (S : Type u_5) (T : Type u_6) [Semiring S] [Semiring T] [Module S M] [Module T N] [SMulCommClass S k M] [SMulCommClass T k N] [SMulCommClass S Aᵐᵒᵖ M] [SMulCommClass A T N] : SMulCommClass S T (BalancedTensorProduct k A M N)

Actions on different factors of a balanced tensor product commute.

theorem TauCeti.BalancedTensorProduct.gradedSMul_left {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 A] {𝒜 : ℤ → Submodule k A} [DirectSum.Decomposition 𝒜] (G : InternalGrading k M ℤ) (H : InternalGrading k N ℤ) [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) (G.piece ℤ)] [SetLike.GradedSMul 𝒜 (H.piece ℤ)] (S : Type u_5) [Semiring S] [Module k S] [Module S M] [SMulCommClass S k M] [SMulCommClass S Aᵐᵒᵖ M] (𝒮 : ℤ → Submodule k S) [SetLike.GradedSMul 𝒮 (G.piece ℤ)] : SetLike.GradedSMul 𝒮 ((grading G H).piece ℤ)

A graded outer action on the first factor adds degrees on the balanced tensor product.

theorem TauCeti.BalancedTensorProduct.gradedSMul_right {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 A] {𝒜 : ℤ → Submodule k A} [DirectSum.Decomposition 𝒜] (G : InternalGrading k M ℤ) (H : InternalGrading k N ℤ) [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) (G.piece ℤ)] [SetLike.GradedSMul 𝒜 (H.piece ℤ)] (T : Type u_5) [Semiring T] [Module k T] [Module T N] [SMulCommClass T k N] [SMulCommClass A T N] (𝒯 : ℤ → Submodule k T) [SetLike.GradedSMul 𝒯 (H.piece ℤ)] : SetLike.GradedSMul 𝒯 ((grading G H).piece ℤ)

A graded outer action on the second factor adds degrees on the balanced tensor product.

theorem TauCeti.BalancedTensorProduct.ext_threefold {k : Type u_5} {B : Type u_6} {C : Type u_7} {M : Type u_8} {N : Type u_9} {P : Type u_10} [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 Cᵐᵒᵖ k N] [SMulCommClass B Cᵐᵒᵖ N] {Q : Type u_11} [AddCommGroup Q] [Module k Q] {f g : BalancedTensorProduct k C (BalancedTensorProduct k B M N) P →ₗ[k] Q} (h : ∀ (m : M) (n : N) (p : P), f (tmul k C (tmul k B m n) p) = g (tmul k C (tmul k B m n) p)) : f = g

Linear maps out of a left-associated triple balanced tensor product are determined by their values on nested pure tensors.

theorem TauCeti.BalancedTensorProduct.ext_fourfold {k : Type u_5} {B : Type u_6} {C : Type u_7} {M : Type u_8} {N : Type u_9} {P : Type u_10} [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 Cᵐᵒᵖ k N] [SMulCommClass B Cᵐᵒᵖ N] {D : Type u_11} {Q : Type u_12} [Semiring D] [Module Dᵐᵒᵖ P] [SMulCommClass Dᵐᵒᵖ k P] [SMulCommClass C Dᵐᵒᵖ P] [AddCommGroup Q] [Module k Q] [Module D Q] {T : Type u_13} [AddCommGroup T] [Module k T] {f g : BalancedTensorProduct k D (BalancedTensorProduct k C (BalancedTensorProduct k B M N) P) Q →ₗ[k] T} (h : ∀ (m : M) (n : N) (p : P) (q : Q), f (tmul k D (tmul k C (tmul k B m n) p) q) = g (tmul k D (tmul k C (tmul k B m n) p) q)) : f = g

Linear maps out of a left-associated fourfold balanced tensor product are determined by their values on nested pure tensors.