mathlib3 documentation

topology.algebra.continuous_monoid_hom

Continuous Monoid Homs #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the space of continuous homomorphisms between two topological groups.

Main definitions #

source
structure continuous_add_monoid_hom (A : Type u_7) (B : Type u_8) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :
Type (max u_7 u_8)

The type of continuous additive monoid homomorphisms from A to B.

When possible, instead of parametrizing results over (f : continuous_add_monoid_hom A B), you should parametrize over (F : Type*) [continuous_add_monoid_hom_class F A B] (f : F).

When you extend this structure, make sure to extend continuous_add_monoid_hom_class.

Instances for continuous_add_monoid_hom
source
structure continuous_monoid_hom (A : Type u_2) (B : Type u_3) [monoid A] [monoid B] [topological_space A] [topological_space B] :
Type (max u_2 u_3)

The type of continuous monoid homomorphisms from A to B.

When possible, instead of parametrizing results over (f : continuous_monoid_hom A B), you should parametrize over (F : Type*) [continuous_monoid_hom_class F A B] (f : F).

When you extend this structure, make sure to extend continuous_add_monoid_hom_class.

Instances for continuous_monoid_hom
source
@[class]
structure continuous_add_monoid_hom_class (F : Type u_1) (A : Type u_7) (B : Type u_8) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :
Type (max u_1 u_7 u_8)

continuous_add_monoid_hom_class F A B states that F is a type of continuous additive monoid homomorphisms.

You should also extend this typeclass when you extend continuous_add_monoid_hom.

Instances of this typeclass
Instances of other typeclasses for continuous_add_monoid_hom_class
  • continuous_add_monoid_hom_class.has_sizeof_inst
source
@[instance]
def continuous_add_monoid_hom_class.to_add_monoid_hom_class (F : Type u_1) (A : Type u_7) (B : Type u_8) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] [self : continuous_add_monoid_hom_class F A B] :
add_monoid_hom_class F A B
source
@[instance]
def continuous_monoid_hom_class.to_monoid_hom_class (F : Type u_1) (A : Type u_2) (B : Type u_3) [monoid A] [monoid B] [topological_space A] [topological_space B] [self : continuous_monoid_hom_class F A B] :
monoid_hom_class F A B
source
@[class]
structure continuous_monoid_hom_class (F : Type u_1) (A : Type u_2) (B : Type u_3) [monoid A] [monoid B] [topological_space A] [topological_space B] :
Type (max u_1 u_2 u_3)

continuous_monoid_hom_class F A B states that F is a type of continuous additive monoid homomorphisms.

You should also extend this typeclass when you extend continuous_monoid_hom.

Instances of this typeclass
Instances of other typeclasses for continuous_monoid_hom_class
  • continuous_monoid_hom_class.has_sizeof_inst
