topology.algebra.continuous_monoid_hom

source

structure continuous_monoid_hom (A : Type u_1) (B : Type u_2) [monoid A] [monoid B] [topological_space A] [topological_space B] :

Type (max u_1 u_2)

to_fun : A → B
map_one' : self.to_fun 1 = 1
map_mul' : ∀ (x y : A), self.to_fun (x * y) = (self.to_fun x) * self.to_fun y
continuous_to_fun : continuous self.to_fun . "continuity'"

Continuous homomorphisms between two topological groups.

source

def continuous_monoid_hom.to_continuous_map {A : Type u_1} {B : Type u_2} [monoid A] [monoid B] [topological_space A] [topological_space B] (self : continuous_monoid_hom A B) :

C(A, B)

Reinterpret a continuous_monoid_hom as a continuous_map.

source

def continuous_monoid_hom.to_monoid_hom {A : Type u_1} {B : Type u_2} [monoid A] [monoid B] [topological_space A] [topological_space B] (self : continuous_monoid_hom A B) :

A →* B

Reinterpret a continuous_monoid_hom as a monoid_hom.

source

def continuous_add_monoid_hom.to_add_monoid_hom {A : Type u_6} {B : Type u_7} [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] (self : continuous_add_monoid_hom A B) :

A →+ B

Reinterpret a continuous_add_monoid_hom as an add_monoid_hom.

source

structure continuous_add_monoid_hom (A : Type u_6) (B : Type u_7) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :

Type (max u_6 u_7)

to_fun : A → B
map_zero' : self.to_fun 0 = 0
map_add' : ∀ (x y : A), self.to_fun (x + y) = self.to_fun x + self.to_fun y
continuous_to_fun : continuous self.to_fun . "continuity'"

Continuous homomorphisms between two topological groups.

source

def continuous_add_monoid_hom.to_continuous_map {A : Type u_6} {B : Type u_7} [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] (self : continuous_add_monoid_hom A B) :

C(A, B)

Reinterpret a continuous_add_monoid_hom as a continuous_map.

source

@[protected, instance]

def continuous_monoid_hom.has_coe_to_fun {A : Type u_1} {B : Type u_2} [monoid A] [monoid B] [topological_space A] [topological_space B] :

has_coe_to_fun (continuous_monoid_hom A B) (λ (_x : continuous_monoid_hom A B), A → B)

Equations

continuous_monoid_hom.has_coe_to_fun = {coe := continuous_monoid_hom.to_fun _inst_7}

source

@[protected, instance]

