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.topological_closure
/subsemiring.topological_closure
: the topological closure of asubring
/subsemiring
is itself asub(semi)ring
.prod.topological_semiring
/prod.topological_ring
: The product of two topological (semi)rings.pi.topological_semiring
/pi.topological_ring
: The arbitrary product of topological (semi)rings.ideal.closure
: The closure of an ideal is an ideal.topological_ring_quotient
: The quotient of a topological semiring by an ideal is a topological ring.
- to_has_continuous_add : has_continuous_add α
- to_has_continuous_mul : has_continuous_mul α
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 topological_semiring
class should only be instantiated in the presence of a
non_unital_non_assoc_semiring
instance; if there is an instance of non_unital_non_assoc_ring
,
then topological_ring
should be used. Note: in the presence of non_assoc_ring
, these classes are
mathematically equivalent (see topological_semiring.has_continuous_neg_of_mul
or
topological_semiring.to_topological_ring
).
Instances of this typeclass
- discrete_topology.topological_semiring
- topological_ring.to_topological_semiring
- subsemiring.topological_semiring
- prod.topological_semiring
- pi.topological_semiring
- mul_opposite.topological_semiring
- add_opposite.topological_semiring
- nnreal.topological_semiring
- matrix.topological_semiring
- subalgebra.topological_semiring
- to_topological_semiring : topological_semiring α
- to_has_continuous_neg : has_continuous_neg α
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
topological_semiring.has_continuous_neg_of_mul
and
topological_semiring.to_topological_add_group
)
Instances of this typeclass
- discrete_topology.topological_ring
- topological_division_ring.to_topological_ring
- semi_normed_top_ring
- ring_filter_basis.is_topological_ring
- nonarchimedean_ring.to_topological_ring
- valued.topological_ring
- prod.topological_ring
- pi.topological_ring
- mul_opposite.topological_ring
- add_opposite.topological_ring
- subring.topological_ring
- topological_ring_quotient
- real.topological_ring
- rat.topological_ring
- matrix.topological_ring
- TopCommRing.is_topological_ring
- TopCommRing.forget_topological_ring
- TopCommRing.forget_to_Top_topological_ring
- uniform_space.completion.top_ring_compl
- uniform_space.topological_ring
- function.topological_ring
- pi.matrix_topological_ring
- localization.topological_ring
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
.
The (topological-space) closure of a subsemiring of a topological semiring is itself a subsemiring.
If a subsemiring of a topological semiring is commutative, then so is its topological closure.
Equations
- s.comm_semiring_topological_closure hs = {add := semiring.add s.topological_closure.to_semiring, add_assoc := _, zero := semiring.zero s.topological_closure.to_semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul s.topological_closure.to_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul s.topological_closure.to_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one s.topological_closure.to_semiring, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast s.topological_closure.to_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow s.topological_closure.to_semiring, npow_zero' := _, npow_succ' := _, mul_comm := _}
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 add_monoid_hom
is continuous.
In a topological semiring, the right-multiplication add_monoid_hom
is continuous.
The (topological-space) closure of a subring of a topological ring is itself a subring.
If a subring of a topological ring is commutative, then so is its topological closure.
Equations
- s.comm_ring_topological_closure hs = {add := ring.add s.topological_closure.to_ring, add_assoc := _, zero := ring.zero s.topological_closure.to_ring, zero_add := _, add_zero := _, nsmul := ring.nsmul s.topological_closure.to_ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg s.topological_closure.to_ring, sub := ring.sub s.topological_closure.to_ring, sub_eq_add_neg := _, zsmul := ring.zsmul s.topological_closure.to_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast s.topological_closure.to_ring, nat_cast := ring.nat_cast s.topological_closure.to_ring, one := ring.one s.topological_closure.to_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul s.topological_closure.to_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow s.topological_closure.to_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
Equations
Lattice of ring topologies #
We define a type class ring_topology α
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 : topological_space α → ring_topology β
.
- to_topological_space : topological_space α
- to_topological_ring : topological_ring α
A ring topology on a ring α
is a topology for which addition, negation and multiplication
are continuous.
Instances for ring_topology
- ring_topology.has_sizeof_inst
- ring_topology.inhabited
- ring_topology.partial_order
- ring_topology.complete_semilattice_Inf
- ring_topology.complete_lattice
Equations
- ring_topology.inhabited = {default := {to_topological_space := ⊤, to_topological_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
).
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
- ring_topology.complete_semilattice_Inf = {le := partial_order.le ring_topology.partial_order, lt := partial_order.lt ring_topology.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, Inf := def_Inf _inst_1, Inf_le := _, le_Inf := _}
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
- ring_topology.coinduced f = has_Inf.Inf {b : ring_topology β | topological_space.coinduced f t ≤ b.to_topological_space}
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
.
Equations
- ring_topology.to_add_group_topology.order_embedding = {to_embedding := {to_fun := λ (t : ring_topology α), t.to_add_group_topology, inj' := _}, map_rel_iff' := _}