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.

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

    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

      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
      • One or more equations did not get rendered due to their size.
      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
        • 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_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 : A →A[R] B} {g : A →A[R] B} :
            f = g ∀ (x : A), f x = g x
            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]
                    @[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

                    coercion from ContinuousAlgHom to AlgHom as a RingHom.

                    Equations
                    • ContinuousAlgHom.toAlgHomMonoidHom = { toFun := AlgHomClass.toAlgHom, map_one' := , map_mul' := }
                    Instances For
                      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₂
                              @[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.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
                                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