Morita equivalence with the corner ring of a full idempotent #
Let e be an idempotent of a ring A, and let eAe be its corner ring
(IsIdempotentElem.Corner), the ring of elements e * a * e, with unit e. Every A-module M
has a piece eM = e • M (written e • (⊤ : Submodule ℤ M), as in
TauCeti.RingTheory.Idempotents.Module), which is a module over eAe. This defines the
corner functor
IsIdempotentElem.cornerFunctor : ModuleCat A ⥤ ModuleCat eAe, M ↦ eM.
In the other direction, eA is a left eAe-module and a right A-module, so for an
eAe-module N the homomorphisms Hom_{eAe}(eA, N) form an A-module, A acting by right
multiplication on eA. This is the coinduction functor
IsIdempotentElem.cornerCoindFunctor : ModuleCat eAe ⥤ ModuleCat A.
The composite N ↦ e Hom_{eAe}(eA, N) is always isomorphic to the identity, by evaluation at e
(IsIdempotentElem.smulTopCoindEquiv). The other composite M ↦ Hom_{eAe}(eA, eM) receives the
action map m ↦ (x ↦ x • m) (IsIdempotentElem.smulTopActionHom), and this map is bijective as
soon as e is full, that is, generates A as a two-sided ideal, AeA = A: writing
1 = ∑ aᵢ e bᵢ, an element killed by eA is killed by 1, and a homomorphism f : eA → eM is
the action of ∑ aᵢ • f(e bᵢ). So for a full idempotent the two functors are mutually inverse
equivalences (IsIdempotentElem.cornerEquivalence), and the corner functor is linear over any
commutative semiring R over which A is an algebra. This is the Morita equivalence between A
and eAe, in Mathlib's sense (IsIdempotentElem.moritaEquivalenceCorner).
Fullness is the hypothesis that makes the corner ring see every module. It is the hypothesis
used to reduce a finite-dimensional algebra to a basic one: there the idempotent is the sum of
one primitive idempotent for each isomorphism class of simple modules, which is full and has a
basic corner ring. Such an idempotent exists in every semiperfect ring
(TauCeti.IsSemiperfectRing.exists_isIdempotentElem_full_isBasic_corner), which gives the Morita
reduction to a basic ring (TauCeti.IsSemiperfectRing.exists_isBasic_isMoritaEquivalent); both
are in TauCeti.RingTheory.Morita.BasicAlgebra.
Main definitions #
IsIdempotentElem.cornerFunctor: the functorM ↦ eMfromA-modules toeAe-modules.IsIdempotentElem.cornerCoindFunctor: the functorN ↦ Hom_{eAe}(eA, N)back.IsIdempotentElem.cornerEquivalence: for a full idempotent, the two functors form an equivalence of categories.IsIdempotentElem.moritaEquivalenceCorner: for a full idempotent of anR-algebraA, the Morita equivalence betweenAandeAeasR-algebras.
Main results #
IsIdempotentElem.smulTopActionHom_injectiveandIsIdempotentElem.smulTopActionHom_surjective: for a full idempotent, the action mapM → Hom_{eAe}(eA, eM)is bijective.IsIdempotentElem.isMoritaEquivalent_corner: a ring is Morita equivalent to the corner ring of any full idempotent.
Implementation notes #
The inverse functor is built from homomorphisms out of eA rather than from the tensor product
Ae ⊗_{eAe} N, which would need tensor products over the noncommutative ring eAe. The two
functors are given @[expose] so that their objects can be read as the pieces eM and the spaces
of homomorphisms Hom_{eAe}(eA, N), on which the action lemmas of this file are stated. The
equivalence is built with CategoryTheory.Equivalence.mk', so that its unit and counit are exactly
IsIdempotentElem.cornerUnitIso and IsIdempotentElem.cornerCounitIso, and is given @[expose]
so that this identification can be stated. The types of the unit and counit depend on the
equivalence's functor and inverse: without exposure, the public statements of
IsIdempotentElem.cornerEquivalence_unitIso and IsIdempotentElem.cornerEquivalence_counitIso
cannot identify those types with the ones of the supplied natural isomorphisms. The functor and
inverse projection equalities alone do not supply this definitional equality during elaboration.
References #
- T. Y. Lam, Lectures on Modules and Rings, Graduate Texts in Mathematics 189, §18 (Morita theory, full idempotents).
- I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Section I.6 (basic algebras).
The bimodule eA #
The idempotent e, as an element of the piece eA of the regular module.
Instances For
Homomorphisms out of eA as an A-module #
A acts on Hom_{eAe}(eA, N) through right multiplication on eA.
Hom_{eAe}(eA, N) is an A-module, A acting by right multiplication on eA.
The two functors #
The corner functor M ↦ eM, from modules over A to modules over the corner ring
eAe.
Instances For
The coinduction functor N ↦ Hom_{eAe}(eA, N), from modules over the corner ring eAe
to modules over A.
Instances For
The counit: e Hom_{eAe}(eA, N) ≅ N #
Evaluation at e identifies e Hom_{eAe}(eA, N) with N, for every idempotent e. The
inverse sends n to the homomorphism x ↦ (x * e) • n.
Instances For
The unit: M ≅ Hom_{eAe}(eA, eM) for a full idempotent #
For a full idempotent e, an element of an A-module killed by eA is zero.
For a full idempotent e, every homomorphism eA → eM of modules over the corner ring is the
action of an element of M.
The equivalence #
The counit of the corner equivalence, e Hom_{eAe}(eA, N) ≅ N, natural in N.
Instances For
The unit of the corner equivalence, M ≅ Hom_{eAe}(eA, eM), natural in M, for a full
idempotent e.
Instances For
A full idempotent e makes the module categories of A and of its corner ring eAe
equivalent: the corner functor M ↦ eM is an equivalence, with inverse
N ↦ Hom_{eAe}(eA, N), unit IsIdempotentElem.cornerUnitIso and counit
IsIdempotentElem.cornerCounitIso.
Instances For
The corner functor is linear over any commutative semiring R over which A is an algebra.
Morita equivalence with the corner ring of a full idempotent: for a full idempotent e
of an R-algebra A, the corner functor M ↦ eM is an R-linear equivalence between the
module categories of A and of eAe.
Instances For
A ring is Morita equivalent to the corner ring of any full idempotent.