Closed two-sided ideals

The closure of a two-sided ideal in a topological ring is again two-sided, and closed two-sided ideals in rings with an approximate unit absorb compatible scalar multiplication. We also supply the topological-ring structure on Mathlib's existing quotient topology for quotients of noncommutative rings by native ideals. The closed ideal generated by an ideal of the center presents discrete modules with central relations. Continuous algebra equivalences carrying one central character to another map the closed ideal generated by the kernel of the first into that of the second (AlgEquiv.apply_mem_closedCentralIdeal_ker), so continuous automorphisms with continuous inverses fixing a character preserve its closed ideal (MonoidHom.map_closedCentralIdeal_ker). When ring automorphisms preserving a two-sided ideal have continuous inverses, so do the automorphisms they induce on the quotient (MonoidHom.continuous_quotientRingAut_symm).

The quotient-ring construction generalizes Patrick Massot's QuotientRing.topologicalRing_quotient in Mathlib from commutative rings, using the same native additive quotient and open quotient-map argument.

@[instance 100]

instance Ideal.isTopologicalRingQuotient {A : Type u_1} [Ring A] [TopologicalSpace A] [IsTopologicalRing A] (I : Ideal A) [I.IsTwoSided] : IsTopologicalRing (A ⧸ I)

A quotient of a possibly noncommutative topological ring is a topological ring.

instance Ideal.isTwoSided_closure {A : Type u_1} [Ring A] [TopologicalSpace A] [IsTopologicalRing A] (I : Ideal A) [I.IsTwoSided] : I.closure.IsTwoSided

The closure of a two-sided ideal is two-sided.

theorem MonoidHom.continuous_quotientRingAut_symm {H : Type u_1} [Monoid H] {A : Type u_2} [Ring A] [TopologicalSpace A] (a : H →* RingAut A) (I : Ideal A) [I.IsTwoSided] (hI : ∀ (h : H), Ideal.map (↑(a h)) I = I) {h : H} (ha : Continuous ⇑(RingEquiv.symm (a h))) : Continuous ⇑(RingEquiv.symm ((a.quotientRingAut I hI) h))

If the inverse of an automorphism preserving I is continuous, so is the inverse of the induced automorphism of A ⧸ I, for the quotient topology.

def TwoSidedIdeal.topologicalClosure {A : Type u_1} [NonUnitalRing A] [TopologicalSpace A] [IsTopologicalRing A] (I : TwoSidedIdeal A) : TwoSidedIdeal A

The topological closure of a two-sided ideal in a possibly nonunital topological ring, as a native two-sided ideal.

@[simp]

theorem TwoSidedIdeal.coe_topologicalClosure {A : Type u_1} [NonUnitalRing A] [TopologicalSpace A] [IsTopologicalRing A] (I : TwoSidedIdeal A) : ↑I.topologicalClosure = closure ↑I

@[simp]

theorem TwoSidedIdeal.mem_topologicalClosure {A : Type u_1} [NonUnitalRing A] [TopologicalSpace A] [IsTopologicalRing A] {I : TwoSidedIdeal A} {a : A} : a ∈ I.topologicalClosure ↔ a ∈ closure ↑I

theorem TwoSidedIdeal.le_topologicalClosure {A : Type u_1} [NonUnitalRing A] [TopologicalSpace A] [IsTopologicalRing A] (I : TwoSidedIdeal A) : I ≤ I.topologicalClosure

A two-sided ideal is contained in its topological closure.

theorem TwoSidedIdeal.isClosed_topologicalClosure {A : Type u_1} [NonUnitalRing A] [TopologicalSpace A] [IsTopologicalRing A] (I : TwoSidedIdeal A) : IsClosed ↑I.topologicalClosure

The topological closure is closed.

@[simp]

theorem TwoSidedIdeal.topologicalClosure_eq_self {A : Type u_1} [NonUnitalRing A] [TopologicalSpace A] [IsTopologicalRing A] (I : TwoSidedIdeal A) [hI : IsClosed ↑I] : I.topologicalClosure = I

A closed two-sided ideal equals its topological closure.

theorem TwoSidedIdeal.topologicalClosure_idem {A : Type u_1} [NonUnitalRing A] [TopologicalSpace A] [IsTopologicalRing A] (I : TwoSidedIdeal A) : I.topologicalClosure.topologicalClosure = I.topologicalClosure

Taking topological closure of a two-sided ideal is idempotent.

theorem TwoSidedIdeal.topologicalClosure_mono {A : Type u_1} [NonUnitalRing A] [TopologicalSpace A] [IsTopologicalRing A] {I J : TwoSidedIdeal A} (h : I ≤ J) : I.topologicalClosure ≤ J.topologicalClosure

Taking topological closure of two-sided ideals is monotone.

theorem TwoSidedIdeal.topologicalClosure_le_iff {A : Type u_1} [NonUnitalRing A] [TopologicalSpace A] [IsTopologicalRing A] (I J : TwoSidedIdeal A) (hJ : IsClosed ↑J) : I.topologicalClosure ≤ J ↔ I ≤ J

