mathlib3 documentation

topology.algebra.star_subalgebra

Topological star (sub)algebras #

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

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

Results #

This is just a minimal stub for now!

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

theorem star_subalgebra.embedding_inclusion {R : Type u_1} {A : Type u_2} [comm_semiring R] [star_ring R] [topological_space A] [semiring A] [algebra R A] [star_ring A] [star_module R A] {S₁ S₂ : star_subalgebra R A} (h : S₁ S₂) :

The star_subalgebra.inclusion of a star subalgebra is an embedding.

theorem star_subalgebra.closed_embedding_inclusion {R : Type u_1} {A : Type u_2} [comm_semiring R] [star_ring R] [topological_space A] [semiring A] [algebra R A] [star_ring A] [star_module R A] {S₁ S₂ : star_subalgebra R A} (h : S₁ S₂) (hS₁ : is_closed S₁) :

The star_subalgebra.inclusion of a closed star subalgebra is a closed_embedding.

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

Equations
Instances for star_subalgebra.topological_closure
@[reducible]

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

Equations
@[reducible]

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

Equations

Continuous star_alg_homs from the the topological closure of a star_subalgebra whose compositions with the star_subalgebra.inclusion map agree are, in fact, equal.

@[protected, instance]

The elemental_star_algebra generated by a normal element is commutative.

Equations

The coercion from an elemental algebra to the full algebra as a closed_embedding.

theorem elemental_star_algebra.star_alg_hom_class_ext (R : Type u_1) {A : Type u_2} {B : Type u_3} [comm_semiring R] [star_ring R] [topological_space A] [semiring A] [star_ring A] [topological_semiring A] [has_continuous_star A] [algebra R A] [star_module R A] [topological_space B] [semiring B] [star_ring B] [algebra R B] [t2_space B] {F : Type u_4} {a : A} [star_alg_hom_class F R (elemental_star_algebra R a) B] {φ ψ : F} (hφ : continuous φ) (hψ : continuous ψ) (h : φ a, _⟩ = ψ a, _⟩) :
φ = ψ