mathlib documentation

topology.algebra.ring

Topological (semi)rings #

A topological (semi)ring is a (semi)ring equipped with a topology such that all operations are continuous. Besides this definition, this file proves that the topological closure of a subring (resp. an ideal) is a subring (resp. an ideal) and defines products and quotients of topological (semi)rings.

Main Results #

The (topological-space) closure of a subsemiring of a topological semiring is itself a subsemiring.

Equations
@[instance]
def prod.topological_ring {α : Type u_1} [topological_space α] [semiring α] [topological_ring α] {β : Type u_2} [semiring β] [topological_space β] [topological_ring β] :

The product topology on the cartesian product of two topological semirings makes the product into a topological semiring.

@[instance]
def pi.topological_ring {β : Type u_1} {C : β → Type u_2} [Π (b : β), topological_space (C b)] [Π (b : β), semiring (C b)] [∀ (b : β), topological_ring (C b)] :
topological_ring (Π (b : β), C b)
theorem mul_left_continuous {α : Type u_1} [ring α] [topological_space α] [topological_ring α] (x : α) :

In a topological ring, the left-multiplication add_monoid_hom is continuous.

In a topological ring, the right-multiplication add_monoid_hom is continuous.

def subring.topological_closure {α : Type u_1} [ring α] [topological_space α] [topological_ring α] (S : subring α) :

The (topological-space) closure of a subring of a topological semiring is itself a subring.

Equations
theorem subring.topological_closure_minimal {α : Type u_1} [ring α] [topological_space α] [topological_ring α] (s : subring α) {t : subring α} (h : s t) (ht : is_closed t) :
def ideal.closure {α : Type u_1} [topological_space α] [comm_ring α] [topological_ring α] (S : ideal α) :

The closure of an ideal in a topological ring as an ideal.

Equations
@[simp]
theorem ideal.coe_closure {α : Type u_1} [topological_space α] [comm_ring α] [topological_ring α] (S : ideal α) :
@[instance]

Lattice of ring topologies #

We define a type class ring_topology α which endows a ring α with a topology such that all ring operations are continuous.

Ring topologies on a fixed ring α are ordered, by reverse inclusion. They form a complete lattice, with the discrete topology and the indiscrete topology.

Any function f : α → β induces coinduced f : topological_space α → ring_topology β.

theorem ring_topology.ext_iff {α : Type u} {_inst_1 : ring α} (x y : ring_topology α) :
@[ext]
structure ring_topology (α : Type u) [ring α] :
Type u

A ring topology on a ring α is a topology for which addition, negation and multiplication are continuous.

theorem ring_topology.ext {α : Type u} {_inst_1 : ring α} (x y : ring_topology α) (h : x.to_topological_space = y.to_topological_space) :
x = y
@[ext]
theorem ring_topology.ext' {α : Type u_1} [ring α] {f g : ring_topology α} (h : f.to_topological_space.is_open = g.to_topological_space.is_open) :
f = g
@[instance]
def ring_topology.partial_order {α : Type u_1} [ring α] :

The ordering on ring topologies on the ring α. t ≤ s if every set open in s is also open in t (t is finer than s).

Equations
@[instance]

Ring topologies on α form a complete lattice, with the discrete topology and the indiscrete topology.

The infimum of a collection of ring topologies is the topology generated by all their open sets (which is a ring topology).

The supremum of two ring topologies s and t is the infimum of the family of all ring topologies contained in the intersection of s and t.

Equations
def ring_topology.coinduced {α : Type u_1} {β : Type u_2} [t : topological_space α] [ring β] (f : α → β) :

Given f : α → β and a topology on α, the coinduced ring topology on β is the finest topology such that f is continuous and β is a topological ring.

Equations
theorem ring_topology.coinduced_continuous {α : Type u_1} {β : Type u_2} [t : topological_space α] [ring β] (f : α → β) :