def continuous_add_monoid_hom.has_coe_to_fun {A : Type u_1} {B : Type u_2} [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :

has_coe_to_fun (continuous_add_monoid_hom A B) (λ (_x : continuous_add_monoid_hom A B), A → B)

Equations

continuous_add_monoid_hom.has_coe_to_fun = {coe := continuous_add_monoid_hom.to_fun _inst_7}

source

theorem continuous_add_monoid_hom.ext {A : Type u_1} {B : Type u_2} [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] {f g : continuous_add_monoid_hom A B} (h : ∀ (x : A), ⇑f x = ⇑g x) :

f = g

source

theorem continuous_monoid_hom.ext {A : Type u_1} {B : Type u_2} [monoid A] [monoid B] [topological_space A] [topological_space B] {f g : continuous_monoid_hom A B} (h : ∀ (x : A), ⇑f x = ⇑g x) :

f = g

source

@[simp]

theorem continuous_add_monoid_hom.mk'_apply {A : Type u_1} {B : Type u_2} [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] (f : A →+ B) (hf : continuous ⇑f) (ᾰ : A) :

(continuous_add_monoid_hom.mk' f hf).to_fun ᾰ = f.to_fun ᾰ

source

def continuous_add_monoid_hom.mk' {A : Type u_1} {B : Type u_2} [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] (f : A →+ B) (hf : continuous ⇑f) :

continuous_add_monoid_hom A B

Construct a continuous_add_monoid_hom from a continuous add_monoid_hom.

Equations

continuous_add_monoid_hom.mk' f hf = {to_fun := f.to_fun, map_zero' := _, map_add' := _, continuous_to_fun := hf}

source

@[simp]

theorem continuous_monoid_hom.mk'_apply {A : Type u_1} {B : Type u_2} [monoid A] [monoid B] [topological_space A] [topological_space B] (f : A →* B) (hf : continuous ⇑f) (ᾰ : A) :

(continuous_monoid_hom.mk' f hf).to_fun ᾰ = f.to_fun ᾰ

source

def continuous_monoid_hom.mk' {A : Type u_1} {B : Type u_2} [monoid A] [monoid B] [topological_space A] [topological_space B] (f : A →* B) (hf : continuous ⇑f) :

continuous_monoid_hom A B

Construct a continuous_monoid_hom from a continuous monoid_hom.

Equations

continuous_monoid_hom.mk' f hf = {to_fun := f.to_fun, map_one' := _, map_mul' := _, continuous_to_fun := hf}

source

def continuous_add_monoid_hom.comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [add_monoid A] [add_monoid B] [add_monoid C] [topological_space A] [topological_space B] [topological_space C] (g : continuous_add_monoid_hom B C) (f : continuous_add_monoid_hom A B) :

continuous_add_monoid_hom A C

Composition of two continuous homomorphisms.

Equations

g.comp f = continuous_add_monoid_hom.mk' (g.to_add_monoid_hom.comp f.to_add_monoid_hom) _

source

def continuous_monoid_hom.comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [monoid A] [monoid B] [monoid C] [topological_space A] [topological_space B] [topological_space C] (g : continuous_monoid_hom B C) (f : continuous_monoid_hom A B) :

continuous_monoid_hom A C

Composition of two continuous homomorphisms.

Equations

g.comp f = continuous_monoid_hom.mk' (g.to_monoid_hom.comp f.to_monoid_hom) _

source

@[simp]

theorem continuous_monoid_hom.comp_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} [monoid A] [monoid B] [monoid C] [topological_space A] [topological_space B] [topological_space C] (g : continuous_monoid_hom B C) (f : continuous_monoid_hom A B) (ᾰ : A) :

(g.comp f).to_fun ᾰ = ⇑(g.to_monoid_hom) (⇑(f.to_monoid_hom) ᾰ)

source

@[simp]

theorem continuous_add_monoid_hom.comp_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} [add_monoid A] [add_monoid B] [add_monoid C] [topological_space A] [topological_space B] [topological_space C] (g : continuous_add_monoid_hom B C) (f : continuous_add_monoid_hom A B) (ᾰ : A) :

(g.comp f).to_fun ᾰ = ⇑(g.to_add_monoid_hom) (⇑(f.to_add_monoid_hom) ᾰ)

source

def continuous_add_monoid_hom.sum {A : Type u_1} {B : Type u_2} {C : Type u_3} [add_monoid A] [add_monoid B] [add_monoid C] [topological_space A] [topological_space B] [topological_space C] (f : continuous_add_monoid_hom A B) (g : continuous_add_monoid_hom A C) :

continuous_add_monoid_hom A (B × C)

Product of two continuous homomorphisms on the same space.

Equations

f.sum g = continuous_add_monoid_hom.mk' (f.to_add_monoid_hom.prod g.to_add_monoid_hom) _

source

def continuous_monoid_hom.prod {A : Type u_1} {B : Type u_2} {C : Type u_3} [monoid A] [monoid B] [monoid C] [topological_space A] [topological_space B] [topological_space C] (f : continuous_monoid_hom A B) (g : continuous_monoid_hom A C) :

continuous_monoid_hom A (B × C)

Product of two continuous homomorphisms on the same space.

Equations

f.prod g = continuous_monoid_hom.mk' (f.to_monoid_hom.prod g.to_monoid_hom) _

source

@[simp]

theorem continuous_monoid_hom.prod_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} [monoid A] [monoid B] [monoid C] [topological_space A] [topological_space B] [topological_space C] (f : continuous_monoid_hom A B) (g : continuous_monoid_hom A C) (ᾰ : A) :

(f.prod g).to_fun ᾰ = (⇑(f.to_monoid_hom) ᾰ, ⇑(g.to_monoid_hom) ᾰ)

source

@[simp]

theorem continuous_add_monoid_hom.sum_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} [add_monoid A] [add_monoid B] [add_monoid C] [topological_space A] [topological_space B] [topological_space C] (f : continuous_add_monoid_hom A B) (g : continuous_add_monoid_hom A C) (ᾰ : A) :

