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.

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 : R × A) => p.1 • p.2

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)

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

@[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

@[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

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

• algebraMapCLM R A = let __src := Algebra.linearMap R A; { toLinearMap := { toAddHom := { toFun := ⇑(algebraMap R A), map_add' := ⋯ }, map_smul' := ⋯ }, cont := ⋯ }

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)

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

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.

@[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

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 ↥s

Equations

• ⋯ = ⋯

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

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)

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

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 : ↥s), x * y = y * x) : CommSemiring ↥(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.

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.

@[reducible]

def Subalgebra.commRingTopologicalClosure {R : Type u_1} [CommRing R] {A : Type u} [TopologicalSpace A] [Ring A] [Algebra R A] [TopologicalRing A] [T2Space A] (s : Subalgebra R A) (hs : ∀ (x y : ↥s), x * y = y * x) : CommRing ↥(Subalgebra.topologicalClosure s)

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

Equations

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

def Algebra.elementalAlgebra (R : Type u_1) [CommRing R] {A : Type u} [TopologicalSpace A] [Ring A] [Algebra R A] [TopologicalRing A] (x : A) : Subalgebra R A

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

Equations

• Algebra.elementalAlgebra R x = Subalgebra.topologicalClosure (Algebra.adjoin R {x})

theorem Algebra.self_mem_elementalAlgebra (R : Type u_1) [CommRing R] {A : Type u} [TopologicalSpace A] [Ring A] [Algebra R A] [TopologicalRing A] (x : A) : x ∈ Algebra.elementalAlgebra R x

instance instCommRingSubtypeMemSubalgebraToCommSemiringToSemiringInstMembershipInstSetLikeSubalgebraElementalAlgebra {R : Type u_1} [CommRing R] {A : Type u} [TopologicalSpace A] [Ring A] [Algebra R A] [TopologicalRing A] [T2Space A] {x : A} : CommRing ↥(Algebra.elementalAlgebra R x)

Equations

• instCommRingSubtypeMemSubalgebraToCommSemiringToSemiringInstMembershipInstSetLikeSubalgebraElementalAlgebra = Subalgebra.commRingTopologicalClosure (Algebra.adjoin R {x}) ⋯

instance DivisionRing.continuousConstSMul_rat {A : Type u_1} [DivisionRing A] [TopologicalSpace A] [ContinuousMul A] [CharZero A] : ContinuousConstSMul ℚ A

The action induced by algebraRat is continuous.

Equations

• ⋯ = ⋯