# mathlib3documentation

topology.algebra.ring.basic

# Topological (semi)rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• subring.topological_closure/subsemiring.topological_closure: the topological closure of a subring/subsemiring is itself a sub(semi)ring.
• prod.topological_semiring/prod.topological_ring: The product of two topological (semi)rings.
• pi.topological_semiring/pi.topological_ring: The arbitrary product of topological (semi)rings.
@[class]
structure topological_semiring (α : Type u_1)  :
Prop
• to_has_continuous_mul :

a topological semiring is a semiring R where addition and multiplication are continuous. We allow for non-unital and non-associative semirings as well.

The topological_semiring class should only be instantiated in the presence of a non_unital_non_assoc_semiring instance; if there is an instance of non_unital_non_assoc_ring, then topological_ring should be used. Note: in the presence of non_assoc_ring, these classes are mathematically equivalent (see topological_semiring.has_continuous_neg_of_mul or topological_semiring.to_topological_ring).

Instances of this typeclass
@[class]
structure topological_ring (α : Type u_1)  :
Prop
• to_topological_semiring :
• to_has_continuous_neg :

A topological ring is a ring R where addition, multiplication and negation are continuous.

If R is a (unital) ring, then continuity of negation can be derived from continuity of multiplication as it is multiplication with -1. (See topological_semiring.has_continuous_neg_of_mul and topological_semiring.to_topological_add_group)

Instances of this typeclass

If R is a ring with a continuous multiplication, then negation is continuous as well since it is just multiplication with -1.

If R is a ring which is a topological semiring, then it is automatically a topological ring. This exists so that one can place a topological ring structure on R without explicitly proving continuous_neg.

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def subsemiring.topological_semiring {α : Type u_1} [semiring α] (S : subsemiring α) :
def subsemiring.topological_closure {α : Type u_1} [semiring α] (s : subsemiring α) :

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

Equations
@[simp]
theorem subsemiring.topological_closure_coe {α : Type u_1} [semiring α] (s : subsemiring α) :
theorem subsemiring.le_topological_closure {α : Type u_1} [semiring α] (s : subsemiring α) :
theorem subsemiring.topological_closure_minimal {α : Type u_1} [semiring α] (s : subsemiring α) {t : subsemiring α} (h : s t) (ht : is_closed t) :
def subsemiring.comm_semiring_topological_closure {α : Type u_1} [semiring α] [t2_space α] (s : subsemiring α) (hs : (x y : s), x * y = y * x) :

If a subsemiring of a topological semiring is commutative, then so is its topological closure.

Equations
@[protected, instance]
def prod.topological_semiring {α : Type u_1} {β : Type u_2}  :

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

@[protected, instance]
def prod.topological_ring {α : Type u_1} {β : Type u_2}  :

The product topology on the cartesian product of two topological rings makes the product into a topological ring.

@[protected, instance]
def pi.topological_semiring {β : Type u_1} {C : β Type u_2} [Π (b : β), topological_space (C b)] [Π (b : β), ] [ (b : β), topological_semiring (C b)] :
topological_semiring (Π (b : β), C b)
@[protected, instance]
def pi.topological_ring {β : Type u_1} {C : β Type u_2} [Π (b : β), topological_space (C b)] [Π (b : β), ] [ (b : β), topological_ring (C b)] :
topological_ring (Π (b : β), C b)
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def mul_opposite.topological_ring {α : Type u_1}  :
@[protected, instance]
@[protected, instance]
@[protected, instance]
def add_opposite.topological_ring {α : Type u_1}  :
theorem topological_ring.of_add_group_of_nhds_zero {R : Type u_2} (hmul : ((nhds 0).prod (nhds 0)) (nhds 0)) (hmul_left : (x₀ : R), filter.tendsto (λ (x : R), x₀ * x) (nhds 0) (nhds 0)) (hmul_right : (x₀ : R), filter.tendsto (λ (x : R), x * x₀) (nhds 0) (nhds 0)) :
theorem topological_ring.of_nhds_zero {R : Type u_2} (hadd : ((nhds 0).prod (nhds 0)) (nhds 0)) (hneg : filter.tendsto (λ (x : R), -x) (nhds 0) (nhds 0)) (hmul : ((nhds 0).prod (nhds 0)) (nhds 0)) (hmul_left : (x₀ : R), filter.tendsto (λ (x : R), x₀ * x) (nhds 0) (nhds 0)) (hmul_right : (x₀ : R), filter.tendsto (λ (x : R), x * x₀) (nhds 0) (nhds 0)) (hleft : (x₀ : R), nhds x₀ = filter.map (λ (x : R), x₀ + x) (nhds 0)) :
theorem mul_left_continuous {α : Type u_1} (x : α) :

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

theorem mul_right_continuous {α : Type u_1} (x : α) :

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

@[protected, instance]
def subring.topological_ring {α : Type u_1} [ring α] (S : subring α) :
def subring.topological_closure {α : Type u_1} [ring α] (S : subring α) :

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

Equations
theorem subring.le_topological_closure {α : Type u_1} [ring α] (s : subring α) :
theorem subring.is_closed_topological_closure {α : Type u_1} [ring α] (s : subring α) :
theorem subring.topological_closure_minimal {α : Type u_1} [ring α] (s : subring α) {t : subring α} (h : s t) (ht : is_closed t) :
def subring.comm_ring_topological_closure {α : Type u_1} [ring α] [t2_space α] (s : subring α) (hs : (x y : s), x * y = y * x) :

If a subring of a topological ring is commutative, then so is its topological closure.

Equations

### 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 α] :
• to_topological_space :
• to_topological_ring :

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

Instances for ring_topology
theorem ring_topology.ext {α : Type u} {_inst_1 : ring α} (x y : ring_topology α)  :
x = y
@[protected, instance]
def ring_topology.inhabited {α : Type u} [ring α] :
Equations
@[ext]
theorem ring_topology.ext' {α : Type u_1} [ring α] {f g : ring_topology α}  :
f = g
@[protected, 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
@[protected, 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
@[protected, instance]
def ring_topology.complete_lattice {α : Type u_1} [ring α] :
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 : α β) :

The forgetful functor from ring topologies on a to additive group topologies on a.

Equations

The order embedding from ring topologies on a to additive group topologies on a.

Equations
def absolute_value.comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [semiring T] [semiring R] (v : S) {f : T →+* R} (hf : function.injective f) :

Construct an absolute value on a semiring T from an absolute value on a semiring R and an injective ring homomorphism f : T →+* R

Equations