Documentation

Mathlib.Topology.Algebra.Algebra

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.

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

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

    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
      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) :

      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

        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 : { x // x 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.
        Instances For
          def Algebra.elementalAlgebra (R : Type u_1) [CommRing R] {A : Type u} [TopologicalSpace A] [Ring A] [Algebra R A] [TopologicalRing A] (x : A) :

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

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