Mathlib.Topology.Algebra.Ring.Ideal

Module docstring

{"# Ideals and quotients of topological rings

In this file we define Ideal.closure to be the topological closure of an ideal in a topological ring. We also define a TopologicalSpace structure on the quotient of a topological ring by an ideal and prove that the quotient is a topological ring. "}

Ideal.closure definition

(I : Ideal R) : Ideal R

Full source

/-- The closure of an ideal in a topological ring as an ideal. -/
protected def Ideal.closure (I : Ideal R) : Ideal R :=
  {
    AddSubmonoid.topologicalClosure
      I.toAddSubmonoid with
    carrier := closure I
    smul_mem' := fun c _ hx => map_mem_closure (mulLeft_continuous _) hx fun _ => I.mul_mem_left c }

Topological closure of an ideal

Informal description

The topological closure of an ideal $I$ in a topological ring $R$ is the smallest closed ideal containing $I$. It is defined as the topological closure of $I$ as a set, equipped with the ideal structure inherited from $I$. Specifically, for any $c \in R$ and $x$ in the closure of $I$, the product $c \cdot x$ remains in the closure of $I$.

Ideal.coe_closure theorem

(I : Ideal R) : (I.closure : Set R) = closure I

Full source

@[simp]
theorem Ideal.coe_closure (I : Ideal R) : (I.closure : Set R) = closure I :=
  rfl

Equality of Ideal Closure and Set Closure in Topological Rings

Informal description

For any ideal $I$ in a topological ring $R$, the underlying set of the topological closure of $I$ is equal to the topological closure of the underlying set of $I$. That is, $(I.\text{closure} : \text{Set } R) = \text{closure}(I)$.

Ideal.closure_eq_of_isClosed theorem

(I : Ideal R) (hI : IsClosed (I : Set R)) : I.closure = I

Full source

theorem Ideal.closure_eq_of_isClosed (I : Ideal R) (hI : IsClosed (I : Set R)) : I.closure = I :=
  SetLike.ext' hI.closure_eq

Closure of Closed Ideal Equals Itself

Informal description

For any ideal $I$ in a topological ring $R$, if $I$ is closed as a subset of $R$, then the topological closure of $I$ equals $I$ itself, i.e., $\overline{I} = I$.

topologicalRingQuotientTopology instance

: TopologicalSpace (R ⧸ N)

Full source

instance topologicalRingQuotientTopology : TopologicalSpace (R ⧸ N) :=
  instTopologicalSpaceQuotient

Topology on Quotient Rings

Informal description

For any topological ring $R$ and ideal $N$ of $R$, the quotient ring $R ⧸ N$ inherits a topological space structure from $R$.

QuotientRing.isOpenMap_coe theorem

: IsOpenMap (mk N)

Full source

theorem QuotientRing.isOpenMap_coe : IsOpenMap (mk N) :=
  QuotientAddGroup.isOpenMap_coe

Quotient Map is Open for Topological Rings

Informal description

The quotient map $\pi : R \to R/N$ from a topological ring $R$ to its quotient ring $R/N$ by an ideal $N$ is an open map. That is, for every open subset $U \subseteq R$, the image $\pi(U)$ is open in $R/N$.

QuotientRing.isOpenQuotientMap_mk theorem

: IsOpenQuotientMap (mk N)

Full source

theorem QuotientRing.isOpenQuotientMap_mk : IsOpenQuotientMap (mk N) :=
  QuotientAddGroup.isOpenQuotientMap_mk

Open Quotient Map Property of Ring Quotient

Informal description

The canonical quotient map $\pi : R \to R ⧸ N$ from a topological ring $R$ to its quotient by an ideal $N$ is an open quotient map. That is, $\pi$ is surjective, continuous, and maps open sets in $R$ to open sets in $R ⧸ N$.

QuotientRing.isQuotientMap_coe_coe theorem

: IsQuotientMap fun p : R × R => (mk N p.1, mk N p.2)

Full source

theorem QuotientRing.isQuotientMap_coe_coe : IsQuotientMap fun p : R × R => (mk N p.1, mk N p.2) :=
  ((isOpenQuotientMap_mk N).prodMap (isOpenQuotientMap_mk N)).isQuotientMap

Quotient Map Property of the Product of Quotient Maps in Topological Rings

Informal description

The map $(x, y) \mapsto ([x], [y])$ from $R \times R$ to $(R/N) \times (R/N)$, where $[x]$ denotes the equivalence class of $x$ in the quotient ring $R/N$, is a quotient map of topological spaces.

topologicalRing_quotient instance

: IsTopologicalRing (R ⧸ N)

Full source

instance topologicalRing_quotient : IsTopologicalRing (R ⧸ N) where
  __ := QuotientAddGroup.instIsTopologicalAddGroup _
  continuous_mul := (QuotientRing.isQuotientMap_coe_coe N).continuous_iff.2 <|
    continuous_quot_mk.comp continuous_mul

Quotient of a Topological Ring by an Ideal is a Topological Ring

Informal description

For any topological ring $R$ and ideal $N$ of $R$, the quotient ring $R ⧸ N$ is a topological ring with the quotient topology.

instCompactSpaceQuotientIdeal instance

[CompactSpace R] : CompactSpace (R ⧸ N)

Full source

instance [CompactSpace R] : CompactSpace (R ⧸ N) :=
  Quotient.compactSpace

Compactness of Quotient Rings from Compact Topological Rings

Informal description

For any compact topological ring $R$ and ideal $N$ of $R$, the quotient ring $R ⧸ N$ is also compact.