mathlib3 documentation

topology.algebra.ring.basic

Topological (semi)rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 a subring/subsemiring is itself a sub(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.

@[class]

structure topological_semiring (α : Type u_1) [topological_space α] [non_unital_non_assoc_semiring α] :

Prop

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

@[class]

structure topological_ring (α : Type u_1) [topological_space α] [non_unital_non_assoc_ring α] :

Prop

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

theorem topological_semiring.has_continuous_neg_of_mul {α : Type u_1} [topological_space α] [non_assoc_ring α] [has_continuous_mul α] :

has_continuous_neg α

If R is a ring with a continuous multiplication, then negation is continuous as well since it is just multiplication with -1.

theorem topological_semiring.to_topological_ring {α : Type u_1} [topological_space α] [non_assoc_ring α] (h : topological_semiring α) :

topological_ring α

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.

@[protected, instance]

def topological_ring.to_topological_add_group {α : Type u_1} [non_unital_non_assoc_ring α] [topological_space α] [topological_ring α] :

topological_add_group α

@[protected, instance]

def discrete_topology.topological_semiring {α : Type u_1} [topological_space α] [non_unital_non_assoc_semiring α] [discrete_topology α] :

topological_semiring α

@[protected, instance]

def discrete_topology.topological_ring {α : Type u_1} [topological_space α] [non_unital_non_assoc_ring α] [discrete_topology α] :

topological_ring α

@[protected, instance]

def subsemiring.topological_semiring {α : Type u_1} [topological_space α] [semiring α] [topological_semiring α] (S : subsemiring α) :

topological_semiring ↥S

def subsemiring.topological_closure {α : Type u_1} [topological_space α] [semiring α] [topological_semiring α] (s : subsemiring α) :

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

Equations

s.topological_closure = {carrier := closure ↑s, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _}

@[simp]

theorem subsemiring.topological_closure_coe {α : Type u_1} [topological_space α] [semiring α] [topological_semiring α] (s : subsemiring α) :

↑(s.topological_closure) = closure ↑s

theorem subsemiring.le_topological_closure {α : Type u_1} [topological_space α] [semiring α] [topological_semiring α] (s : subsemiring α) :

s ≤ s.topological_closure

theorem subsemiring.is_closed_topological_closure {α : Type u_1} [topological_space α] [semiring α] [topological_semiring α] (s : subsemiring α) :

is_closed ↑(s.topological_closure)

theorem subsemiring.topological_closure_minimal {α : Type u_1} [topological_space α] [semiring α] [topological_semiring α] (s : subsemiring α) {t : subsemiring α} (h : s ≤ t) (ht : is_closed ↑t) :

s.topological_closure ≤ t

def subsemiring.comm_semiring_topological_closure {α : Type u_1} [topological_space α] [semiring α] [topological_semiring α] [t2_space α] (s : subsemiring α) (hs : ∀ (x y : ↥s), x * y = y * x) :

comm_semiring ↥(s.topological_closure)

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 := _}

@[protected, instance]

