Quotients of normed rings by two-sided ideals

Let I be a two-sided ideal of a possibly noncommutative seminormed ring R. The quotient ring R ⧸ I carries the quotient norm ‖x‖ = inf {‖a‖ : a ↦ x}, and this norm is submultiplicative, so R ⧸ I is a seminormed ring; it is a normed ring when I is closed, and it is complete when R is (Submodule.Quotient.completeSpace). For a normed 𝕜-algebra the quotient is a normed 𝕜-algebra. Mathlib provides these structures for commutative rings; the statements here are their noncommutative counterparts, as needed for Banach algebras such as operator algebras. A TwoSidedIdeal J is covered through its underlying ideal J.asIdeal, which is two-sided.

No normalization ‖1‖ = 1 is assumed. The identity of the quotient satisfies ‖1‖ ≤ ‖(1 : R)‖, and when geometric series are summable in R (for instance when R is complete) and I is proper, also 1 ≤ ‖1‖, because a proper ideal contains no element within distance 1 of the identity. In particular a quotient of a Banach algebra with ‖1‖ = 1 by a proper closed ideal again has ‖1‖ = 1.

The quotient map Ideal.Quotient.mkA does not increase norms (Ideal.Quotient.norm_mkA_le), and a continuous algebra homomorphism vanishing on I descends to a continuous algebra homomorphism Ideal.Quotient.liftA on R ⧸ I with the same bound on representatives. The continuous first isomorphism theorem says that a continuous surjective homomorphism f : A → B of Banach algebras induces an isomorphism A ⧸ ker f ≃ B of topological algebras. Its inverse is bounded by the open mapping theorem, but it is in general not an isometry: the quotient norm of a is the distance from a to ker f, which need not be ‖f a‖.

Main definitions

• Ideal.Quotient.seminormedRing, Ideal.Quotient.normedRing, Ideal.Quotient.normedAlgebraOfIsTwoSided: the quotient norm structures.
• ContinuousAlgHom.quotientKerEquivOfSurjective: the continuous first isomorphism theorem for Banach algebras.

Main results

• Ideal.Quotient.norm_mk_le_norm and Ideal.Quotient.exists_norm_mk_lt: the quotient norm is at most the norm of any representative, and is approached by representatives.
• Ideal.Quotient.norm_one_le and Ideal.Quotient.one_le_norm_one: bounds for the norm of the identity of a quotient.
• Ideal.Quotient.norm_liftA_apply_le: a norm bound for an induced homomorphism.

Kernels of continuous algebra homomorphisms into normed algebras are closed (ContinuousAlgHom.isClosed_ker), so the quotient by such a kernel is a normed algebra.

References

• H. G. Dales, Banach Algebras and Automatic Continuity, §1.3 and §2.1.
• F. F. Bonsall and J. Duncan, Complete Normed Algebras, §7.

theorem Ideal.Quotient.norm_mk_le_norm {R : Type u_1} [SeminormedRing R] (I : Ideal R) [I.IsTwoSided] (a : R) : ‖(mk I) a‖ ≤ ‖a‖

The quotient map by a two-sided ideal does not increase norms.

theorem Ideal.Quotient.exists_norm_mk_lt {R : Type u_1} [SeminormedRing R] {I : Ideal R} [I.IsTwoSided] (x : R ⧸ I) {ε : ℝ} (hε : 0 < ε) : ∃ (a : R), (mk I) a = x ∧ ‖a‖ < ‖x‖ + ε

Every element of the quotient by a two-sided ideal has a representative of norm less than its quotient norm plus ε.

@[instance_reducible]

noncomputable instance Ideal.Quotient.seminormedRing {R : Type u_1} [SeminormedRing R] (I : Ideal R) [I.IsTwoSided] : SeminormedRing (R ⧸ I)

The quotient of a seminormed ring by a two-sided ideal, with the quotient norm, is a seminormed ring.

@[instance_reducible]

noncomputable instance Ideal.Quotient.normedRing {R : Type u_1} [SeminormedRing R] (I : Ideal R) [I.IsTwoSided] [IsClosed ↑I] : NormedRing (R ⧸ I)

The quotient of a seminormed ring by a closed two-sided ideal is a normed ring.

theorem Ideal.Quotient.norm_one_le {R : Type u_1} [SeminormedRing R] (I : Ideal R) [I.IsTwoSided] : ‖1‖ ≤ ‖1‖

The identity of a quotient has norm at most the norm of the identity.

