Isomorphisms of topological algebras #

This file contains an API for ContinuousAlgEquiv R A B, the type of continuous R-algebra isomorphisms with continuous inverses. Here R is a commutative (semi)ring, and A and B are R-algebras with topologies.

Main definitions #

Let R be a commutative semiring and let A and B be R-algebras which are also topological spaces.

ContinuousAlgEquiv R A B: the type of continuous R-algebra isomorphisms from A to B with continuous inverses.

Notation #

A ≃A[R] B : notation for ContinuousAlgEquiv R A B.

Tags #

continuous, isomorphism, algebra

source

structure ContinuousAlgEquiv (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] extends A ≃ₐ[R] B, A ≃ₜ B :

Type (max u_2 u_3)

ContinuousAlgEquiv R A B, with notation A ≃A[R] B, is the type of bijections between the topological R-algebras A and B which are both homeomorphisms and R-algebra isomorphisms.

toFun : A → B
invFun : B → A
left_inv : Function.LeftInverse self.invFun self.toFun
right_inv : Function.RightInverse self.invFun self.toFun
map_mul' (x y : A) : self.toFun (x * y) = self.toFun x * self.toFun y
map_add' (x y : A) : self.toFun (x + y) = self.toFun x + self.toFun y
commutes' (r : R) : self.toFun ((algebraMap R A) r) = (algebraMap R B) r
continuous_toFun : Continuous self.toFun
continuous_invFun : Continuous self.invFun

Instances For

source

def «term_≃A[_]_» :

Lean.TrailingParserDescr

ContinuousAlgEquiv R A B, with notation A ≃A[R] B, is the type of bijections between the topological R-algebras A and B which are both homeomorphisms and R-algebra isomorphisms.

Equations

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

Instances For

source

class ContinuousAlgEquivClass (F : Type u_1) (R : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] [EquivLike F A B] extends AlgEquivClass F R A B, HomeomorphClass F A B :

Prop

ContinuousAlgEquivClass F R A B states that F is a type of topological algebra structure-preserving equivalences. You should extend this class when you extend ContinuousAlgEquiv.

map_mul (f : F) (a b : A) : f (a * b) = f a * f b
map_add (f : F) (a b : A) : f (a + b) = f a + f b
commutes (f : F) (r : R) : f ((algebraMap R A) r) = (algebraMap R B) r
map_continuous (f : F) : Continuous ⇑f
inv_continuous (f : F) : Continuous (EquivLike.inv f)

Instances

source

def ContinuousAlgEquiv.toContinuousAlgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) :

A →A[R] B

The natural coercion from a continuous algebra isomorphism to a continuous algebra morphism.

Equations

↑e = { toAlgHom := ↑e.toAlgEquiv, cont := ⋯ }

Instances For

source

instance ContinuousAlgEquiv.coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :

Coe (A ≃A[R] B) (A →A[R] B)

Equations

ContinuousAlgEquiv.coe = { coe := ContinuousAlgEquiv.toContinuousAlgHom }

source

