# 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 #

• Subring.topologicalClosure/Subsemiring.topologicalClosure: the topological closure of a Subring/Subsemiring is itself a sub(semi)ring.
• The product of two topological (semi)rings is a topological (semi)ring.
• The indexed product of topological (semi)rings is a topological (semi)ring.
class TopologicalSemiring (α : Type u_1) [] extends , :

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 TopologicalSemiring class should only be instantiated in the presence of a NonUnitalNonAssocSemiring instance; if there is an instance of NonUnitalNonAssocRing, then TopologicalRing should be used. Note: in the presence of NonAssocRing, these classes are mathematically equivalent (see TopologicalSemiring.continuousNeg_of_mul or TopologicalSemiring.toTopologicalRing).

Instances
class TopologicalRing (α : Type u_1) [] extends , :

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 TopologicalSemiring.continuousNeg_of_mul and topological_semiring.to_topological_add_group)

Instances
theorem TopologicalSemiring.continuousNeg_of_mul {α : Type u_1} [] [] [] :

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

theorem TopologicalSemiring.toTopologicalRing {α : Type u_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.

@[instance 100]
instance TopologicalRing.to_topologicalAddGroup {α : Type u_1} [] [] :
Equations
• =
@[instance 50]
instance DiscreteTopology.topologicalSemiring {α : Type u_1} [] [] :
Equations
• =
@[instance 50]
instance DiscreteTopology.topologicalRing {α : Type u_1} [] [] :
Equations
• =
Equations
• =
instance Subsemiring.topologicalSemiring {α : Type u_1} [] [] (S : ) :
Equations
• =
def Subsemiring.topologicalClosure {α : Type u_1} [] [] (s : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Subsemiring.topologicalClosure_coe {α : Type u_1} [] [] (s : ) :
s.topologicalClosure = closure s
theorem Subsemiring.le_topologicalClosure {α : Type u_1} [] [] (s : ) :
s s.topologicalClosure
theorem Subsemiring.isClosed_topologicalClosure {α : Type u_1} [] [] (s : ) :
IsClosed s.topologicalClosure
theorem Subsemiring.topologicalClosure_minimal {α : Type u_1} [] [] (s : ) {t : } (h : s t) (ht : IsClosed t) :
s.topologicalClosure t
def Subsemiring.commSemiringTopologicalClosure {α : Type u_1} [] [] [] (s : ) (hs : ∀ (x y : s), x * y = y * x) :
CommSemiring s.topologicalClosure

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

Equations
• s.commSemiringTopologicalClosure hs = let __src := s.topologicalClosure.toSemiring; let __src_1 := s.commMonoidTopologicalClosure hs;
Instances For
instance instTopologicalSemiringProd {α : Type u_1} {β : Type u_2} [] [] :

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

Equations
• =
instance instTopologicalRingProd {α : Type u_1} {β : Type u_2} [] [] [] [] :

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

Equations
• =
instance instContinuousAddForallOfTopologicalSemiring {β : Type u_2} {C : βType u_3} [(b : β) → TopologicalSpace (C b)] [(b : β) → ] [∀ (b : β), TopologicalSemiring (C b)] :
ContinuousAdd ((b : β) → C b)
Equations
• =
instance Pi.instTopologicalSemiring {β : Type u_2} {C : βType u_3} [(b : β) → TopologicalSpace (C b)] [(b : β) → ] [∀ (b : β), TopologicalSemiring (C b)] :
TopologicalSemiring ((b : β) → C b)
Equations
• =
instance Pi.instTopologicalRing {β : Type u_2} {C : βType u_3} [(b : β) → TopologicalSpace (C b)] [(b : β) → ] [∀ (b : β), TopologicalRing (C b)] :
TopologicalRing ((b : β) → C b)
Equations
• =
instance instContinuousAddMulOpposite {α : Type u_1} [] [] :
Equations
• =
instance instTopologicalSemiringMulOpposite {α : Type u_1} [] :
Equations
• =
instance instContinuousNegMulOpposite {α : Type u_1} [] [] :
Equations
• =
instance instTopologicalRingMulOpposite {α : Type u_1} [] [] :
Equations
• =
instance instContinuousMulAddOpposite {α : Type u_1} [] [] :
Equations
• =
instance instTopologicalSemiringAddOpposite {α : Type u_1} [] :
Equations
• =
instance instTopologicalRingAddOpposite {α : Type u_1} [] [] :
Equations
• =
theorem TopologicalRing.of_addGroup_of_nhds_zero {R : Type u_2} [] (hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : R) => x * x_1) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hmul_left : ∀ (x₀ : R), Filter.Tendsto (fun (x : R) => x₀ * x) (nhds 0) (nhds 0)) (hmul_right : ∀ (x₀ : R), Filter.Tendsto (fun (x : R) => x * x₀) (nhds 0) (nhds 0)) :
theorem TopologicalRing.of_nhds_zero {R : Type u_2} [] (hadd : Filter.Tendsto (Function.uncurry fun (x x_1 : R) => x + x_1) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hneg : Filter.Tendsto (fun (x : R) => -x) (nhds 0) (nhds 0)) (hmul : Filter.Tendsto (Function.uncurry fun (x x_1 : R) => x * x_1) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hmul_left : ∀ (x₀ : R), Filter.Tendsto (fun (x : R) => x₀ * x) (nhds 0) (nhds 0)) (hmul_right : ∀ (x₀ : R), Filter.Tendsto (fun (x : R) => x * x₀) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : R), nhds x₀ = Filter.map (fun (x : R) => x₀ + x) (nhds 0)) :
instance instTopologicalRingULift {α : Type u_1} [] [] :
Equations
• =
theorem mulLeft_continuous {α : Type u_1} [] [] (x : α) :

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

