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 →R[A] B.

TODO: add continuous algebra isomorphisms.

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

Equations
Instances For
    @[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
    @[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 #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 AlgHom :
    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.

    • toFun : AB
    • map_one' : (↑self.toRingHom).toFun 1 = 1
    • map_mul' : ∀ (x y : A), (↑self.toRingHom).toFun (x * y) = (↑self.toRingHom).toFun x * (↑self.toRingHom).toFun y
    • map_zero' : (↑self.toRingHom).toFun 0 = 0
    • map_add' : ∀ (x y : A), (↑self.toRingHom).toFun (x + y) = (↑self.toRingHom).toFun x + (↑self.toRingHom).toFun y
    • commutes' : ∀ (r : R), (↑self.toRingHom).toFun ((algebraMap R A) r) = (algebraMap R B) r
    • cont : Continuous (↑self.toRingHom).toFun
    Instances For
      theorem ContinuousAlgHom.cont {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] (self : A →A[R] B) :
      Continuous (↑self.toRingHom).toFun
      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
      • ContinuousAlgHom.instFunLike = { coe := fun (f : A →A[R] B) => f.toAlgHom, coe_injective' := }
      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
      Equations
      • =
      @[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 : A →A[R] B} {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
      Equations
      • =
      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₂] [UniformAddGroup E₁] [UniformAddGroup 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 : A →A[R] B} {g : A →A[R] B} (h : ∀ (x : A), f x = g x) :
          f = g
          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
          • f.copy f' h = { toRingHom := f.copy f' h, commutes' := , cont := }
          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 : A) (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 : R →A[R] A} {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 : R →A[R] A} {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 : A →A[R] B} {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 : A →A[R] B} {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
            • s.topologicalClosure = { toSubsemiring := s.topologicalClosure, algebraMap_mem' := }
            Instances For
              theorem Subalgebra.topologicalClosure_map {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] [TopologicalSemiring A] [TopologicalSemiring B] (f : A →A[R] B) (s : Subalgebra R A) :
              Subalgebra.map (↑f) s.topologicalClosure (Subalgebra.map f.toAlgHom s).topologicalClosure

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

              @[simp]
              theorem Subalgebra.topologicalClosure_coe {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] [TopologicalSemiring A] (s : Subalgebra R A) :
              s.topologicalClosure = closure s
              theorem DenseRange.topologicalClosure_map_subalgebra {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] [TopologicalSemiring A] [TopologicalSemiring B] {f : A →A[R] B} (hf' : DenseRange f) {s : Subalgebra R A} (hs : s.topologicalClosure = ) :
              (Subalgebra.map (↑f) s).topologicalClosure =

              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
                • g.comp f = { toAlgHom := (↑g).comp f, cont := }
                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) :
                  f.comp (ContinuousAlgHom.id R A) = f
                  @[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) :
                  (ContinuousAlgHom.id R B).comp f = f
                  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
                  • ContinuousAlgHom.instMul = { mul := ContinuousAlgHom.comp }
                  theorem ContinuousAlgHom.mul_def {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] (f : A →A[R] A) (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 : A →A[R] A) (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 : A →A[R] A) (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
                  • ContinuousAlgHom.instMonoid = Monoid.mk npowRecAuto
                  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
                  • ContinuousAlgHom.toAlgHomMonoidHom = { toFun := AlgHomClass.toAlgHom, map_one' := , map_mul' := }
                  Instances For
                    @[simp]
                    theorem ContinuousAlgHom.toAlgHomMonoidHom_apply {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] (f : A →A[R] A) :
                    ContinuousAlgHom.toAlgHomMonoidHom f = f
                    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
                    • f₁.prod f₂ = { toAlgHom := (↑f₁).prod f₂, cont := }
                    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] :
                          @[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] :
                          (ContinuousAlgHom.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] :
                          @[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] :
                          (ContinuousAlgHom.snd R A B) = Prod.snd
                          @[simp]
                          @[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) :
                          (ContinuousAlgHom.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) :
                          (ContinuousAlgHom.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
                            • One or more equations did not get rendered due to their size.
                            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)) :
                              ContinuousAlgHom.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
                              • f.codRestrict p h = { toAlgHom := (↑f).codRestrict p h, cont := }
                              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
                                • f.rangeRestrict = f.codRestrict (↑f).range
                                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) :
                                  f.rangeRestrict = (↑f).rangeRestrict
                                  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
                                  • p.valA = { toAlgHom := p.val, cont := }
                                  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 : S) (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) :
                                      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
                                      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
                                        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