The closure is the least closed two-sided ideal containing the original ideal.

theorem TwoSidedIdeal.isClosed_ker {A : Type u_1} {B : Type u_2} {F : Type u_3} [NonUnitalNonAssocRing A] [TopologicalSpace A] [NonUnitalNonAssocSemiring B] [TopologicalSpace B] [T1Space B] [FunLike F A B] [NonUnitalRingHomClass F A B] {f : F} (hf : Continuous ⇑f) : IsClosed ↑(ker f)

The kernel two-sided ideal of a continuous nonunital ring homomorphism into a T₁ space is closed.

theorem TwoSidedIdeal.smul_mem_of_isApproximateUnit {R : Type u_1} {A : Type u_2} [Semiring R] [NonUnitalRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [ContinuousConstSMul R A] (I : TwoSidedIdeal A) [hI : IsClosed ↑I] {l : Filter A} (hl : l.IsApproximateUnit) (c : R) {a : A} (ha : a ∈ I) : c • a ∈ I

In a topological ring with a scalar-compatible R-module structure and an approximate unit, every closed two-sided ideal is closed under scalar multiplication by R.

def Ideal.closedCentralIdeal {R : Type u_1} [CommRing R] {A : Type u_2} [Ring A] [Algebra R A] [TopologicalSpace A] [IsTopologicalRing A] (L : Ideal ↥(Subalgebra.center R A)) : TwoSidedIdeal A

The closed two-sided ideal generated by an ideal of the center.

theorem Ideal.isClosed_closedCentralIdeal {R : Type u_1} [CommRing R] {A : Type u_2} [Ring A] [Algebra R A] [TopologicalSpace A] [IsTopologicalRing A] (L : Ideal ↥(Subalgebra.center R A)) : IsClosed ↑L.closedCentralIdeal

The generated central ideal is closed.

theorem Ideal.mem_closedCentralIdeal {R : Type u_1} [CommRing R] {A : Type u_2} [Ring A] [Algebra R A] [TopologicalSpace A] [IsTopologicalRing A] (L : Ideal ↥(Subalgebra.center R A)) {z : ↥(Subalgebra.center R A)} (hz : z ∈ L) : ↑z ∈ L.closedCentralIdeal

Every central relation belongs to the closed generated ideal.

theorem Ideal.closedCentralIdeal_le_iff {R : Type u_1} [CommRing R] {A : Type u_2} [Ring A] [Algebra R A] [TopologicalSpace A] [IsTopologicalRing A] (L : Ideal ↥(Subalgebra.center R A)) (J : TwoSidedIdeal A) (hJ : IsClosed ↑J) : L.closedCentralIdeal ≤ J ↔ ∀ z ∈ L, ↑z ∈ J

The closed central ideal is the least closed two-sided ideal containing the relations.

theorem AlgEquiv.apply_mem_closedCentralIdeal_ker {R : Type u_1} [CommRing R] {A : Type u_2} [Ring A] [Algebra R A] [TopologicalSpace A] [IsTopologicalRing A] {B : Type u_3} [Ring B] [Algebra R B] [TopologicalSpace B] [IsTopologicalRing B] (e : A ≃ₐ[R] B) (he : Continuous ⇑e) {χ : ↥(Subalgebra.center R A) →ₐ[R] R} {χ' : ↥(Subalgebra.center R B) →ₐ[R] R} (hχ : χ'.comp ↑(TauCeti.centerCongr e) = χ) {x : A} (hx : x ∈ (RingHom.ker χ).closedCentralIdeal) : e x ∈ (RingHom.ker χ').closedCentralIdeal

A continuous algebra equivalence carrying the central character χ to χ' maps the closed ideal generated by the kernel of χ into that generated by the kernel of χ'.

theorem MonoidHom.map_closedCentralIdeal_ker {H : Type u_1} [Monoid H] {R : Type u_2} [CommRing R] {A : Type u_3} [Ring A] [Algebra R A] [TopologicalSpace A] [IsTopologicalRing A] (a : H →* A ≃ₐ[R] A) (χ : ↥(Subalgebra.center R A) →ₐ[R] R) (ha : ∀ (h : H), Continuous ⇑(a h).symm) (ha' : ∀ (h : H), Continuous ⇑(a h)) (hχ : ∀ (h : H), χ.comp ↑(TauCeti.centerCongr (a h)).symm = χ) (h : H) : Ideal.map (↑(((MulSemiringAction.toRingEquiv (A ≃ₐ[R] A) A).comp a) h)) (TwoSidedIdeal.asIdeal (RingHom.ker χ).closedCentralIdeal) = TwoSidedIdeal.asIdeal (RingHom.ker χ).closedCentralIdeal

Continuous automorphisms with continuous inverses that preserve a central character preserve the closed ideal generated by its kernel.