Sets generating the unit two-sided ideal

A subset s of an associative ring generates the unit two-sided ideal, TwoSidedIdeal.span s = ⊤, exactly when 1 is a finite sum of products a * x * b with x ∈ s. For a single idempotent e this is the condition that e is full, the hypothesis under which the corner ring eRe is Morita equivalent to R.

This file records how the condition behaves under the operations used to build full idempotents: it is carried forward along any unital ring homomorphism, and in a finite product of rings it holds exactly when it holds in every factor. These permanence results also hold for nonassociative rings.

Main results

• TwoSidedIdeal.span_image_eq_top: the image of a generating set under a ring homomorphism generates.
• TwoSidedIdeal.span_eq_top_iff_forall_span_image_eval_eq_top: a subset of a finite product generates exactly when its image in every factor does.

theorem TwoSidedIdeal.span_image_eq_top {R : Type u_1} {S : Type u_2} {F : Type u_3} [NonAssocRing R] [NonAssocRing S] [FunLike F R S] [RingHomClass F R S] (f : F) {s : Set R} (hs : span s = ⊤) : span (⇑f '' s) = ⊤

Generation of the unit two-sided ideal is carried along ring homomorphisms. If s generates R as a two-sided ideal, then so does f '' s in S.

theorem TwoSidedIdeal.span_eq_top_iff_forall_span_image_eval_eq_top {ι : Type u_1} [Finite ι] {A : ι → Type u_2} [(i : ι) → NonAssocRing (A i)] {s : Set ((i : ι) → A i)} : span s = ⊤ ↔ ∀ (i : ι), span (Function.eval i '' s) = ⊤

A subset of a finite product of nonassociative rings generates the unit two-sided ideal exactly when its image in every factor does.