theorem mulRight_continuous {α : Type u_1} [] [] (x : α) :

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

instance Subring.instTopologicalRing {α : Type u_1} [] [Ring α] [] (S : ) :
Equations
• =
def Subring.topologicalClosure {α : Type u_1} [] [Ring α] [] (S : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Subring.le_topologicalClosure {α : Type u_1} [] [Ring α] [] (s : ) :
s s.topologicalClosure
theorem Subring.isClosed_topologicalClosure {α : Type u_1} [] [Ring α] [] (s : ) :
IsClosed s.topologicalClosure
theorem Subring.topologicalClosure_minimal {α : Type u_1} [] [Ring α] [] (s : ) {t : } (h : s t) (ht : IsClosed t) :
s.topologicalClosure t
def Subring.commRingTopologicalClosure {α : Type u_1} [] [Ring α] [] [] (s : ) (hs : ∀ (x y : s), x * y = y * x) :
CommRing s.topologicalClosure

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

Equations
• s.commRingTopologicalClosure hs = let __src := s.topologicalClosure.toRing; let __src_1 := s.commMonoidTopologicalClosure hs;
Instances For

### Lattice of ring topologies #

We define a type class RingTopology α 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 : TopologicalSpace α → RingTopology β.

structure RingTopology (α : Type u) [Ring α] extends , :

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

Instances For
instance RingTopology.inhabited {α : Type u} [Ring α] :
Equations
• RingTopology.inhabited = { default := let x := ; { toTopologicalSpace := x, toTopologicalRing := } }
theorem RingTopology.toTopologicalSpace_injective {α : Type u_1} [Ring α] :
Function.Injective RingTopology.toTopologicalSpace
theorem RingTopology.ext {α : Type u_1} [Ring α] {f : } {g : } (h : TopologicalSpace.IsOpen = TopologicalSpace.IsOpen) :
f = g
instance RingTopology.instPartialOrder {α : 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

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
• RingTopology.instCompleteSemilatticeInf =
instance RingTopology.instCompleteLattice {α : Type u_1} [Ring α] :
Equations
• RingTopology.instCompleteLattice =
def RingTopology.coinduced {α : Type u_2} {β : Type u_3} [t : ] [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
• = sInf {b : | b.toTopologicalSpace}
Instances For
theorem RingTopology.coinduced_continuous {α : Type u_2} {β : Type u_3} [t : ] [Ring β] (f : αβ) :
def RingTopology.toAddGroupTopology {α : Type u_1} [Ring α] (t : ) :

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.
Construct an absolute value on a semiring T from an absolute value on a semiring R and an injective ring homomorphism f : T →+* R