(f.sum g).to_fun ᾰ = (⇑(f.to_add_monoid_hom) ᾰ, ⇑(g.to_add_monoid_hom) ᾰ)

source

def continuous_monoid_hom.prod_map {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [monoid A] [monoid B] [monoid C] [monoid D] [topological_space A] [topological_space B] [topological_space C] [topological_space D] (f : continuous_monoid_hom A C) (g : continuous_monoid_hom B D) :

continuous_monoid_hom (A × B) (C × D)

Product of two continuous homomorphisms on different spaces.

Equations

f.prod_map g = continuous_monoid_hom.mk' (f.to_monoid_hom.prod_map g.to_monoid_hom) _

source

@[simp]

theorem continuous_monoid_hom.prod_map_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [monoid A] [monoid B] [monoid C] [monoid D] [topological_space A] [topological_space B] [topological_space C] [topological_space D] (f : continuous_monoid_hom A C) (g : continuous_monoid_hom B D) (ᾰ : A × B) :

(f.prod_map g).to_fun ᾰ = (⇑(f.to_monoid_hom) ᾰ.fst, ⇑(g.to_monoid_hom) ᾰ.snd)

source

@[simp]

theorem continuous_add_monoid_hom.sum_map_apply {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [add_monoid A] [add_monoid B] [add_monoid C] [add_monoid D] [topological_space A] [topological_space B] [topological_space C] [topological_space D] (f : continuous_add_monoid_hom A C) (g : continuous_add_monoid_hom B D) (ᾰ : A × B) :

(f.sum_map g).to_fun ᾰ = (⇑(f.to_add_monoid_hom) ᾰ.fst, ⇑(g.to_add_monoid_hom) ᾰ.snd)

source

def continuous_add_monoid_hom.sum_map {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [add_monoid A] [add_monoid B] [add_monoid C] [add_monoid D] [topological_space A] [topological_space B] [topological_space C] [topological_space D] (f : continuous_add_monoid_hom A C) (g : continuous_add_monoid_hom B D) :

continuous_add_monoid_hom (A × B) (C × D)

Product of two continuous homomorphisms on different spaces.

Equations

f.sum_map g = continuous_add_monoid_hom.mk' (f.to_add_monoid_hom.prod_map g.to_add_monoid_hom) _

source

@[simp]

theorem continuous_monoid_hom.one_apply (A : Type u_1) (B : Type u_2) [monoid A] [monoid B] [topological_space A] [topological_space B] (ᾰ : A) :

(continuous_monoid_hom.one A B).to_fun ᾰ = 1

source

def continuous_add_monoid_hom.zero (A : Type u_1) (B : Type u_2) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :

continuous_add_monoid_hom A B

The trivial continuous homomorphism.

Equations

continuous_add_monoid_hom.zero A B = continuous_add_monoid_hom.mk' 0 _

source

@[simp]

theorem continuous_add_monoid_hom.zero_apply (A : Type u_1) (B : Type u_2) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] (ᾰ : A) :

(continuous_add_monoid_hom.zero A B).to_fun ᾰ = 0

source

def continuous_monoid_hom.one (A : Type u_1) (B : Type u_2) [monoid A] [monoid B] [topological_space A] [topological_space B] :

continuous_monoid_hom A B

The trivial continuous homomorphism.

Equations

continuous_monoid_hom.one A B = continuous_monoid_hom.mk' 1 _

source

@[protected, instance]

def continuous_monoid_hom.inhabited (A : Type u_1) (B : Type u_2) [monoid A] [monoid B] [topological_space A] [topological_space B] :

inhabited (continuous_monoid_hom A B)

Equations

continuous_monoid_hom.inhabited A B = {default := continuous_monoid_hom.one A B _inst_7}

source

@[protected, instance]

def continuous_add_monoid_hom.inhabited (A : Type u_1) (B : Type u_2) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :

inhabited (continuous_add_monoid_hom A B)

Equations

continuous_add_monoid_hom.inhabited A B = {default := continuous_add_monoid_hom.zero A B _inst_7}

source

@[simp]

theorem continuous_add_monoid_hom.id_apply (A : Type u_1) [add_monoid A] [topological_space A] (ᾰ : A) :

(continuous_add_monoid_hom.id A).to_fun ᾰ = ᾰ

source

@[simp]

theorem continuous_monoid_hom.id_apply (A : Type u_1) [monoid A] [topological_space A] (ᾰ : A) :

(continuous_monoid_hom.id A).to_fun ᾰ = ᾰ

source

def continuous_add_monoid_hom.id (A : Type u_1) [add_monoid A] [topological_space A] :

continuous_add_monoid_hom A A

The identity continuous homomorphism.

Equations

continuous_add_monoid_hom.id A = continuous_add_monoid_hom.mk' (add_monoid_hom.id A) continuous_id

source

def continuous_monoid_hom.id (A : Type u_1) [monoid A] [topological_space A] :

continuous_monoid_hom A A

The identity continuous homomorphism.

Equations

continuous_monoid_hom.id A = continuous_monoid_hom.mk' (monoid_hom.id A) continuous_id

source

def continuous_monoid_hom.fst (A : Type u_1) (B : Type u_2) [monoid A] [monoid B] [topological_space A] [topological_space B] :

continuous_monoid_hom (A × B) A

The continuous homomorphism given by projection onto the first factor.

Equations

continuous_monoid_hom.fst A B = continuous_monoid_hom.mk' (monoid_hom.fst A B) continuous_fst

source

@[simp]

theorem continuous_monoid_hom.fst_apply (A : Type u_1) (B : Type u_2) [monoid A] [monoid B] [topological_space A] [topological_space B] (ᾰ : A × B) :

(continuous_monoid_hom.fst A B).to_fun ᾰ = ᾰ.fst

source

def continuous_add_monoid_hom.fst (A : Type u_1) (B : Type u_2) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :

continuous_add_monoid_hom (A × B) A

The continuous homomorphism given by projection onto the first factor.

Equations

continuous_add_monoid_hom.fst A B = continuous_add_monoid_hom.mk' (add_monoid_hom.fst A B) continuous_fst

source

@[simp]

theorem continuous_add_monoid_hom.fst_apply (A : Type u_1) (B : Type u_2) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] (ᾰ : A × B) :

(continuous_add_monoid_hom.fst A B).to_fun ᾰ = ᾰ.fst

source

def continuous_monoid_hom.snd (A : Type u_1) (B : Type u_2) [monoid A] [monoid B] [topological_space A] [topological_space B] :

continuous_monoid_hom (A × B) B

The continuous homomorphism given by projection onto the second factor.

Equations

continuous_monoid_hom.snd A B = continuous_monoid_hom.mk' (monoid_hom.snd A B) continuous_snd

source

def continuous_add_monoid_hom.snd (A : Type u_1) (B : Type u_2) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :

continuous_add_monoid_hom (A × B) B

The continuous homomorphism given by projection onto the second factor.

Equations

continuous_add_monoid_hom.snd A B = continuous_add_monoid_hom.mk' (add_monoid_hom.snd A B) continuous_snd

source

@[simp]

theorem continuous_add_monoid_hom.snd_apply (A : Type u_1) (B : Type u_2) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] (ᾰ : A × B) :

