Balanced tensor products with an idempotent ideal

For an idempotent e and an arbitrary element f of a possibly noncommutative k-algebra A, multiplication identifies eA ⊗[A] Af with the corner eAf. The right ideal eA is represented by Ideal.span {op e} in the opposite algebra. The inverse inserts e in the first factor. In particular the tensor product vanishes exactly when the corner vanishes.

This calculation is the middle-factor identification in products of the bimodules Ae ⊗[k] eA used in complexes of projective bimodules.

See Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Section I.4.

def TauCeti.spanSingletonBalancedTensorProductEquivCorner (k : Type u_1) [CommRing k] {A : Type u_2} [Ring A] [Algebra k A] {e f : A} (he : IsIdempotentElem e) : BalancedTensorProduct k A ↥(Ideal.span {MulOpposite.op e}) ↥(Ideal.span {f}) ≃ₗ[k] ↥(cornerSubmodule k e f)

For an idempotent e and arbitrary f, multiplication identifies the balanced tensor product eA ⊗[A] Af with eAf. The first ideal is taken in the opposite algebra to represent its right action.

@[simp]

theorem TauCeti.coe_spanSingletonBalancedTensorProductEquivCorner_tmul (k : Type u_1) [CommRing k] {A : Type u_2} [Ring A] [Algebra k A] {e f : A} (he : IsIdempotentElem e) (m : ↥(Ideal.span {MulOpposite.op e})) (n : ↥(Ideal.span {f})) : ↑((spanSingletonBalancedTensorProductEquivCorner k he) (BalancedTensorProduct.tmul k A m n)) = MulOpposite.unop ↑m * ↑n

On pure tensors the corner identification is multiplication in A.

@[simp]

theorem TauCeti.spanSingletonBalancedTensorProductEquivCorner_symm_apply (k : Type u_1) [CommRing k] {A : Type u_2} [Ring A] [Algebra k A] {e f : A} (he : IsIdempotentElem e) (x : ↥(cornerSubmodule k e f)) : (spanSingletonBalancedTensorProductEquivCorner k he).symm x = BalancedTensorProduct.tmul k A (spanSingletonGenerator (MulOpposite.op e)) ⟨↑x, ⋯⟩

The inverse corner identification inserts the right-ideal generator e.

theorem TauCeti.subsingleton_spanSingleton_balancedTensorProduct_iff_cornerSubmodule_eq_bot (k : Type u_1) [CommRing k] {A : Type u_2} [Ring A] [Algebra k A] {e f : A} (he : IsIdempotentElem e) : Subsingleton (BalancedTensorProduct k A ↥(Ideal.span {MulOpposite.op e}) ↥(Ideal.span {f})) ↔ cornerSubmodule k e f = ⊥

For an idempotent e and arbitrary f, the tensor product eA ⊗[A] Af vanishes exactly when the corner eAf does.