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 #

The topological closure of a subalgebra is still a subalgebra, which as an algebra is a topological algebra.

In this file we define continuous algebra homomorphisms, as algebra homomorphisms between topological (semi-)rings which are continuous. The set of continuous algebra homomorphisms between the topological R-algebras A and B is denoted by A →A[R] B.

TODO: add continuous algebra isomorphisms.

instance Subalgebra.continuousSMul (R : Type u_1) (A : Type u) [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace A] (S : Subalgebra R A) (X : Type u_2) [TopologicalSpace X] [MulAction A X] [ContinuousSMul A X] :

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

Equations
    Instances For
      @[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

      If R is a discrete topological ring, then any topological ring S which is an R-algebra is also a topological R-algebra.

      NB: This could be an instance but the signature makes it very expensive in search. See https://github.com/leanprover-community/mathlib4/pull/15339 for the regressions caused by making this an instance.

      structure ContinuousAlgHom (R : Type u_3) [CommSemiring R] (A : Type u_4) [Semiring A] [TopologicalSpace A] (B : Type u_5) [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] extends A →ₐ[R] B :
      Type (max u_4 u_5)

      Continuous algebra homomorphisms between algebras. We only put the type classes that are necessary for the definition, although in applications M and B will be topological algebras over the topological ring R.

      Instances For

        Continuous algebra homomorphisms between algebras. We only put the type classes that are necessary for the definition, although in applications M and B will be topological algebras over the topological ring R.

        Equations
          Instances For
            instance ContinuousAlgHom.instFunLike {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :
            FunLike (A →A[R] B) A B
            Equations
              instance ContinuousAlgHom.instAlgHomClass {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :
              AlgHomClass (A →A[R] B) R A B
              @[simp]
              theorem ContinuousAlgHom.toAlgHom_eq_coe {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) :
              f.toAlgHom = f
              @[simp]
              theorem ContinuousAlgHom.coe_inj {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {f g : A →A[R] B} :
              f = g f = g
              @[simp]
              theorem ContinuousAlgHom.coe_mk {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (h : Continuous (↑f.toRingHom).toFun) :
              { toAlgHom := f, cont := h } = f
              @[simp]
              theorem ContinuousAlgHom.coe_mk' {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (h : Continuous (↑f.toRingHom).toFun) :
              { toAlgHom := f, cont := h } = f
              @[simp]
              theorem ContinuousAlgHom.coe_coe {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) :
              f = f
              theorem ContinuousAlgHom.continuous {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) :
              theorem ContinuousAlgHom.uniformContinuous {R : Type u_1} [CommSemiring R] {E₁ : Type u_4} {E₂ : Type u_5} [UniformSpace E₁] [UniformSpace E₂] [Ring E₁] [Ring E₂] [Algebra R E₁] [Algebra R E₂] [IsUniformAddGroup E₁] [IsUniformAddGroup E₂] (f : E₁ →A[R] E₂) :
              def ContinuousAlgHom.Simps.apply {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (h : A →A[R] B) :
              AB

              See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

              Equations
                Instances For
                  def ContinuousAlgHom.Simps.coe {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (h : A →A[R] B) :

                  See Note [custom simps projection].

                  Equations
                    Instances For
                      theorem ContinuousAlgHom.ext {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {f g : A →A[R] B} (h : ∀ (x : A), f x = g x) :
                      f = g
                      theorem ContinuousAlgHom.ext_iff {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {f g : A →A[R] B} :
                      f = g ∀ (x : A), f x = g x
                      def ContinuousAlgHom.copy {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) (f' : AB) (h : f' = f) :
                      A →A[R] B

                      Copy of a ContinuousAlgHom with a new toFun equal to the old one. Useful to fix definitional equalities.

                      Equations
                        Instances For
                          @[simp]
                          theorem ContinuousAlgHom.coe_copy {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) (f' : AB) (h : f' = f) :
                          (f.copy f' h) = f'
                          theorem ContinuousAlgHom.copy_eq {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) (f' : AB) (h : f' = f) :
                          f.copy f' h = f
                          theorem ContinuousAlgHom.map_zero {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) :
                          f 0 = 0
                          theorem ContinuousAlgHom.map_add {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) (x y : A) :
                          f (x + y) = f x + f y
                          theorem ContinuousAlgHom.map_smul {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) (c : R) (x : A) :
                          f (c x) = c f x
                          theorem ContinuousAlgHom.map_smul_of_tower {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] {R : Type u_4} {S : Type u_5} [CommSemiring S] [SMul R A] [Algebra S A] [SMul R B] [Algebra S B] [MulActionHomClass (A →A[S] B) R A B] (f : A →A[S] B) (c : R) (x : A) :
                          f (c x) = c f x
                          theorem ContinuousAlgHom.map_sum {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {ι : Type u_4} (f : A →A[R] B) (s : Finset ι) (g : ιA) :
                          f (∑ is, g i) = is, f (g i)
                          theorem ContinuousAlgHom.ext_ring {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] [TopologicalSpace R] {f g : R →A[R] A} :
                          f = g

                          Any two continuous R-algebra morphisms from R are equal

                          theorem ContinuousAlgHom.ext_ring_iff {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] [TopologicalSpace R] {f g : R →A[R] A} :
                          f = g f 1 = g 1
                          theorem ContinuousAlgHom.eqOn_closure_adjoin {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] [T2Space B] {s : Set A} {f g : A →A[R] B} (h : Set.EqOn (⇑f) (⇑g) s) :
                          Set.EqOn (⇑f) (⇑g) (closure (Algebra.adjoin R s))

                          If two continuous algebra maps are equal on a set s, then they are equal on the closure of the Algebra.adjoin of this set.

                          theorem ContinuousAlgHom.ext_on {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] [T2Space B] {s : Set A} (hs : Dense (Algebra.adjoin R s)) {f g : A →A[R] B} (h : Set.EqOn (⇑f) (⇑g) s) :
                          f = g

                          If the subalgebra generated by a set s is dense in the ambient module, then two continuous algebra maps equal on s are equal.

                          The topological closure of a subalgebra

                          Equations
                            Instances For

                              Under a continuous algebra map, the image of the TopologicalClosure of a subalgebra is contained in the TopologicalClosure of its image.

                              Under a dense continuous algebra map, a subalgebra whose TopologicalClosure is is sent to another such submodule. That is, the image of a dense subalgebra under a map with dense range is dense.

                              def ContinuousAlgHom.id (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [TopologicalSpace A] [Algebra R A] :
                              A →A[R] A

                              The identity map as a continuous algebra homomorphism.

                              Equations
                                Instances For
                                  instance ContinuousAlgHom.instOne (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [TopologicalSpace A] [Algebra R A] :
                                  One (A →A[R] A)
                                  Equations
                                    theorem ContinuousAlgHom.id_apply (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [TopologicalSpace A] [Algebra R A] (x : A) :
                                    @[simp]
                                    theorem ContinuousAlgHom.coe_id (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [TopologicalSpace A] [Algebra R A] :
                                    @[simp]
                                    theorem ContinuousAlgHom.coe_id' (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [TopologicalSpace A] [Algebra R A] :
                                    @[simp]
                                    theorem ContinuousAlgHom.coe_eq_id (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [TopologicalSpace A] [Algebra R A] {f : A →A[R] A} :
                                    @[simp]
                                    theorem ContinuousAlgHom.one_apply (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [TopologicalSpace A] [Algebra R A] (x : A) :
                                    1 x = x
                                    def ContinuousAlgHom.comp {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] (g : B →A[R] C) (f : A →A[R] B) :
                                    A →A[R] C

                                    Composition of continuous algebra homomorphisms.

                                    Equations
                                      Instances For
                                        @[simp]
                                        theorem ContinuousAlgHom.coe_comp {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] (h : B →A[R] C) (f : A →A[R] B) :
                                        (h.comp f) = (↑h).comp f
                                        @[simp]
                                        theorem ContinuousAlgHom.coe_comp' {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] (h : B →A[R] C) (f : A →A[R] B) :
                                        (h.comp f) = h f
                                        theorem ContinuousAlgHom.comp_apply {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] (g : B →A[R] C) (f : A →A[R] B) (x : A) :
                                        (g.comp f) x = g (f x)
                                        @[simp]
                                        theorem ContinuousAlgHom.comp_id {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) :
                                        @[simp]
                                        theorem ContinuousAlgHom.id_comp {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) :
                                        theorem ContinuousAlgHom.comp_assoc {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] {D : Type u_5} [Semiring D] [Algebra R D] [TopologicalSpace D] (h : C →A[R] D) (g : B →A[R] C) (f : A →A[R] B) :
                                        (h.comp g).comp f = h.comp (g.comp f)
                                        instance ContinuousAlgHom.instMul {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] :
                                        Mul (A →A[R] A)
                                        Equations
                                          theorem ContinuousAlgHom.mul_def {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] (f g : A →A[R] A) :
                                          f * g = f.comp g
                                          @[simp]
                                          theorem ContinuousAlgHom.coe_mul {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] (f g : A →A[R] A) :
                                          ⇑(f * g) = f g
                                          theorem ContinuousAlgHom.mul_apply {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] (f g : A →A[R] A) (x : A) :
                                          (f * g) x = f (g x)
                                          instance ContinuousAlgHom.instMonoid {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] :
                                          Monoid (A →A[R] A)
                                          Equations
                                            theorem ContinuousAlgHom.coe_pow {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] (f : A →A[R] A) (n : ) :
                                            ⇑(f ^ n) = (⇑f)^[n]

                                            coercion from ContinuousAlgHom to AlgHom as a RingHom.

                                            Equations
                                              Instances For
                                                @[simp]
                                                def ContinuousAlgHom.prod {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] (f₁ : A →A[R] B) (f₂ : A →A[R] C) :
                                                A →A[R] B × C

                                                The cartesian product of two continuous algebra morphisms as a continuous algebra morphism.

                                                Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem ContinuousAlgHom.coe_prod {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] (f₁ : A →A[R] B) (f₂ : A →A[R] C) :
                                                    (f₁.prod f₂) = (↑f₁).prod f₂
                                                    @[simp]
                                                    theorem ContinuousAlgHom.prod_apply {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] (f₁ : A →A[R] B) (f₂ : A →A[R] C) (x : A) :
                                                    (f₁.prod f₂) x = (f₁ x, f₂ x)
                                                    def ContinuousAlgHom.fst (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [TopologicalSpace A] (B : Type u_3) [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :
                                                    A × B →A[R] A

                                                    Prod.fst as a ContinuousAlgHom.

                                                    Equations
                                                      Instances For
                                                        def ContinuousAlgHom.snd (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [TopologicalSpace A] (B : Type u_3) [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :
                                                        A × B →A[R] B

                                                        Prod.snd as a ContinuousAlgHom.

                                                        Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem ContinuousAlgHom.coe_fst {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :
                                                            (fst R A B) = AlgHom.fst R A B
                                                            @[simp]
                                                            theorem ContinuousAlgHom.coe_fst' {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :
                                                            (fst R A B) = Prod.fst
                                                            @[simp]
                                                            theorem ContinuousAlgHom.coe_snd {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :
                                                            (snd R A B) = AlgHom.snd R A B
                                                            @[simp]
                                                            theorem ContinuousAlgHom.coe_snd' {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :
                                                            (snd R A B) = Prod.snd
                                                            @[simp]
                                                            theorem ContinuousAlgHom.fst_prod_snd {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :
                                                            (fst R A B).prod (snd R A B) = ContinuousAlgHom.id R (A × B)
                                                            @[simp]
                                                            theorem ContinuousAlgHom.fst_comp_prod {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] (f : A →A[R] B) (g : A →A[R] C) :
                                                            (fst R B C).comp (f.prod g) = f
                                                            @[simp]
                                                            theorem ContinuousAlgHom.snd_comp_prod {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] (f : A →A[R] B) (g : A →A[R] C) :
                                                            (snd R B C).comp (f.prod g) = g
                                                            def ContinuousAlgHom.prodMap {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] {D : Type u_6} [Semiring D] [TopologicalSpace D] [Algebra R D] (f₁ : A →A[R] B) (f₂ : C →A[R] D) :
                                                            A × C →A[R] B × D

                                                            Prod.map of two continuous algebra homomorphisms.

                                                            Equations
                                                              Instances For
                                                                @[simp]
                                                                theorem ContinuousAlgHom.coe_prodMap {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] {D : Type u_6} [Semiring D] [TopologicalSpace D] [Algebra R D] (f₁ : A →A[R] B) (f₂ : C →A[R] D) :
                                                                (f₁.prodMap f₂) = (↑f₁).prodMap f₂
                                                                @[simp]
                                                                theorem ContinuousAlgHom.coe_prodMap' {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] {D : Type u_6} [Semiring D] [TopologicalSpace D] [Algebra R D] (f₁ : A →A[R] B) (f₂ : C →A[R] D) :
                                                                (f₁.prodMap f₂) = Prod.map f₁ f₂
                                                                def ContinuousAlgHom.prodEquiv {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] :
                                                                (A →A[R] B) × (A →A[R] C) (A →A[R] B × C)

                                                                ContinuousAlgHom.prod as an Equiv.

                                                                Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem ContinuousAlgHom.prodEquiv_apply {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] (f : (A →A[R] B) × (A →A[R] C)) :
                                                                    prodEquiv f = f.1.prod f.2
                                                                    def ContinuousAlgHom.codRestrict {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) (p : Subalgebra R B) (h : ∀ (x : A), f x p) :
                                                                    A →A[R] p

                                                                    Restrict codomain of a continuous algebra morphism.

                                                                    Equations
                                                                      Instances For
                                                                        theorem ContinuousAlgHom.coe_codRestrict {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) (p : Subalgebra R B) (h : ∀ (x : A), f x p) :
                                                                        (f.codRestrict p h) = (↑f).codRestrict p h
                                                                        @[simp]
                                                                        theorem ContinuousAlgHom.coe_codRestrict_apply {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) (p : Subalgebra R B) (h : ∀ (x : A), f x p) (x : A) :
                                                                        ((f.codRestrict p h) x) = f x
                                                                        @[reducible]
                                                                        def ContinuousAlgHom.rangeRestrict {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) :
                                                                        A →A[R] (↑f).range

                                                                        Restrict the codomain of a continuous algebra homomorphism f to f.range.

                                                                        Equations
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem ContinuousAlgHom.coe_rangeRestrict {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) :
                                                                            def Subalgebra.valA {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] (p : Subalgebra R A) :
                                                                            p →A[R] A

                                                                            Subalgebra.val as a ContinuousAlgHom.

                                                                            Equations
                                                                              Instances For
                                                                                @[simp]
                                                                                theorem Subalgebra.coe_valA {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] (p : Subalgebra R A) :
                                                                                p.valA = p.subtype
                                                                                @[simp]
                                                                                theorem Subalgebra.coe_valA' {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] (p : Subalgebra R A) :
                                                                                p.valA = p.subtype
                                                                                @[simp]
                                                                                theorem Subalgebra.valA_apply {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] (p : Subalgebra R A) (x : p) :
                                                                                p.valA x = x
                                                                                @[simp]
                                                                                theorem Submodule.range_valA {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] (p : Subalgebra R A) :
                                                                                (↑p.valA).range = p
                                                                                theorem ContinuousAlgHom.map_neg (R : Type u_1) [CommSemiring R] {S : Type u_3} [Ring S] [TopologicalSpace S] [Algebra R S] {B : Type u_4} [Ring B] [TopologicalSpace B] [Algebra R B] (f : S →A[R] B) (x : S) :
                                                                                f (-x) = -f x
                                                                                theorem ContinuousAlgHom.map_sub (R : Type u_1) [CommSemiring R] {S : Type u_3} [Ring S] [TopologicalSpace S] [Algebra R S] {B : Type u_4} [Ring B] [TopologicalSpace B] [Algebra R B] (f : S →A[R] B) (x y : S) :
                                                                                f (x - y) = f x - f y
                                                                                def ContinuousAlgHom.restrictScalars (R : Type u_1) [CommSemiring R] {S : Type u_3} [CommSemiring S] [Algebra R S] {B : Type u_4} [Ring B] [TopologicalSpace B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] {C : Type u_5} [Ring C] [TopologicalSpace C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] (f : B →A[S] C) :
                                                                                B →A[R] C

                                                                                If A is an R-algebra, then a continuous A-algebra morphism can be interpreted as a continuous R-algebra morphism.

                                                                                Equations
                                                                                  Instances For
                                                                                    @[simp]
                                                                                    theorem ContinuousAlgHom.coe_restrictScalars {R : Type u_1} [CommSemiring R] {S : Type u_3} [CommSemiring S] [Algebra R S] {B : Type u_4} [Ring B] [TopologicalSpace B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] {C : Type u_5} [Ring C] [TopologicalSpace C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] (f : B →A[S] C) :
                                                                                    @[simp]
                                                                                    theorem ContinuousAlgHom.coe_restrictScalars' {R : Type u_1} [CommSemiring R] {S : Type u_3} [CommSemiring S] [Algebra R S] {B : Type u_4} [Ring B] [TopologicalSpace B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] {C : Type u_5} [Ring C] [TopologicalSpace C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] (f : B →A[S] C) :
                                                                                    (restrictScalars R f) = f
                                                                                    @[reducible, inline]
                                                                                    abbrev Subalgebra.commSemiringTopologicalClosure {R : Type u_1} [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring 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
                                                                                      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.

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

                                                                                        Equations
                                                                                          Instances For
                                                                                            @[deprecated Algebra.elemental (since := "2024-11-05")]

                                                                                            Alias of Algebra.elemental.


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

                                                                                            Equations
                                                                                              Instances For
                                                                                                @[deprecated Algebra.elemental.self_mem (since := "2024-11-05")]

                                                                                                Alias of Algebra.elemental.self_mem.

                                                                                                theorem Algebra.elemental.le_of_mem {R : Type u_1} [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] {x : A} {s : Subalgebra R A} (hs : IsClosed s) (hx : x s) :
                                                                                                theorem Algebra.elemental.le_iff_mem {R : Type u_1} [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] {x : A} {s : Subalgebra R A} (hs : IsClosed s) :
                                                                                                elemental R x s x s

                                                                                                The coercion from an elemental algebra to the full algebra is a IsClosedEmbedding.

                                                                                                @[reducible, inline]
                                                                                                abbrev Subalgebra.commRingTopologicalClosure {R : Type u_1} [CommRing R] {A : Type u} [TopologicalSpace A] [Ring A] [Algebra R A] [IsTopologicalRing 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
                                                                                                  Instances For