(continuous_add_monoid_hom.snd A B).to_fun ᾰ = ᾰ.snd

source

@[simp]

theorem continuous_monoid_hom.snd_apply (A : Type u_1) (B : Type u_2) [monoid A] [monoid B] [topological_space A] [topological_space B] (ᾰ : A × B) :

(continuous_monoid_hom.snd A B).to_fun ᾰ = ᾰ.snd

source

@[simp]

theorem continuous_add_monoid_hom.inl_apply (A : Type u_1) (B : Type u_2) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] (ᾰ : A) :

(continuous_add_monoid_hom.inl A B).to_fun ᾰ = (⇑((continuous_add_monoid_hom.id A).to_add_monoid_hom) ᾰ, ⇑((continuous_add_monoid_hom.zero A B).to_add_monoid_hom) ᾰ)

source

def continuous_monoid_hom.inl (A : Type u_1) (B : Type u_2) [monoid A] [monoid B] [topological_space A] [topological_space B] :

continuous_monoid_hom A (A × B)

The continuous homomorphism given by inclusion of the first factor.

Equations

continuous_monoid_hom.inl A B = (continuous_monoid_hom.id A).prod (continuous_monoid_hom.one A B)

source

def continuous_add_monoid_hom.inl (A : Type u_1) (B : Type u_2) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :

continuous_add_monoid_hom A (A × B)

