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) [TopologicalSpace α] [NonUnitalNonAssocSemiring α] extends ContinuousAdd α, ContinuousMul α : 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 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).

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

class TopologicalRing (α : Type u_1) [TopologicalSpace α] [NonUnitalNonAssocRing α] extends TopologicalSemiring α, ContinuousNeg α : 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 TopologicalSemiring.continuousNeg_of_mul and topological_semiring.to_topological_add_group)

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

theorem TopologicalSemiring.continuousNeg_of_mul {α : Type u_1} [TopologicalSpace α] [NonAssocRing α] [ContinuousMul α] : ContinuousNeg α

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} [TopologicalSpace α] [NonAssocRing α] : TopologicalSemiring α → TopologicalRing α

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} [NonUnitalNonAssocRing α] [TopologicalSpace α] [TopologicalRing α] : TopologicalAddGroup α

Equations

• ⋯ = ⋯

@[instance 50]

instance DiscreteTopology.topologicalSemiring {α : Type u_1} [TopologicalSpace α] [NonUnitalNonAssocSemiring α] [DiscreteTopology α] : TopologicalSemiring α

Equations

• ⋯ = ⋯

@[instance 50]

instance DiscreteTopology.topologicalRing {α : Type u_1} [TopologicalSpace α] [NonUnitalNonAssocRing α] [DiscreteTopology α] : TopologicalRing α

Equations

• ⋯ = ⋯

instance NonUnitalSubsemiring.instTopologicalSemiring {α : Type u_1} [TopologicalSpace α] [NonUnitalSemiring α] [TopologicalSemiring α] (S : NonUnitalSubsemiring α) : TopologicalSemiring ↥S

Equations

• ⋯ = ⋯

def NonUnitalSubsemiring.topologicalClosure {α : Type u_1} [TopologicalSpace α] [NonUnitalSemiring α] [TopologicalSemiring α] (s : NonUnitalSubsemiring α) : NonUnitalSubsemiring α

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' := ⋯ }

@[simp]

theorem NonUnitalSubsemiring.topologicalClosure_coe {α : Type u_1} [TopologicalSpace α] [NonUnitalSemiring α] [TopologicalSemiring α] (s : NonUnitalSubsemiring α) : ↑s.topologicalClosure = closure ↑s

theorem NonUnitalSubsemiring.le_topologicalClosure {α : Type u_1} [TopologicalSpace α] [NonUnitalSemiring α] [TopologicalSemiring α] (s : NonUnitalSubsemiring α) : s ≤ s.topologicalClosure

theorem NonUnitalSubsemiring.isClosed_topologicalClosure {α : Type u_1} [TopologicalSpace α] [NonUnitalSemiring α] [TopologicalSemiring α] (s : NonUnitalSubsemiring α) : IsClosed ↑s.topologicalClosure

theorem NonUnitalSubsemiring.topologicalClosure_minimal {α : Type u_1} [TopologicalSpace α] [NonUnitalSemiring α] [TopologicalSemiring α] (s : NonUnitalSubsemiring α) {t : NonUnitalSubsemiring α} (h : s ≤ t) (ht : IsClosed ↑t) : s.topologicalClosure ≤ t

@[reducible, inline]

