Corners cut out by two idempotents

Let A be a nonunital algebra over a semiring k: a nonunital semiring with a k-module structure whose scalar multiplication commutes with multiplication on either side. This file defines the corner eAf as the range of Mathlib's LinearMap.mulLeftRight k (e, f), the 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 semiring structure even when A has no unit, and a ring structure when A is a nonunital ring. The corner inherits the compatible scalar action and module structure of A. Over a commutative semiring R, this makes it an R-algebra, with algebraMap R eAe r = r • e. When A is unital, this is the structure under which eAe can be compared with A as R-algebras, for instance through Mathlib's MoritaEquivalence.

Main definitions

• TauCeti.cornerSubmodule: the corner eAf, as a k-submodule of A.
• IsIdempotentElem.compress: the compression x ↦ e * x * e of A onto the corner ring eAe.
• IsIdempotentElem.Corner.instAlgebra: the corner eAe of an idempotent of a nonunital R-algebra is a unital R-algebra.
• IsIdempotentElem.cornerFunctional: the compression x ↦ φ x / φ e of a linear functional φ to the corner eAe, normalised at its unit e.
• IsIdempotentElem.cornerLinearEquivCornerSubmodule: the corner ring eAe, as an R-module, agrees with the corner submodule TauCeti.cornerSubmodule R e e.
• IsIdempotentElem.cornerMap: a homomorphism of nonunital semirings restricts to a unital homomorphism of corners; a surjective homomorphism remains surjective on corners.
• IsIdempotentElem.cornerEquiv: a ring equivalence restricts to an equivalence of corners.
• IsIdempotentElem.cornerPiEquiv: the corner of an idempotent in a product of rings is the product of the corners of its components.
• IsIdempotentElem.isNoetherian_corner: the corner of a Noetherian algebra is Noetherian, so the corner of a finite-dimensional algebra is finite-dimensional.

Main results

• TauCeti.mem_cornerSubmodule_iff: the fixed-point characterization of an idempotent corner.
• TauCeti.mem_span_singleton_of_mem_cornerSubmodule: the corner eAf lies in the left ideal Af without idempotency assumptions.
• IsIdempotentElem.mul_corner_val and IsIdempotentElem.corner_val_mul: an element of the corner ring eAe is fixed by e on both sides.
• IsIdempotentElem.val_list_prod_map_compress: a product of compressions in eAe is e (x₁ e) ⋯ (xₙ e) in A.
• Pi.isIdempotentElem_iff: an element of a product is idempotent exactly when each component is.

References

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