The continuous homomorphism given by inclusion of the first factor.

Equations

continuous_add_monoid_hom.inl A B = (continuous_add_monoid_hom.id A).sum (continuous_add_monoid_hom.zero A B)

source

@[simp]

theorem continuous_monoid_hom.inl_apply (A : Type u_1) (B : Type u_2) [monoid A] [monoid B] [topological_space A] [topological_space B] (ᾰ : A) :

(continuous_monoid_hom.inl A B).to_fun ᾰ = (⇑((continuous_monoid_hom.id A).to_monoid_hom) ᾰ, ⇑((continuous_monoid_hom.one A B).to_monoid_hom) ᾰ)

source

def continuous_add_monoid_hom.inr (A : Type u_1) (B : Type u_2) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :

continuous_add_monoid_hom B (A × B)

The continuous homomorphism given by inclusion of the second factor.

Equations

continuous_add_monoid_hom.inr A B = (continuous_add_monoid_hom.zero B A).sum (continuous_add_monoid_hom.id B)

source

def continuous_monoid_hom.inr (A : Type u_1) (B : Type u_2) [monoid A] [monoid B] [topological_space A] [topological_space B] :

continuous_monoid_hom B (A × B)

The continuous homomorphism given by inclusion of the second factor.

Equations

continuous_monoid_hom.inr A B = (continuous_monoid_hom.one B A).prod (continuous_monoid_hom.id B)

source

@[simp]

theorem continuous_add_monoid_hom.inr_apply (A : Type u_1) (B : Type u_2) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] (ᾰ : B) :

(continuous_add_monoid_hom.inr A B).to_fun ᾰ = (⇑((continuous_add_monoid_hom.zero B A).to_add_monoid_hom) ᾰ, ⇑((continuous_add_monoid_hom.id B).to_add_monoid_hom) ᾰ)

source

@[simp]

theorem continuous_monoid_hom.inr_apply (A : Type u_1) (B : Type u_2) [monoid A] [monoid B] [topological_space A] [topological_space B] (ᾰ : B) :

(continuous_monoid_hom.inr A B).to_fun ᾰ = (⇑((continuous_monoid_hom.one B A).to_monoid_hom) ᾰ, ⇑((continuous_monoid_hom.id B).to_monoid_hom) ᾰ)

source

@[simp]

theorem continuous_monoid_hom.diag_apply (A : Type u_1) [monoid A] [topological_space A] (ᾰ : A) :

(continuous_monoid_hom.diag A).to_fun ᾰ = (⇑((continuous_monoid_hom.id A).to_monoid_hom) ᾰ, ⇑((continuous_monoid_hom.id A).to_monoid_hom) ᾰ)

source

def continuous_add_monoid_hom.diag (A : Type u_1) [add_monoid A] [topological_space A] :

continuous_add_monoid_hom A (A × A)

The continuous homomorphism given by the diagonal embedding.

Equations

continuous_add_monoid_hom.diag A = (continuous_add_monoid_hom.id A).sum (continuous_add_monoid_hom.id A)

source

def continuous_monoid_hom.diag (A : Type u_1) [monoid A] [topological_space A] :

continuous_monoid_hom A (A × A)

The continuous homomorphism given by the diagonal embedding.

Equations

continuous_monoid_hom.diag A = (continuous_monoid_hom.id A).prod (continuous_monoid_hom.id A)

source

@[simp]

theorem continuous_add_monoid_hom.diag_apply (A : Type u_1) [add_monoid A] [topological_space A] (ᾰ : A) :

(continuous_add_monoid_hom.diag A).to_fun ᾰ = (⇑((continuous_add_monoid_hom.id A).to_add_monoid_hom) ᾰ, ⇑((continuous_add_monoid_hom.id A).to_add_monoid_hom) ᾰ)

source

def continuous_monoid_hom.swap (A : Type u_1) (B : Type u_2) [monoid A] [monoid B] [topological_space A] [topological_space B] :

continuous_monoid_hom (A × B) (B × A)

The continuous homomorphism given by swapping components.

Equations

continuous_monoid_hom.swap A B = (continuous_monoid_hom.snd A B).prod (continuous_monoid_hom.fst A B)

source

@[simp]

theorem continuous_monoid_hom.swap_apply (A : Type u_1) (B : Type u_2) [monoid A] [monoid B] [topological_space A] [topological_space B] (ᾰ : A × B) :

