Corners cut out by two idempotents

Let A be an algebra over a commutative semiring k. This file defines the corner eAf as the range of the k-linear map x ↦ e * x * f. When e and f are idempotent, membership is equivalent to the fixed-point equation e * x * f = x.

The second part concerns Mathlib's corner ring IsIdempotentElem.Corner of an idempotent e, the ring eAe with unit e. Mathlib gives it a ring structure; when A is an algebra over a commutative semiring R, this file makes it an R-algebra, with algebraMap R eAe r = r • e. This is the structure under which eAe can be compared with A as R-algebras, for instance through Mathlib's MoritaEquivalence.

Main definitions

• TauCeti.cornerMap: the k-linear map x ↦ e * x * f.
• TauCeti.cornerSubmodule: the corner eAf, as a k-submodule of A.
• IsIdempotentElem.Corner.instAlgebra: the corner ring eAe of an idempotent of an R-algebra is an R-algebra.
• IsIdempotentElem.cornerLinearEquivCornerSubmodule: the corner ring eAe, as an R-module, agrees with the corner submodule TauCeti.cornerSubmodule R e e.

Main results

• TauCeti.mem_cornerSubmodule_iff: the fixed-point characterization of an idempotent corner.
• IsIdempotentElem.mul_corner_val and IsIdempotentElem.corner_val_mul: an element of the corner ring eAe is fixed by e on both sides.

References

This is the corner infrastructure used by 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.

def TauCeti.cornerMap (k : Type v) [CommSemiring k] {A : Type u} [Semiring A] [Algebra k A] (e f : A) : A →ₗ[k] A

Cutting an element of A down to the corner at (e, f): multiplying it by e on the left and by f on the right.

Equations

• TauCeti.cornerMap k e f = LinearMap.mulLeft k e ∘ₗ LinearMap.mulRight k f

@[simp]

theorem TauCeti.cornerMap_apply (k : Type v) [CommSemiring k] {A : Type u} [Semiring A] [Algebra k A] (e f x : A) : (cornerMap k e f) x = e * x * f

def TauCeti.cornerSubmodule (k : Type v) [CommSemiring k] {A : Type u} [Semiring A] [Algebra k A] (e f : A) : Submodule k A

The corner eAf, as a k-submodule of A: the range of the map x ↦ e * x * f.

Equations

• TauCeti.cornerSubmodule k e f = (TauCeti.cornerMap k e f).range

theorem TauCeti.cornerSubmodule_def (k : Type v) [CommSemiring k] {A : Type u} [Semiring A] [Algebra k A] (e f : A) : cornerSubmodule k e f = (cornerMap k e f).range

The corner submodule is the range of the corner map.

@[simp]

theorem TauCeti.mem_cornerSubmodule_iff (k : Type v) [CommSemiring k] {A : Type u} [Semiring A] [Algebra k A] {e f x : A} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) : x ∈ cornerSubmodule k e f ↔ e * x * f = x

For idempotents e and f, an element belongs to the corner eAf exactly when multiplying it by e on the left and by f on the right fixes it.

theorem TauCeti.mul_eq_self_of_mem_cornerSubmodule {k : Type v} [CommSemiring k] {A : Type u} [Semiring A] [Algebra k A] {e f x : A} (he : IsIdempotentElem e) (hx : x ∈ cornerSubmodule k e f) : e * x = x

An element of the corner eAf is fixed by e on the left.