instance ContinuousAlgEquiv.equivLike {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :

EquivLike (A ≃A[R] B) A B

Equations

ContinuousAlgEquiv.equivLike = { coe := fun (f : A ≃A[R] B) => f.toFun, inv := fun (f : A ≃A[R] B) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

source

instance ContinuousAlgEquiv.continuousAlgEquivClass {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :

ContinuousAlgEquivClass (A ≃A[R] B) R A B

source

theorem ContinuousAlgEquiv.coe_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) (a : A) :

↑e a = e a

source

@[simp]

theorem ContinuousAlgEquiv.coe_mk {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) (he : Continuous e.toFun) (he' : Continuous e.invFun) :

⇑{ toAlgEquiv := e, continuous_toFun := he, continuous_invFun := he' } = ⇑e

source

@[simp]

theorem ContinuousAlgEquiv.coe_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) :

⇑↑e = ⇑e

source

theorem ContinuousAlgEquiv.toAlgEquiv_injective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :

Function.Injective toAlgEquiv

source

theorem ContinuousAlgEquiv.ext {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {f g : A ≃A[R] B} (h : ⇑f = ⇑g) :

f = g

source

theorem ContinuousAlgEquiv.ext_iff {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {f g : A ≃A[R] B} :

f = g ↔ ⇑f = ⇑g

source

theorem ContinuousAlgEquiv.coe_injective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :

Function.Injective toContinuousAlgHom

source

@[simp]

theorem ContinuousAlgEquiv.coe_inj {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {f g : A ≃A[R] B} :

↑f = ↑g ↔ f = g

source

@[simp]

theorem ContinuousAlgEquiv.coe_toAlgEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) :

⇑e.toAlgEquiv = ⇑e

source

theorem ContinuousAlgEquiv.isOpenMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) :

IsOpenMap ⇑e

source

theorem ContinuousAlgEquiv.image_closure {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) (S : Set A) :

⇑e '' closure S = closure (⇑e '' S)

source

theorem ContinuousAlgEquiv.preimage_closure {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) (S : Set B) :

⇑e ⁻¹' closure S = closure (⇑e ⁻¹' S)

source

@[simp]

theorem ContinuousAlgEquiv.isClosed_image {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) {S : Set A} :

IsClosed (⇑e '' S) ↔ IsClosed S

source

theorem ContinuousAlgEquiv.map_nhds_eq {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) (a : A) :

Filter.map (⇑e) (nhds a) = nhds (e a)

source

theorem ContinuousAlgEquiv.map_eq_zero_iff {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) {a : A} :

e a = 0 ↔ a = 0

source

theorem ContinuousAlgEquiv.continuous {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) :

Continuous ⇑e

source

theorem ContinuousAlgEquiv.continuousOn {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) {S : Set A} :

ContinuousOn (⇑e) S

source

theorem ContinuousAlgEquiv.continuousAt {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) {a : A} :

ContinuousAt (⇑e) a

source

theorem ContinuousAlgEquiv.continuousWithinAt {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) {S : Set A} {a : A} :

ContinuousWithinAt (⇑e) S a

source

theorem ContinuousAlgEquiv.comp_continuous_iff {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {α : Type u_5} [TopologicalSpace α] (e : A ≃A[R] B) {f : α → A} :

Continuous (⇑e ∘ f) ↔ Continuous f

source

theorem ContinuousAlgEquiv.comp_continuous_iff' {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {β : Type u_5} [TopologicalSpace β] (e : A ≃A[R] B) {g : B → β} :

Continuous (g ∘ ⇑e) ↔ Continuous g

source

def ContinuousAlgEquiv.refl (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [TopologicalSpace A] [Algebra R A] :

A ≃A[R] A

The identity isomorphism as a continuous R-algebra equivalence.

Equations

ContinuousAlgEquiv.refl R A = { toAlgEquiv := AlgEquiv.refl, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source

@[simp]

theorem ContinuousAlgEquiv.refl_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [TopologicalSpace A] [Algebra R A] (a : A) :

(refl R A) a = a

source

@[simp]

theorem ContinuousAlgEquiv.coe_refl (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [TopologicalSpace A] [Algebra R A] :

↑(refl R A) = ContinuousAlgHom.id R A

source

@[simp]

theorem ContinuousAlgEquiv.coe_refl' (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [TopologicalSpace A] [Algebra R A] :

⇑(refl R A) = id

source

def ContinuousAlgEquiv.symm {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) :

B ≃A[R] A

The inverse of a continuous algebra equivalence.

Equations

e.symm = { toAlgEquiv := e.symm, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source

@[simp]

theorem ContinuousAlgEquiv.apply_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) (b : B) :

e (e.symm b) = b

source

@[simp]

theorem ContinuousAlgEquiv.symm_apply_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) (a : A) :

e.symm (e a) = a

source

@[simp]

theorem ContinuousAlgEquiv.symm_image_image {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) (S : Set A) :

⇑e.symm '' (⇑e '' S) = S

source

@[simp]

theorem ContinuousAlgEquiv.image_symm_image {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) (S : Set B) :

⇑e '' (⇑e.symm '' S) = S

source

@[simp]

theorem ContinuousAlgEquiv.symm_toAlgEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) :

e.symm.toAlgEquiv = e.symm

source

@[simp]

theorem ContinuousAlgEquiv.symm_toHomeomorph {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) :

e.symm.toHomeomorph = e.toHomeomorph.symm

source

theorem ContinuousAlgEquiv.symm_map_nhds_eq {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) (a : A) :

Filter.map (⇑e.symm) (nhds (e a)) = nhds a

source

def ContinuousAlgEquiv.trans {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Semiring C] [TopologicalSpace C] [Algebra R A] [Algebra R B] [Algebra R C] (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) :

A ≃A[R] C

The composition of two continuous algebra equivalences.

Equations

e₁.trans e₂ = { toAlgEquiv := e₁.trans e₂.toAlgEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source

@[simp]

theorem ContinuousAlgEquiv.trans_toAlgEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Semiring C] [TopologicalSpace C] [Algebra R A] [Algebra R B] [Algebra R C] (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) :

(e₁.trans e₂).toAlgEquiv = e₁.trans e₂.toAlgEquiv

source

@[simp]

theorem ContinuousAlgEquiv.trans_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Semiring C] [TopologicalSpace C] [Algebra R A] [Algebra R B] [Algebra R C] (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) (a : A) :

(e₁.trans e₂) a = e₂ (e₁ a)

source

@[simp]

theorem ContinuousAlgEquiv.symm_trans_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Semiring C] [TopologicalSpace C] [Algebra R A] [Algebra R B] [Algebra R C] (e₁ : B ≃A[R] A) (e₂ : C ≃A[R] B) (a : A) :

(e₂.trans e₁).symm a = e₂.symm (e₁.symm a)

source

theorem ContinuousAlgEquiv.comp_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Semiring C] [TopologicalSpace C] [Algebra R A] [Algebra R B] [Algebra R C] (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) :

(↑e₂.toAlgEquiv).comp ↑e₁.toAlgEquiv = ↑(e₁.trans e₂)

source

@[simp]

theorem ContinuousAlgEquiv.coe_comp_coe_symm {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) :

(↑e).comp ↑e.symm = ContinuousAlgHom.id R B

source

@[simp]

theorem ContinuousAlgEquiv.coe_symm_comp_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) :

(↑e.symm).comp ↑e = ContinuousAlgHom.id R A

source

@[simp]

theorem ContinuousAlgEquiv.symm_comp_self {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) :

⇑e.symm ∘ ⇑e = id

source

@[simp]

theorem ContinuousAlgEquiv.self_comp_symm {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) :

⇑e ∘ ⇑e.symm = id

source

@[simp]

theorem ContinuousAlgEquiv.symm_symm {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) :

e.symm.symm = e

source

theorem ContinuousAlgEquiv.symm_bijective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] :

