mathlib documentation

topology.algebra.continuous_monoid_hom

Continuous Monoid Homs #

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

Main definitions #

structure continuous_add_monoid_hom (A : Type u_9) (B : Type u_10) [add_monoid A] [add_monoid B] [topological_space A] [topological_space B] :
Type (max u_10 u_9)

The type of continuous additive monoid homomorphisms from α to β.

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

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

Instances for continuous_add_monoid_hom
structure continuous_monoid_hom (A : Type u_4) (B : Type u_5) [monoid A] [monoid B] [topological_space A] [topological_space B] :
Type (max u_4 u_5)

The type of continuous monoid homomorphisms from α to β.

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

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

Instances for continuous_monoid_hom
@[class]
structure continuous_add_monoid_hom_class (F : Type u_9) (α : Type u_10) (β : Type u_11) [add_monoid α] [add_monoid β] [topological_space α] [topological_space β] :
Type (max u_10 u_11 u_9)

continuous_add_monoid_hom_class F α β 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
@[class]
structure continuous_monoid_hom_class (F : Type u_9) (α : Type u_10) (β : Type u_11) [monoid α] [monoid β] [topological_space α] [topological_space β] :
Type (max u_10 u_11 u_9)

continuous_monoid_hom_class F α β 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
@[protected, instance]
def continuous_monoid_hom.has_coe_to_fun {A : Type u_4} {B : Type u_5} [monoid A] [monoid B] [topological_space A] [topological_space B] :

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

Equations
theorem continuous_add_monoid_hom.ext {A : Type u_4} {B : Type u_5} [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
theorem continuous_monoid_hom.ext {A : Type u_4} {B : Type u_5} [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
@[simp]
@[simp]
theorem continuous_monoid_hom.mk'_to_monoid_hom_apply {A : Type u_4} {B : Type u_5} [monoid A] [monoid B] [topological_space A] [topological_space B] (f : A →* B) (hf : continuous f) (ᾰ : A) :

Composition of two continuous homomorphisms.

Equations
def continuous_monoid_hom.comp {A : Type u_4} {B : Type u_5} {C : Type u_6} [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) :

Composition of two continuous homomorphisms.

Equations

Product of two continuous homomorphisms on the same space.

Equations
def continuous_monoid_hom.prod {A : Type u_4} {B : Type u_5} {C : Type u_6} [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) :

Product of two continuous homomorphisms on the same space.

Equations
def continuous_monoid_hom.prod_map {A : Type u_4} {B : Type u_5} {C : Type u_6} {D : Type u_7} [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) :

Product of two continuous homomorphisms on different spaces.

Equations
@[simp]

Product of two continuous homomorphisms on different spaces.

Equations

The trivial continuous homomorphism.

Equations
def continuous_monoid_hom.one (A : Type u_4) (B : Type u_5) [monoid A] [monoid B] [topological_space A] [topological_space B] :

The trivial continuous homomorphism.

Equations
@[protected, instance]
Equations
def continuous_monoid_hom.fst (A : Type u_4) (B : Type u_5) [monoid A] [monoid B] [topological_space A] [topological_space B] :

The continuous homomorphism given by projection onto the first factor.

Equations

The continuous homomorphism given by projection onto the first factor.

Equations
def continuous_monoid_hom.snd (A : Type u_4) (B : Type u_5) [monoid A] [monoid B] [topological_space A] [topological_space B] :

The continuous homomorphism given by projection onto the second factor.

Equations

The continuous homomorphism given by projection onto the second factor.

Equations
def continuous_monoid_hom.inl (A : Type u_4) (B : Type u_5) [monoid A] [monoid B] [topological_space A] [topological_space B] :

The continuous homomorphism given by inclusion of the first factor.

Equations

The continuous homomorphism given by inclusion of the first factor.

Equations

The continuous homomorphism given by inclusion of the second factor.

Equations
def continuous_monoid_hom.inr (A : Type u_4) (B : Type u_5) [monoid A] [monoid B] [topological_space A] [topological_space B] :

The continuous homomorphism given by inclusion of the second factor.

Equations

The continuous homomorphism given by the diagonal embedding.

Equations

The continuous homomorphism given by the diagonal embedding.

Equations
def continuous_monoid_hom.swap (A : Type u_4) (B : Type u_5) [monoid A] [monoid B] [topological_space A] [topological_space B] :

The continuous homomorphism given by swapping components.

Equations

The continuous homomorphism given by swapping components.

Equations

The continuous homomorphism given by multiplication.

Equations

The continuous homomorphism given by inversion.

Equations

Coproduct of two continuous homomorphisms to the same space.

Equations

Coproduct of two continuous homomorphisms to the same space.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable def pontryagin_dual.inhabited (G : Type u_1) [monoid G] [topological_space G] :
def pontryagin_dual (G : Type u_1) [monoid G] [topological_space G] :
Type u_1

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

Equations
Instances for pontryagin_dual
@[protected, instance]
@[protected, instance]
noncomputable def pontryagin_dual.comm_group (G : Type u_1) [monoid G] [topological_space G] :