Topological (sub)algebras #
A topological algebra over a topological semiring R
is a topological ring 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.
theorem
continuous_algebra_map_iff_smul
(R : Type u_1)
[topological_space R]
[comm_semiring R]
(A : Type u)
[topological_space A]
[semiring A]
[algebra R A]
[topological_ring A] :
continuous ⇑(algebra_map R A) ↔ continuous (λ (p : R × A), p.fst • p.snd)
@[continuity]
theorem
continuous_algebra_map
(R : Type u_1)
[topological_space R]
[comm_semiring R]
(A : Type u)
[topological_space A]
[semiring A]
[algebra R A]
[topological_ring A]
[has_continuous_smul R A] :
continuous ⇑(algebra_map R A)
theorem
has_continuous_smul_of_algebra_map
(R : Type u_1)
[topological_space R]
[comm_semiring R]
(A : Type u)
[topological_space A]
[semiring A]
[algebra R A]
[topological_ring A]
(h : continuous ⇑(algebra_map R A)) :
def
subalgebra.topological_closure
{R : Type u_1}
[comm_semiring R]
{A : Type u}
[topological_space A]
[semiring A]
[algebra R A]
[topological_ring A]
(s : subalgebra R A) :
subalgebra R A
The closure of a subalgebra in a topological algebra as a subalgebra.
@[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_ring A]
(s : subalgebra R A) :
↑(s.topological_closure) = closure ↑s
@[protected, instance]
def
subalgebra.topological_closure_topological_ring
{R : Type u_1}
[comm_semiring R]
{A : Type u}
[topological_space A]
[semiring A]
[algebra R A]
[topological_ring A]
(s : subalgebra R A) :
@[protected, instance]
def
subalgebra.topological_closure_topological_algebra
{R : Type u_1}
[comm_semiring R]
{A : Type u}
[topological_space A]
[semiring A]
[algebra R A]
[topological_ring A]
[topological_space R]
[has_continuous_smul R A]
(s : subalgebra R A) :
theorem
subalgebra.subalgebra_topological_closure
{R : Type u_1}
[comm_semiring R]
{A : Type u}
[topological_space A]
[semiring A]
[algebra R A]
[topological_ring A]
(s : subalgebra R A) :
s ≤ s.topological_closure
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_ring A]
(s : subalgebra R A) :
theorem
subalgebra.topological_closure_minimal
{R : Type u_1}
[comm_semiring R]
{A : Type u}
[topological_space A]
[semiring A]
[algebra R A]
[topological_ring A]
(s : subalgebra R A)
{t : subalgebra R A}
(h : s ≤ t)
(ht : is_closed ↑t) :
s.topological_closure ≤ t
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_ring 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') :
s.topological_closure.comap' f = (s.comap' f).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.