Function.Bijective symm

source

@[simp]

theorem ContinuousAlgEquiv.refl_symm {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Algebra R A] :

(refl R A).symm = refl R A

source

theorem ContinuousAlgEquiv.symm_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) (a : A) :

e.symm.symm a = e a

source

theorem ContinuousAlgEquiv.symm_apply_eq {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) {a : A} {b : B} :

e.symm b = a ↔ b = e a

source

theorem ContinuousAlgEquiv.eq_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) {a : A} {b : B} :

a = e.symm b ↔ e a = b

source

theorem ContinuousAlgEquiv.image_eq_preimage_symm {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) (S : Set A) :

⇑e '' S = ⇑e.symm ⁻¹' S

source

theorem ContinuousAlgEquiv.image_symm_eq_preimage {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) (S : Set B) :

⇑e.symm '' S = ⇑e ⁻¹' S

source

@[simp]

theorem ContinuousAlgEquiv.symm_preimage_preimage {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) (S : Set B) :

⇑e.symm ⁻¹' (⇑e ⁻¹' S) = S

source

@[simp]

theorem ContinuousAlgEquiv.preimage_symm_preimage {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) (S : Set A) :

⇑e ⁻¹' (⇑e.symm ⁻¹' S) = S

source

theorem ContinuousAlgEquiv.isUniformEmbedding {R : Type u_1} [CommSemiring R] {E₁ : Type u_5} {E₂ : Type u_6} [UniformSpace E₁] [UniformSpace E₂] [Ring E₁] [IsUniformAddGroup E₁] [Algebra R E₁] [Ring E₂] [IsUniformAddGroup E₂] [Algebra R E₂] (e : E₁ ≃A[R] E₂) :

IsUniformEmbedding ⇑e

source

theorem AlgEquiv.isUniformEmbedding {R : Type u_1} [CommSemiring R] {E₁ : Type u_5} {E₂ : Type u_6} [UniformSpace E₁] [UniformSpace E₂] [Ring E₁] [IsUniformAddGroup E₁] [Algebra R E₁] [Ring E₂] [IsUniformAddGroup E₂] [Algebra R E₂] (e : E₁ ≃ₐ[R] E₂) (h₁ : Continuous ⇑e) (h₂ : Continuous ⇑e.symm) :

IsUniformEmbedding ⇑e

source

theorem ContinuousAlgEquiv.surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [TopologicalSpace A] [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] (e : A ≃A[R] B) :

Function.Surjective ⇑e

source

def ContinuousAlgEquiv.cast {R : Type u_1} [CommSemiring R] {ι : Type u_5} {A : ι → Type u_6} [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] [(i : ι) → TopologicalSpace (A i)] {i j : ι} (h : i = j) :

A i ≃A[R] A j

Equiv.cast (congrArg _ h) as a continuous algebra equiv.

Note that unlike Equiv.cast, this takes an equality of indices rather than an equality of types, to avoid having to deal with an equality of the algebraic structure itself.

Equations

ContinuousAlgEquiv.cast h = { toAlgEquiv := AlgEquiv.cast h, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source

@[simp]

theorem ContinuousAlgEquiv.cast_apply {R : Type u_1} [CommSemiring R] {ι : Type u_5} {A : ι → Type u_6} [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] [(i : ι) → TopologicalSpace (A i)] {i j : ι} (h : i = j) (x : A i) :

(cast h) x = (Equiv.cast ⋯) x

source

@[simp]

theorem ContinuousAlgEquiv.cast_symm_apply {R : Type u_1} [CommSemiring R] {ι : Type u_5} {A : ι → Type u_6} [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] [(i : ι) → TopologicalSpace (A i)] {i j : ι} (h : i = j) (x : A j) :

(cast h).symm x = (Equiv.cast ⋯) x

Documentation

Mathlib.Topology.Algebra.Algebra.Equiv

Isomorphisms of topological algebras #

Main definitions #

Notation #

Tags #