(continuous_monoid_hom.swap A B).to_fun ᾰ = (⇑((continuous_monoid_hom.snd A B).to_monoid_hom) ᾰ, ⇑((continuous_monoid_hom.fst A B).to_monoid_hom) ᾰ)

source

@[simp]

theorem continuous_add_monoid_hom.swap_apply (A : Type u_1) (B : Type u_2) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] (ᾰ : A × B) :

(continuous_add_monoid_hom.swap A B).to_fun ᾰ = (⇑((continuous_add_monoid_hom.snd A B).to_add_monoid_hom) ᾰ, ⇑((continuous_add_monoid_hom.fst A B).to_add_monoid_hom) ᾰ)

source

def continuous_add_monoid_hom.swap (A : Type u_1) (B : Type u_2) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :

continuous_add_monoid_hom (A × B) (B × A)

The continuous homomorphism given by swapping components.

Equations

continuous_add_monoid_hom.swap A B = (continuous_add_monoid_hom.snd A B).sum (continuous_add_monoid_hom.fst A B)

source

def continuous_monoid_hom.mul (E : Type u_5) [comm_group E] [topological_space E] [topological_group E] :

continuous_monoid_hom (E × E) E

The continuous homomorphism given by multiplication.

Equations

continuous_monoid_hom.mul E = continuous_monoid_hom.mk' mul_monoid_hom _

source

def continuous_add_monoid_hom.add (E : Type u_5) [add_comm_group E] [topological_space E] [topological_add_group E] :

continuous_add_monoid_hom (E × E) E

The continuous homomorphism given by addition.

Equations

continuous_add_monoid_hom.add E = continuous_add_monoid_hom.mk' add_add_monoid_hom _

source

@[simp]

theorem continuous_add_monoid_hom.add_apply (E : Type u_5) [add_comm_group E] [topological_space E] [topological_add_group E] (ᾰ : E × E) :

(continuous_add_monoid_hom.add E).to_fun ᾰ = ᾰ.fst + ᾰ.snd

source

@[simp]

theorem continuous_monoid_hom.mul_apply (E : Type u_5) [comm_group E] [topological_space E] [topological_group E] (ᾰ : E × E) :

(continuous_monoid_hom.mul E).to_fun ᾰ = (ᾰ.fst) * ᾰ.snd

source

def continuous_add_monoid_hom.neg (E : Type u_5) [add_comm_group E] [topological_space E] [topological_add_group E] :

continuous_add_monoid_hom E E

The continuous homomorphism given by negation.

Equations

continuous_add_monoid_hom.neg E = continuous_add_monoid_hom.mk' add_comm_group.neg_add_monoid_hom _

source

@[simp]

theorem continuous_monoid_hom.inv_apply (E : Type u_5) [comm_group E] [topological_space E] [topological_group E] (ᾰ : E) :

(continuous_monoid_hom.inv E).to_fun ᾰ = ᾰ⁻¹

source

def continuous_monoid_hom.inv (E : Type u_5) [comm_group E] [topological_space E] [topological_group E] :

continuous_monoid_hom E E

The continuous homomorphism given by inversion.

Equations

continuous_monoid_hom.inv E = continuous_monoid_hom.mk' comm_group.inv_monoid_hom _

source

@[simp]

theorem continuous_add_monoid_hom.neg_apply (E : Type u_5) [add_comm_group E] [topological_space E] [topological_add_group E] (ᾰ : E) :

(continuous_add_monoid_hom.neg E).to_fun ᾰ = -ᾰ

source

def continuous_monoid_hom.coprod {A : Type u_1} {B : Type u_2} {E : Type u_5} [monoid A] [monoid B] [comm_group E] [topological_space A] [topological_space B] [topological_space E] [topological_group E] (f : continuous_monoid_hom A E) (g : continuous_monoid_hom B E) :

continuous_monoid_hom (A × B) E

Coproduct of two continuous homomorphisms to the same space.

Equations

f.coprod g = (continuous_monoid_hom.mul E).comp (f.prod_map g)

source

def continuous_add_monoid_hom.coprod {A : Type u_1} {B : Type u_2} {E : Type u_5} [add_monoid A] [add_monoid B] [add_comm_group E] [topological_space A] [topological_space B] [topological_space E] [topological_add_group E] (f : continuous_add_monoid_hom A E) (g : continuous_add_monoid_hom B E) :

