Homomorphisms between the left ideals generated by two idempotents

Let A be an algebra over a commutative semiring k and let e and f be idempotents of A. The left ideals Ae and Af are the modules an idempotent decomposition of 1 cuts the regular module into, and this file identifies the homomorphisms between two of them:

Hom_A(Ae, Af) ≅ eAf, by φ ↦ φ e.

The corner eAf is defined in TauCeti.RingTheory.Idempotents.Corner as the range of the k-linear map x ↦ e x f. When e and f are idempotent, the identification here is k-linear.

Both directions are elementary. A homomorphism φ out of Ae is right multiplication by φ e (TauCeti.coe_apply_eq_mul_apply_generator, proved for an arbitrary target ideal), which therefore determines it; and φ e lies in eAf because e is fixed by e on the left and every element of Af is fixed by f on the right. Conversely right multiplication by an element of eAf is a homomorphism Ae → Af.

Specializing to f = e recovers the dictionary between the corner ring eAe and End (Ae) which TauCeti.RingTheory.Idempotents.Primitive.Basic uses to compare primitivity of e with indecomposability of Ae; the point of the two-idempotent version is that it computes the graded homomorphism spaces between the indecomposable projectives of a graded algebra with a distinguished family of idempotents, since the corner inherits the grading of A.

Main definitions

• TauCeti.cornerToSpanSingletonHom: right multiplication by an element of eAf, as a homomorphism Ae → Af.

Main results

• TauCeti.spanSingletonHomEquivCorner: the dictionary Hom_A(Ae, Af) ≃ₗ[k] eAf.
• TauCeti.coe_apply_eq_mul_apply_generator: a homomorphism out of Ae is right multiplication by its value at e.

References

This is the general input to the graded homomorphism spaces of Layer 3 of TauCetiRoadmap/ZigzagPreprojective/README.md. See I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Section I.4.

The dictionary

theorem TauCeti.mem_span_singleton_of_mem_cornerSubmodule {k : Type v} [CommSemiring k] {A : Type u} [Semiring A] [Algebra k A] {e f x : A} (hf : IsIdempotentElem f) (hx : x ∈ cornerSubmodule k e f) : x ∈ Ideal.span {f}

An element of the corner eAf is fixed by f on the right, hence lies in the left ideal Af.

theorem TauCeti.apply_generator_mem_cornerSubmodule {k : Type v} [CommSemiring k] {A : Type u} [Semiring A] [Algebra k A] {e f : A} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) (φ : ↥(Ideal.span {e}) →ₗ[A] ↥(Ideal.span {f})) : ↑(φ (spanSingletonGenerator e)) ∈ cornerSubmodule k e f

The value at the generator of a homomorphism Ae → Af lies in the corner eAf.

def TauCeti.cornerToSpanSingletonHom {k : Type v} [CommSemiring k] {A : Type u} [Semiring A] [Algebra k A] {e f : A} (hf : IsIdempotentElem f) (x : ↥(cornerSubmodule k e f)) : ↥(Ideal.span {e}) →ₗ[A] ↥(Ideal.span {f})

Right multiplication by an element of the corner eAf, as a homomorphism Ae → Af.

Equations

• TauCeti.cornerToSpanSingletonHom hf x = { toFun := fun (y : ↥(Ideal.span {e})) => ⟨↑y * ↑x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.coe_cornerToSpanSingletonHom_apply {k : Type v} [CommSemiring k] {A : Type u} [Semiring A] [Algebra k A] {e f : A} (hf : IsIdempotentElem f) (x : ↥(cornerSubmodule k e f)) (y : ↥(Ideal.span {e})) : ↑((cornerToSpanSingletonHom hf x) y) = ↑y * ↑x

def TauCeti.spanSingletonHomEquivCorner {k : Type v} [CommSemiring k] {A : Type u} [Semiring A] [Algebra k A] {e f : A} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) : (↥(Ideal.span {e}) →ₗ[A] ↥(Ideal.span {f})) ≃ₗ[k] ↥(cornerSubmodule k e f)

The homomorphisms from Ae to Af are the corner eAf, by evaluation at the generator e. The inverse sends an element of the corner to right multiplication by it.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.coe_spanSingletonHomEquivCorner_apply {k : Type v} [CommSemiring k] {A : Type u} [Semiring A] [Algebra k A] {e f : A} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) (φ : ↥(Ideal.span {e}) →ₗ[A] ↥(Ideal.span {f})) : ↑((spanSingletonHomEquivCorner he hf) φ) = ↑(φ (spanSingletonGenerator e))

@[simp]

theorem TauCeti.coe_spanSingletonHomEquivCorner_symm_apply {k : Type v} [CommSemiring k] {A : Type u} [Semiring A] [Algebra k A] {e f : A} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) (x : ↥(cornerSubmodule k e f)) (y : ↥(Ideal.span {e})) : ↑(((spanSingletonHomEquivCorner he hf).symm x) y) = ↑y * ↑x