@[instance_reducible]

noncomputable instance Ideal.Quotient.normedAlgebraOfIsTwoSided {R : Type u_1} [SeminormedRing R] (I : Ideal R) [I.IsTwoSided] (𝕜 : Type u_2) [NormedField 𝕜] [NormedAlgebra 𝕜 R] : NormedAlgebra 𝕜 (R ⧸ I)

The quotient of a seminormed 𝕜-algebra by a two-sided ideal is a normed 𝕜-algebra.

theorem Ideal.Quotient.one_le_norm_one {R : Type u_1} [NormedRing R] [HasSummableGeomSeries R] {I : Ideal R} [I.IsTwoSided] (hI : I ≠ ⊤) : 1 ≤ ‖1‖

In a normed ring with summable geometric series (for instance a Banach algebra), the identity of the quotient by a proper two-sided ideal has norm at least 1.

instance Ideal.Quotient.normOneClass {R : Type u_1} [NormedRing R] [HasSummableGeomSeries R] {I : Ideal R} [I.IsTwoSided] [NormOneClass R] [Nontrivial (R ⧸ I)] : NormOneClass (R ⧸ I)

A quotient of a normed ring with ‖1‖ = 1 and summable geometric series (for instance a Banach algebra) by a proper two-sided ideal again has ‖1‖ = 1.

theorem Ideal.Quotient.norm_mkA_le {R : Type u_1} {A : Type u_2} [CommSemiring R] [SeminormedRing A] [Algebra R A] (I : Ideal A) [I.IsTwoSided] (a : A) : ‖(mkA R I) a‖ ≤ ‖a‖

The quotient map by a two-sided ideal, as a continuous algebra homomorphism, does not increase norms.

theorem Ideal.Quotient.norm_liftA_apply_le {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [SeminormedRing A] [Algebra R A] (I : Ideal A) [I.IsTwoSided] [SeminormedRing B] [Algebra R B] (f : A →A[R] B) (hI : ∀ a ∈ I, f a = 0) {C : ℝ} (hC : ∀ (a : A), ‖f a‖ ≤ C * ‖a‖) (x : A ⧸ I) : ‖(liftA I f hI) x‖ ≤ C * ‖x‖

A homomorphism bounded by C on A is bounded by C on the quotient.

noncomputable def ContinuousAlgHom.quotientKerEquivOfSurjective {𝕜 : Type u_1} {A : Type u_2} {B : Type u_3} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [NormedRing B] [NormedAlgebra 𝕜 B] [CompleteSpace B] (f : A →A[𝕜] B) (hf : Function.Surjective ⇑f) : (A ⧸ RingHom.ker f) ≃A[𝕜] B

The continuous first isomorphism theorem for Banach algebras: a continuous surjective algebra homomorphism f : A → B induces an isomorphism of topological algebras A ⧸ ker f ≃ B. Its inverse is continuous by the open mapping theorem; it need not be an isometry.

@[simp]

theorem ContinuousAlgHom.toAlgEquiv_quotientKerEquivOfSurjective {𝕜 : Type u_1} {A : Type u_2} {B : Type u_3} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [NormedRing B] [NormedAlgebra 𝕜 B] [CompleteSpace B] (f : A →A[𝕜] B) (hf : Function.Surjective ⇑f) : (f.quotientKerEquivOfSurjective hf).toAlgEquiv = Ideal.quotientKerAlgEquivOfSurjective hf

The underlying algebra isomorphism is the algebraic first isomorphism theorem.

@[simp]

theorem ContinuousAlgHom.quotientKerEquivOfSurjective_mk {𝕜 : Type u_1} {A : Type u_2} {B : Type u_3} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [NormedRing B] [NormedAlgebra 𝕜 B] [CompleteSpace B] (f : A →A[𝕜] B) (hf : Function.Surjective ⇑f) (a : A) : (f.quotientKerEquivOfSurjective hf) ((Ideal.Quotient.mk (RingHom.ker f)) a) = f a

@[simp]

theorem ContinuousAlgHom.quotientKerEquivOfSurjective_symm_apply {𝕜 : Type u_1} {A : Type u_2} {B : Type u_3} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [NormedRing B] [NormedAlgebra 𝕜 B] [CompleteSpace B] (f : A →A[𝕜] B) (hf : Function.Surjective ⇑f) (a : A) : (f.quotientKerEquivOfSurjective hf).symm (f a) = (Ideal.Quotient.mk (RingHom.ker f)) a