abbrev NonUnitalSubsemiring.nonUnitalCommSemiringTopologicalClosure {α : Type u_1} [TopologicalSpace α] [NonUnitalSemiring α] [TopologicalSemiring α] [T2Space α] (s : NonUnitalSubsemiring α) (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 = NonUnitalCommSemiring.mk ⋯

instance instTopologicalSemiringULift {α : Type u_1} [TopologicalSpace α] [Semiring α] [TopologicalSemiring α] : TopologicalSemiring (ULift.{u_2, u_1} α)

Equations

• ⋯ = ⋯

instance Subsemiring.topologicalSemiring {α : Type u_1} [TopologicalSpace α] [Semiring α] [TopologicalSemiring α] (S : Subsemiring α) : TopologicalSemiring ↥S

Equations

• ⋯ = ⋯

def Subsemiring.topologicalClosure {α : Type u_1} [TopologicalSpace α] [Semiring α] [TopologicalSemiring α] (s : Subsemiring α) : Subsemiring α

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' := ⋯ }

@[simp]

theorem Subsemiring.topologicalClosure_coe {α : Type u_1} [TopologicalSpace α] [Semiring α] [TopologicalSemiring α] (s : Subsemiring α) : ↑s.topologicalClosure = closure ↑s

theorem Subsemiring.le_topologicalClosure {α : Type u_1} [TopologicalSpace α] [Semiring α] [TopologicalSemiring α] (s : Subsemiring α) : s ≤ s.topologicalClosure

theorem Subsemiring.isClosed_topologicalClosure {α : Type u_1} [TopologicalSpace α] [Semiring α] [TopologicalSemiring α] (s : Subsemiring α) : IsClosed ↑s.topologicalClosure

theorem Subsemiring.topologicalClosure_minimal {α : Type u_1} [TopologicalSpace α] [Semiring α] [TopologicalSemiring α] (s : Subsemiring α) {t : Subsemiring α} (h : s ≤ t) (ht : IsClosed ↑t) : s.topologicalClosure ≤ t

@[reducible, inline]

abbrev Subsemiring.commSemiringTopologicalClosure {α : Type u_1} [TopologicalSpace α] [Semiring α] [TopologicalSemiring α] [T2Space α] (s : Subsemiring α) (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 = CommSemiring.mk ⋯

instance instTopologicalSemiringProd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [TopologicalSemiring α] [TopologicalSemiring β] : TopologicalSemiring (α × β)

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} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalNonAssocRing α] [NonUnitalNonAssocRing β] [TopologicalRing α] [TopologicalRing β] : TopologicalRing (α × β)

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 : β) → NonUnitalNonAssocSemiring (C 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 : β) → NonUnitalNonAssocSemiring (C 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 : β) → NonUnitalNonAssocRing (C b)] [∀ (b : β), TopologicalRing (C b)] : TopologicalRing ((b : β) → C b)

Equations

• ⋯ = ⋯

instance instContinuousAddMulOpposite {α : Type u_1} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [ContinuousAdd α] : ContinuousAdd αᵐᵒᵖ

Equations

• ⋯ = ⋯

instance instTopologicalSemiringMulOpposite {α : Type u_1} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] : TopologicalSemiring αᵐᵒᵖ

Equations

• ⋯ = ⋯

instance instContinuousNegMulOpposite {α : Type u_1} [NonUnitalNonAssocRing α] [TopologicalSpace α] [ContinuousNeg α] : ContinuousNeg αᵐᵒᵖ

Equations

• ⋯ = ⋯

instance instTopologicalRingMulOpposite {α : Type u_1} [NonUnitalNonAssocRing α] [TopologicalSpace α] [TopologicalRing α] : TopologicalRing αᵐᵒᵖ

Equations

• ⋯ = ⋯

instance instContinuousMulAddOpposite {α : Type u_1} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [ContinuousMul α] : ContinuousMul αᵃᵒᵖ

Equations

• ⋯ = ⋯

instance instTopologicalSemiringAddOpposite {α : Type u_1} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] : TopologicalSemiring αᵃᵒᵖ

Equations

• ⋯ = ⋯

instance instTopologicalRingAddOpposite {α : Type u_1} [NonUnitalNonAssocRing α] [TopologicalSpace α] [TopologicalRing α] : TopologicalRing αᵃᵒᵖ

Equations

• ⋯ = ⋯

theorem TopologicalRing.of_addGroup_of_nhds_zero {R : Type u_2} [NonUnitalNonAssocRing R] [TopologicalSpace R] [TopologicalAddGroup 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)) : TopologicalRing R

theorem TopologicalRing.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)) : TopologicalRing R

instance instTopologicalRingULift {α : Type u_1} [TopologicalSpace α] [NonUnitalNonAssocRing α] [TopologicalRing α] : TopologicalRing (ULift.{u_2, u_1} α)

Equations

• ⋯ = ⋯

theorem mulLeft_continuous {α : Type u_1} [TopologicalSpace α] [NonUnitalNonAssocRing α] [TopologicalRing α] (x : α) : Continuous ⇑(AddMonoidHom.mulLeft x)

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

theorem mulRight_continuous {α : Type u_1} [TopologicalSpace α] [NonUnitalNonAssocRing α] [TopologicalRing α] (x : α) : Continuous ⇑(AddMonoidHom.mulRight x)

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

instance NonUnitalSubring.instTopologicalRing {α : Type u_1} [TopologicalSpace α] [NonUnitalRing α] [TopologicalRing α] (S : NonUnitalSubring α) : TopologicalRing ↥S

