Mathlib.Topology.Algebra.Ring.Basic

IsTopologicalSemiring structure

[TopologicalSpace R] [NonUnitalNonAssocSemiring R] : Prop
    extends ContinuousAdd R, ContinuousMul R

Full source

/-- 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`). -/
class IsTopologicalSemiring [TopologicalSpace R] [NonUnitalNonAssocSemiring R] : Prop
    extends ContinuousAdd R, ContinuousMul R

Topological semiring

Informal description

A topological semiring is a semiring $ R $ equipped with a topology such that both addition and multiplication are continuous operations. This definition applies to non-unital and non-associative semirings as well.

IsTopologicalRing structure

[TopologicalSpace R] [NonUnitalNonAssocRing R] : Prop
    extends IsTopologicalSemiring R, ContinuousNeg R

Full source

/-- 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`) -/
class IsTopologicalRing [TopologicalSpace R] [NonUnitalNonAssocRing R] : Prop
    extends IsTopologicalSemiring R, ContinuousNeg R

Topological ring

Informal description

A topological ring is a non-unital non-associative ring $ R $ equipped with a topology such that the operations of addition, multiplication, and negation are continuous.

IsTopologicalSemiring.continuousNeg_of_mul theorem

[TopologicalSpace R] [NonAssocRing R] [ContinuousMul R] : ContinuousNeg R

Full source

/-- If `R` is a ring with a continuous multiplication, then negation is continuous as well since it
is just multiplication with `-1`. -/
theorem IsTopologicalSemiring.continuousNeg_of_mul [TopologicalSpace R] [NonAssocRing R]
    [ContinuousMul R] : ContinuousNeg R where
  continuous_neg := by
    simpa using (continuous_const.mul continuous_id : Continuous fun x : R => -1 * x)

Continuity of Negation via Multiplication in Topological Rings

Informal description

Let $R$ be a topological space equipped with a non-associative ring structure. If the multiplication operation on $R$ is continuous, then the negation operation $x \mapsto -x$ is also continuous.

IsTopologicalSemiring.toIsTopologicalRing theorem

[TopologicalSpace R] [NonAssocRing R] (_ : IsTopologicalSemiring R) : IsTopologicalRing R

Full source