theorem TauCeti.mul_eq_self_of_mem_cornerSubmodule_right {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 * f = x

An element of the corner eAf is fixed by f on the right.

The corner ring as an algebra

@[simp]

theorem IsIdempotentElem.mul_corner_val {A : Type u} [Semiring A] {e : A} (he : IsIdempotentElem e) (b : he.Corner) : e * ↑b = ↑b

An element of the corner ring eAe is fixed by e on the left.

@[simp]

theorem IsIdempotentElem.corner_val_mul {A : Type u} [Semiring A] {e : A} (he : IsIdempotentElem e) (b : he.Corner) : ↑b * e = ↑b

An element of the corner ring eAe is fixed by e on the right.

@[simp]

theorem IsIdempotentElem.Corner.val_one {A : Type u} [Semiring A] {e : A} {he : IsIdempotentElem e} : ↑1 = e

The unit of the corner ring eAe is e.

@[simp]

theorem IsIdempotentElem.Corner.val_mul {A : Type u} [Semiring A] {e : A} {he : IsIdempotentElem e} (b c : he.Corner) : ↑(b * c) = ↑b * ↑c

@[simp]

theorem IsIdempotentElem.Corner.val_zero {A : Type u} [Semiring A] {e : A} {he : IsIdempotentElem e} : ↑0 = 0

@[simp]

theorem IsIdempotentElem.Corner.val_add {A : Type u} [Semiring A] {e : A} {he : IsIdempotentElem e} (b c : he.Corner) : ↑(b + c) = ↑b + ↑c

@[simp]

theorem IsIdempotentElem.Corner.val_neg {A : Type u} [Ring A] {e : A} {he : IsIdempotentElem e} (b : he.Corner) : ↑(-b) = -↑b

@[simp]

theorem IsIdempotentElem.Corner.val_sub {A : Type u} [Ring A] {e : A} {he : IsIdempotentElem e} (b c : he.Corner) : ↑(b - c) = ↑b - ↑c

@[instance_reducible]

instance IsIdempotentElem.Corner.instSMul {A : Type u} [Semiring A] {e : A} {he : IsIdempotentElem e} {R : Type v} [CommSemiring R] [Algebra R A] : SMul R he.Corner

Equations

• IsIdempotentElem.Corner.instSMul = { smul := fun (r : R) (b : he.Corner) => ⟨r • ↑b, ⋯⟩ }

@[simp]

theorem IsIdempotentElem.Corner.val_smul {A : Type u} [Semiring A] {e : A} {he : IsIdempotentElem e} {R : Type v} [CommSemiring R] [Algebra R A] (r : R) (b : he.Corner) : ↑(r • b) = r • ↑b

@[instance_reducible]

instance IsIdempotentElem.Corner.instModule {A : Type u} [Semiring A] {e : A} {he : IsIdempotentElem e} {R : Type v} [CommSemiring R] [Algebra R A] : Module R he.Corner

Equations

• IsIdempotentElem.Corner.instModule = Function.Injective.module R { toFun := fun (b : he.Corner) => ↑b, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

@[instance_reducible]

instance IsIdempotentElem.Corner.instAlgebra {A : Type u} [Semiring A] {e : A} {he : IsIdempotentElem e} {R : Type v} [CommSemiring R] [Algebra R A] : Algebra R he.Corner

The corner ring eAe of an idempotent of an R-algebra is an R-algebra, with algebraMap R eAe r = r • e.

Equations

• IsIdempotentElem.Corner.instAlgebra = Algebra.ofModule' ⋯ ⋯

@[simp]

theorem IsIdempotentElem.Corner.val_algebraMap {A : Type u} [Semiring A] {e : A} {he : IsIdempotentElem e} {R : Type v} [CommSemiring R] [Algebra R A] (r : R) : ↑((algebraMap R he.Corner) r) = r • e

theorem IsIdempotentElem.coe_corner_eq_cornerSubmodule {A : Type u} [Semiring A] {R : Type v} [CommSemiring R] [Algebra R A] (e : A) : ↑(Subsemigroup.corner e) = ↑(TauCeti.cornerSubmodule R e e)

The carrier of the corner ring eAe is the corner submodule TauCeti.cornerSubmodule R e e: both are the range of x ↦ e * x * e.

def IsIdempotentElem.cornerLinearEquivCornerSubmodule {A : Type u} [Semiring A] {e : A} (he : IsIdempotentElem e) {R : Type v} [CommSemiring R] [Algebra R A] : he.Corner ≃ₗ[R] ↥(TauCeti.cornerSubmodule R e e)

The corner ring eAe, as an R-module, is the corner submodule TauCeti.cornerSubmodule R e e.

Equations

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

@[simp]

theorem IsIdempotentElem.coe_cornerLinearEquivCornerSubmodule_apply {A : Type u} [Semiring A] {e : A} (he : IsIdempotentElem e) {R : Type v} [CommSemiring R] [Algebra R A] (b : he.Corner) : ↑(he.cornerLinearEquivCornerSubmodule b) = ↑b

@[simp]

theorem IsIdempotentElem.val_cornerLinearEquivCornerSubmodule_symm_apply {A : Type u} [Semiring A] {e : A} (he : IsIdempotentElem e) {R : Type v} [CommSemiring R] [Algebra R A] (x : ↥(TauCeti.cornerSubmodule R e e)) : ↑(he.cornerLinearEquivCornerSubmodule.symm x) = ↑x