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

source
class IsTopologicalSemiring (R : Type u_1) [TopologicalSpace R] [NonUnitalNonAssocSemiring R] extends ContinuousAdd R, ContinuousMul R :
Prop

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

- continuous_add : Continuous fun (p : R × R) => p.1 + p.2
- continuous_mul : Continuous fun (p : R × R) => p.1 * p.2

Instances

source
class IsTopologicalRing (R : Type u_1) [TopologicalSpace R] [NonUnitalNonAssocRing R] extends IsTopologicalSemiring R, ContinuousNeg R :
Prop

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

- continuous_add : Continuous fun (p : R × R) => p.1 + p.2
- continuous_mul : Continuous fun (p : R × R) => p.1 * p.2
- continuous_neg : Continuous fun (a : R) => -a

Instances

source
theorem IsTopologicalSemiring.continuousNeg_of_mul {R : Type u_1} [TopologicalSpace R] [NonAssocRing R] [ContinuousMul R] :
ContinuousNeg R

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

source
theorem IsTopologicalSemiring.toIsTopologicalRing {R : Type u_1} [TopologicalSpace R] [NonAssocRing R] :
IsTopologicalSemiring R → IsTopologicalRing R

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`.

source
@[instance 100]
instance IsTopologicalRing.to_topologicalAddGroup {R : Type u_1} [NonUnitalNonAssocRing R] [TopologicalSpace R] [IsTopologicalRing R] :
IsTopologicalAddGroup R
source
@[instance 50]
instance DiscreteTopology.topologicalSemiring {R : Type u_1} [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [DiscreteTopology R] :
IsTopologicalSemiring R
source
@[instance 50]
instance DiscreteTopology.topologicalRing {R : Type u_1} [TopologicalSpace R] [NonUnitalNonAssocRing R] [DiscreteTopology R] :
IsTopologicalRing R
source
instance NonUnitalSubsemiring.instIsTopologicalSemiring {R : Type u_1} [TopologicalSpace R] [NonUnitalSemiring R] [IsTopologicalSemiring R] (S : NonUnitalSubsemiring R) :
IsTopologicalSemiring ↥S
source
def NonUnitalSubsemiring.topologicalClosure {R : Type u_1} [TopologicalSpace R] [NonUnitalSemiring R] [IsTopologicalSemiring R] (s : NonUnitalSubsemiring R) :
NonUnitalSubsemiring R

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

Equations

- s.topologicalClosure = { carrier := closure ↑s, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯ }

Instances For

source
@[simp]
theorem NonUnitalSubsemiring.topologicalClosure_coe {R : Type u_1} [TopologicalSpace R] [NonUnitalSemiring R] [IsTopologicalSemiring R] (s : NonUnitalSubsemiring R) :
↑s.topologicalClosure = _root_.closure ↑s
source
theorem NonUnitalSubsemiring.le_topologicalClosure {R : Type u_1} [TopologicalSpace R] [NonUnitalSemiring R] [IsTopologicalSemiring R] (s : NonUnitalSubsemiring R) :
s ≤ s.topologicalClosure
source
theorem NonUnitalSubsemiring.isClosed_topologicalClosure {R : Type u_1} [TopologicalSpace R] [NonUnitalSemiring R] [IsTopologicalSemiring R] (s : NonUnitalSubsemiring R) :
IsClosed ↑s.topologicalClosure
source
theorem NonUnitalSubsemiring.topologicalClosure_minimal {R : Type u_1} [TopologicalSpace R] [NonUnitalSemiring R] [IsTopologicalSemiring R] (s : NonUnitalSubsemiring R) {t : NonUnitalSubsemiring R} (h : s ≤ t) (ht : IsClosed ↑t) :
s.topologicalClosure ≤ t
source
@[reducible, inline]
abbrev NonUnitalSubsemiring.nonUnitalCommSemiringTopologicalClosure {R : Type u_1} [TopologicalSpace R] [NonUnitalSemiring R] [IsTopologicalSemiring R] [T2Space R] (s : NonUnitalSubsemiring R) (hs : ∀ (x y : ↥s), x * y = y * x) :
NonUnitalCommSemiring ↥s.topologicalClosure

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

See note [reducible non-instances]

Equations

- s.nonUnitalCommSemiringTopologicalClosure hs = { toNonUnitalSemiring := NonUnitalSubsemiringClass.toNonUnitalSemiring s.topologicalClosure, mul_comm := ⋯ }

Instances For

source
instance instIsTopologicalSemiringULift {R : Type u_1} [TopologicalSpace R] [Semiring R] [IsTopologicalSemiring R] :
IsTopologicalSemiring (ULift.{u_2, u_1} R)
source
instance Subsemiring.topologicalSemiring {R : Type u_1} [TopologicalSpace R] [Semiring R] [IsTopologicalSemiring R] (S : Subsemiring R) :
IsTopologicalSemiring ↥S
source
instance Subsemiring.continuousSMul {R : Type u_1} [TopologicalSpace R] [Semiring R] (s : Subsemiring R) (X : Type u_2) [TopologicalSpace X] [MulAction R X] [ContinuousSMul R X] :
ContinuousSMul (↥s) X
source
def Subsemiring.topologicalClosure {R : Type u_1} [TopologicalSpace R] [Semiring R] [IsTopologicalSemiring R] (s : Subsemiring R) :
Subsemiring R

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

Equations

- s.topologicalClosure = { carrier := closure ↑s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }

Instances For

source
@[simp]
theorem Subsemiring.topologicalClosure_coe {R : Type u_1} [TopologicalSpace R] [Semiring R] [IsTopologicalSemiring R] (s : Subsemiring R) :
↑s.topologicalClosure = _root_.closure ↑s
source
theorem Subsemiring.le_topologicalClosure {R : Type u_1} [TopologicalSpace R] [Semiring R] [IsTopologicalSemiring R] (s : Subsemiring R) :
s ≤ s.topologicalClosure
source
theorem Subsemiring.isClosed_topologicalClosure {R : Type u_1} [TopologicalSpace R] [Semiring R] [IsTopologicalSemiring R] (s : Subsemiring R) :
IsClosed ↑s.topologicalClosure
source
theorem Subsemiring.topologicalClosure_minimal {R : Type u_1} [TopologicalSpace R] [Semiring R] [IsTopologicalSemiring R] (s : Subsemiring R) {t : Subsemiring R} (h : s ≤ t) (ht : IsClosed ↑t) :
s.topologicalClosure ≤ t
source
@[reducible, inline]
abbrev Subsemiring.commSemiringTopologicalClosure {R : Type u_1} [TopologicalSpace R] [Semiring R] [IsTopologicalSemiring R] [T2Space R] (s : Subsemiring R) (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.

See note [reducible non-instances].

Equations

- s.commSemiringTopologicalClosure hs = { toSemiring := s.topologicalClosure.toSemiring, mul_comm := ⋯ }

Instances For

source
instance instIsTopologicalSemiringProd {R : Type u_1} {S : Type u_2} [TopologicalSpace R] [TopologicalSpace S] [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [IsTopologicalSemiring R] [IsTopologicalSemiring S] :
IsTopologicalSemiring (R × S)

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

source
instance instIsTopologicalRingProd {R : Type u_1} {S : Type u_2} [TopologicalSpace R] [TopologicalSpace S] [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [IsTopologicalRing R] [IsTopologicalRing S] :
IsTopologicalRing (R × S)

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

source
instance instContinuousAddForallOfIsTopologicalSemiring {ι : Type u_2} {R : ι → Type u_3} [(i : ι) → TopologicalSpace (R i)] [(i : ι) → NonUnitalNonAssocSemiring (R i)] [∀ (i : ι), IsTopologicalSemiring (R i)] :
ContinuousAdd ((i : ι) → R i)
source
instance Pi.instIsTopologicalSemiring {ι : Type u_2} {R : ι → Type u_3} [(i : ι) → TopologicalSpace (R i)] [(i : ι) → NonUnitalNonAssocSemiring (R i)] [∀ (i : ι), IsTopologicalSemiring (R i)] :
IsTopologicalSemiring ((i : ι) → R i)
source
instance Pi.instIsTopologicalRing {ι : Type u_2} {R : ι → Type u_3} [(i : ι) → TopologicalSpace (R i)] [(i : ι) → NonUnitalNonAssocRing (R i)] [∀ (i : ι), IsTopologicalRing (R i)] :
IsTopologicalRing ((i : ι) → R i)
source
instance instContinuousAddMulOpposite {R : Type u_1} [NonUnitalNonAssocSemiring R] [TopologicalSpace R] [ContinuousAdd R] :
ContinuousAdd R ᵐᵒᵖ
source
instance instIsTopologicalSemiringMulOpposite {R : Type u_1} [NonUnitalNonAssocSemiring R] [TopologicalSpace R] [IsTopologicalSemiring R] :
IsTopologicalSemiring R ᵐᵒᵖ
source
instance instContinuousNegMulOpposite {R : Type u_1} [NonUnitalNonAssocRing R] [TopologicalSpace R] [ContinuousNeg R] :
ContinuousNeg R ᵐᵒᵖ
source
instance instIsTopologicalRingMulOpposite {R : Type u_1} [NonUnitalNonAssocRing R] [TopologicalSpace R] [IsTopologicalRing R] :
IsTopologicalRing R ᵐᵒᵖ
source
instance instContinuousMulAddOpposite {R : Type u_1} [NonUnitalNonAssocSemiring R] [TopologicalSpace R] [ContinuousMul R] :
ContinuousMul R ᵃᵒᵖ
source
instance instIsTopologicalSemiringAddOpposite {R : Type u_1} [NonUnitalNonAssocSemiring R] [TopologicalSpace R] [IsTopologicalSemiring R] :
IsTopologicalSemiring R ᵃᵒᵖ
source
instance instIsTopologicalRingAddOpposite {R : Type u_1} [NonUnitalNonAssocRing R] [TopologicalSpace R] [IsTopologicalRing R] :
IsTopologicalRing R ᵃᵒᵖ
source
theorem IsTopologicalRing.of_addGroup_of_nhds_zero {R : Type u_2} [NonUnitalNonAssocRing R] [TopologicalSpace R] [IsTopologicalAddGroup R] (hmul : Filter.Tendsto (Function.uncurry fun (x1 x2 : R) => x1 * x2) (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)) :
IsTopologicalRing R
source
theorem IsTopologicalRing.of_nhds_zero {R : Type u_2} [NonUnitalNonAssocRing R] [TopologicalSpace R] (hadd : Filter.Tendsto (Function.uncurry fun (x1 x2 : R) => x1 + x2) (nhds 0 ×ˢ nhds 0) (nhds 0)) (hneg : Filter.Tendsto (fun (x : R) => -x) (nhds 0) (nhds 0)) (hmul : Filter.Tendsto (Function.uncurry fun (x1 x2 : R) => x1 * x2) (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)) :
IsTopologicalRing R
source
instance instIsTopologicalRingULift {R : Type u_1} [TopologicalSpace R] [NonUnitalNonAssocRing R] [IsTopologicalRing R] :
IsTopologicalRing (ULift.{u_2, u_1} R)
source
theorem mulLeft_continuous {R : Type u_1} [TopologicalSpace R] [NonUnitalNonAssocRing R] [IsTopologicalRing R] (x : R) :
Continuous ⇑(AddMonoidHom.mulLeft x)

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

source
theorem mulRight_continuous {R : Type u_1} [TopologicalSpace R] [NonUnitalNonAssocRing R] [IsTopologicalRing R] (x : R) :
Continuous ⇑(AddMonoidHom.mulRight x)

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

source
instance NonUnitalSubring.instIsTopologicalRing {R : Type u_1} [TopologicalSpace R] [NonUnitalRing R] [IsTopologicalRing R] (S : NonUnitalSubring R) :
IsTopologicalRing ↥S
source
def NonUnitalSubring.topologicalClosure {R : Type u_1} [TopologicalSpace R] [NonUnitalRing R] [IsTopologicalRing R] (S : NonUnitalSubring R) :
NonUnitalSubring R

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

Equations

- S.topologicalClosure = { carrier := closure ↑S, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, neg_mem' := ⋯ }

Instances For

source
theorem NonUnitalSubring.le_topologicalClosure {R : Type u_1} [TopologicalSpace R] [NonUnitalRing R] [IsTopologicalRing R] (s : NonUnitalSubring R) :
s ≤ s.topologicalClosure
source
theorem NonUnitalSubring.isClosed_topologicalClosure {R : Type u_1} [TopologicalSpace R] [NonUnitalRing R] [IsTopologicalRing R] (s : NonUnitalSubring R) :
IsClosed ↑s.topologicalClosure
source
theorem NonUnitalSubring.topologicalClosure_minimal {R : Type u_1} [TopologicalSpace R] [NonUnitalRing R] [IsTopologicalRing R] (s : NonUnitalSubring R) {t : NonUnitalSubring R} (h : s ≤ t) (ht : IsClosed ↑t) :
s.topologicalClosure ≤ t
source
@[reducible, inline]
abbrev NonUnitalSubring.nonUnitalCommRingTopologicalClosure {R : Type u_1} [TopologicalSpace R] [NonUnitalRing R] [IsTopologicalRing R] [T2Space R] (s : NonUnitalSubring R) (hs : ∀ (x y : ↥s), x * y = y * x) :
NonUnitalCommRing ↥s.topologicalClosure

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

See note [reducible non-instances]

Equations

- s.nonUnitalCommRingTopologicalClosure hs = { toNonUnitalRing := s.topologicalClosure.toNonUnitalRing, mul_comm := ⋯ }

Instances For

source
instance Subring.instIsTopologicalRing {R : Type u_1} [TopologicalSpace R] [Ring R] [IsTopologicalRing R] (S : Subring R) :
IsTopologicalRing ↥S
source
instance Subring.continuousSMul {R : Type u_1} [TopologicalSpace R] [Ring R] (s : Subring R) (X : Type u_2) [TopologicalSpace X] [MulAction R X] [ContinuousSMul R X] :
ContinuousSMul (↥s) X
source
def Subring.topologicalClosure {R : Type u_1} [TopologicalSpace R] [Ring R] [IsTopologicalRing R] (S : Subring R) :
Subring R

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

Equations

- S.topologicalClosure = { carrier := closure ↑S, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

Instances For

source
theorem Subring.le_topologicalClosure {R : Type u_1} [TopologicalSpace R] [Ring R] [IsTopologicalRing R] (s : Subring R) :
s ≤ s.topologicalClosure
source
theorem Subring.isClosed_topologicalClosure {R : Type u_1} [TopologicalSpace R] [Ring R] [IsTopologicalRing R] (s : Subring R) :
IsClosed ↑s.topologicalClosure
source
theorem Subring.topologicalClosure_minimal {R : Type u_1} [TopologicalSpace R] [Ring R] [IsTopologicalRing R] (s : Subring R) {t : Subring R} (h : s ≤ t) (ht : IsClosed ↑t) :
s.topologicalClosure ≤ t
source
@[reducible, inline]
abbrev Subring.commRingTopologicalClosure {R : Type u_1} [TopologicalSpace R] [Ring R] [IsTopologicalRing R] [T2Space R] (s : Subring R) (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.

See note [reducible non-instances].

Equations

- s.commRingTopologicalClosure hs = { toRing := s.topologicalClosure.toRing, mul_comm := ⋯ }

Instances For

### Lattice of ring topologies #

We define a type class `RingTopology R` which endows a ring `R` with a topology such that all ring operations are continuous.

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

Any function `f : R → S` induces `coinduced f : TopologicalSpace R → RingTopology S`.

source
structure RingTopology (R : Type u) [Ring R] extends TopologicalSpace R, IsTopologicalRing R :
Type u

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

- IsOpen : Set R → Prop
- isOpen_univ : TopologicalSpace.IsOpen Set.univ
- isOpen_inter (s t : Set R) : TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
- isOpen_sUnion (s : Set (Set R)) : (∀ t ∈ s, TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s)
- continuous_add : Continuous fun (p : R × R) => p.1 + p.2
- continuous_mul : Continuous fun (p : R × R) => p.1 * p.2
- continuous_neg : Continuous fun (a : R) => -a

Instances For

source
instance RingTopology.inhabited {R : Type u} [Ring R] :
Inhabited (RingTopology R)
Equations

- RingTopology.inhabited = { default := let x := ⊤; { toTopologicalSpace := x, toIsTopologicalRing := ⋯ } }

source
theorem RingTopology.toTopologicalSpace_injective {R : Type u_1} [Ring R] :
Function.Injective toTopologicalSpace
source
theorem RingTopology.ext {R : Type u_1} [Ring R] {f g : RingTopology R} (h : TopologicalSpace.IsOpen = TopologicalSpace.IsOpen) :
f = g
source
theorem RingTopology.ext_iff {R : Type u_1} [Ring R] {f g : RingTopology R} :
f = g ↔ TopologicalSpace.IsOpen = TopologicalSpace.IsOpen
source
instance RingTopology.instPartialOrder {R : Type u_1} [Ring R] :
PartialOrder (RingTopology R)

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

Equations

- RingTopology.instPartialOrder = PartialOrder.lift RingTopology.toTopologicalSpace ⋯

source
instance RingTopology.instCompleteSemilatticeInf {R : Type u_1} [Ring R] :
CompleteSemilatticeInf (RingTopology R)

Ring topologies on `R` 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 = { toPartialOrder := RingTopology.instPartialOrder, sInf := RingTopology.def_sInf✝, sInf_le := ⋯, le_sInf := ⋯ }

source
instance RingTopology.instCompleteLattice {R : Type u_1} [Ring R] :
CompleteLattice (RingTopology R)
Equations

- RingTopology.instCompleteLattice = completeLatticeOfCompleteSemilatticeInf (RingTopology R)

source
def RingTopology.coinduced {R : Type u_2} {S : Type u_3} [t : TopologicalSpace R] [Ring S] (f : R → S) :
RingTopology S

Given `f : R → S` and a topology on `R`, the coinduced ring topology on `S` is the finest topology such that `f` is continuous and `S` is a topological ring.

Equations

- RingTopology.coinduced f = sInf {b : RingTopology S | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}

Instances For

source
theorem RingTopology.coinduced_continuous {R : Type u_2} {S : Type u_3} [t : TopologicalSpace R] [Ring S] (f : R → S) :
Continuous f
source
def RingTopology.toAddGroupTopology {R : Type u_1} [Ring R] (t : RingTopology R) :
AddGroupTopology R

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

Equations

- t.toAddGroupTopology = { toTopologicalSpace := t.toTopologicalSpace, toIsTopologicalAddGroup := ⋯ }

Instances For

source
def RingTopology.toAddGroupTopology.orderEmbedding {R : Type u_1} [Ring R] :
RingTopology R ↪o AddGroupTopology R

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

Equations

- RingTopology.toAddGroupTopology.orderEmbedding = OrderEmbedding.ofMapLEIff RingTopology.toAddGroupTopology ⋯

Instances For

source
def AbsoluteValue.comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [Semiring T] [Semiring R] [Semiring S] [PartialOrder S] (v : AbsoluteValue R S) {f : T →+* R} (hf : Function.Injective ⇑f) :
AbsoluteValue T S

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

- v.comp hf = { toMulHom := v.comp ↑f, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ }

Instances For