def TauCeti.cornerSubmodule (k : Type v) [Semiring k] {A : Type u} [NonUnitalSemiring A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A 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.

theorem TauCeti.cornerSubmodule_def (k : Type v) [Semiring k] {A : Type u} [NonUnitalSemiring A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] (e f : A) : cornerSubmodule k e f = (LinearMap.mulLeftRight k (e, f)).range

The corner submodule is the range of the corner map.

theorem TauCeti.mul_mul_mem_cornerSubmodule (k : Type v) [Semiring k] {A : Type u} [NonUnitalSemiring A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] (e f x : A) : e * x * f ∈ cornerSubmodule k e f

Cutting an element down by e on the left and f on the right lands in the corner eAf.

@[simp]

theorem TauCeti.mem_cornerSubmodule_iff (k : Type v) [Semiring k] {A : Type u} [NonUnitalSemiring A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A 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} [Semiring k] {A : Type u} [NonUnitalSemiring A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A 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} [Semiring k] {A : Type u} [NonUnitalSemiring A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A 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.

theorem TauCeti.mem_span_singleton_of_mem_cornerSubmodule {k : Type v} [Semiring k] {A : Type u} [Semiring A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] {e f x : A} (hx : x ∈ cornerSubmodule k e f) : x ∈ Ideal.span {f}

An element of the corner eAf lies in the left ideal Af, without any idempotency assumption.

The corner ring as an algebra

@[simp]

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

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

@[simp]

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

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

def IsIdempotentElem.compress {A : Type u} [Semigroup A] {e : A} (he : IsIdempotentElem e) (x : A) : he.Corner

The compression x ↦ e * x * e of A onto the corner eAe.

@[simp]

theorem IsIdempotentElem.val_compress {A : Type u} [Semigroup A] {e : A} (he : IsIdempotentElem e) (x : A) : ↑(he.compress x) = e * x * e

@[simp]

theorem IsIdempotentElem.compress_val {A : Type u} [Semigroup A] {e : A} (he : IsIdempotentElem e) (b : he.Corner) : he.compress ↑b = b

The compression fixes the elements of the corner.

@[instance_reducible]

instance IsIdempotentElem.Corner.instSMul {A : Type u} [Semigroup A] {e : A} {he : IsIdempotentElem e} {R : Type v} [SMul R A] [SMulCommClass R A A] [IsScalarTower R A A] : SMul R he.Corner

A scalar action compatible with multiplication restricts to the corner.

@[simp]

theorem IsIdempotentElem.Corner.val_smul {A : Type u} [Semigroup A] {e : A} {he : IsIdempotentElem e} {R : Type v} [SMul R A] [SMulCommClass R A A] [IsScalarTower R A A] (r : R) (b : he.Corner) : ↑(r • b) = r • ↑b

@[simp]

theorem IsIdempotentElem.compress_smul {A : Type u} [Semigroup A] {e : A} (he : IsIdempotentElem e) {R : Type v} [SMul R A] [SMulCommClass R A A] [IsScalarTower R A A] (r : R) (x : A) : he.compress (r • x) = r • he.compress x

@[simp]

theorem IsIdempotentElem.Corner.val_one {A : Type u} [NonUnitalSemiring 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} [NonUnitalSemiring A] {e : A} {he : IsIdempotentElem e} (b c : he.Corner) : ↑(b * c) = ↑b * ↑c

@[simp]

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

@[simp]

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

@[instance_reducible]

instance IsIdempotentElem.Corner.instModule {A : Type u} [NonUnitalSemiring A] {e : A} {he : IsIdempotentElem e} {R : Type v} [Semiring R] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] : Module R he.Corner

The corner inherits the module structure of the ambient nonunital algebra.

@[simp]

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

@[simp]

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

@[instance_reducible]

instance IsIdempotentElem.Corner.instAlgebra {A : Type u} [NonUnitalSemiring A] {e : A} {he : IsIdempotentElem e} {R : Type v} [CommSemiring R] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] : Algebra R he.Corner

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

@[simp]

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

@[simp]

theorem IsIdempotentElem.compress_zero {A : Type u} [NonUnitalSemiring A] {e : A} (he : IsIdempotentElem e) : he.compress 0 = 0

@[simp]

theorem IsIdempotentElem.compress_add {A : Type u} [NonUnitalSemiring A] {e : A} (he : IsIdempotentElem e) (x y : A) : he.compress (x + y) = he.compress x + he.compress y

theorem IsIdempotentElem.val_list_prod_map_compress {A : Type u} [Semiring A] {e : A} (he : IsIdempotentElem e) (l : List A) : ↑(List.map he.compress l).prod = e * (List.map (fun (x : A) => x * e) l).prod

The product in the corner eAe of the compressions e xᵢ e of a list x₁, …, xₙ is e (x₁ e) ⋯ (xₙ e).

def IsIdempotentElem.cornerFunctional {A : Type u} [NonUnitalSemiring A] {e : A} (he : IsIdempotentElem e) {R : Type v} [Semifield R] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (φ : A →ₗ[R] R) : he.Corner →ₗ[R] R

The compression of a linear functional φ to the corner eAe of an idempotent e, normalised at the unit e of the corner: x ↦ φ x / φ e. When φ e ≠ 0 it takes the value 1 at the unit (IsIdempotentElem.cornerFunctional_one).

@[simp]

theorem IsIdempotentElem.cornerFunctional_apply {A : Type u} [NonUnitalSemiring A] {e : A} (he : IsIdempotentElem e) {R : Type v} [Semifield R] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (φ : A →ₗ[R] R) (x : he.Corner) : (he.cornerFunctional φ) x = (φ e)⁻¹ * φ ↑x

theorem IsIdempotentElem.cornerFunctional_one {A : Type u} [NonUnitalSemiring A] {e : A} (he : IsIdempotentElem e) {R : Type v} [Semifield R] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {φ : A →ₗ[R] R} (hφe : φ e ≠ 0) : (he.cornerFunctional φ) 1 = 1

The compression of φ to the corner eAe is normalised when φ e ≠ 0.