/-- 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`. -/
theorem IsTopologicalSemiring.toIsTopologicalRing [TopologicalSpace R] [NonAssocRing R]
    (_ : IsTopologicalSemiring R) : IsTopologicalRing R where
  toContinuousNeg := IsTopologicalSemiring.continuousNeg_of_mul

Topological Semiring Implies Topological Ring

Informal description

Let $R$ be a topological space equipped with a non-associative ring structure. If $R$ is a topological semiring (i.e., addition and multiplication are continuous), then $R$ is automatically a topological ring (i.e., negation is also continuous).

IsTopologicalRing.to_topologicalAddGroup instance

[NonUnitalNonAssocRing R] [TopologicalSpace R] [IsTopologicalRing R] : IsTopologicalAddGroup R

Full source

instance (priority := 100) IsTopologicalRing.to_topologicalAddGroup [NonUnitalNonAssocRing R]
    [TopologicalSpace R] [IsTopologicalRing R] : IsTopologicalAddGroup R := ⟨⟩

Topological Rings are Topological Additive Groups

Informal description

For any topological ring $R$ (a non-unital non-associative ring with a topology where addition, multiplication, and negation are continuous), the additive group structure on $R$ is also topological, meaning addition and negation are continuous operations.

DiscreteTopology.topologicalSemiring instance

[TopologicalSpace R] [NonUnitalNonAssocSemiring R] [DiscreteTopology R] : IsTopologicalSemiring R

Full source

instance (priority := 50) DiscreteTopology.topologicalSemiring [TopologicalSpace R]
    [NonUnitalNonAssocSemiring R] [DiscreteTopology R] : IsTopologicalSemiring R := ⟨⟩

Discrete Topological Spaces as Topological Semirings

Informal description

For any topological space $R$ with a non-unital non-associative semiring structure and discrete topology, $R$ is a topological semiring.

DiscreteTopology.topologicalRing instance

[TopologicalSpace R] [NonUnitalNonAssocRing R] [DiscreteTopology R] : IsTopologicalRing R

Full source

instance (priority := 50) DiscreteTopology.topologicalRing [TopologicalSpace R]
    [NonUnitalNonAssocRing R] [DiscreteTopology R] : IsTopologicalRing R := ⟨⟩

Discrete Topological Spaces as Topological Rings

Informal description

For any topological space $R$ with a non-unital non-associative ring structure and discrete topology, $R$ is a topological ring.

NonUnitalSubsemiring.instIsTopologicalSemiring instance

(S : NonUnitalSubsemiring R) : IsTopologicalSemiring S

Full source

instance instIsTopologicalSemiring (S : NonUnitalSubsemiring R) : IsTopologicalSemiring S :=
  { S.toSubsemigroup.continuousMul, S.toAddSubmonoid.continuousAdd with }

Topological Semiring Structure on Non-Unital Subsemirings

Informal description

For any non-unital subsemiring $S$ of a topological semiring $R$, the subspace topology on $S$ makes it a topological semiring, meaning both addition and multiplication are continuous operations on $S$.

NonUnitalSubsemiring.topologicalClosure definition

(s : NonUnitalSubsemiring R) : NonUnitalSubsemiring R

Full source

/-- The (topological) closure of a non-unital subsemiring of a non-unital topological semiring is
itself a non-unital subsemiring. -/
def topologicalClosure (s : NonUnitalSubsemiring R) : NonUnitalSubsemiring R :=
  { s.toSubsemigroup.topologicalClosure, s.toAddSubmonoid.topologicalClosure with
    carrier := _root_.closure (s : Set R) }

Topological closure of a non-unital subsemiring

Informal description

Given a non-unital subsemiring $s$ of a topological semiring $R$, the topological closure of $s$ is itself a non-unital subsemiring. The underlying set of the closure is the topological closure of the underlying set of $s$, and it inherits the algebraic structure from $s$.

NonUnitalSubsemiring.topologicalClosure_coe theorem

(s : NonUnitalSubsemiring R) : (s.topologicalClosure : Set R) = _root_.closure (s : Set R)

Full source

@[simp]
theorem topologicalClosure_coe (s : NonUnitalSubsemiring R) :
    (s.topologicalClosure : Set R) = _root_.closure (s : Set R) :=
  rfl

Equality of Subsemiring Closure and Set Closure

Informal description

For any non-unital subsemiring $s$ of a topological semiring $R$, the underlying set of the topological closure of $s$ is equal to the topological closure of the underlying set of $s$ in $R$. In other words, $(s.\text{topologicalClosure}) = \overline{s}$ where $\overline{s}$ denotes the closure of $s$ as a subset of $R$.

NonUnitalSubsemiring.le_topologicalClosure theorem

(s : NonUnitalSubsemiring R) : s ≤ s.topologicalClosure

Full source

theorem le_topologicalClosure (s : NonUnitalSubsemiring R) : s ≤ s.topologicalClosure :=
  _root_.subset_closure

Subsemiring is Contained in its Topological Closure

Informal description

For any non-unital subsemiring $s$ of a topological semiring $R$, the subsemiring $s$ is contained in its topological closure, i.e., $s \subseteq \overline{s}$.

NonUnitalSubsemiring.isClosed_topologicalClosure theorem

(s : NonUnitalSubsemiring R) : IsClosed (s.topologicalClosure : Set R)

Full source

theorem isClosed_topologicalClosure (s : NonUnitalSubsemiring R) :
    IsClosed (s.topologicalClosure : Set R) := isClosed_closure

Topological Closure of Non-Unital Subsemiring is Closed

Informal description

For any non-unital subsemiring $s$ of a topological semiring $R$, the topological closure of $s$ is a closed subset of $R$.

NonUnitalSubsemiring.topologicalClosure_minimal theorem

 (s : NonUnitalSubsemiring R) {t : NonUnitalSubsemiring R} (h : s ≤ t) (ht : IsClosed (t : Set R)) :
  s.topologicalClosure ≤ t

Full source

theorem topologicalClosure_minimal (s : NonUnitalSubsemiring R) {t : NonUnitalSubsemiring R}
    (h : s ≤ t) (ht : IsClosed (t : Set R)) : s.topologicalClosure ≤ t :=
  closure_minimal h ht

Minimality of Topological Closure for Non-Unital Subsemirings: $\overline{s} \leq t$ when $s \leq t$ and $t$ is closed

Informal description

For any non-unital subsemiring $s$ of a topological semiring $R$, and any non-unital subsemiring $t$ such that $s \leq t$ and $t$ is closed in the topology of $R$, the topological closure of $s$ is contained in $t$.

NonUnitalSubsemiring.nonUnitalCommSemiringTopologicalClosure abbrev

[T2Space R] (s : NonUnitalSubsemiring R) (hs : ∀ x y : s, x * y = y * x) : NonUnitalCommSemiring s.topologicalClosure

Full source

/-- If a non-unital subsemiring of a non-unital topological semiring is commutative, then so is its
topological closure.

See note [reducible non-instances] -/
abbrev nonUnitalCommSemiringTopologicalClosure [T2Space R] (s : NonUnitalSubsemiring R)
    (hs : ∀ x y : s, x * y = y * x) : NonUnitalCommSemiring s.topologicalClosure :=
  { NonUnitalSubsemiringClass.toNonUnitalSemiring s.topologicalClosure,
    s.toSubsemigroup.commSemigroupTopologicalClosure hs with }

Commutativity of Topological Closure for Non-Unital Commutative Subsemirings

Informal description

Let $R$ be a Hausdorff topological semiring and $s$ a non-unital subsemiring of $R$ such that $x \cdot y = y \cdot x$ for all $x, y \in s$. Then the topological closure of $s$ is a non-unital commutative semiring.

instIsTopologicalSemiringULift instance

: IsTopologicalSemiring (ULift R)

Full source

instance : IsTopologicalSemiring (ULift R) where

Topological Semiring Structure on Lifted Types

Informal description

For any topological semiring $R$, the lifted type $\mathrm{ULift}\, R$ is also a topological semiring, where both addition and multiplication are continuous operations.

Subsemiring.topologicalSemiring instance

(S : Subsemiring R) : IsTopologicalSemiring S

Full source

instance topologicalSemiring (S : Subsemiring R) : IsTopologicalSemiring S :=
  { S.toSubmonoid.continuousMul, S.toAddSubmonoid.continuousAdd with }

Topological Semiring Structure on Subsemirings

Informal description

For any subsemiring $S$ of a topological semiring $R$, the subsemiring $S$ equipped with the subspace topology is also a topological semiring, meaning both addition and multiplication are continuous operations on $S$.

Subsemiring.continuousSMul instance

(s : Subsemiring R) (X) [TopologicalSpace X] [MulAction R X] [ContinuousSMul R X] : ContinuousSMul s X

Full source

instance continuousSMul (s : Subsemiring R) (X) [TopologicalSpace X] [MulAction R X]
    [ContinuousSMul R X] : ContinuousSMul s X :=
  Submonoid.continuousSMul

Continuous Scalar Multiplication by Subsemirings

Informal description

For any subsemiring $s$ of a topological semiring $R$, and any topological space $X$ with a continuous scalar multiplication action by $R$, the scalar multiplication action of $s$ on $X$ is also continuous.

Subsemiring.topologicalClosure definition

(s : Subsemiring R) : Subsemiring R

Full source

/-- The (topological-space) closure of a subsemiring of a topological semiring is
itself a subsemiring. -/
def Subsemiring.topologicalClosure (s : Subsemiring R) : Subsemiring R :=
  { s.toSubmonoid.topologicalClosure, s.toAddSubmonoid.topologicalClosure with
    carrier := _root_.closure (s : Set R) }

Topological closure of a subsemiring

Informal description

Given a subsemiring $ s $ of a topological semiring $ R $, the topological closure of $ s $ is itself a subsemiring of $ R $. The underlying set of this closure is the topological closure of the underlying set of $ s $, and it inherits the algebraic structure of a subsemiring.

Subsemiring.topologicalClosure_coe theorem

(s : Subsemiring R) : (s.topologicalClosure : Set R) = _root_.closure (s : Set R)

Full source

@[simp]
theorem Subsemiring.topologicalClosure_coe (s : Subsemiring R) :
    (s.topologicalClosure : Set R) = _root_.closure (s : Set R) :=
  rfl

Equality of Subsemiring Closure and Set Closure

Informal description

For any subsemiring $s$ of a topological semiring $R$, the underlying set of the topological closure of $s$ is equal to the topological closure of the underlying set of $s$ in $R$. In other words, $\overline{s} = \overline{(s : \text{Set } R)}$, where $\overline{\cdot}$ denotes the topological closure operator.

Subsemiring.le_topologicalClosure theorem

(s : Subsemiring R) : s ≤ s.topologicalClosure

Full source

theorem Subsemiring.le_topologicalClosure (s : Subsemiring R) : s ≤ s.topologicalClosure :=
  _root_.subset_closure

Subsemiring is Contained in its Topological Closure

Informal description

For any subsemiring $s$ of a topological semiring $R$, the subsemiring $s$ is contained in its topological closure, i.e., $s \subseteq \overline{s}$.

Subsemiring.isClosed_topologicalClosure theorem

(s : Subsemiring R) : IsClosed (s.topologicalClosure : Set R)

Full source

theorem Subsemiring.isClosed_topologicalClosure (s : Subsemiring R) :
    IsClosed (s.topologicalClosure : Set R) := isClosed_closure

Topological Closure of a Subsemiring is Closed

Informal description

For any subsemiring $s$ of a topological semiring $R$, the topological closure of $s$ is a closed subset of $R$.

Subsemiring.topologicalClosure_minimal theorem

(s : Subsemiring R) {t : Subsemiring R} (h : s ≤ t) (ht : IsClosed (t : Set R)) : s.topologicalClosure ≤ t

Full source

theorem Subsemiring.topologicalClosure_minimal (s : Subsemiring R) {t : Subsemiring R} (h : s ≤ t)
    (ht : IsClosed (t : Set R)) : s.topologicalClosure ≤ t :=
  closure_minimal h ht

Minimality of Topological Closure for Subsemirings: $\overline{s} \leq t$ when $s \leq t$ and $t$ is closed

Informal description

For any subsemiring $s$ of a topological semiring $R$, if $s$ is contained in another subsemiring $t$ and $t$ is closed in the topology of $R$, then the topological closure of $s$ is also contained in $t$. In other words, if $s \leq t$ and $t$ is closed, then $\overline{s} \leq t$.

Subsemiring.commSemiringTopologicalClosure abbrev

[T2Space R] (s : Subsemiring R) (hs : ∀ x y : s, x * y = y * x) : CommSemiring s.topologicalClosure

Full source

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

See note [reducible non-instances]. -/
abbrev Subsemiring.commSemiringTopologicalClosure [T2Space R] (s : Subsemiring R)
    (hs : ∀ x y : s, x * y = y * x) : CommSemiring s.topologicalClosure :=
  { s.topologicalClosure.toSemiring, s.toSubmonoid.commMonoidTopologicalClosure hs with }

Commutativity of Topological Closure for Commutative Subsemirings

Informal description

Let $R$ be a Hausdorff topological semiring and $s$ a subsemiring of $R$ such that $x \cdot y = y \cdot x$ for all $x, y \in s$. Then the topological closure of $s$ is a commutative semiring.

instIsTopologicalSemiringProd instance

 [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [IsTopologicalSemiring R] [IsTopologicalSemiring S] :
  IsTopologicalSemiring (R × S)

Full source

/-- The product topology on the cartesian product of two topological semirings
  makes the product into a topological semiring. -/
instance [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [IsTopologicalSemiring R]
    [IsTopologicalSemiring S] : IsTopologicalSemiring (R × S) where

Product of Topological Semirings is a Topological Semiring

Informal description

For any two topological semirings $R$ and $S$, the product space $R \times S$ equipped with the product topology is also a topological semiring. This means that both addition and multiplication operations on $R \times S$ are continuous with respect to the product topology.

instIsTopologicalRingProd instance

 [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [IsTopologicalRing R] [IsTopologicalRing S] :
  IsTopologicalRing (R × S)

Full source

/-- The product topology on the cartesian product of two topological rings
  makes the product into a topological ring. -/
instance [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [IsTopologicalRing R]
    [IsTopologicalRing S] : IsTopologicalRing (R × S) where

Product of Topological Rings is a Topological Ring

Informal description

For any two topological rings $R$ and $S$, the product space $R \times S$ equipped with the product topology is also a topological ring. This means that the operations of addition, multiplication, and negation on $R \times S$ are continuous with respect to the product topology.

instContinuousAddForallOfIsTopologicalSemiring instance

 {ι : Type*} {R : ι → Type*} [∀ i, TopologicalSpace (R i)] [∀ i, NonUnitalNonAssocSemiring (R i)]
  [∀ i, IsTopologicalSemiring (R i)] : ContinuousAdd ((i : ι) → R i)

Full source

instance {ι : Type*} {R : ι → Type*} [∀ i, TopologicalSpace (R i)]
    [∀ i, NonUnitalNonAssocSemiring (R i)] [∀ i, IsTopologicalSemiring (R i)] :
    ContinuousAdd ((i : ι) → R i) :=
  inferInstance

Continuity of Addition in Product of Topological Semirings

Informal description

For any family of topological semirings $\{R_i\}_{i \in \iota}$ indexed by a type $\iota$, the addition operation on the product space $\prod_{i \in \iota} R_i$ is continuous.

Pi.instIsTopologicalSemiring instance

 {ι : Type*} {R : ι → Type*} [∀ i, TopologicalSpace (R i)] [∀ i, NonUnitalNonAssocSemiring (R i)]
  [∀ i, IsTopologicalSemiring (R i)] : IsTopologicalSemiring (∀ i, R i)

Full source

instance Pi.instIsTopologicalSemiring {ι : Type*} {R : ι → Type*} [∀ i, TopologicalSpace (R i)]
    [∀ i, NonUnitalNonAssocSemiring (R i)] [∀ i, IsTopologicalSemiring (R i)] :
    IsTopologicalSemiring (∀ i, R i) where

Product of Topological Semirings is a Topological Semiring

Informal description

For any family of topological semirings $\{R_i\}_{i \in \iota}$ indexed by a type $\iota$, the product space $\prod_{i \in \iota} R_i$ is also a topological semiring, where both addition and multiplication are continuous operations.

Pi.instIsTopologicalRing instance

 {ι : Type*} {R : ι → Type*} [∀ i, TopologicalSpace (R i)] [∀ i, NonUnitalNonAssocRing (R i)]
  [∀ i, IsTopologicalRing (R i)] : IsTopologicalRing (∀ i, R i)

Full source

instance Pi.instIsTopologicalRing {ι : Type*} {R : ι → Type*} [∀ i, TopologicalSpace (R i)]
    [∀ i, NonUnitalNonAssocRing (R i)] [∀ i, IsTopologicalRing (R i)] :
    IsTopologicalRing (∀ i, R i) := ⟨⟩

Product of Topological Rings is a Topological Ring

Informal description

For any family of topological rings $\{R_i\}_{i \in \iota}$ indexed by a type $\iota$, the product space $\prod_{i \in \iota} R_i$ is also a topological ring, where addition, multiplication, and negation are continuous operations.

instContinuousAddMulOpposite instance

[NonUnitalNonAssocSemiring R] [TopologicalSpace R] [ContinuousAdd R] : ContinuousAdd Rᵐᵒᵖ

Full source

instance [NonUnitalNonAssocSemiring R] [TopologicalSpace R] [ContinuousAdd R] :
    ContinuousAdd Rᵐᵒᵖ :=
  continuousAdd_induced opAddEquiv.symm

Continuous Addition on the Multiplicative Opposite of a Topological Semiring

Informal description

For any topological non-unital non-associative semiring $R$ with continuous addition, the multiplicative opposite $R^{\text{op}}$ also has continuous addition.

instIsTopologicalSemiringMulOpposite instance

[NonUnitalNonAssocSemiring R] [TopologicalSpace R] [IsTopologicalSemiring R] : IsTopologicalSemiring Rᵐᵒᵖ

Full source

instance [NonUnitalNonAssocSemiring R] [TopologicalSpace R] [IsTopologicalSemiring R] :
    IsTopologicalSemiring Rᵐᵒᵖ := ⟨⟩

Topological Semiring Structure on the Multiplicative Opposite

Informal description

For any topological non-unital non-associative semiring $R$ where addition and multiplication are continuous, the multiplicative opposite $R^{\text{op}}$ is also a topological semiring with continuous addition and multiplication.

instContinuousNegMulOpposite instance

[NonUnitalNonAssocRing R] [TopologicalSpace R] [ContinuousNeg R] : ContinuousNeg Rᵐᵒᵖ

Full source

instance [NonUnitalNonAssocRing R] [TopologicalSpace R] [ContinuousNeg R] : ContinuousNeg Rᵐᵒᵖ :=
  opHomeomorph.symm.isInducing.continuousNeg fun _ => rfl

Continuous Negation on the Multiplicative Opposite of a Topological Ring

Informal description

For any topological non-unital non-associative ring $R$ with continuous negation, the multiplicative opposite $R^{\text{op}}$ also has continuous negation.

instIsTopologicalRingMulOpposite instance

[NonUnitalNonAssocRing R] [TopologicalSpace R] [IsTopologicalRing R] : IsTopologicalRing Rᵐᵒᵖ

Full source

instance [NonUnitalNonAssocRing R] [TopologicalSpace R] [IsTopologicalRing R] :
    IsTopologicalRing Rᵐᵒᵖ := ⟨⟩

Topological Ring Structure on the Multiplicative Opposite

Informal description

For any topological non-unital non-associative ring $R$ where addition, multiplication, and negation are continuous, the multiplicative opposite $R^{\text{op}}$ is also a topological ring with continuous addition, multiplication, and negation.

instContinuousMulAddOpposite instance

[NonUnitalNonAssocSemiring R] [TopologicalSpace R] [ContinuousMul R] : ContinuousMul Rᵃᵒᵖ

Full source

instance [NonUnitalNonAssocSemiring R] [TopologicalSpace R] [ContinuousMul R] :
    ContinuousMul Rᵃᵒᵖ :=
  continuousMul_induced opMulEquiv.symm

Continuous Multiplication on the Additive Opposite of a Topological Semiring

Informal description

For any non-unital non-associative semiring $R$ equipped with a topology such that multiplication is continuous, the additive opposite $R^{\text{aop}}$ also has continuous multiplication.

instIsTopologicalSemiringAddOpposite instance

[NonUnitalNonAssocSemiring R] [TopologicalSpace R] [IsTopologicalSemiring R] : IsTopologicalSemiring Rᵃᵒᵖ

Full source

instance [NonUnitalNonAssocSemiring R] [TopologicalSpace R] [IsTopologicalSemiring R] :
    IsTopologicalSemiring Rᵃᵒᵖ := ⟨⟩

Topological Semiring Structure on the Additive Opposite

Informal description

For any non-unital non-associative semiring $R$ equipped with a topology that makes it a topological semiring (i.e., addition and multiplication are continuous), the additive opposite $R^{\text{aop}}$ is also a topological semiring.

instIsTopologicalRingAddOpposite instance

[NonUnitalNonAssocRing R] [TopologicalSpace R] [IsTopologicalRing R] : IsTopologicalRing Rᵃᵒᵖ

Full source

instance [NonUnitalNonAssocRing R] [TopologicalSpace R] [IsTopologicalRing R] :
    IsTopologicalRing Rᵃᵒᵖ := ⟨⟩

Topological Ring Structure on the Additive Opposite

Informal description

For any non-unital non-associative topological ring $R$, the additive opposite $R^{\text{aop}}$ is also a topological ring. This means that the operations of addition, multiplication, and negation in $R^{\text{aop}}$ are continuous with respect to the induced topology.

IsTopologicalRing.of_addGroup_of_nhds_zero theorem

 [IsTopologicalAddGroup R] (hmul : Tendsto (uncurry ((· * ·) : R → R → R)) (𝓝 0 ×ˢ 𝓝 0) <| 𝓝 0)
  (hmul_left : ∀ x₀ : R, Tendsto (fun x : R => x₀ * x) (𝓝 0) <| 𝓝 0)
  (hmul_right : ∀ x₀ : R, Tendsto (fun x : R => x * x₀) (𝓝 0) <| 𝓝 0) : IsTopologicalRing R

Full source

theorem IsTopologicalRing.of_addGroup_of_nhds_zero [IsTopologicalAddGroup R]
    (hmul : Tendsto (uncurry ((· * ·) : R → R → R)) (𝓝 0 ×ˢ 𝓝 0) <| 𝓝 0)
    (hmul_left : ∀ x₀ : R, Tendsto (fun x : R => x₀ * x) (𝓝 0) <| 𝓝 0)
    (hmul_right : ∀ x₀ : R, Tendsto (fun x : R => x * x₀) (𝓝 0) <| 𝓝 0) : IsTopologicalRing R where
  continuous_mul := by
    refine continuous_of_continuousAt_zero₂ (AddMonoidHom.mul (R := R)) ?_ ?_ ?_ <;>
      simpa only [ContinuousAt, mul_zero, zero_mul, nhds_prod_eq, AddMonoidHom.mul_apply]

Sufficient Conditions for a Topological Additive Group to be a Topological Ring via Neighborhoods of Zero

Informal description

Let $R$ be a non-unital non-associative ring with a topology such that $R$ is a topological additive group. Suppose the following conditions hold: 1. The multiplication map $(x, y) \mapsto x * y$ tends to $0$ as $(x, y)$ tends to $(0, 0)$. 2. For every $x_0 \in R$, the left multiplication map $x \mapsto x_0 * x$ tends to $0$ as $x$ tends to $0$. 3. For every $x_0 \in R$, the right multiplication map $x \mapsto x * x_0$ tends to $0$ as $x$ tends to $0$. Then $R$ is a topological ring (i.e., addition, negation, and multiplication are continuous).

IsTopologicalRing.of_nhds_zero theorem

 (hadd : Tendsto (uncurry ((· + ·) : R → R → R)) (𝓝 0 ×ˢ 𝓝 0) <| 𝓝 0) (hneg : Tendsto (fun x => -x : R → R) (𝓝 0) (𝓝 0))
  (hmul : Tendsto (uncurry ((· * ·) : R → R → R)) (𝓝 0 ×ˢ 𝓝 0) <| 𝓝 0)
  (hmul_left : ∀ x₀ : R, Tendsto (fun x : R => x₀ * x) (𝓝 0) <| 𝓝 0)
  (hmul_right : ∀ x₀ : R, Tendsto (fun x : R => x * x₀) (𝓝 0) <| 𝓝 0)
  (hleft : ∀ x₀ : R, 𝓝 x₀ = map (fun x => x₀ + x) (𝓝 0)) : IsTopologicalRing R

Full source

theorem IsTopologicalRing.of_nhds_zero
    (hadd : Tendsto (uncurry ((· + ·) : R → R → R)) (𝓝 0 ×ˢ 𝓝 0) <| 𝓝 0)
    (hneg : Tendsto (fun x => -x : R → R) (𝓝 0) (𝓝 0))
    (hmul : Tendsto (uncurry ((· * ·) : R → R → R)) (𝓝 0 ×ˢ 𝓝 0) <| 𝓝 0)
    (hmul_left : ∀ x₀ : R, Tendsto (fun x : R => x₀ * x) (𝓝 0) <| 𝓝 0)
    (hmul_right : ∀ x₀ : R, Tendsto (fun x : R => x * x₀) (𝓝 0) <| 𝓝 0)
    (hleft : ∀ x₀ : R, 𝓝 x₀ = map (fun x => x₀ + x) (𝓝 0)) : IsTopologicalRing R :=
  have := IsTopologicalAddGroup.of_comm_of_nhds_zero hadd hneg hleft
  IsTopologicalRing.of_addGroup_of_nhds_zero hmul hmul_left hmul_right

Sufficient Conditions for a Topological Ring via Neighborhoods of Zero

Informal description

Let $R$ be a non-unital non-associative ring with a topology. Suppose the following conditions hold: 1. Addition is continuous at zero: $(x, y) \mapsto x + y$ tends to $0$ as $(x, y)$ tends to $(0, 0)$. 2. Negation is continuous at zero: $x \mapsto -x$ tends to $0$ as $x$ tends to $0$. 3. Multiplication is continuous at zero: $(x, y) \mapsto x * y$ tends to $0$ as $(x, y)$ tends to $(0, 0)$. 4. For every $x_0 \in R$, left multiplication $x \mapsto x_0 * x$ tends to $0$ as $x$ tends to $0$. 5. For every $x_0 \in R$, right multiplication $x \mapsto x * x_0$ tends to $0$ as $x$ tends to $0$. 6. The neighborhood filter at any $x_0 \in R$ is obtained by translating the neighborhood filter at $0$ via $x \mapsto x_0 + x$. Then $R$ is a topological ring (i.e., addition, negation, and multiplication are continuous everywhere).

instIsTopologicalRingULift instance

: IsTopologicalRing (ULift R)

Full source

instance : IsTopologicalRing (ULift R) where

Topological Ring Structure on Lifted Types

Informal description

For any topological ring $R$, the lifted type $\mathrm{ULift}\, R$ is also a topological ring, meaning that the operations of addition, multiplication, and negation are continuous with respect to the inherited topology.

mulLeft_continuous theorem

(x : R) : Continuous (AddMonoidHom.mulLeft x)

Full source

/-- In a topological semiring, the left-multiplication `AddMonoidHom` is continuous. -/
theorem mulLeft_continuous (x : R) : Continuous (AddMonoidHom.mulLeft x) :=
  continuous_const.mul continuous_id

Continuity of Left Multiplication in Topological Semirings

Informal description

For any element $x$ in a topological semiring $R$, the left-multiplication map $L_x \colon R \to R$ defined by $L_x(y) = x \cdot y$ is continuous.

mulRight_continuous theorem

(x : R) : Continuous (AddMonoidHom.mulRight x)

Full source

/-- In a topological semiring, the right-multiplication `AddMonoidHom` is continuous. -/
theorem mulRight_continuous (x : R) : Continuous (AddMonoidHom.mulRight x) :=
  continuous_id.mul continuous_const

Continuity of Right Multiplication in Topological Semirings

Informal description

For any element $x$ in a topological semiring $R$, the right-multiplication map $R_x \colon R \to R$ defined by $R_x(y) = y \cdot x$ is continuous.

NonUnitalSubring.instIsTopologicalRing instance

(S : NonUnitalSubring R) : IsTopologicalRing S

Full source

instance instIsTopologicalRing (S : NonUnitalSubring R) : IsTopologicalRing S :=
  { S.toSubsemigroup.continuousMul, inferInstanceAs (IsTopologicalAddGroup S.toAddSubgroup) with }

Subspace Topology Induces Topological Ring Structure on Non-unital Subrings

Informal description

For any non-unital subring $S$ of a topological ring $R$, the subspace topology on $S$ makes it a topological ring, meaning the operations of addition, multiplication, and negation are continuous with respect to this topology.

NonUnitalSubring.topologicalClosure definition

(S : NonUnitalSubring R) : NonUnitalSubring R

Full source

/-- The (topological) closure of a non-unital subring of a non-unital topological ring is
itself a non-unital subring. -/
def topologicalClosure (S : NonUnitalSubring R) : NonUnitalSubring R :=
  { S.toSubsemigroup.topologicalClosure, S.toAddSubgroup.topologicalClosure with
    carrier := _root_.closure (S : Set R) }

Topological closure of a non-unital subring

Informal description

Given a non-unital subring $ S $ of a non-unital topological ring $ R $, the topological closure of $ S $ is the smallest closed non-unital subring of $ R $ containing $ S $. It is constructed as the intersection of all closed subsets of $ R $ that contain $ S $ and are closed under addition, negation, and multiplication.

NonUnitalSubring.le_topologicalClosure theorem

(s : NonUnitalSubring R) : s ≤ s.topologicalClosure

Full source

theorem le_topologicalClosure (s : NonUnitalSubring R) : s ≤ s.topologicalClosure :=
  _root_.subset_closure

Inclusion of Non-unital Subring in its Topological Closure

Informal description

For any non-unital subring $s$ of a topological ring $R$, the subring $s$ is contained in its topological closure, i.e., $s \subseteq \overline{s}$.

NonUnitalSubring.isClosed_topologicalClosure theorem

(s : NonUnitalSubring R) : IsClosed (s.topologicalClosure : Set R)

Full source

theorem isClosed_topologicalClosure (s : NonUnitalSubring R) :
    IsClosed (s.topologicalClosure : Set R) := isClosed_closure

Topological Closure of Non-Unital Subring is Closed

Informal description

For any non-unital subring $s$ of a topological ring $R$, the topological closure $\overline{s}$ is a closed subset of $R$.

NonUnitalSubring.topologicalClosure_minimal theorem

 (s : NonUnitalSubring R) {t : NonUnitalSubring R} (h : s ≤ t) (ht : IsClosed (t : Set R)) : s.topologicalClosure ≤ t

Full source

theorem topologicalClosure_minimal (s : NonUnitalSubring R) {t : NonUnitalSubring R} (h : s ≤ t)
    (ht : IsClosed (t : Set R)) : s.topologicalClosure ≤ t :=
  closure_minimal h ht

Minimality of Topological Closure for Non-Unital Subrings

Informal description

Let $R$ be a topological ring and $s$ be a non-unital subring of $R$. For any non-unital subring $t$ of $R$ such that $s \subseteq t$ and $t$ is closed in the topology of $R$, the topological closure of $s$ is contained in $t$, i.e., $\overline{s} \subseteq t$.

NonUnitalSubring.nonUnitalCommRingTopologicalClosure abbrev

[T2Space R] (s : NonUnitalSubring R) (hs : ∀ x y : s, x * y = y * x) : NonUnitalCommRing s.topologicalClosure

Full source

/-- If a non-unital subring of a non-unital topological ring is commutative, then so is its
topological closure.

See note [reducible non-instances] -/
abbrev nonUnitalCommRingTopologicalClosure [T2Space R] (s : NonUnitalSubring R)
    (hs : ∀ x y : s, x * y = y * x) : NonUnitalCommRing s.topologicalClosure :=
  { s.topologicalClosure.toNonUnitalRing, s.toSubsemigroup.commSemigroupTopologicalClosure hs with }

Commutativity of Topological Closure for Commutative Non-unital Subrings

Informal description

Let $R$ be a Hausdorff topological ring and $s$ a non-unital subring of $R$ such that $x \cdot y = y \cdot x$ for all $x, y \in s$. Then the topological closure of $s$ in $R$ is a commutative non-unital topological ring.

Subring.instIsTopologicalRing instance

(S : Subring R) : IsTopologicalRing S

Full source

instance Subring.instIsTopologicalRing (S : Subring R) : IsTopologicalRing S :=
  { S.toSubmonoid.continuousMul, inferInstanceAs (IsTopologicalAddGroup S.toAddSubgroup) with }

Topological Ring Structure on Subrings

Informal description

For any subring $S$ of a topological ring $R$, the subring $S$ inherits a topological ring structure from $R$, where the ring operations (addition, multiplication, and negation) are continuous with respect to the subspace topology.

Subring.continuousSMul instance

(s : Subring R) (X) [TopologicalSpace X] [MulAction R X] [ContinuousSMul R X] : ContinuousSMul s X

Full source

instance Subring.continuousSMul (s : Subring R) (X) [TopologicalSpace X] [MulAction R X]
    [ContinuousSMul R X] : ContinuousSMul s X :=
  Subsemiring.continuousSMul s.toSubsemiring X

Continuous Scalar Multiplication by Subrings

Informal description

For any subring $s$ of a topological ring $R$, and any topological space $X$ with a continuous scalar multiplication action by $R$, the scalar multiplication action of $s$ on $X$ is also continuous.

Subring.topologicalClosure definition

(S : Subring R) : Subring R

Full source

/-- The (topological-space) closure of a subring of a topological ring is
itself a subring. -/
def Subring.topologicalClosure (S : Subring R) : Subring R :=
  { S.toSubmonoid.topologicalClosure, S.toAddSubgroup.topologicalClosure with
    carrier := _root_.closure (S : Set R) }

Topological closure of a subring

Informal description

Given a subring $ S $ of a topological ring $ R $, the topological closure of $ S $ is itself a subring of $ R $. The underlying set of this closure is the topological closure of the underlying set of $ S $, and it is closed under addition, multiplication, and contains the additive and multiplicative identities.

Subring.le_topologicalClosure theorem

(s : Subring R) : s ≤ s.topologicalClosure

Full source

theorem Subring.le_topologicalClosure (s : Subring R) : s ≤ s.topologicalClosure :=
  _root_.subset_closure

Subring is Contained in its Topological Closure

Informal description

For any subring $s$ of a topological ring $R$, the subring $s$ is contained in its topological closure, i.e., $s \subseteq \overline{s}$.

Subring.isClosed_topologicalClosure theorem

(s : Subring R) : IsClosed (s.topologicalClosure : Set R)

Full source

theorem Subring.isClosed_topologicalClosure (s : Subring R) :
    IsClosed (s.topologicalClosure : Set R) := isClosed_closure

Topological Closure of a Subring is Closed

Informal description

For any subring $S$ of a topological ring $R$, the topological closure $\overline{S}$ is a closed subset of $R$.

Subring.topologicalClosure_minimal theorem

(s : Subring R) {t : Subring R} (h : s ≤ t) (ht : IsClosed (t : Set R)) : s.topologicalClosure ≤ t

Full source

theorem Subring.topologicalClosure_minimal (s : Subring R) {t : Subring R} (h : s ≤ t)
    (ht : IsClosed (t : Set R)) : s.topologicalClosure ≤ t :=
  closure_minimal h ht

Minimality of Subring Closure: $\overline{s} \subseteq t$ for $s \subseteq t$ and $t$ closed

Informal description

Let $R$ be a topological ring and $s$ be a subring of $R$. For any subring $t$ of $R$ such that $s \subseteq t$ and $t$ is closed in the topology of $R$, the topological closure of $s$ is contained in $t$.

Subring.commRingTopologicalClosure abbrev

[T2Space R] (s : Subring R) (hs : ∀ x y : s, x * y = y * x) : CommRing s.topologicalClosure

Full source

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

See note [reducible non-instances]. -/
abbrev Subring.commRingTopologicalClosure [T2Space R] (s : Subring R)
    (hs : ∀ x y : s, x * y = y * x) : CommRing s.topologicalClosure :=
  { s.topologicalClosure.toRing, s.toSubmonoid.commMonoidTopologicalClosure hs with }

Commutativity of Topological Closure for Commutative Subrings

Informal description

Let $R$ be a Hausdorff topological ring. If $s$ is a subring of $R$ such that $x \cdot y = y \cdot x$ for all $x, y \in s$, then the topological closure of $s$ is a commutative ring.

RingTopology structure

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

Full source

/-- A ring topology on a ring `R` is a topology for which addition, negation and multiplication
are continuous. -/
structure RingTopology (R : Type u) [Ring R] : Type u
  extends TopologicalSpace R, IsTopologicalRing R

Ring Topology

Informal description

A ring topology on a ring $ R $ is a topology on $ R $ such that the operations of addition, negation, and multiplication are continuous with respect to this topology.

RingTopology.inhabited instance

{R : Type u} [Ring R] : Inhabited (RingTopology R)

Full source

instance inhabited {R : Type u} [Ring R] : Inhabited (RingTopology R) :=
  ⟨let _ : TopologicalSpace R := ⊤;
    { continuous_add := continuous_top
      continuous_mul := continuous_top
      continuous_neg := continuous_top }⟩

Nonempty Ring Topologies on a Ring

Informal description

For any ring $R$, the collection of ring topologies on $R$ is nonempty.

RingTopology.toTopologicalSpace_injective theorem

: Injective (toTopologicalSpace : RingTopology R → TopologicalSpace R)

Full source

theorem toTopologicalSpace_injective :
    Injective (toTopologicalSpace : RingTopology R → TopologicalSpace R) := by
  intro f g _; cases f; cases g; congr

Injectivity of Ring Topology to Topological Space Map

Informal description

The function that maps a ring topology on a ring $R$ to its underlying topological space is injective. In other words, if two ring topologies on $R$ induce the same topological space, then they are equal.

RingTopology.ext theorem

{f g : RingTopology R} (h : f.IsOpen = g.IsOpen) : f = g

Full source

@[ext]
theorem ext {f g : RingTopology R} (h : f.IsOpen = g.IsOpen) : f = g :=
  toTopologicalSpace_injective <| TopologicalSpace.ext h

Equality of Ring Topologies via Open Sets

Informal description

For any two ring topologies $f$ and $g$ on a ring $R$, if their collections of open sets are equal, then the ring topologies are equal, i.e., $f = g$.

RingTopology.instPartialOrder instance

: PartialOrder (RingTopology R)

Full source

/-- 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`). -/
instance : PartialOrder (RingTopology R) :=
  PartialOrder.lift RingTopology.toTopologicalSpace toTopologicalSpace_injective