Equations

• ⋯ = ⋯

def NonUnitalSubring.topologicalClosure {α : Type u_1} [TopologicalSpace α] [NonUnitalRing α] [TopologicalRing α] (S : NonUnitalSubring α) : NonUnitalSubring α

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' := ⋯ }

theorem NonUnitalSubring.le_topologicalClosure {α : Type u_1} [TopologicalSpace α] [NonUnitalRing α] [TopologicalRing α] (s : NonUnitalSubring α) : s ≤ s.topologicalClosure

theorem NonUnitalSubring.isClosed_topologicalClosure {α : Type u_1} [TopologicalSpace α] [NonUnitalRing α] [TopologicalRing α] (s : NonUnitalSubring α) : IsClosed ↑s.topologicalClosure

theorem NonUnitalSubring.topologicalClosure_minimal {α : Type u_1} [TopologicalSpace α] [NonUnitalRing α] [TopologicalRing α] (s : NonUnitalSubring α) {t : NonUnitalSubring α} (h : s ≤ t) (ht : IsClosed ↑t) : s.topologicalClosure ≤ t

@[reducible, inline]

abbrev NonUnitalSubring.nonUnitalCommRingTopologicalClosure {α : Type u_1} [TopologicalSpace α] [NonUnitalRing α] [TopologicalRing α] [T2Space α] (s : NonUnitalSubring α) (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 = NonUnitalCommRing.mk ⋯

instance Subring.instTopologicalRing {α : Type u_1} [TopologicalSpace α] [Ring α] [TopologicalRing α] (S : Subring α) : TopologicalRing ↥S

Equations

• ⋯ = ⋯

def Subring.topologicalClosure {α : Type u_1} [TopologicalSpace α] [Ring α] [TopologicalRing α] (S : Subring α) : Subring α

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' := ⋯ }

theorem Subring.le_topologicalClosure {α : Type u_1} [TopologicalSpace α] [Ring α] [TopologicalRing α] (s : Subring α) : s ≤ s.topologicalClosure

theorem Subring.isClosed_topologicalClosure {α : Type u_1} [TopologicalSpace α] [Ring α] [TopologicalRing α] (s : Subring α) : IsClosed ↑s.topologicalClosure

theorem Subring.topologicalClosure_minimal {α : Type u_1} [TopologicalSpace α] [Ring α] [TopologicalRing α] (s : Subring α) {t : Subring α} (h : s ≤ t) (ht : IsClosed ↑t) : s.topologicalClosure ≤ t

@[reducible, inline]

abbrev Subring.commRingTopologicalClosure {α : Type u_1} [TopologicalSpace α] [Ring α] [TopologicalRing α] [T2Space α] (s : Subring α) (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 = CommRing.mk ⋯

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 TopologicalSpace α, TopologicalRing α : Type u

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

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

instance RingTopology.inhabited {α : Type u} [Ring α] : Inhabited (RingTopology α)

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 : RingTopology α} (h : TopologicalSpace.IsOpen = TopologicalSpace.IsOpen) : f = g

instance RingTopology.instPartialOrder {α : Type u_1} [Ring α] : PartialOrder (RingTopology α)

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

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

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

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 = CompleteSemilatticeInf.mk ⋯ ⋯

instance RingTopology.instCompleteLattice {α : Type u_1} [Ring α] : CompleteLattice (RingTopology α)

Equations

• RingTopology.instCompleteLattice = completeLatticeOfCompleteSemilatticeInf (RingTopology α)

def RingTopology.coinduced {α : Type u_2} {β : Type u_3} [t : TopologicalSpace α] [Ring β] (f : α → β) : RingTopology β

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

• RingTopology.coinduced f = sInf {b : RingTopology β | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}

theorem RingTopology.coinduced_continuous {α : Type u_2} {β : Type u_3} [t : TopologicalSpace α] [Ring β] (f : α → β) : Continuous f

def RingTopology.toAddGroupTopology {α : Type u_1} [Ring α] (t : RingTopology α) : AddGroupTopology α

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

Equations

• t.toAddGroupTopology = { toTopologicalSpace := t.toTopologicalSpace, toTopologicalAddGroup := ⋯ }

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

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

Equations

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

def AbsoluteValue.comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [Semiring T] [Semiring R] [OrderedSemiring 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' := ⋯ }