def IsIdempotentElem.cornerMap {A : Type u_1} {B : Type u_2} [NonUnitalSemiring A] [NonUnitalSemiring B] {e : A} (he : IsIdempotentElem e) (f : A →ₙ+* B) : he.Corner →+* ⋯.Corner

A nonunital homomorphism restricts to a unital homomorphism between idempotent corners. The unit in the source is e, and the unit in the target is its image.

@[simp]

theorem IsIdempotentElem.val_cornerMap {A : Type u_1} {B : Type u_2} [NonUnitalSemiring A] [NonUnitalSemiring B] {e : A} (he : IsIdempotentElem e) (f : A →ₙ+* B) (x : he.Corner) : ↑((he.cornerMap f) x) = f ↑x

theorem IsIdempotentElem.cornerMap_surjective {A : Type u_1} {B : Type u_2} [NonUnitalSemiring A] [NonUnitalSemiring B] {e : A} (he : IsIdempotentElem e) (f : A →ₙ+* B) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(he.cornerMap f)

A surjective homomorphism is surjective on every idempotent corner.

def IsIdempotentElem.cornerEquiv {A : Type u_1} {B : Type u_2} [NonUnitalSemiring A] [NonUnitalSemiring B] {e : A} (he : IsIdempotentElem e) (f : A ≃+* B) : he.Corner ≃+* ⋯.Corner

A ring equivalence restricts to an equivalence between the corner eAe and the corner of the image of e.

@[simp]

theorem IsIdempotentElem.val_cornerEquiv_apply {A : Type u_1} {B : Type u_2} [NonUnitalSemiring A] [NonUnitalSemiring B] {e : A} (he : IsIdempotentElem e) (f : A ≃+* B) (x : he.Corner) : ↑((he.cornerEquiv f) x) = f ↑x

@[simp]

theorem IsIdempotentElem.val_cornerEquiv_symm_apply {A : Type u_1} {B : Type u_2} [NonUnitalSemiring A] [NonUnitalSemiring B] {e : A} (he : IsIdempotentElem e) (f : A ≃+* B) (y : ⋯.Corner) : ↑((he.cornerEquiv f).symm y) = f.symm ↑y

@[simp]

theorem Pi.isIdempotentElem_iff {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → Mul (A i)] {e : (i : ι) → A i} : IsIdempotentElem e ↔ ∀ (i : ι), IsIdempotentElem (e i)

An element of a product is idempotent exactly when each of its components is.

def IsIdempotentElem.cornerPiEquiv {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → NonUnitalSemiring (A i)] {e : (i : ι) → A i} (he : IsIdempotentElem e) : he.Corner ≃+* ((i : ι) → ⋯.Corner)

The corner of an idempotent in a product is the product of the corners of its components.

@[simp]

theorem IsIdempotentElem.val_cornerPiEquiv_apply {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → NonUnitalSemiring (A i)] {e : (i : ι) → A i} (he : IsIdempotentElem e) (x : he.Corner) (i : ι) : ↑(he.cornerPiEquiv x i) = ↑x i

@[simp]

theorem IsIdempotentElem.val_cornerPiEquiv_symm_apply {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → NonUnitalSemiring (A i)] {e : (i : ι) → A i} (he : IsIdempotentElem e) (y : (i : ι) → ⋯.Corner) : ↑(he.cornerPiEquiv.symm y) = fun (i : ι) => ↑(y i)

theorem IsIdempotentElem.coe_corner_eq_cornerSubmodule {A : Type u} [NonUnitalSemiring A] {R : Type v} [Semiring R] [Module R A] [SMulCommClass R A A] [IsScalarTower R A 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} [NonUnitalSemiring A] {e : A} (he : IsIdempotentElem e) {R : Type v} [Semiring R] [Module R A] [SMulCommClass R A A] [IsScalarTower R A 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.

@[simp]

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

@[simp]

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

instance IsIdempotentElem.isNoetherian_corner {A : Type u} [NonUnitalSemiring A] {e : A} (he : IsIdempotentElem e) {R : Type v} [Semiring R] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [IsNoetherian R A] : IsNoetherian R he.Corner

The corner of a Noetherian algebra is Noetherian: if A is a Noetherian R-module, so is eAe, a submodule of A. In particular the corner of a finite-dimensional algebra is finite-dimensional.