continuous_add_monoid_hom (A × B) E

Coproduct of two continuous homomorphisms to the same space.

Equations

f.coprod g = (continuous_add_monoid_hom.add E).comp (f.sum_map g)

source

@[simp]

theorem continuous_monoid_hom.coprod_apply {A : Type u_1} {B : Type u_2} {E : Type u_5} [monoid A] [monoid B] [comm_group E] [topological_space A] [topological_space B] [topological_space E] [topological_group E] (f : continuous_monoid_hom A E) (g : continuous_monoid_hom B E) (ᾰ : A × B) :

(f.coprod g).to_fun ᾰ = ⇑((continuous_monoid_hom.mul E).to_monoid_hom) (⇑((f.prod_map g).to_monoid_hom) ᾰ)

source

@[simp]

theorem continuous_add_monoid_hom.coprod_apply {A : Type u_1} {B : Type u_2} {E : Type u_5} [add_monoid A] [add_monoid B] [add_comm_group E] [topological_space A] [topological_space B] [topological_space E] [topological_add_group E] (f : continuous_add_monoid_hom A E) (g : continuous_add_monoid_hom B E) (ᾰ : A × B) :

(f.coprod g).to_fun ᾰ = ⇑((continuous_add_monoid_hom.add E).to_add_monoid_hom) (⇑((f.sum_map g).to_add_monoid_hom) ᾰ)

source

@[protected, instance]

def continuous_add_monoid_hom.add_comm_group {A : Type u_1} {E : Type u_5} [add_monoid A] [add_comm_group E] [topological_space A] [topological_space E] [topological_add_group E] :

add_comm_group (continuous_add_monoid_hom A E)

Equations

continuous_add_monoid_hom.add_comm_group = {add := λ (f g : continuous_add_monoid_hom A E), (continuous_add_monoid_hom.add E).comp (f.sum g), add_assoc := _, zero := continuous_add_monoid_hom.zero A E _inst_10, zero_add := _, add_zero := _, nsmul := add_group.nsmul._default (continuous_add_monoid_hom.zero A E) (λ (f g : continuous_add_monoid_hom A E), (continuous_add_monoid_hom.add E).comp (f.sum g)) continuous_add_monoid_hom.add_comm_group._proof_4 continuous_add_monoid_hom.add_comm_group._proof_5, nsmul_zero' := _, nsmul_succ' := _, neg := λ (f : continuous_add_monoid_hom A E), (continuous_add_monoid_hom.neg E).comp f, sub := add_group.sub._default (λ (f g : continuous_add_monoid_hom A E), (continuous_add_monoid_hom.add E).comp (f.sum g)) continuous_add_monoid_hom.add_comm_group._proof_8 (continuous_add_monoid_hom.zero A E) continuous_add_monoid_hom.add_comm_group._proof_9 continuous_add_monoid_hom.add_comm_group._proof_10 (add_group.nsmul._default (continuous_add_monoid_hom.zero A E) (λ (f g : continuous_add_monoid_hom A E), (continuous_add_monoid_hom.add E).comp (f.sum g)) continuous_add_monoid_hom.add_comm_group._proof_4 continuous_add_monoid_hom.add_comm_group._proof_5) continuous_add_monoid_hom.add_comm_group._proof_11 continuous_add_monoid_hom.add_comm_group._proof_12 (λ (f : continuous_add_monoid_hom A E), (continuous_add_monoid_hom.neg E).comp f), sub_eq_add_neg := _, zsmul := add_group.zsmul._default (λ (f g : continuous_add_monoid_hom A E), (continuous_add_monoid_hom.add E).comp (f.sum g)) continuous_add_monoid_hom.add_comm_group._proof_14 (continuous_add_monoid_hom.zero A E) continuous_add_monoid_hom.add_comm_group._proof_15 continuous_add_monoid_hom.add_comm_group._proof_16 (add_group.nsmul._default (continuous_add_monoid_hom.zero A E) (λ (f g : continuous_add_monoid_hom A E), (continuous_add_monoid_hom.add E).comp (f.sum g)) continuous_add_monoid_hom.add_comm_group._proof_4 continuous_add_monoid_hom.add_comm_group._proof_5) continuous_add_monoid_hom.add_comm_group._proof_17 continuous_add_monoid_hom.add_comm_group._proof_18 (λ (f : continuous_add_monoid_hom A E), (continuous_add_monoid_hom.neg E).comp f), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}

