Topological (sub)algebras #

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

A topological algebra over a topological semiring R is a topological semiring with a compatible continuous scalar multiplication by elements of R. We reuse typeclass has_continuous_smul for topological algebras.

Results #

This is just a minimal stub for now!

The topological closure of a subalgebra is still a subalgebra, which as an algebra is a topological algebra.

source

theorem continuous_algebra_map_iff_smul (R : Type u_1) (A : Type u) [comm_semiring R] [semiring A] [algebra R A] [topological_space R] [topological_space A] [topological_semiring A] :

continuous ⇑(algebra_map R A) ↔ continuous (λ (p : R × A), p.fst • p.snd)

source

@[continuity]

theorem continuous_algebra_map (R : Type u_1) (A : Type u) [comm_semiring R] [semiring A] [algebra R A] [topological_space R] [topological_space A] [topological_semiring A] [has_continuous_smul R A] :

continuous ⇑(algebra_map R A)

source

theorem has_continuous_smul_of_algebra_map (R : Type u_1) (A : Type u) [comm_semiring R] [semiring A] [algebra R A] [topological_space R] [topological_space A] [topological_semiring A] (h : continuous ⇑(algebra_map R A)) :

has_continuous_smul R A

source

@[simp]

theorem algebra_map_clm_coe_apply (R : Type u_1) (A : Type u) [comm_semiring R] [semiring A] [algebra R A] [topological_space R] [topological_space A] [topological_semiring A] [has_continuous_smul R A] (ᾰ : R) :

⇑↑(algebra_map_clm R A) ᾰ = ⇑(algebra_map R A) ᾰ

source

def algebra_map_clm (R : Type u_1) (A : Type u) [comm_semiring R] [semiring A] [algebra R A] [topological_space R] [topological_space A] [topological_semiring A] [has_continuous_smul R A] :

R →L[R] A

The inclusion of the base ring in a topological algebra as a continuous linear map.

Equations

algebra_map_clm R A = {to_linear_map := {to_fun := ⇑(algebra_map R A), map_add' := _, map_smul' := _}, cont := _}

source

@[simp]

theorem algebra_map_clm_apply (R : Type u_1) (A : Type u) [comm_semiring R] [semiring A] [algebra R A] [topological_space R] [topological_space A] [topological_semiring A] [has_continuous_smul R A] (ᾰ : R) :

⇑(algebra_map_clm R A) ᾰ = ⇑(algebra_map R A) ᾰ

source

theorem algebra_map_clm_coe (R : Type u_1) (A : Type u) [comm_semiring R] [semiring A] [algebra R A] [topological_space R] [topological_space A] [topological_semiring A] [has_continuous_smul R A] :

⇑(algebra_map_clm R A) = ⇑(algebra_map R A)

source

theorem algebra_map_clm_to_linear_map (R : Type u_1) (A : Type u) [comm_semiring R] [semiring A] [algebra R A] [topological_space R] [topological_space A] [topological_semiring A] [has_continuous_smul R A] :

(algebra_map_clm R A).to_linear_map = algebra.linear_map R A

source

@[protected, instance]

def subalgebra.has_continuous_smul {R : Type u_1} [comm_semiring R] {A : Type u} [topological_space A] [semiring A] [algebra R A] [topological_space R] [has_continuous_smul R A] (s : subalgebra R A) :

has_continuous_smul R ↥s

source

def subalgebra.topological_closure {R : Type u_1} [comm_semiring R] {A : Type u} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] (s : subalgebra R A) :

subalgebra R A

The closure of a subalgebra in a topological algebra as a subalgebra.

Equations

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

source

@[simp]

theorem subalgebra.topological_closure_coe {R : Type u_1} [comm_semiring R] {A : Type u} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] (s : subalgebra R A) :

↑(s.topological_closure) = closure ↑s

source

@[protected, instance]

def subalgebra.topological_semiring {R : Type u_1} [comm_semiring R] {A : Type u} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] (s : subalgebra R A) :

topological_semiring ↥s

source

theorem subalgebra.le_topological_closure {R : Type u_1} [comm_semiring R] {A : Type u} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] (s : subalgebra R A) :

s ≤ s.topological_closure

source

theorem subalgebra.is_closed_topological_closure {R : Type u_1} [comm_semiring R] {A : Type u} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] (s : subalgebra R A) :

is_closed ↑(s.topological_closure)

source

theorem subalgebra.topological_closure_minimal {R : Type u_1} [comm_semiring R] {A : Type u} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] (s : subalgebra R A) {t : subalgebra R A} (h : s ≤ t) (ht : is_closed ↑t) :

s.topological_closure ≤ t

source

def subalgebra.comm_semiring_topological_closure {R : Type u_1} [comm_semiring R] {A : Type u} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] [t2_space A] (s : subalgebra R A) (hs : ∀ (x y : ↥s), x * y = y * x) :

comm_semiring ↥(s.topological_closure)

If a subalgebra of a topological algebra 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 := _}

source

theorem subalgebra.topological_closure_comap_homeomorph {R : Type u_1} [comm_semiring R] {A : Type u} [topological_space A] [semiring A] [algebra R A] [topological_semiring A] (s : subalgebra R A) {B : Type u_2} [topological_space B] [ring B] [topological_ring B] [algebra R B] (f : B →ₐ[R] A) (f' : B ≃ₜ A) (w : ⇑f = ⇑f') :

subalgebra.comap f s.topological_closure = (subalgebra.comap f s).topological_closure

This is really a statement about topological algebra isomorphisms, but we don't have those, so we use the clunky approach of talking about an algebra homomorphism, and a separate homeomorphism, along with a witness that as functions they are the same.

source

@[reducible]

def subalgebra.comm_ring_topological_closure {R : Type u_1} [comm_ring R] {A : Type u} [topological_space A] [ring A] [algebra R A] [topological_ring A] [t2_space A] (s : subalgebra R A) (hs : ∀ (x y : ↥s), x * y = y * x) :

comm_ring ↥(s.topological_closure)

If a subalgebra of a topological algebra is commutative, then so is its topological closure. See note [reducible non-instances].

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

source

def algebra.elemental_algebra (R : Type u_1) [comm_ring R] {A : Type u} [topological_space A] [ring A] [algebra R A] [topological_ring A] (x : A) :

subalgebra R A

The topological closure of the subalgebra generated by a single element.

Equations

algebra.elemental_algebra R x = (algebra.adjoin R {x}).topological_closure

Instances for ↥algebra.elemental_algebra

algebra.elemental_algebra.comm_ring

source

theorem algebra.self_mem_elemental_algebra (R : Type u_1) [comm_ring R] {A : Type u} [topological_space A] [ring A] [algebra R A] [topological_ring A] (x : A) :

x ∈ algebra.elemental_algebra R x

source

@[protected, instance]

def algebra.elemental_algebra.comm_ring {R : Type u_1} [comm_ring R] {A : Type u} [topological_space A] [ring A] [algebra R A] [topological_ring A] [t2_space A] {x : A} :

comm_ring ↥(algebra.elemental_algebra R x)

Equations

algebra.elemental_algebra.comm_ring = (algebra.adjoin R {x}).comm_ring_topological_closure algebra.elemental_algebra.comm_ring._proof_1

source

@[protected, instance]

def division_ring.has_continuous_const_smul_rat {A : Type u_1} [division_ring A] [topological_space A] [has_continuous_mul A] [char_zero A] :

has_continuous_const_smul ℚ A

The action induced by algebra_rat is continuous.