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 #

@[class]
structure topological_semiring (α : Type u_1) [topological_space α] [semiring α] :
Prop

A topological semiring is a semiring where addition and multiplication are continuous.

Instances

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

Equations
@[instance]
def prod_semiring {α : Type u_1} [topological_space α] [semiring α] [topological_semiring α] {β : Type u_2} [semiring β] [topological_space β] [topological_semiring β] :

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

@[instance]
def prod_ring {α : Type u_1} [ring α] [topological_space α] [topological_ring α] {β : Type u_2} [ring β] [topological_space β] [topological_ring β] :

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

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]