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] [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] [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
Instances For

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

    Equations
    • s.topologicalClosure = let __src := s.topologicalClosure; { carrier := closure s, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , algebraMap_mem' := }
    Instances For
      @[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) :
      s.topologicalClosure = closure 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 s.topologicalClosure
      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 s.topologicalClosure
      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) :
      s.topologicalClosure 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 s.topologicalClosure

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

      Equations
      • s.commSemiringTopologicalClosure hs = let __src := s.topologicalClosure.toSemiring; let __src_1 := s.commMonoidTopologicalClosure hs; CommSemiring.mk
      Instances For
        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 s.topologicalClosure = (Subalgebra.comap f s).topologicalClosure

        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, inline]
        abbrev 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 s.topologicalClosure

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

        Equations
        • s.commRingTopologicalClosure hs = let __src := s.topologicalClosure.toRing; let __src_1 := s.commMonoidTopologicalClosure hs; CommRing.mk
        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
            • instCommRingSubtypeMemSubalgebraElementalAlgebraOfT2Space = (Algebra.adjoin R {x}).commRingTopologicalClosure