Partial Order on Ring Topologies by Fineness

Informal description

The collection of all ring topologies on a ring $R$ forms a partial order, where one topology is less than or equal to another if every open set in the second topology is also open in the first (i.e., the first topology is finer than the second).

RingTopology.instCompleteSemilatticeInf instance

: CompleteSemilatticeInf (RingTopology R)

Full source

/-- 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`. -/
instance : CompleteSemilatticeInf (RingTopology R) where
  sInf := def_sInf
  sInf_le := fun _ a haS => sInf_le (α := TopologicalSpace R) ⟨a, ⟨haS, rfl⟩⟩
  le_sInf := fun _ _ h => le_sInf (α := TopologicalSpace R) <| forall_mem_image.2 h

Complete Meet-Semilattice Structure on Ring Topologies

Informal description

The collection of all ring topologies on a ring $R$ forms a complete meet-semilattice, where the infimum of a family of ring topologies is the ring topology generated by their intersection.

RingTopology.instCompleteLattice instance

: CompleteLattice (RingTopology R)

Full source

instance : CompleteLattice (RingTopology R) :=
  completeLatticeOfCompleteSemilatticeInf _

Complete Lattice Structure on Ring Topologies

Informal description

The collection of all ring topologies on a ring $R$ forms a complete lattice, where the order is given by reverse inclusion of topologies. In this lattice, the supremum of a family of ring topologies is the intersection of their underlying topologies, and the infimum is the ring topology generated by their union. The discrete topology is the bottom element, and the indiscrete topology is the top element.

RingTopology.coinduced definition

{R S : Type*} [t : TopologicalSpace R] [Ring S] (f : R → S) : RingTopology S

Full source

/-- 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. -/
def coinduced {R S : Type*} [t : TopologicalSpace R] [Ring S] (f : R → S) : RingTopology S :=
  sInf { b : RingTopology S | t.coinduced f ≤ b.toTopologicalSpace }

Coinduced ring topology

Informal description

Given a function $ f : R \to S $ from a topological space $ R $ to a ring $ S $, the *coinduced ring topology* on $ S $ is the finest ring topology such that $ f $ is continuous and $ S $ is a topological ring. It is defined as the infimum of all ring topologies on $ S $ for which the coinduced topology (from $ R $) is finer than or equal to the given topology.

RingTopology.coinduced_continuous theorem

{R S : Type*} [t : TopologicalSpace R] [Ring S] (f : R → S) : Continuous[t, (coinduced f).toTopologicalSpace] f

Full source

theorem coinduced_continuous {R S : Type*} [t : TopologicalSpace R] [Ring S] (f : R → S) :
    Continuous[t, (coinduced f).toTopologicalSpace] f :=
  continuous_sInf_rng.2 <| forall_mem_image.2 fun _ => continuous_iff_coinduced_le.2

Continuity of Functions under Coinduced Ring Topology

Informal description

Let $R$ be a topological space with topology $t$, and let $S$ be a ring. For any function $f \colon R \to S$, the coinduced ring topology on $S$ makes $f$ continuous. That is, $f$ is continuous when $S$ is equipped with the coinduced ring topology from $f$.

RingTopology.toAddGroupTopology definition

(t : RingTopology R) : AddGroupTopology R

Full source

/-- The forgetful functor from ring topologies on `a` to additive group topologies on `a`. -/
def toAddGroupTopology (t : RingTopology R) : AddGroupTopology R where
  toTopologicalSpace := t.toTopologicalSpace
  toIsTopologicalAddGroup :=
    @IsTopologicalRing.to_topologicalAddGroup _ _ t.toTopologicalSpace t.toIsTopologicalRing

Additive group topology induced by a ring topology

Informal description

Given a ring topology $ t $ on a ring $ R $, the function returns the corresponding additive group topology on $ R $, where the topology is the same as $ t $ and the additive group operations are continuous with respect to this topology.

RingTopology.toAddGroupTopology.orderEmbedding definition

: OrderEmbedding (RingTopology R) (AddGroupTopology R)

Full source

/-- The order embedding from ring topologies on `a` to additive group topologies on `a`. -/
def toAddGroupTopology.orderEmbedding : OrderEmbedding (RingTopology R) (AddGroupTopology R) :=
  OrderEmbedding.ofMapLEIff toAddGroupTopology fun _ _ => Iff.rfl

Order embedding from ring topologies to additive group topologies

Informal description

The order embedding from the lattice of ring topologies on a ring $ R $ to the lattice of additive group topologies on $ R $. This embedding preserves the order structure, meaning for any two ring topologies $ t_1 $ and $ t_2 $ on $ R $, $ t_1 $ is finer than $ t_2 $ if and only if the corresponding additive group topology of $ t_1 $ is finer than that of $ t_2 $.

AbsoluteValue.comp definition

 {R S T : Type*} [Semiring T] [Semiring R] [Semiring S] [PartialOrder S] (v : AbsoluteValue R S) {f : T →+* R}
  (hf : Function.Injective f) : AbsoluteValue T S

Full source

/-- Construct an absolute value on a semiring `T` from an absolute value on a semiring `R`
and an injective ring homomorphism `f : T →+* R` -/
def AbsoluteValue.comp {R S T : Type*} [Semiring T] [Semiring R] [Semiring S] [PartialOrder S]
    (v : AbsoluteValue R S) {f : T →+* R} (hf : Function.Injective f) : AbsoluteValue T S where
  toMulHom := v.1.comp f
  nonneg' _ := v.nonneg _
  eq_zero' _ := v.eq_zero.trans (map_eq_zero_iff f hf)
  add_le' _ _ := (congr_arg v (map_add f _ _)).trans_le (v.add_le _ _)

Absolute value induced by an injective ring homomorphism

Informal description

Given an absolute value $v$ on a semiring $R$ with values in a partially ordered semiring $S$, and an injective ring homomorphism $f \colon T \to R$ from another semiring $T$, the composition $v \circ f$ defines an absolute value on $T$ with values in $S$. This absolute value satisfies: 1. Nonnegativity: $(v \circ f)(x) \geq 0$ for all $x \in T$ 2. Positive definiteness: $(v \circ f)(x) = 0$ if and only if $x = 0$ 3. Triangle inequality: $(v \circ f)(x + y) \leq (v \circ f)(x) + (v \circ f)(y)$ for all $x, y \in T$ 4. Multiplicativity: $(v \circ f)(x \cdot y) = (v \circ f)(x) \cdot (v \circ f)(y)$ for all $x, y \in T$

Main Results