source

@[protected, instance]

def continuous_monoid_hom.comm_group {A : Type u_1} {E : Type u_5} [monoid A] [comm_group E] [topological_space A] [topological_space E] [topological_group E] :

comm_group (continuous_monoid_hom A E)

Equations

continuous_monoid_hom.comm_group = {mul := λ (f g : continuous_monoid_hom A E), (continuous_monoid_hom.mul E).comp (f.prod g), mul_assoc := _, one := continuous_monoid_hom.one A E _inst_10, one_mul := _, mul_one := _, npow := group.npow._default (continuous_monoid_hom.one A E) (λ (f g : continuous_monoid_hom A E), (continuous_monoid_hom.mul E).comp (f.prod g)) continuous_monoid_hom.comm_group._proof_4 continuous_monoid_hom.comm_group._proof_5, npow_zero' := _, npow_succ' := _, inv := λ (f : continuous_monoid_hom A E), (continuous_monoid_hom.inv E).comp f, div := group.div._default (λ (f g : continuous_monoid_hom A E), (continuous_monoid_hom.mul E).comp (f.prod g)) continuous_monoid_hom.comm_group._proof_8 (continuous_monoid_hom.one A E) continuous_monoid_hom.comm_group._proof_9 continuous_monoid_hom.comm_group._proof_10 (group.npow._default (continuous_monoid_hom.one A E) (λ (f g : continuous_monoid_hom A E), (continuous_monoid_hom.mul E).comp (f.prod g)) continuous_monoid_hom.comm_group._proof_4 continuous_monoid_hom.comm_group._proof_5) continuous_monoid_hom.comm_group._proof_11 continuous_monoid_hom.comm_group._proof_12 (λ (f : continuous_monoid_hom A E), (continuous_monoid_hom.inv E).comp f), div_eq_mul_inv := _, zpow := group.zpow._default (λ (f g : continuous_monoid_hom A E), (continuous_monoid_hom.mul E).comp (f.prod g)) continuous_monoid_hom.comm_group._proof_14 (continuous_monoid_hom.one A E) continuous_monoid_hom.comm_group._proof_15 continuous_monoid_hom.comm_group._proof_16 (group.npow._default (continuous_monoid_hom.one A E) (λ (f g : continuous_monoid_hom A E), (continuous_monoid_hom.mul E).comp (f.prod g)) continuous_monoid_hom.comm_group._proof_4 continuous_monoid_hom.comm_group._proof_5) continuous_monoid_hom.comm_group._proof_17 continuous_monoid_hom.comm_group._proof_18 (λ (f : continuous_monoid_hom A E), (continuous_monoid_hom.inv E).comp f), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}

source

@[protected, instance]

def continuous_monoid_hom.topological_space {A : Type u_1} {B : Type u_2} [monoid A] [monoid B] [topological_space A] [topological_space B] :

topological_space (continuous_monoid_hom A B)

Equations

continuous_monoid_hom.topological_space = topological_space.induced continuous_monoid_hom.to_continuous_map continuous_map.compact_open

source

theorem continuous_monoid_hom.is_inducing (A : Type u_1) (B : Type u_2) [monoid A] [monoid B] [topological_space A] [topological_space B] :

inducing continuous_monoid_hom.to_continuous_map

source

theorem continuous_monoid_hom.is_embedding (A : Type u_1) (B : Type u_2) [monoid A] [monoid B] [topological_space A] [topological_space B] :

embedding continuous_monoid_hom.to_continuous_map

source

@[protected, instance]

def continuous_monoid_hom.t2_space {A : Type u_1} {B : Type u_2} [monoid A] [monoid B] [topological_space A] [topological_space B] [locally_compact_space A] [t2_space B] :

t2_space (continuous_monoid_hom A B)

source

@[protected, instance]

def continuous_monoid_hom.topological_group {A : Type u_1} {E : Type u_5} [monoid A] [comm_group E] [topological_space A] [topological_space E] [topological_group E] :

topological_group (continuous_monoid_hom A E)

mathlib documentation

Continuous Monoid Homs #

Main definitions #