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

    Instances

      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)

        Instances

          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.

          @[instance 50]
          Equations
          • =

          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
            @[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
            def 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.

            Equations
            Instances For

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

              Equations
              • =

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

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

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

              Equations
              • =

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

                Equations
                Instances For

                  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 :

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

                    Instances For
                      Equations
                      • RingTopology.inhabited = { default := let x := ; { toTopologicalSpace := x, toTopologicalRing := } }
                      theorem RingTopology.toTopologicalSpace_injective {α : Type u_1} [Ring α] :
                      Function.Injective RingTopology.toTopologicalSpace
                      theorem RingTopology.ext_iff {α : Type u_1} [Ring α] {f : RingTopology α} {g : RingTopology α} :
                      f = g TopologicalSpace.IsOpen = TopologicalSpace.IsOpen
                      theorem RingTopology.ext {α : Type u_1} [Ring α] {f : RingTopology α} {g : RingTopology α} (h : TopologicalSpace.IsOpen = TopologicalSpace.IsOpen) :
                      f = g

                      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

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

                      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
                      Instances For
                        theorem RingTopology.coinduced_continuous {α : Type u_2} {β : Type u_3} [t : TopologicalSpace α] [Ring β] (f : αβ) :

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

                        Equations
                        • t.toAddGroupTopology = { toTopologicalSpace := t.toTopologicalSpace, toTopologicalAddGroup := }
                        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] [OrderedSemiring 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
                            • v.comp hf = { toMulHom := v.comp f, nonneg' := , eq_zero' := , add_le' := }
                            Instances For