source
@[protected, instance]
def continuous_monoid_hom_class.to_continuous_map_class (F : Type u_1) (A : Type u_2) (B : Type u_3) [monoid A] [monoid B] [topological_space A] [topological_space B] [continuous_monoid_hom_class F A B] :
continuous_map_class F A B
Equations
source
@[protected, instance]
def continuous_add_monoid_hom_class.to_continuous_map_class (F : Type u_1) (A : Type u_2) (B : Type u_3) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] [continuous_add_monoid_hom_class F A B] :
continuous_map_class F A B
Equations
source
@[protected, instance]
def continuous_monoid_hom.continuous_monoid_hom_class {A : Type u_2} {B : Type u_3} [monoid A] [monoid B] [topological_space A] [topological_space B] :
continuous_monoid_hom_class (continuous_monoid_hom A B) A B
Equations
source
@[protected, instance]
def continuous_add_monoid_hom.continuous_add_monoid_hom_class {A : Type u_2} {B : Type u_3} [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :
continuous_add_monoid_hom_class (continuous_add_monoid_hom A B) A B
Equations
source
@[protected, instance]
def continuous_monoid_hom.has_coe_to_fun {A : Type u_2} {B : Type u_3} [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)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
source
@[protected, instance]
def continuous_add_monoid_hom.has_coe_to_fun {A : Type u_2} {B : Type u_3} [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)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
source
theorem continuous_add_monoid_hom.ext {A : Type u_2} {B : Type u_3} [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
@[ext]
theorem continuous_monoid_hom.ext {A : Type u_2} {B : Type u_3} [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
def continuous_monoid_hom.to_continuous_map {A : Type u_2} {B : Type u_3} [monoid A] [monoid B] [topological_space A] [topological_space B] (f : continuous_monoid_hom A B) :
C(A, B)

Reinterpret a continuous_monoid_hom as a continuous_map.

Equations
source
def continuous_add_monoid_hom.to_continuous_map {A : Type u_2} {B : Type u_3} [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] (f : continuous_add_monoid_hom A B) :
C(A, B)

Reinterpret a continuous_add_monoid_hom as a continuous_map.

Equations
source
theorem continuous_add_monoid_hom.to_continuous_map_injective {A : Type u_2} {B : Type u_3} [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :
function.injective continuous_add_monoid_hom.to_continuous_map
source
theorem continuous_monoid_hom.to_continuous_map_injective {A : Type u_2} {B : Type u_3} [monoid A] [monoid B] [topological_space A] [topological_space B] :
function.injective continuous_monoid_hom.to_continuous_map
source
@[simp]
theorem continuous_add_monoid_hom.mk'_to_add_monoid_hom_apply {A : Type u_2} {B : Type u_3} [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_add_monoid_hom) ᾰ = f.to_fun ᾰ
source
def continuous_add_monoid_hom.mk' {A : Type u_2} {B : Type u_3} [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
source
@[simp]
theorem continuous_monoid_hom.mk'_to_monoid_hom_apply {A : Type u_2} {B : Type u_3} [monoid A] [monoid B] [topological_space A] [topological_space B] (f : A →* B) (hf : continuous ⇑f) (ᾰ : A) :
⇑((continuous_monoid_hom.mk' f hf).to_monoid_hom) ᾰ = f.to_fun ᾰ
source
def continuous_monoid_hom.mk' {A : Type u_2} {B : Type u_3} [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
source
def continuous_add_monoid_hom.comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [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
source
def continuous_monoid_hom.comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [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
source
@[simp]
theorem continuous_add_monoid_hom.comp_to_add_monoid_hom {A : Type u_2} {B : Type u_3} {C : Type u_4} [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) :
(g.comp f).to_add_monoid_hom = g.to_add_monoid_hom.comp f.to_add_monoid_hom
source
@[simp]
theorem continuous_monoid_hom.comp_to_monoid_hom {A : Type u_2} {B : Type u_3} {C : Type u_4} [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) :
(g.comp f).to_monoid_hom = g.to_monoid_hom.comp f.to_monoid_hom
source
@[simp]
theorem continuous_add_monoid_hom.sum_to_add_monoid_hom {A : Type u_2} {B : Type u_3} {C : Type u_4} [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) :
(f.sum g).to_add_monoid_hom = f.to_add_monoid_hom.prod g.to_add_monoid_hom
source
def continuous_add_monoid_hom.sum {A : Type u_2} {B : Type u_3} {C : Type u_4} [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
source
def continuous_monoid_hom.prod {A : Type u_2} {B : Type u_3} {C : Type u_4} [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
source
@[simp]
theorem continuous_monoid_hom.prod_to_monoid_hom {A : Type u_2} {B : Type u_3} {C : Type u_4} [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) :
(f.prod g).to_monoid_hom = f.to_monoid_hom.prod g.to_monoid_hom
source
@[simp]
theorem continuous_add_monoid_hom.sum_map_to_add_monoid_hom {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [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) :
(f.sum_map g).to_add_monoid_hom = f.to_add_monoid_hom.prod_map g.to_add_monoid_hom
source
def continuous_monoid_hom.prod_map {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [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
source
@[simp]
theorem continuous_monoid_hom.prod_map_to_monoid_hom {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [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) :
(f.prod_map g).to_monoid_hom = f.to_monoid_hom.prod_map g.to_monoid_hom
source
def continuous_add_monoid_hom.sum_map {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [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
source
def continuous_add_monoid_hom.zero (A : Type u_2) (B : Type u_3) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :
continuous_add_monoid_hom A B

The trivial continuous homomorphism.

Equations
source
@[simp]
theorem continuous_add_monoid_hom.zero_to_add_monoid_hom (A : Type u_2) (B : Type u_3) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :
(continuous_add_monoid_hom.zero A B).to_add_monoid_hom = 0
source
@[simp]
theorem continuous_monoid_hom.one_to_monoid_hom (A : Type u_2) (B : Type u_3) [monoid A] [monoid B] [topological_space A] [topological_space B] :
(continuous_monoid_hom.one A B).to_monoid_hom = 1
source
def continuous_monoid_hom.one (A : Type u_2) (B : Type u_3) [monoid A] [monoid B] [topological_space A] [topological_space B] :
continuous_monoid_hom A B

The trivial continuous homomorphism.

Equations
source
@[protected, instance]
def continuous_monoid_hom.inhabited (A : Type u_2) (B : Type u_3) [monoid A] [monoid B] [topological_space A] [topological_space B] :
inhabited (continuous_monoid_hom A B)
Equations
source
@[protected, instance]
def continuous_add_monoid_hom.inhabited (A : Type u_2) (B : Type u_3) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :
inhabited (continuous_add_monoid_hom A B)
Equations
source
@[simp]
theorem continuous_monoid_hom.id_to_monoid_hom (A : Type u_2) [monoid A] [topological_space A] :
(continuous_monoid_hom.id A).to_monoid_hom = monoid_hom.id A
source
def continuous_add_monoid_hom.id (A : Type u_2) [add_monoid A] [topological_space A] :
continuous_add_monoid_hom A A

The identity continuous homomorphism.

Equations
source
@[simp]
theorem continuous_add_monoid_hom.id_to_add_monoid_hom (A : Type u_2) [add_monoid A] [topological_space A] :
(continuous_add_monoid_hom.id A).to_add_monoid_hom = add_monoid_hom.id A
source
def continuous_monoid_hom.id (A : Type u_2) [monoid A] [topological_space A] :
continuous_monoid_hom A A

The identity continuous homomorphism.

Equations
source
def continuous_monoid_hom.fst (A : Type u_2) (B : Type u_3) [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
source
def continuous_add_monoid_hom.fst (A : Type u_2) (B : Type u_3) [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
source
@[simp]
theorem continuous_monoid_hom.fst_to_monoid_hom (A : Type u_2) (B : Type u_3) [monoid A] [monoid B] [topological_space A] [topological_space B] :
(continuous_monoid_hom.fst A B).to_monoid_hom = monoid_hom.fst A B
source
@[simp]
theorem continuous_add_monoid_hom.fst_to_add_monoid_hom (A : Type u_2) (B : Type u_3) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :
(continuous_add_monoid_hom.fst A B).to_add_monoid_hom = add_monoid_hom.fst A B
source
@[simp]
theorem continuous_monoid_hom.snd_to_monoid_hom (A : Type u_2) (B : Type u_3) [monoid A] [monoid B] [topological_space A] [topological_space B] :
(continuous_monoid_hom.snd A B).to_monoid_hom = monoid_hom.snd A B
source
def continuous_monoid_hom.snd (A : Type u_2) (B : Type u_3) [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
source
def continuous_add_monoid_hom.snd (A : Type u_2) (B : Type u_3) [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
source
@[simp]
theorem continuous_add_monoid_hom.snd_to_add_monoid_hom (A : Type u_2) (B : Type u_3) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :
(continuous_add_monoid_hom.snd A B).to_add_monoid_hom = add_monoid_hom.snd A B
source
@[simp]
theorem continuous_add_monoid_hom.inl_to_add_monoid_hom (A : Type u_2) (B : Type u_3) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :
(continuous_add_monoid_hom.inl A B).to_add_monoid_hom = (add_monoid_hom.id A).prod 0
source
def continuous_monoid_hom.inl (A : Type u_2) (B : Type u_3) [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
source
def continuous_add_monoid_hom.inl (A : Type u_2) (B : Type u_3) [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
source
@[simp]
theorem continuous_monoid_hom.inl_to_monoid_hom (A : Type u_2) (B : Type u_3) [monoid A] [monoid B] [topological_space A] [topological_space B] :
(continuous_monoid_hom.inl A B).to_monoid_hom = (monoid_hom.id A).prod 1
source
@[simp]
theorem continuous_monoid_hom.inr_to_monoid_hom (A : Type u_2) (B : Type u_3) [monoid A] [monoid B] [topological_space A] [topological_space B] :
(continuous_monoid_hom.inr A B).to_monoid_hom = 1.prod (monoid_hom.id B)
source
@[simp]
theorem continuous_add_monoid_hom.inr_to_add_monoid_hom (A : Type u_2) (B : Type u_3) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :
(continuous_add_monoid_hom.inr A B).to_add_monoid_hom = 0.prod (add_monoid_hom.id B)
source
def continuous_add_monoid_hom.inr (A : Type u_2) (B : Type u_3) [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
source
def continuous_monoid_hom.inr (A : Type u_2) (B : Type u_3) [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
source
@[simp]
theorem continuous_add_monoid_hom.diag_to_add_monoid_hom (A : Type u_2) [add_monoid A] [topological_space A] :
(continuous_add_monoid_hom.diag A).to_add_monoid_hom = (add_monoid_hom.id A).prod (add_monoid_hom.id A)
source
@[simp]
theorem continuous_monoid_hom.diag_to_monoid_hom (A : Type u_2) [monoid A] [topological_space A] :
(continuous_monoid_hom.diag A).to_monoid_hom = (monoid_hom.id A).prod (monoid_hom.id A)
source
def continuous_add_monoid_hom.diag (A : Type u_2) [add_monoid A] [topological_space A] :
continuous_add_monoid_hom A (A × A)

The continuous homomorphism given by the diagonal embedding.

Equations
source
def continuous_monoid_hom.diag (A : Type u_2) [monoid A] [topological_space A] :
continuous_monoid_hom A (A × A)

The continuous homomorphism given by the diagonal embedding.

Equations
source
def continuous_monoid_hom.swap (A : Type u_2) (B : Type u_3) [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
source
def continuous_add_monoid_hom.swap (A : Type u_2) (B : Type u_3) [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
source
@[simp]
theorem continuous_monoid_hom.swap_to_monoid_hom (A : Type u_2) (B : Type u_3) [monoid A] [monoid B] [topological_space A] [topological_space B] :
(continuous_monoid_hom.swap A B).to_monoid_hom = (monoid_hom.snd A B).prod (monoid_hom.fst A B)
source
@[simp]
theorem continuous_add_monoid_hom.swap_to_add_monoid_hom (A : Type u_2) (B : Type u_3) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :
(continuous_add_monoid_hom.swap A B).to_add_monoid_hom = (add_monoid_hom.snd A B).prod (add_monoid_hom.fst A B)
source
@[simp]
theorem continuous_monoid_hom.mul_to_monoid_hom (E : Type u_6) [comm_group E] [topological_space E] [topological_group E] :
(continuous_monoid_hom.mul E).to_monoid_hom = mul_monoid_hom
source
@[simp]
theorem continuous_add_monoid_hom.add_to_add_monoid_hom (E : Type u_6) [add_comm_group E] [topological_space E] [topological_add_group E] :
(continuous_add_monoid_hom.add E).to_add_monoid_hom = add_add_monoid_hom
source
def continuous_monoid_hom.mul (E : Type u_6) [comm_group E] [topological_space E] [topological_group E] :
continuous_monoid_hom (E × E) E

The continuous homomorphism given by multiplication.

Equations
source
def continuous_add_monoid_hom.add (E : Type u_6) [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
source
@[simp]
theorem continuous_add_monoid_hom.neg_to_add_monoid_hom (E : Type u_6) [add_comm_group E] [topological_space E] [topological_add_group E] :
(continuous_add_monoid_hom.neg E).to_add_monoid_hom = neg_add_monoid_hom
source
@[simp]
theorem continuous_monoid_hom.inv_to_monoid_hom (E : Type u_6) [comm_group E] [topological_space E] [topological_group E] :
(continuous_monoid_hom.inv E).to_monoid_hom = inv_monoid_hom
source
def continuous_add_monoid_hom.neg (E : Type u_6) [add_comm_group E] [topological_space E] [topological_add_group E] :
continuous_add_monoid_hom E E

The continuous homomorphism given by negation.

Equations
source
def continuous_monoid_hom.inv (E : Type u_6) [comm_group E] [topological_space E] [topological_group E] :
continuous_monoid_hom E E

The continuous homomorphism given by inversion.

Equations
source
@[simp]
theorem continuous_monoid_hom.coprod_to_monoid_hom {A : Type u_2} {B : Type u_3} {E : Type u_6} [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) :
(f.coprod g).to_monoid_hom = mul_monoid_hom.comp (f.to_monoid_hom.prod_map g.to_monoid_hom)
source
def continuous_monoid_hom.coprod {A : Type u_2} {B : Type u_3} {E : Type u_6} [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
source
@[simp]
theorem continuous_add_monoid_hom.coprod_to_add_monoid_hom {A : Type u_2} {B : Type u_3} {E : Type u_6} [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) :
(f.coprod g).to_add_monoid_hom = add_add_monoid_hom.comp (f.to_add_monoid_hom.prod_map g.to_add_monoid_hom)
source
def continuous_add_monoid_hom.coprod {A : Type u_2} {B : Type u_3} {E : Type u_6} [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
source
@[protected, instance]
def continuous_add_monoid_hom.add_comm_group {A : Type u_2} {E : Type u_6} [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
source
@[protected, instance]
def continuous_monoid_hom.comm_group {A : Type u_2} {E : Type u_6} [monoid A] [comm_group E] [topological_space A] [topological_space E] [topological_group E] :
comm_group (continuous_monoid_hom A E)
Equations
source
@[protected, instance]
def continuous_monoid_hom.topological_space {A : Type u_2} {B : Type u_3} [monoid A] [monoid B] [topological_space A] [topological_space B] :
topological_space (continuous_monoid_hom A B)
Equations
source
@[protected, instance]
def continuous_add_monoid_hom.topological_space {A : Type u_2} {B : Type u_3} [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :
topological_space (continuous_add_monoid_hom A B)
Equations
source
theorem continuous_add_monoid_hom.inducing_to_continuous_map (A : Type u_2) (B : Type u_3) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :
inducing continuous_add_monoid_hom.to_continuous_map
source
theorem continuous_monoid_hom.inducing_to_continuous_map (A : Type u_2) (B : Type u_3) [monoid A] [monoid B] [topological_space A] [topological_space B] :
inducing continuous_monoid_hom.to_continuous_map
source
theorem continuous_add_monoid_hom.embedding_to_continuous_map (A : Type u_2) (B : Type u_3) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :
embedding continuous_add_monoid_hom.to_continuous_map
source
theorem continuous_monoid_hom.embedding_to_continuous_map (A : Type u_2) (B : Type u_3) [monoid A] [monoid B] [topological_space A] [topological_space B] :
embedding continuous_monoid_hom.to_continuous_map
source
theorem continuous_add_monoid_hom.closed_embedding_to_continuous_map (A : Type u_2) (B : Type u_3) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] [has_continuous_add B] [t2_space B] :
closed_embedding continuous_add_monoid_hom.to_continuous_map
source
theorem continuous_monoid_hom.closed_embedding_to_continuous_map (A : Type u_2) (B : Type u_3) [monoid A] [monoid B] [topological_space A] [topological_space B] [has_continuous_mul B] [t2_space B] :
closed_embedding continuous_monoid_hom.to_continuous_map
source
@[protected, instance]
def continuous_monoid_hom.t2_space {A : Type u_2} {B : Type u_3} [monoid A] [monoid B] [topological_space A] [topological_space B] [t2_space B] :
t2_space (continuous_monoid_hom A B)
source
@[protected, instance]
def continuous_add_monoid_hom.t2_space {A : Type u_2} {B : Type u_3} [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] [t2_space B] :
t2_space (continuous_add_monoid_hom A B)
source
@[protected, instance]
def continuous_add_monoid_hom.topological_add_group {A : Type u_2} {E : Type u_6} [add_monoid A] [add_comm_group E] [topological_space A] [topological_space E] [topological_add_group E] :
topological_add_group (continuous_add_monoid_hom A E)
source
@[protected, instance]
def continuous_monoid_hom.topological_group {A : Type u_2} {E : Type u_6} [monoid A] [comm_group E] [topological_space A] [topological_space E] [topological_group E] :
topological_group (continuous_monoid_hom A E)
source
theorem continuous_add_monoid_hom.continuous_of_continuous_uncurry {B : Type u_3} {C : Type u_4} [add_monoid B] [add_monoid C] [topological_space B] [topological_space C] {A : Type u_1} [topological_space A] (f : A → continuous_add_monoid_hom B C) (h : continuous (function.uncurry (λ (x : A) (y : B), ⇑(f x) y))) :
continuous f
source
theorem continuous_monoid_hom.continuous_of_continuous_uncurry {B : Type u_3} {C : Type u_4} [monoid B] [monoid C] [topological_space B] [topological_space C] {A : Type u_1} [topological_space A] (f : A → continuous_monoid_hom B C) (h : continuous (function.uncurry (λ (x : A) (y : B), ⇑(f x) y))) :
continuous f
source
theorem continuous_add_monoid_hom.continuous_comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [add_monoid A] [add_monoid B] [add_monoid C] [topological_space A] [topological_space B] [topological_space C] [locally_compact_space B] :
continuous (λ (f : continuous_add_monoid_hom A B × continuous_add_monoid_hom B C), f.snd.comp f.fst)
source
theorem continuous_monoid_hom.continuous_comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [monoid A] [monoid B] [monoid C] [topological_space A] [topological_space B] [topological_space C] [locally_compact_space B] :
continuous (λ (f : continuous_monoid_hom A B × continuous_monoid_hom B C), f.snd.comp f.fst)
source
theorem continuous_add_monoid_hom.continuous_comp_left {A : Type u_2} {B : Type u_3} {C : Type u_4} [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) :
continuous (λ (g : continuous_add_monoid_hom B C), g.comp f)
source
theorem continuous_monoid_hom.continuous_comp_left {A : Type u_2} {B : Type u_3} {C : Type u_4} [monoid A] [monoid B] [monoid C] [topological_space A] [topological_space B] [topological_space C] (f : continuous_monoid_hom A B) :
continuous (λ (g : continuous_monoid_hom B C), g.comp f)
source
theorem continuous_add_monoid_hom.continuous_comp_right {A : Type u_2} {B : Type u_3} {C : Type u_4} [add_monoid A] [add_monoid B] [add_monoid C] [topological_space A] [topological_space B] [topological_space C] (f : continuous_add_monoid_hom B C) :
continuous (λ (g : continuous_add_monoid_hom A B), f.comp g)
source
theorem continuous_monoid_hom.continuous_comp_right {A : Type u_2} {B : Type u_3} {C : Type u_4} [monoid A] [monoid B] [monoid C] [topological_space A] [topological_space B] [topological_space C] (f : continuous_monoid_hom B C) :
continuous (λ (g : continuous_monoid_hom A B), f.comp g)
source
def continuous_add_monoid_hom.comp_left {A : Type u_2} {B : Type u_3} (E : Type u_6) [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 B) :
continuous_add_monoid_hom (continuous_add_monoid_hom B E) (continuous_add_monoid_hom A E)

continuous_add_monoid_hom _ f is a functor.

Equations
source
def continuous_monoid_hom.comp_left {A : Type u_2} {B : Type u_3} (E : Type u_6) [monoid A] [monoid B] [comm_group E] [topological_space A] [topological_space B] [topological_space E] [topological_group E] (f : continuous_monoid_hom A B) :
continuous_monoid_hom (continuous_monoid_hom B E) (continuous_monoid_hom A E)

continuous_monoid_hom _ f is a functor.

Equations
source
def continuous_monoid_hom.comp_right (A : Type u_2) {E : Type u_6} [monoid A] [comm_group E] [topological_space A] [topological_space E] [topological_group E] {B : Type u_1} [comm_group B] [topological_space B] [topological_group B] (f : continuous_monoid_hom B E) :
continuous_monoid_hom (continuous_monoid_hom A B) (continuous_monoid_hom A E)

continuous_monoid_hom f _ is a functor.

Equations
source
def continuous_add_monoid_hom.comp_right (A : Type u_2) {E : Type u_6} [add_monoid A] [add_comm_group E] [topological_space A] [topological_space E] [topological_add_group E] {B : Type u_1} [add_comm_group B] [topological_space B] [topological_add_group B] (f : continuous_add_monoid_hom B E) :
continuous_add_monoid_hom (continuous_add_monoid_hom A B) (continuous_add_monoid_hom A E)

continuous_add_monoid_hom f _ is a functor.

Equations
source
@[protected, instance]
noncomputable def pontryagin_dual.topological_space (A : Type u_2) [monoid A] [topological_space A] :
topological_space (pontryagin_dual A)
source
@[protected, instance]
def pontryagin_dual.topological_group (A : Type u_2) [monoid A] [topological_space A] :
topological_group (pontryagin_dual A)
source
@[protected, instance]
noncomputable def pontryagin_dual.inhabited (A : Type u_2) [monoid A] [topological_space A] :
inhabited (pontryagin_dual A)
source
def pontryagin_dual (A : Type u_2) [monoid A] [topological_space A] :
Type u_2

The Pontryagin dual of A is the group of continuous homomorphism A → circle.

Equations
Instances for pontryagin_dual
source
@[protected, instance]
def pontryagin_dual.t2_space (A : Type u_2) [monoid A] [topological_space A] :
t2_space (pontryagin_dual A)
source
@[protected, instance]
noncomputable def pontryagin_dual.comm_group (A : Type u_2) [monoid A] [topological_space A] :
comm_group (pontryagin_dual A)
source
@[protected, instance]
noncomputable def pontryagin_dual.circle.continuous_monoid_hom_class {A : Type u_2} [monoid A] [topological_space A] :
continuous_monoid_hom_class (pontryagin_dual A) A ↥circle
Equations
source
noncomputable def pontryagin_dual.map {A : Type u_2} {B : Type u_3} [monoid A] [monoid B] [topological_space A] [topological_space B] (f : continuous_monoid_hom A B) :
continuous_monoid_hom (pontryagin_dual B) (pontryagin_dual A)

pontryagin_dual is a functor.

Equations
source
@[simp]
theorem pontryagin_dual.map_apply {A : Type u_2} {B : Type u_3} [monoid A] [monoid B] [topological_space A] [topological_space B] (f : continuous_monoid_hom A B) (x : pontryagin_dual B) (y : A) :
⇑(⇑(pontryagin_dual.map f) x) y = ⇑x (⇑f y)
source
@[simp]
theorem pontryagin_dual.map_one {A : Type u_2} {B : Type u_3} [monoid A] [monoid B] [topological_space A] [topological_space B] :
pontryagin_dual.map (continuous_monoid_hom.one A B) = continuous_monoid_hom.one (pontryagin_dual B) (pontryagin_dual A)
source
@[simp]
theorem pontryagin_dual.map_comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [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) :
pontryagin_dual.map (g.comp f) = (pontryagin_dual.map f).comp (pontryagin_dual.map g)
source
@[simp]
theorem pontryagin_dual.map_mul {A : Type u_2} {E : Type u_6} [monoid A] [comm_group E] [topological_space A] [topological_space E] [topological_group E] (f g : continuous_monoid_hom A E) :
pontryagin_dual.map (f * g) = pontryagin_dual.map f * pontryagin_dual.map g
source
noncomputable def pontryagin_dual.map_hom (A : Type u_2) (E : Type u_6) [monoid A] [comm_group E] [topological_space A] [topological_space E] [topological_group E] [locally_compact_space E] :
continuous_monoid_hom (continuous_monoid_hom A E) (continuous_monoid_hom (pontryagin_dual E) (pontryagin_dual A))

continuous_monoid_hom.dual as a continuous_monoid_hom.

Equations