# 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.

source
theorem continuous_algebraMap (R : Type u_1) (A : Type u) [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace R] [TopologicalSpace A] [ContinuousSMul R A] :
Continuous ⇑(algebraMap R A)
source
theorem continuous_algebraMap_iff_smul (R : Type u_1) (A : Type u) [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace R] [TopologicalSpace A] [ContinuousMul A] :
Continuous ⇑(algebraMap R A) ↔ Continuous fun (p : R × A) => p.1 • p.2
source
theorem continuousSMul_of_algebraMap (R : Type u_1) (A : Type u) [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace R] [TopologicalSpace A] [ContinuousMul A] (h : Continuous ⇑(algebraMap R A)) :
ContinuousSMul R A
source
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] :
ContinuousSMul (↥S) X
source
def algebraMapCLM (R : Type u_1) (A : Type u) [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace R] [TopologicalSpace A] [ContinuousSMul R A] :
R →L[R] A

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

Equations

- algebraMapCLM R A = { toFun := ⇑(algebraMap R A), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

Instances For

source
@[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
source
theorem algebraMapCLM_coe (R : Type u_1) (A : Type u) [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace R] [TopologicalSpace A] [ContinuousSMul R A] :
⇑(algebraMapCLM R A) = ⇑(algebraMap R A)
source
theorem algebraMapCLM_toLinearMap (R : Type u_1) (A : Type u) [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace R] [TopologicalSpace A] [ContinuousSMul R A] :
↑(algebraMapCLM R A) = Algebra.linearMap R A
source
theorem DiscreteTopology.instContinuousSMul (R : Type u_1) (A : Type u) [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace R] [TopologicalSpace A] [IsTopologicalSemiring A] [DiscreteTopology R] :
ContinuousSMul R 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.

source
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`.

- toFun : A → B
- 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

source
def «term_→A[_]_» :
Lean.TrailingParserDescr

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

source
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' := ⋯ }

source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
instance ContinuousAlgHom.instContinuousMapClass {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] :
ContinuousMapClass (A →A[R] B) A B
source
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) :
Continuous ⇑f
source
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₂) :
UniformContinuous ⇑f
source
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) :
A → B

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

Equations

- ContinuousAlgHom.Simps.apply h = ⇑h

Instances For

source
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) :
A →ₐ[R] B

See Note [custom simps projection].

Equations

- ContinuousAlgHom.Simps.coe h = ↑h

Instances For

source
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
source
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
source
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' : A → B) (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 = { toAlgHom := let __RingHom := f.copy f' h; { toRingHom := __RingHom, commutes' := ⋯ }, cont := ⋯ }

Instances For

source
@[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' : A → B) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
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' : A → B) (h : f' = ⇑f) :
f.copy f' h = f
source
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
source
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
source
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
source
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
source
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 (∑ i ∈ s, g i) = ∑ i ∈ s, f (g i)
source
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

source
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
source
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.

source
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.

source
def Subalgebra.topologicalClosure {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] [IsTopologicalSemiring A] (s : Subalgebra R A) :
Subalgebra R A

The topological closure of a subalgebra

Equations

- s.topologicalClosure = { toSubsemiring := s.topologicalClosure, algebraMap_mem' := ⋯ }

Instances For

source
theorem Subalgebra.map_topologicalClosure_le {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] [IsTopologicalSemiring A] [IsTopologicalSemiring B] (f : A →A[R] B) (s : Subalgebra R A) :
map (↑f) s.topologicalClosure ≤ (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.

source
theorem Subalgebra.topologicalClosure_map_le {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] [IsTopologicalSemiring A] [IsTopologicalSemiring B] (f : A →ₐ[R] B) (hf : IsClosedMap ⇑f) (s : Subalgebra R A) :
(map f s).topologicalClosure ≤ map f s.topologicalClosure
source
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] [IsTopologicalSemiring A] [IsTopologicalSemiring B] (f : A →A[R] B) (hf : IsClosedMap ⇑f) (s : Subalgebra R A) :
(map f.toAlgHom s).topologicalClosure = map f.toAlgHom s.topologicalClosure
source
@[simp]
theorem Subalgebra.topologicalClosure_coe {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] [IsTopologicalSemiring A] (s : Subalgebra R A) :
↑s.topologicalClosure = closure ↑s
source
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] [IsTopologicalSemiring A] [IsTopologicalSemiring 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.

source
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

- ContinuousAlgHom.id R A = { toAlgHom := AlgHom.id R A, cont := ⋯ }

Instances For

source
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

- ContinuousAlgHom.instOne R A = { one := ContinuousAlgHom.id R A }

source
theorem ContinuousAlgHom.one_def (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [TopologicalSpace A] [Algebra R A] :
1 = ContinuousAlgHom.id R A
source
theorem ContinuousAlgHom.id_apply (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [TopologicalSpace A] [Algebra R A] (x : A) :
(ContinuousAlgHom.id R A) x = x
source
@[simp]
theorem ContinuousAlgHom.coe_id (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [TopologicalSpace A] [Algebra R A] :
↑(ContinuousAlgHom.id R A) = AlgHom.id R A
source
@[simp]
theorem ContinuousAlgHom.coe_id' (R : Type u_1) [CommSemiring R] (A : Type u_2) [Semiring A] [TopologicalSpace A] [Algebra R A] :
⇑(ContinuousAlgHom.id R A) = id
source
@[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} :
↑f = AlgHom.id R A ↔ f = ContinuousAlgHom.id R A
source
@[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
source
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

source
@[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
source
@[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
source
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)
source
@[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
source
@[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
source
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)
source
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 }

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

- One or more equations did not get rendered due to their size.

source
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]
source
def ContinuousAlgHom.toAlgHomMonoidHom {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] :
(A →A[R] A) →* A →ₐ[R] A

coercion from `ContinuousAlgHom` to `AlgHom` as a `RingHom`.

Equations

- ContinuousAlgHom.toAlgHomMonoidHom = { toFun := AlgHomClass.toAlgHom, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
@[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) :
toAlgHomMonoidHom f = ↑f
source
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

source
@[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₂
source
@[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)
source
instance ContinuousAlgHom.instCompleteSpaceSubtypeMemSubalgebraEqualizerOfT2SpaceOfContinuousMapClass {R : Type u_1} [CommSemiring R] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R B] {F : Type u_5} {D : Type u_6} [UniformSpace D] [CompleteSpace D] [Semiring D] [Algebra R D] [T2Space B] [FunLike F D B] [AlgHomClass F R D B] [ContinuousMapClass F D B] (f g : F) :
CompleteSpace ↥(AlgHom.equalizer f g)
source
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

- ContinuousAlgHom.fst R A B = { toAlgHom := AlgHom.fst R A B, cont := ⋯ }

Instances For

source
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

- ContinuousAlgHom.snd R A B = { toAlgHom := AlgHom.snd R A B, cont := ⋯ }

Instances For

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

- f₁.prodMap f₂ = (f₁.comp (ContinuousAlgHom.fst R A C)).prod (f₂.comp (ContinuousAlgHom.snd R A C))

Instances For

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

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

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

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

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

- ContinuousAlgHom.restrictScalars R f = { toAlgHom := AlgHom.restrictScalars R ↑f, cont := ⋯ }

Instances For

source
@[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) = AlgHom.restrictScalars R ↑f
source
@[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
source
instance instIsTopologicalSemiringSubtypeMemSubalgebra {R : Type u_1} [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] (s : Subalgebra R A) :
IsTopologicalSemiring ↥s
source
theorem Subalgebra.le_topologicalClosure {R : Type u_1} [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] (s : Subalgebra R A) :
s ≤ s.topologicalClosure
source
theorem Subalgebra.isClosed_topologicalClosure {R : Type u_1} [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] (s : Subalgebra R A) :
IsClosed ↑s.topologicalClosure
source
theorem Subalgebra.topologicalClosure_minimal {R : Type u_1} [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] {s t : Subalgebra R A} (h : s ≤ t) (ht : IsClosed ↑t) :
s.topologicalClosure ≤ t
source
theorem Subalgebra.topologicalClosure_adjoin_le_centralizer_centralizer (R : Type u_1) [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] [T2Space A] (s : Set A) :
(Algebra.adjoin R s).topologicalClosure ≤ centralizer R ↑(centralizer R s)
source
@[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) :
CommSemiring ↥s.topologicalClosure

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

See note [reducible non-instances].

Equations

- s.commSemiringTopologicalClosure hs = { toSemiring := s.topologicalClosure.toSemiring, mul_comm := ⋯ }

Instances For

source
theorem Subalgebra.topologicalClosure_comap_homeomorph {R : Type u_1} [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] (s : Subalgebra R A) {B : Type u_2} [TopologicalSpace B] [Ring B] [IsTopologicalRing B] [Algebra R B] (f : B →ₐ[R] A) (f' : B ≃ₜ A) (w : ⇑f = ⇑f') :
comap f s.topologicalClosure = (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.

source
def Algebra.elemental (R : Type u_1) [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] (x : A) :
Subalgebra R A

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

Equations

- Algebra.elemental R x = (Algebra.adjoin R {x}).topologicalClosure

Instances For

source
@[simp]
theorem Algebra.elemental.self_mem (R : Type u_1) [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] (x : A) :
x ∈ elemental R x
source
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) :
elemental R x ≤ s
source
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
source
instance Algebra.elemental.isClosed (R : Type u_1) [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] (x : A) :
IsClosed ↑(elemental R x)
source
instance Algebra.elemental.instCommSemiringSubtypeMemSubalgebraOfT2Space (R : Type u_1) [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] [T2Space A] {x : A} :
CommSemiring ↥(elemental R x)
Equations

- Algebra.elemental.instCommSemiringSubtypeMemSubalgebraOfT2Space R = (Algebra.adjoin R {x}).commSemiringTopologicalClosure ⋯

source
instance Algebra.elemental.instCompleteSpaceSubtypeMemSubalgebra (R : Type u_1) [CommSemiring R] {A : Type u_2} [UniformSpace A] [CompleteSpace A] [Semiring A] [IsTopologicalSemiring A] [Algebra R A] (x : A) :
CompleteSpace ↥(elemental R x)
source
theorem Algebra.elemental.isClosedEmbedding_coe (R : Type u_1) [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] (x : A) :
Topology.IsClosedEmbedding Subtype.val

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

source
theorem Algebra.elemental.le_centralizer_centralizer (R : Type u_1) [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] [T2Space A] (x : A) :
elemental R x ≤ Subalgebra.centralizer R ↑(Subalgebra.centralizer R {x})
source
@[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) :
CommRing ↥s.topologicalClosure

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

Equations

- s.commRingTopologicalClosure hs = { toRing := s.topologicalClosure.toRing, mul_comm := ⋯ }

Instances For

source
instance instCommRingSubtypeMemSubalgebraElementalOfT2Space {R : Type u_1} [CommRing R] {A : Type u} [TopologicalSpace A] [Ring A] [Algebra R A] [IsTopologicalRing A] [T2Space A] {x : A} :
CommRing ↥(Algebra.elemental R x)
Equations

- instCommRingSubtypeMemSubalgebraElementalOfT2Space = { toRing := (Algebra.elemental R x).toRing, mul_comm := ⋯ }