Tensor products of idempotent left ideals

For idempotents e and f in ground-ring algebras A and B, Ae ⊗ Bf is the left ideal generated by e ⊗ f in A ⊗ B. The identification uses the split projections onto the two ideals and TensorProduct.map; it needs no flatness assumption.

This relates the cyclic enveloping-algebra presentation of the zigzag vertex bimodule to its two outer factors. It lets the full balanced self-tensor calculation reuse BalancedTensorProduct.outerFactors and the middle corner identification before constructing inverse braid homotopy equivalences.

See Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Section I.4, for the idempotent-ideal description of projective modules.

theorem IsIdempotentElem.tmul {k : Type u_4} {A : Type u_5} {B : Type u_6} [CommSemiring k] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] {e : A} {f : B} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) : IsIdempotentElem (e ⊗ₜ[k] f)

A pure tensor of idempotents is idempotent in the tensor product.

def TauCeti.spanSingletonTensorProductEquiv (k : Type u_1) [CommSemiring k] {A : Type u_2} {B : Type u_3} [Semiring A] [Semiring B] [Algebra k A] [Algebra k B] {e : A} {f : B} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) : TensorProduct k ↥(Ideal.span {e}) ↥(Ideal.span {f}) ≃ₗ[k] ↥(Ideal.span {e ⊗ₜ[k] f})

The tensor of two idempotent left ideals is the ideal generated by their pure tensor. The equivalence is ground-linear, and its forward map is the tensor of the inclusions.

@[simp]

theorem TauCeti.coe_spanSingletonTensorProductEquiv_apply (k : Type u_1) [CommSemiring k] {A : Type u_2} {B : Type u_3} [Semiring A] [Semiring B] [Algebra k A] [Algebra k B] {e : A} {f : B} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) (t : TensorProduct k ↥(Ideal.span {e}) ↥(Ideal.span {f})) : ↑((spanSingletonTensorProductEquiv k he hf) t) = (TensorProduct.map (↑k (Submodule.subtype (Ideal.span {e}))) (↑k (Submodule.subtype (Ideal.span {f})))) t

The forward map is the tensor product of the two ideal inclusions.

@[simp]

theorem TauCeti.spanSingletonTensorProductEquiv_symm_tmul_smul_generator (k : Type u_1) [CommSemiring k] {A : Type u_2} {B : Type u_3} [Semiring A] [Semiring B] [Algebra k A] [Algebra k B] {e : A} {f : B} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) (a : A) (b : B) : (spanSingletonTensorProductEquiv k he hf).symm (a ⊗ₜ[k] b • spanSingletonGenerator (e ⊗ₜ[k] f)) = (a • spanSingletonGenerator e) ⊗ₜ[k] (b • spanSingletonGenerator f)

The inverse sends a scaled tensor generator to the tensor of the scaled generators.

@[simp]

theorem TauCeti.spanSingletonTensorProductEquiv_map_smul (k : Type u_1) [CommSemiring k] {A : Type u_2} {B : Type u_3} [Semiring A] [Semiring B] [Algebra k A] [Algebra k B] {e : A} {f : B} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) (a : A) (b : B) (t : TensorProduct k ↥(Ideal.span {e}) ↥(Ideal.span {f})) : (spanSingletonTensorProductEquiv k he hf) ((TensorProduct.map ((Algebra.lsmul k k ↥(Ideal.span {e})) a) ((Algebra.lsmul k k ↥(Ideal.span {f})) b)) t) = a ⊗ₜ[k] b • (spanSingletonTensorProductEquiv k he hf) t

The identification carries the two factor actions to the tensor-algebra action.