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 aSubring/Subsemiringis itself aSub(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.
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
Alias of IsTopologicalSemiring.
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).
Equations
Instances For
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
Alias of IsTopologicalRing.
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)
Equations
Instances For
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.
Alias of IsTopologicalSemiring.toIsTopologicalRing.
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.
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
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
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
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
The product topology on the cartesian product of two topological semirings makes the product into a topological semiring.
The product topology on the cartesian product of two topological rings makes the product into a topological ring.
In a topological semiring, the left-multiplication AddMonoidHom is continuous.
In a topological semiring, the right-multiplication AddMonoidHom is continuous.
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
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
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
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.
A ring topology on a ring R is a topology for which addition, negation and multiplication
are continuous.
- 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
Equations
- RingTopology.inhabited = { default := let x := ⊤; { toTopologicalSpace := x, toIsTopologicalRing := ⋯ } }
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).
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 := ⋯ }
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
Instances For
The forgetful functor from ring topologies on a to additive group topologies on a.
Equations
- t.toAddGroupTopology = { toTopologicalSpace := t.toTopologicalSpace, toIsTopologicalAddGroup := ⋯ }
Instances For
The order embedding from ring topologies on a to additive group topologies on a.
Equations
Instances For
Construct an absolute value on a semiring T from an absolute value on a semiring R
and an injective ring homomorphism f : T →+* R