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.

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)

theorem continuous_algebraMap_iff_smul (R : Type u_1) (A : Type u) [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace R] [TopologicalSpace A] [IsTopologicalSemiring A] : Continuous ⇑(algebraMap R A) ↔ Continuous fun (p : R × A) => p.1 • p.2

theorem continuousSMul_of_algebraMap (R : Type u_1) (A : Type u) [CommSemiring R] [Semiring A] [Algebra R A] [TopologicalSpace R] [TopologicalSpace A] [IsTopologicalSemiring A] (h : Continuous ⇑(algebraMap R A)) : ContinuousSMul R A

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

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

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

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)

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

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.

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

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.

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

@[simp]

theorem ContinuousAlgHom.toAlgHom_eq_coe {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) : f.toAlgHom = ↑f

@[simp]

theorem ContinuousAlgHom.coe_inj {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {f g : A →A[R] B} : ↑f = ↑g ↔ f = g

@[simp]

theorem ContinuousAlgHom.coe_mk {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (h : Continuous (↑↑f.toRingHom).toFun) : ↑{ toAlgHom := f, cont := h } = f

@[simp]

theorem ContinuousAlgHom.coe_mk' {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (h : Continuous (↑↑f.toRingHom).toFun) : ⇑{ toAlgHom := f, cont := h } = ⇑f

@[simp]

theorem ContinuousAlgHom.coe_coe {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) : ⇑↑f = ⇑f

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

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

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₂) : UniformContinuous ⇑f

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

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

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

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 = { toRingHom := f.copy f' h, commutes' := ⋯, cont := ⋯ }

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

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

theorem ContinuousAlgHom.map_zero {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) : f 0 = 0

theorem ContinuousAlgHom.map_add {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) (x y : A) : f (x + y) = f x + f y

theorem ContinuousAlgHom.map_smul {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) (c : R) (x : A) : f (c • x) = c • f x

theorem ContinuousAlgHom.map_smul_of_tower {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] {R : Type u_4} {S : Type u_5} [CommSemiring S] [SMul R A] [Algebra S A] [SMul R B] [Algebra S B] [MulActionHomClass (A →A[S] B) R A B] (f : A →A[S] B) (c : R) (x : A) : f (c • x) = c • f x

theorem ContinuousAlgHom.map_sum {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {ι : Type u_4} (f : A →A[R] B) (s : Finset ι) (g : ι → A) : f (∑ i ∈ s, g i) = ∑ i ∈ s, f (g i)

theorem ContinuousAlgHom.ext_ring {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] [TopologicalSpace R] {f g : R →A[R] A} : f = g

Any two continuous R-algebra morphisms from R are equal

theorem ContinuousAlgHom.ext_ring_iff {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] [TopologicalSpace R] {f g : R →A[R] A} : f = g ↔ f 1 = g 1

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

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

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

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

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

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) (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.

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

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.

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

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 }

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

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

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

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

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

@[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 := ⋯ }

@[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 g : A →A[R] A) : f * g = f.comp g

@[simp]

theorem ContinuousAlgHom.coe_mul {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] (f g : A →A[R] A) : ⇑(f * g) = ⇑f ∘ ⇑g

theorem ContinuousAlgHom.mul_apply {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] (f g : A →A[R] A) (x : A) : (f * g) x = f (g x)

instance ContinuousAlgHom.instMonoid {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] : Monoid (A →A[R] A)

Equations

• 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]

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

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

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

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

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)

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

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

@[simp]

theorem ContinuousAlgHom.coe_fst {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] : ↑(fst R A B) = AlgHom.fst R A B

@[simp]

theorem ContinuousAlgHom.coe_fst' {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] : ⇑(fst R A B) = Prod.fst

@[simp]

theorem ContinuousAlgHom.coe_snd {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] : ↑(snd R A B) = AlgHom.snd R A B

@[simp]

theorem ContinuousAlgHom.coe_snd' {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] : ⇑(snd R A B) = Prod.snd

