Topological (sub)algebras #

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 ContinuousSMul 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_algebraMap_iff_smul (R : Type u_1) (A : Type u) [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace R] [TopologicalSpace A] [TopologicalSemiring A] :

Continuous ↑(algebraMap R A) ↔ Continuous fun p => p.fst • p.snd

source

theorem continuous_algebraMap (R : Type u_1) (A : Type u) [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace R] [TopologicalSpace A] [TopologicalSemiring A] [ContinuousSMul R A] :

Continuous ↑(algebraMap R A)

source

theorem continuousSMul_of_algebraMap (R : Type u_1) (A : Type u) [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace R] [TopologicalSpace A] [TopologicalSemiring A] (h : Continuous ↑(algebraMap R A)) :

ContinuousSMul R A

source

@[simp]

theorem algebraMapClm_apply (R : Type u_1) (A : Type u) [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace R] [TopologicalSpace A] [TopologicalSemiring A] [ContinuousSMul R A] (a : R) :

↑(algebraMapClm R A) a = ↑(algebraMap R A) a

source

@[simp]

theorem algebraMapClm_toFun (R : Type u_1) (A : Type u) [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace R] [TopologicalSpace A] [TopologicalSemiring A] [ContinuousSMul R A] (a : R) :

↑(algebraMapClm R A) a = ↑(algebraMap R A) a

source

def algebraMapClm (R : Type u_1) (A : Type u) [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace R] [TopologicalSpace A] [TopologicalSemiring A] [ContinuousSMul R A] :

R →L[R] A

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem algebraMapClm_coe (R : Type u_1) (A : Type u) [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace R] [TopologicalSpace A] [TopologicalSemiring A] [ContinuousSMul R A] :

↑(algebraMapClm R A) = ↑(algebraMap R A)

source

theorem algebraMapClm_toLinearMap (R : Type u_1) (A : Type u) [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace R] [TopologicalSpace A] [TopologicalSemiring A] [ContinuousSMul R A] :

↑(algebraMapClm R A) = Algebra.linearMap R A

source

instance Subalgebra.continuousSMul {R : Type u_1} [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSpace R] [ContinuousSMul R A] (s : Subalgebra R A) :

ContinuousSMul R { x // x ∈ s }

Equations

@Subalgebra.continuousSMul = @Subalgebra.continuousSMul.proof_1

source

def Subalgebra.topologicalClosure {R : Type u_1} [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] (s : Subalgebra R A) :

Subalgebra R A

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Subalgebra.topologicalClosure_coe {R : Type u_1} [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] (s : Subalgebra R A) :

↑(Subalgebra.topologicalClosure s) = closure ↑s

source

instance Subalgebra.topologicalSemiring {R : Type u_1} [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] (s : Subalgebra R A) :

TopologicalSemiring { x // x ∈ s }

Equations

@Subalgebra.topologicalSemiring = @Subalgebra.topologicalSemiring.proof_1

source

theorem Subalgebra.le_topologicalClosure {R : Type u_1} [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] (s : Subalgebra R A) :

s ≤ Subalgebra.topologicalClosure s

source

theorem Subalgebra.isClosed_topologicalClosure {R : Type u_1} [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] (s : Subalgebra R A) :

IsClosed ↑(Subalgebra.topologicalClosure s)

source

theorem Subalgebra.topologicalClosure_minimal {R : Type u_1} [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] (s : Subalgebra R A) {t : Subalgebra R A} (h : s ≤ t) (ht : IsClosed ↑t) :

Subalgebra.topologicalClosure s ≤ t

source

def Subalgebra.commSemiringTopologicalClosure {R : Type u_1} [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] [T2Space A] (s : Subalgebra R A) (hs : ∀ (x y : { x // x ∈ s }), x * y = y * x) :

CommSemiring { x // x ∈ Subalgebra.topologicalClosure s }

If a subalgebra of a topological algebra is commutative, then so is its topological closure.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Subalgebra.topologicalClosure_comap_homeomorph {R : Type u_1} [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [TopologicalSemiring A] (s : Subalgebra R A) {B : Type u_2} [TopologicalSpace B] [Ring B] [TopologicalRing B] [Algebra R B] (f : B →ₐ[R] A) (f' : B ≃ₜ A) (w : ↑f = ↑f') :

Subalgebra.comap f (Subalgebra.topologicalClosure s) = Subalgebra.topologicalClosure (Subalgebra.comap f s)

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]