Two-sided spans and generation modulo the radical

In a ring, the two-sided ideal spanned by a set s is the additive subgroup generated by the products a * x * b with x ∈ s (Mathlib's TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure). So an additive subgroup contains TwoSidedIdeal.span s exactly when it contains every such product. This is how fullness of an idempotent e, TwoSidedIdeal.span {e} = ⊤, is used: to show that 1 lies in an additive subgroup it suffices to show that every a * e * b does.

A surjective ring homomorphism with kernel contained in the Jacobson radical reflects generation of the whole ring as a two-sided ideal. In particular, fullness of an element can be checked in a quotient by an ideal contained in the radical, such as the radical quotient itself, where idempotents are easier to select.

Main results

• TauCeti.TwoSidedIdeal.coe_span_subset_addSubgroup_iff: an additive subgroup contains the two-sided ideal spanned by s if and only if it contains every product a * x * b with x ∈ s.
• RingHom.twoSidedIdeal_span_image_eq_top_iff: generation as a two-sided ideal is detected by a surjective map whose kernel lies in the Jacobson radical.

theorem TauCeti.TwoSidedIdeal.coe_span_subset_addSubgroup_iff {R : Type u_1} [Ring R] {s : Set R} {H : AddSubgroup R} : ↑(TwoSidedIdeal.span s) ⊆ ↑H ↔ ∀ (a x : R), x ∈ s → ∀ (b : R), a * x * b ∈ H

An additive subgroup contains the two-sided ideal spanned by s if and only if it contains every product a * x * b with x ∈ s.

theorem RingHom.twoSidedIdeal_span_image_eq_top_iff {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) (hf : Function.Surjective ⇑f) (hker : ker f ≤ Ring.jacobson R) (s : Set R) : TwoSidedIdeal.span (⇑f '' s) = ⊤ ↔ TwoSidedIdeal.span s = ⊤

Generation as a two-sided ideal is reflected by a surjective ring map whose kernel lies in the Jacobson radical. In particular, fullness can be checked modulo the radical.