@[simp]

theorem ContinuousAlgHom.fst_prod_snd {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] : (fst R A B).prod (snd R A B) = ContinuousAlgHom.id R (A × B)

@[simp]

theorem ContinuousAlgHom.fst_comp_prod {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] (f : A →A[R] B) (g : A →A[R] C) : (fst R B C).comp (f.prod g) = f

@[simp]

theorem ContinuousAlgHom.snd_comp_prod {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] (f : A →A[R] B) (g : A →A[R] C) : (snd R B C).comp (f.prod g) = g

def ContinuousAlgHom.prodMap {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] {D : Type u_6} [Semiring D] [TopologicalSpace D] [Algebra R D] (f₁ : A →A[R] B) (f₂ : C →A[R] D) : A × C →A[R] B × D

Prod.map of two continuous algebra homomorphisms.

Equations

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

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

@[simp]

theorem ContinuousAlgHom.prodEquiv_apply {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] (f : (A →A[R] B) × (A →A[R] C)) : prodEquiv f = f.1.prod f.2

def ContinuousAlgHom.codRestrict {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (f : A →A[R] B) (p : Subalgebra R B) (h : ∀ (x : A), f x ∈ p) : A →A[R] ↥p

Restrict codomain of a continuous algebra morphism.

Equations

• f.codRestrict p h = { toAlgHom := (↑f).codRestrict p h, cont := ⋯ }

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 ⋯

@[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 := ⋯ }

@[simp]

theorem Subalgebra.coe_valA {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] (p : Subalgebra R A) : ↑↑p.valA = p.subtype

@[simp]

theorem Subalgebra.coe_valA' {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] (p : Subalgebra R A) : ⇑p.valA = ⇑p.subtype

@[simp]

theorem Subalgebra.valA_apply {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] (p : Subalgebra R A) (x : ↥p) : p.valA x = ↑x

@[simp]

theorem Submodule.range_valA {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] [Algebra R A] (p : Subalgebra R A) : (↑p.valA).range = p

theorem ContinuousAlgHom.map_neg (R : Type u_1) [CommSemiring R] {S : Type u_3} [Ring S] [TopologicalSpace S] [Algebra R S] {B : Type u_4} [Ring B] [TopologicalSpace B] [Algebra R B] (f : S →A[R] B) (x : S) : f (-x) = -f x

theorem ContinuousAlgHom.map_sub (R : Type u_1) [CommSemiring R] {S : Type u_3} [Ring S] [TopologicalSpace S] [Algebra R S] {B : Type u_4} [Ring B] [TopologicalSpace B] [Algebra R B] (f : S →A[R] B) (x y : S) : f (x - y) = f x - f y

def ContinuousAlgHom.restrictScalars (R : Type u_1) [CommSemiring R] {S : Type u_3} [CommSemiring S] [Algebra R S] {B : Type u_4} [Ring B] [TopologicalSpace B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] {C : Type u_5} [Ring C] [TopologicalSpace C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] (f : B →A[S] C) : B →A[R] C

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

Equations

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

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

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

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

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

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

theorem Subalgebra.topologicalClosure_minimal {R : Type u_1} [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] (s : Subalgebra R A) {t : Subalgebra R A} (h : s ≤ t) (ht : IsClosed ↑t) : s.topologicalClosure ≤ t

@[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 = CommSemiring.mk ⋯

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.

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

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

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

Alias of Algebra.elemental.

---

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

Equations

• Algebra.elementalAlgebra = Algebra.elemental

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

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

theorem Algebra.self_mem_elementalAlgebra (R : Type u_1) [CommSemiring R] {A : Type u} [TopologicalSpace A] [Semiring A] [Algebra R A] [IsTopologicalSemiring A] (x : A) : x ∈ elemental R x

Alias of Algebra.elemental.self_mem.

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

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

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)

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 ⋯

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)

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.

@[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 = CommRing.mk ⋯

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 = CommRing.mk ⋯