def prod.topological_semiring {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [non_unital_non_assoc_semiring α] [non_unital_non_assoc_semiring β] [topological_semiring α] [topological_semiring β] :

topological_semiring (α × β)

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

@[protected, instance]

def prod.topological_ring {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [non_unital_non_assoc_ring α] [non_unital_non_assoc_ring β] [topological_ring α] [topological_ring β] :

topological_ring (α × β)

The product topology on the cartesian product of two topological rings makes the product into a topological ring.

@[protected, instance]

def pi.topological_semiring {β : Type u_1} {C : β → Type u_2} [Π (b : β), topological_space (C b)] [Π (b : β), non_unital_non_assoc_semiring (C b)] [∀ (b : β), topological_semiring (C b)] :

topological_semiring (Π (b : β), C b)

@[protected, instance]

def pi.topological_ring {β : Type u_1} {C : β → Type u_2} [Π (b : β), topological_space (C b)] [Π (b : β), non_unital_non_assoc_ring (C b)] [∀ (b : β), topological_ring (C b)] :

topological_ring (Π (b : β), C b)

@[protected, instance]

def mul_opposite.has_continuous_add {α : Type u_1} [non_unital_non_assoc_semiring α] [topological_space α] [has_continuous_add α] :

has_continuous_add αᵐᵒᵖ

@[protected, instance]

def mul_opposite.topological_semiring {α : Type u_1} [non_unital_non_assoc_semiring α] [topological_space α] [topological_semiring α] :

topological_semiring αᵐᵒᵖ

@[protected, instance]

def mul_opposite.has_continuous_neg {α : Type u_1} [non_unital_non_assoc_ring α] [topological_space α] [has_continuous_neg α] :

has_continuous_neg αᵐᵒᵖ

@[protected, instance]

def mul_opposite.topological_ring {α : Type u_1} [non_unital_non_assoc_ring α] [topological_space α] [topological_ring α] :

topological_ring αᵐᵒᵖ

@[protected, instance]

def add_opposite.has_continuous_mul {α : Type u_1} [non_unital_non_assoc_semiring α] [topological_space α] [has_continuous_mul α] :

has_continuous_mul αᵃᵒᵖ

@[protected, instance]

def add_opposite.topological_semiring {α : Type u_1} [non_unital_non_assoc_semiring α] [topological_space α] [topological_semiring α] :

topological_semiring αᵃᵒᵖ

@[protected, instance]

def add_opposite.topological_ring {α : Type u_1} [non_unital_non_assoc_ring α] [topological_space α] [topological_ring α] :

topological_ring αᵃᵒᵖ

theorem topological_ring.of_add_group_of_nhds_zero {R : Type u_2} [non_unital_non_assoc_ring R] [topological_space R] [topological_add_group R] (hmul : filter.tendsto (function.uncurry has_mul.mul) ((nhds 0).prod (nhds 0)) (nhds 0)) (hmul_left : ∀ (x₀ : R), filter.tendsto (λ (x : R), x₀ * x) (nhds 0) (nhds 0)) (hmul_right : ∀ (x₀ : R), filter.tendsto (λ (x : R), x * x₀) (nhds 0) (nhds 0)) :

topological_ring R

theorem topological_ring.of_nhds_zero {R : Type u_2} [non_unital_non_assoc_ring R] [topological_space R] (hadd : filter.tendsto (function.uncurry has_add.add) ((nhds 0).prod (nhds 0)) (nhds 0)) (hneg : filter.tendsto (λ (x : R), -x) (nhds 0) (nhds 0)) (hmul : filter.tendsto (function.uncurry has_mul.mul) ((nhds 0).prod (nhds 0)) (nhds 0)) (hmul_left : ∀ (x₀ : R), filter.tendsto (λ (x : R), x₀ * x) (nhds 0) (nhds 0)) (hmul_right : ∀ (x₀ : R), filter.tendsto (λ (x : R), x * x₀) (nhds 0) (nhds 0)) (hleft : ∀ (x₀ : R), nhds x₀ = filter.map (λ (x : R), x₀ + x) (nhds 0)) :

topological_ring R

theorem mul_left_continuous {α : Type u_1} [topological_space α] [non_unital_non_assoc_ring α] [topological_ring α] (x : α) :

continuous ⇑(add_monoid_hom.mul_left x)

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

theorem mul_right_continuous {α : Type u_1} [topological_space α] [non_unital_non_assoc_ring α] [topological_ring α] (x : α) :

continuous ⇑(add_monoid_hom.mul_right x)

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

@[protected, instance]

def subring.topological_ring {α : Type u_1} [topological_space α] [ring α] [topological_ring α] (S : subring α) :

topological_ring ↥S

def subring.topological_closure {α : Type u_1} [topological_space α] [ring α] [topological_ring α] (S : subring α) :

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

Equations

S.topological_closure = {carrier := closure ↑S, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, neg_mem' := _}

theorem subring.le_topological_closure {α : Type u_1} [topological_space α] [ring α] [topological_ring α] (s : subring α) :

s ≤ s.topological_closure

theorem subring.is_closed_topological_closure {α : Type u_1} [topological_space α] [ring α] [topological_ring α] (s : subring α) :

is_closed ↑(s.topological_closure)

theorem subring.topological_closure_minimal {α : Type u_1} [topological_space α] [ring α] [topological_ring α] (s : subring α) {t : subring α} (h : s ≤ t) (ht : is_closed ↑t) :

s.topological_closure ≤ t

def subring.comm_ring_topological_closure {α : Type u_1} [topological_space α] [ring α] [topological_ring α] [t2_space α] (s : subring α) (hs : ∀ (x y : ↥s), x * y = y * x) :

comm_ring ↥(s.topological_closure)

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 := _}

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

theorem ring_topology.ext_iff {α : Type u} {_inst_1 : ring α} (x y : ring_topology α) :

x = y ↔ x.to_topological_space = y.to_topological_space

@[ext]

structure ring_topology (α : Type u) [ring α] :

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

theorem ring_topology.ext {α : Type u} {_inst_1 : ring α} (x y : ring_topology α) (h : x.to_topological_space = y.to_topological_space) :

x = y

@[protected, instance]

def ring_topology.inhabited {α : Type u} [ring α] :

inhabited (ring_topology α)

Equations

ring_topology.inhabited = {default := {to_topological_space := ⊤, to_topological_ring := _}}

@[ext]

theorem ring_topology.ext' {α : Type u_1} [ring α] {f g : ring_topology α} (h : topological_space.is_open = topological_space.is_open) :

f = g

@[protected, instance]

def ring_topology.partial_order {α : Type u_1} [ring α] :

partial_order (ring_topology α)

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_topology.partial_order = partial_order.lift ring_topology.to_topological_space ring_topology.ext

@[protected, instance]

def ring_topology.complete_semilattice_Inf {α : Type u_1} [ring α] :

complete_semilattice_Inf (ring_topology α)

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 := _}

@[protected, instance]

def ring_topology.complete_lattice {α : Type u_1} [ring α] :

complete_lattice (ring_topology α)

Equations

ring_topology.complete_lattice = complete_lattice_of_complete_semilattice_Inf (ring_topology α)

def ring_topology.coinduced {α : Type u_1} {β : Type u_2} [t : topological_space α] [ring β] (f : α → β) :

ring_topology β

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}

theorem ring_topology.coinduced_continuous {α : Type u_1} {β : Type u_2} [t : topological_space α] [ring β] (f : α → β) :

def ring_topology.to_add_group_topology {α : Type u_1} [ring α] (t : ring_topology α) :

add_group_topology α

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

Equations

t.to_add_group_topology = {to_topological_space := t.to_topological_space, to_topological_add_group := _}

def ring_topology.to_add_group_topology.order_embedding {α : Type u_1} [ring α] :

ring_topology α ↪o add_group_topology α

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

Equations

ring_topology.to_add_group_topology.order_embedding = order_embedding.of_map_le_iff ring_topology.to_add_group_topology ring_topology.to_add_group_topology.order_embedding._proof_1

def absolute_value.comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [semiring T] [semiring R] [ordered_semiring S] (v : absolute_value R S) {f : T →+* R} (hf : function.injective ⇑f) :

absolute_value T S

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 = {to_mul_hom := {to_fun := ⇑v ∘ ⇑f, map_mul' := _}, nonneg' := _, eq_zero' := _, add_le' := _}