Documentation

Mathlib.Topology.Algebra.Ring.Basic

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 #

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

Instances
    @[deprecated IsTopologicalSemiring (since := "2025-02-14")]

    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)

        Instances
          @[deprecated IsTopologicalRing (since := "2025-02-14")]

          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.

              @[deprecated IsTopologicalSemiring.toIsTopologicalRing (since := "2025-02-14")]

              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
                Instances For
                  @[reducible, inline]

                  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
                    Instances For

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

                      Equations
                        Instances For
                          @[reducible, inline]

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

                          See note [reducible non-instances].

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

                              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)
                              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)
                              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)
                              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)) :
                              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)) :

                              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
                                Instances For
                                  @[reducible, inline]

                                  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
                                    Instances For
                                      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] :

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

                                      Equations
                                        Instances For
                                          @[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) :

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

                                          See note [reducible non-instances].

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

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

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

                                              Instances For
                                                Equations

                                                  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

                                                    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
                                                      def RingTopology.coinduced {R : Type u_2} {S : Type u_3} [t : TopologicalSpace R] [Ring S] (f : RS) :

                                                      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
                                                          theorem RingTopology.coinduced_continuous {R : Type u_2} {S : Type u_3} [t : TopologicalSpace R] [Ring S] (f : RS) :

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

                                                          Equations
                                                            Instances For

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

                                                              Equations
                                                                Instances For
                                                                  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) :

                                                                  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
                                                                    Instances For