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]
:
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)
:
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)
:
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)
:
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)
:
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)
:
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')
:
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)
:
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
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]
:
The action induced by algebraRat is continuous.
Equations
- ⋯ = ⋯