Continuous Monoid Homs

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

Main definitions

• ContinuousMonoidHom A B: The continuous homomorphisms A →* B.
• ContinuousAddMonoidHom A B: The continuous additive homomorphisms A →+ B.

structure ContinuousAddMonoidHom (A : Type u_7) (B : Type u_8) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] extends AddMonoidHom : 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 : ContinuousAddMonoidHom A B), you should parametrize over (F : Type*) [ContinuousAddMonoidHomClass F A B] (f : F).

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

• toFun : A → B
• map_zero' : (↑self.toAddMonoidHom).toFun 0 = 0
• map_add' : ∀ (x y : A), (↑self.toAddMonoidHom).toFun (x + y) = (↑self.toAddMonoidHom).toFun x + (↑self.toAddMonoidHom).toFun y
• continuous_toFun : Continuous self.toFun

  Proof of continuity of the Hom.

structure ContinuousMonoidHom (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] extends MonoidHom : Type (max u_2 u_3)

The type of continuous monoid homomorphisms from A to B.

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

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

• toFun : A → B
• map_one' : (↑self.toMonoidHom).toFun 1 = 1
• map_mul' : ∀ (x y : A), (↑self.toMonoidHom).toFun (x * y) = (↑self.toMonoidHom).toFun x * (↑self.toMonoidHom).toFun y
• continuous_toFun : Continuous self.toFun

  Proof of continuity of the Hom.

class ContinuousAddMonoidHomClass (F : Type u_1) (A : outParam (Type u_7)) (B : outParam (Type u_8)) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] [FunLike F A B] extends AddMonoidHomClass : Prop

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

You should also extend this typeclass when you extend ContinuousAddMonoidHom.

• map_add : ∀ (f : F) (x y : A), f (x + y) = f x + f y
• map_zero : ∀ (f : F), f 0 = 0
• map_continuous : ∀ (f : F), Continuous ⇑f

  Proof of the continuity of the map.

class ContinuousMonoidHomClass (F : Type u_1) (A : outParam (Type u_7)) (B : outParam (Type u_8)) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [FunLike F A B] extends MonoidHomClass : Prop

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

You should also extend this typeclass when you extend ContinuousMonoidHom.

• map_mul : ∀ (f : F) (x y : A), f (x * y) = f x * f y
• map_one : ∀ (f : F), f 1 = 1
• map_continuous : ∀ (f : F), Continuous ⇑f

  Proof of the continuity of the map.

instance ContinuousAddMonoidHomClass.toContinuousMapClass (F : Type u_1) (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] [FunLike F A B] [ContinuousAddMonoidHomClass F A B] : ContinuousMapClass F A B

Equations

• (_ : ContinuousMapClass F A B) = (_ : ContinuousMapClass F A B)

instance ContinuousMonoidHomClass.toContinuousMapClass (F : Type u_1) (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [FunLike F A B] [ContinuousMonoidHomClass F A B] : ContinuousMapClass F A B

Equations

• (_ : ContinuousMapClass F A B) = (_ : ContinuousMapClass F A B)

instance ContinuousAddMonoidHom.ContinuousMonoidHom.funLike {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : FunLike (ContinuousAddMonoidHom A B) A B

Equations

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

theorem ContinuousAddMonoidHom.ContinuousMonoidHom.funLike.proof_1 {A : Type u_2} {B : Type u_1} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (f : ContinuousAddMonoidHom A B) (g : ContinuousAddMonoidHom A B) (h : (fun (f : ContinuousAddMonoidHom A B) => f.toFun) f = (fun (f : ContinuousAddMonoidHom A B) => f.toFun) g) : f = g

instance ContinuousMonoidHom.ContinuousMonoidHom.funLike {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : FunLike (ContinuousMonoidHom A B) A B

Equations

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

instance ContinuousAddMonoidHom.ContinuousMonoidHom.ContinuousAddMonoidHomClass {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousAddMonoidHomClass (ContinuousAddMonoidHom A B) A B

Equations

• (_ : ContinuousAddMonoidHomClass (ContinuousAddMonoidHom A B) A B) = (_ : ContinuousAddMonoidHomClass (ContinuousAddMonoidHom A B) A B)

instance ContinuousMonoidHom.ContinuousMonoidHom.ContinuousMonoidHomClass {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousMonoidHomClass (ContinuousMonoidHom A B) A B

Equations

• (_ : ContinuousMonoidHomClass (ContinuousMonoidHom A B) A B) = (_ : ContinuousMonoidHomClass (ContinuousMonoidHom A B) A B)

theorem ContinuousAddMonoidHom.ext {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] {f : ContinuousAddMonoidHom A B} {g : ContinuousAddMonoidHom A B} (h : ∀ (x : A), f x = g x) : f = g

theorem ContinuousMonoidHom.ext {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] {f : ContinuousMonoidHom A B} {g : ContinuousMonoidHom A B} (h : ∀ (x : A), f x = g x) : f = g

def ContinuousAddMonoidHom.toContinuousMap {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (f : ContinuousAddMonoidHom A B) : C(A, B)

Reinterpret a ContinuousAddMonoidHom as a ContinuousMap.

Equations

• ContinuousAddMonoidHom.toContinuousMap f = ContinuousMap.mk f.toFun

def ContinuousMonoidHom.toContinuousMap {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (f : ContinuousMonoidHom A B) : C(A, B)

Reinterpret a ContinuousMonoidHom as a ContinuousMap.

Equations

• ContinuousMonoidHom.toContinuousMap f = ContinuousMap.mk f.toFun

theorem ContinuousAddMonoidHom.toContinuousMap_injective {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : Function.Injective ContinuousAddMonoidHom.toContinuousMap

theorem ContinuousMonoidHom.toContinuousMap_injective {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : Function.Injective ContinuousMonoidHom.toContinuousMap

def ContinuousAddMonoidHom.mk' {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (f : A →+ B) (hf : Continuous ⇑f) : ContinuousAddMonoidHom A B

Construct a ContinuousAddMonoidHom from a Continuous AddMonoidHom.

Equations

• ContinuousAddMonoidHom.mk' f hf = { toAddMonoidHom := f, continuous_toFun := hf }

def ContinuousMonoidHom.mk' {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (f : A →* B) (hf : Continuous ⇑f) : ContinuousMonoidHom A B

Construct a ContinuousMonoidHom from a Continuous MonoidHom.

Equations

• ContinuousMonoidHom.mk' f hf = { toMonoidHom := f, continuous_toFun := hf }

theorem ContinuousAddMonoidHom.comp.proof_1 {A : Type u_1} {B : Type u_3} {C : Type u_2} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (g : ContinuousAddMonoidHom B C) (f : ContinuousAddMonoidHom A B) : Continuous (g.toFun ∘ fun (x : A) => f.toAddMonoidHom x)

def ContinuousAddMonoidHom.comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (g : ContinuousAddMonoidHom B C) (f : ContinuousAddMonoidHom A B) : ContinuousAddMonoidHom A C

Composition of two continuous homomorphisms.

Equations

• ContinuousAddMonoidHom.comp g f = ContinuousAddMonoidHom.mk' (AddMonoidHom.comp g.toAddMonoidHom f.toAddMonoidHom) (_ : Continuous (g.toFun ∘ fun (x : A) => f.toAddMonoidHom x))

@[simp]

theorem ContinuousMonoidHom.comp_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (g : ContinuousMonoidHom B C) (f : ContinuousMonoidHom A B) : ∀ (a : A), (ContinuousMonoidHom.comp g f) a = g.toMonoidHom (f.toMonoidHom a)

@[simp]

theorem ContinuousAddMonoidHom.comp_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (g : ContinuousAddMonoidHom B C) (f : ContinuousAddMonoidHom A B) : ∀ (a : A), (ContinuousAddMonoidHom.comp g f) a = g.toAddMonoidHom (f.toAddMonoidHom a)

def ContinuousMonoidHom.comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (g : ContinuousMonoidHom B C) (f : ContinuousMonoidHom A B) : ContinuousMonoidHom A C

Composition of two continuous homomorphisms.

Equations

• ContinuousMonoidHom.comp g f = ContinuousMonoidHom.mk' (MonoidHom.comp g.toMonoidHom f.toMonoidHom) (_ : Continuous (g.toFun ∘ fun (x : A) => f.toMonoidHom x))

def ContinuousAddMonoidHom.sum {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : ContinuousAddMonoidHom A B) (g : ContinuousAddMonoidHom A C) : ContinuousAddMonoidHom A (B × C)

Product of two continuous homomorphisms on the same space.

Equations

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

theorem ContinuousAddMonoidHom.sum.proof_1 {A : Type u_1} {B : Type u_3} {C : Type u_2} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : ContinuousAddMonoidHom A B) (g : ContinuousAddMonoidHom A C) : Continuous fun (x : A) => ((↑f.toAddMonoidHom).toFun x, g.toAddMonoidHom x)

@[simp]

theorem ContinuousMonoidHom.prod_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : ContinuousMonoidHom A B) (g : ContinuousMonoidHom A C) (i : A) : (ContinuousMonoidHom.prod f g) i = (f.toMonoidHom i, g.toMonoidHom i)

@[simp]

theorem ContinuousAddMonoidHom.sum_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : ContinuousAddMonoidHom A B) (g : ContinuousAddMonoidHom A C) (i : A) : (ContinuousAddMonoidHom.sum f g) i = (f.toAddMonoidHom i, g.toAddMonoidHom i)

def ContinuousMonoidHom.prod {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : ContinuousMonoidHom A B) (g : ContinuousMonoidHom A C) : ContinuousMonoidHom A (B × C)

Product of two continuous homomorphisms on the same space.

Equations

• ContinuousMonoidHom.prod f g = ContinuousMonoidHom.mk' (MonoidHom.prod f.toMonoidHom g.toMonoidHom) (_ : Continuous fun (x : A) => ((↑f.toMonoidHom).toFun x, g.toMonoidHom x))

theorem ContinuousAddMonoidHom.sum_map.proof_1 {A : Type u_1} {B : Type u_2} {C : Type u_4} {D : Type u_3} [AddMonoid A] [AddMonoid B] [AddMonoid C] [AddMonoid D] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D] (f : ContinuousAddMonoidHom A C) (g : ContinuousAddMonoidHom B D) : Continuous fun (p : A × B) => ((↑f.toAddMonoidHom).toFun p.1, (↑g.toAddMonoidHom).1 p.2)

def ContinuousAddMonoidHom.sum_map {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddMonoid A] [AddMonoid B] [AddMonoid C] [AddMonoid D] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D] (f : ContinuousAddMonoidHom A C) (g : ContinuousAddMonoidHom B D) : ContinuousAddMonoidHom (A × B) (C × D)

Product of two continuous homomorphisms on different spaces.

Equations

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

@[simp]

theorem ContinuousAddMonoidHom.sum_map_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddMonoid A] [AddMonoid B] [AddMonoid C] [AddMonoid D] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D] (f : ContinuousAddMonoidHom A C) (g : ContinuousAddMonoidHom B D) (i : A × B) : (ContinuousAddMonoidHom.sum_map f g) i = (f.toAddMonoidHom i.1, g.toAddMonoidHom i.2)

@[simp]

theorem ContinuousMonoidHom.prod_map_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [Monoid A] [Monoid B] [Monoid C] [Monoid D] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D] (f : ContinuousMonoidHom A C) (g : ContinuousMonoidHom B D) (i : A × B) : (ContinuousMonoidHom.prod_map f g) i = (f.toMonoidHom i.1, g.toMonoidHom i.2)

def ContinuousMonoidHom.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] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D] (f : ContinuousMonoidHom A C) (g : ContinuousMonoidHom B D) : ContinuousMonoidHom (A × B) (C × D)

Product of two continuous homomorphisms on different spaces.

Equations

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

theorem ContinuousAddMonoidHom.zero.proof_1 (A : Type u_1) (B : Type u_2) [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : Continuous fun (x : A) => AddZeroClass.toZero.1

def ContinuousAddMonoidHom.zero (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousAddMonoidHom A B

The trivial continuous homomorphism.

Equations

• ContinuousAddMonoidHom.zero A B = ContinuousAddMonoidHom.mk' 0 (_ : Continuous fun (x : A) => AddZeroClass.toZero.1)

@[simp]

theorem ContinuousMonoidHom.one_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : ∀ (x : A), (ContinuousMonoidHom.one A B) x = 1

@[simp]

theorem ContinuousAddMonoidHom.zero_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : ∀ (x : A), (ContinuousAddMonoidHom.zero A B) x = 0

def ContinuousMonoidHom.one (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousMonoidHom A B

The trivial continuous homomorphism.

Equations

• ContinuousMonoidHom.one A B = ContinuousMonoidHom.mk' 1 (_ : Continuous fun (x : A) => MulOneClass.toOne.1)

instance ContinuousAddMonoidHom.instInhabitedContinuousAddMonoidHom (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : Inhabited (ContinuousAddMonoidHom A B)

Equations

• ContinuousAddMonoidHom.instInhabitedContinuousAddMonoidHom A B = { default := ContinuousAddMonoidHom.zero A B }

instance ContinuousMonoidHom.instInhabitedContinuousMonoidHom (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : Inhabited (ContinuousMonoidHom A B)

Equations

• ContinuousMonoidHom.instInhabitedContinuousMonoidHom A B = { default := ContinuousMonoidHom.one A B }

def ContinuousAddMonoidHom.id (A : Type u_2) [AddMonoid A] [TopologicalSpace A] : ContinuousAddMonoidHom A A

The identity continuous homomorphism.

Equations

• ContinuousAddMonoidHom.id A = ContinuousAddMonoidHom.mk' (AddMonoidHom.id A) (_ : Continuous id)

@[simp]

theorem ContinuousMonoidHom.id_toFun (A : Type u_2) [Monoid A] [TopologicalSpace A] (x : A) : (ContinuousMonoidHom.id A) x = x

@[simp]

theorem ContinuousAddMonoidHom.id_toFun (A : Type u_2) [AddMonoid A] [TopologicalSpace A] (x : A) : (ContinuousAddMonoidHom.id A) x = x

def ContinuousMonoidHom.id (A : Type u_2) [Monoid A] [TopologicalSpace A] : ContinuousMonoidHom A A

The identity continuous homomorphism.

Equations

• ContinuousMonoidHom.id A = ContinuousMonoidHom.mk' (MonoidHom.id A) (_ : Continuous id)

def ContinuousAddMonoidHom.fst (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousAddMonoidHom (A × B) A

The continuous homomorphism given by projection onto the first factor.

Equations

• ContinuousAddMonoidHom.fst A B = ContinuousAddMonoidHom.mk' (AddMonoidHom.fst A B) (_ : Continuous Prod.fst)

@[simp]

theorem ContinuousMonoidHom.fst_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) : (ContinuousMonoidHom.fst A B) self = self.1

@[simp]

theorem ContinuousAddMonoidHom.fst_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) : (ContinuousAddMonoidHom.fst A B) self = self.1

def ContinuousMonoidHom.fst (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousMonoidHom (A × B) A

The continuous homomorphism given by projection onto the first factor.

Equations

• ContinuousMonoidHom.fst A B = ContinuousMonoidHom.mk' (MonoidHom.fst A B) (_ : Continuous Prod.fst)

def ContinuousAddMonoidHom.snd (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousAddMonoidHom (A × B) B

The continuous homomorphism given by projection onto the second factor.

Equations

• ContinuousAddMonoidHom.snd A B = ContinuousAddMonoidHom.mk' (AddMonoidHom.snd A B) (_ : Continuous Prod.snd)

@[simp]

theorem ContinuousMonoidHom.snd_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) : (ContinuousMonoidHom.snd A B) self = self.2

@[simp]

theorem ContinuousAddMonoidHom.snd_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) : (ContinuousAddMonoidHom.snd A B) self = self.2

def ContinuousMonoidHom.snd (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousMonoidHom (A × B) B

The continuous homomorphism given by projection onto the second factor.

Equations

• ContinuousMonoidHom.snd A B = ContinuousMonoidHom.mk' (MonoidHom.snd A B) (_ : Continuous Prod.snd)

def ContinuousAddMonoidHom.inl (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousAddMonoidHom A (A × B)

The continuous homomorphism given by inclusion of the first factor.

Equations

• ContinuousAddMonoidHom.inl A B = ContinuousAddMonoidHom.sum (ContinuousAddMonoidHom.id A) (ContinuousAddMonoidHom.zero A B)

@[simp]

theorem ContinuousAddMonoidHom.inl_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A) : (ContinuousAddMonoidHom.inl A B) i = ((ContinuousAddMonoidHom.id A).toAddMonoidHom i, (ContinuousAddMonoidHom.zero A B).toAddMonoidHom i)

@[simp]

theorem ContinuousMonoidHom.inl_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A) : (ContinuousMonoidHom.inl A B) i = ((ContinuousMonoidHom.id A).toMonoidHom i, (ContinuousMonoidHom.one A B).toMonoidHom i)

def ContinuousMonoidHom.inl (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousMonoidHom A (A × B)

The continuous homomorphism given by inclusion of the first factor.

Equations

• ContinuousMonoidHom.inl A B = ContinuousMonoidHom.prod (ContinuousMonoidHom.id A) (ContinuousMonoidHom.one A B)

def ContinuousAddMonoidHom.inr (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousAddMonoidHom B (A × B)

The continuous homomorphism given by inclusion of the second factor.

Equations

• ContinuousAddMonoidHom.inr A B = ContinuousAddMonoidHom.sum (ContinuousAddMonoidHom.zero B A) (ContinuousAddMonoidHom.id B)

@[simp]

theorem ContinuousAddMonoidHom.inr_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (i : B) : (ContinuousAddMonoidHom.inr A B) i = ((ContinuousAddMonoidHom.zero B A).toAddMonoidHom i, (ContinuousAddMonoidHom.id B).toAddMonoidHom i)

@[simp]

theorem ContinuousMonoidHom.inr_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (i : B) : (ContinuousMonoidHom.inr A B) i = ((ContinuousMonoidHom.one B A).toMonoidHom i, (ContinuousMonoidHom.id B).toMonoidHom i)

def ContinuousMonoidHom.inr (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousMonoidHom B (A × B)

The continuous homomorphism given by inclusion of the second factor.

Equations

• ContinuousMonoidHom.inr A B = ContinuousMonoidHom.prod (ContinuousMonoidHom.one B A) (ContinuousMonoidHom.id B)

def ContinuousAddMonoidHom.diag (A : Type u_2) [AddMonoid A] [TopologicalSpace A] : ContinuousAddMonoidHom A (A × A)

The continuous homomorphism given by the diagonal embedding.

Equations

• ContinuousAddMonoidHom.diag A = ContinuousAddMonoidHom.sum (ContinuousAddMonoidHom.id A) (ContinuousAddMonoidHom.id A)

@[simp]

theorem ContinuousAddMonoidHom.diag_toFun (A : Type u_2) [AddMonoid A] [TopologicalSpace A] (i : A) : (ContinuousAddMonoidHom.diag A) i = ((ContinuousAddMonoidHom.id A).toAddMonoidHom i, (ContinuousAddMonoidHom.id A).toAddMonoidHom i)

@[simp]

theorem ContinuousMonoidHom.diag_toFun (A : Type u_2) [Monoid A] [TopologicalSpace A] (i : A) : (ContinuousMonoidHom.diag A) i = ((ContinuousMonoidHom.id A).toMonoidHom i, (ContinuousMonoidHom.id A).toMonoidHom i)

def ContinuousMonoidHom.diag (A : Type u_2) [Monoid A] [TopologicalSpace A] : ContinuousMonoidHom A (A × A)

The continuous homomorphism given by the diagonal embedding.

Equations

• ContinuousMonoidHom.diag A = ContinuousMonoidHom.prod (ContinuousMonoidHom.id A) (ContinuousMonoidHom.id A)

def ContinuousAddMonoidHom.swap (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousAddMonoidHom (A × B) (B × A)

The continuous homomorphism given by swapping components.

Equations

• ContinuousAddMonoidHom.swap A B = ContinuousAddMonoidHom.sum (ContinuousAddMonoidHom.snd A B) (ContinuousAddMonoidHom.fst A B)

@[simp]

theorem ContinuousAddMonoidHom.swap_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A × B) : (ContinuousAddMonoidHom.swap A B) i = ((ContinuousAddMonoidHom.snd A B).toAddMonoidHom i, (ContinuousAddMonoidHom.fst A B).toAddMonoidHom i)

@[simp]

theorem ContinuousMonoidHom.swap_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A × B) : (ContinuousMonoidHom.swap A B) i = ((ContinuousMonoidHom.snd A B).toMonoidHom i, (ContinuousMonoidHom.fst A B).toMonoidHom i)

def ContinuousMonoidHom.swap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousMonoidHom (A × B) (B × A)

The continuous homomorphism given by swapping components.

Equations

• ContinuousMonoidHom.swap A B = ContinuousMonoidHom.prod (ContinuousMonoidHom.snd A B) (ContinuousMonoidHom.fst A B)

theorem ContinuousAddMonoidHom.add.proof_1 (E : Type u_1) [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] : Continuous fun (p : E × E) => p.1 + p.2

def ContinuousAddMonoidHom.add (E : Type u_6) [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] : ContinuousAddMonoidHom (E × E) E

The continuous homomorphism given by addition.

Equations

• ContinuousAddMonoidHom.add E = ContinuousAddMonoidHom.mk' addAddMonoidHom (_ : Continuous fun (p : E × E) => p.1 + p.2)

@[simp]

theorem ContinuousAddMonoidHom.add_toFun (E : Type u_6) [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] : ∀ (a : E × E), (ContinuousAddMonoidHom.add E) a = a.1 + a.2

@[simp]

theorem ContinuousMonoidHom.mul_toFun (E : Type u_6) [CommGroup E] [TopologicalSpace E] [TopologicalGroup E] : ∀ (a : E × E), (ContinuousMonoidHom.mul E) a = a.1 * a.2

def ContinuousMonoidHom.mul (E : Type u_6) [CommGroup E] [TopologicalSpace E] [TopologicalGroup E] : ContinuousMonoidHom (E × E) E

The continuous homomorphism given by multiplication.

Equations

• ContinuousMonoidHom.mul E = ContinuousMonoidHom.mk' mulMonoidHom (_ : Continuous fun (p : E × E) => p.1 * p.2)

theorem ContinuousAddMonoidHom.neg.proof_1 (E : Type u_1) [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] : Continuous fun (a : E) => -a

def ContinuousAddMonoidHom.neg (E : Type u_6) [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] : ContinuousAddMonoidHom E E

The continuous homomorphism given by negation.

Equations

• ContinuousAddMonoidHom.neg E = ContinuousAddMonoidHom.mk' negAddMonoidHom (_ : Continuous fun (a : E) => -a)

@[simp]

theorem ContinuousAddMonoidHom.neg_toFun (E : Type u_6) [AddCommGroup E] [TopologicalSpace E] [TopologicalAddGroup E] : ∀ (a : E), (ContinuousAddMonoidHom.neg E) a = -a

@[simp]

theorem ContinuousMonoidHom.inv_toFun (E : Type u_6) [CommGroup E] [TopologicalSpace E] [TopologicalGroup E] : ∀ (a : E), (ContinuousMonoidHom.inv E) a = a⁻¹

def ContinuousMonoidHom.inv (E : Type u_6) [CommGroup E] [TopologicalSpace E] [TopologicalGroup E] : ContinuousMonoidHom E E

The continuous homomorphism given by inversion.

Equations

• ContinuousMonoidHom.inv E = ContinuousMonoidHom.mk' invMonoidHom (_ : Continuous fun (a : E) => a⁻¹)

def ContinuousAddMonoidHom.coprod {A : Type u_2} {B : Type u_3} {E : Type u_6} [AddMonoid A] [AddMonoid B] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace E] [TopologicalAddGroup E] (f : ContinuousAddMonoidHom A E) (g : ContinuousAddMonoidHom B E) : ContinuousAddMonoidHom (A × B) E

Coproduct of two continuous homomorphisms to the same space.

Equations

• ContinuousAddMonoidHom.coprod f g = ContinuousAddMonoidHom.comp (ContinuousAddMonoidHom.add E) (ContinuousAddMonoidHom.sum_map f g)

@[simp]

theorem ContinuousMonoidHom.coprod_toFun {A : Type u_2} {B : Type u_3} {E : Type u_6} [Monoid A] [Monoid B] [CommGroup E] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace E] [TopologicalGroup E] (f : ContinuousMonoidHom A E) (g : ContinuousMonoidHom B E) : ∀ (a : A × B), (ContinuousMonoidHom.coprod f g) a = (ContinuousMonoidHom.mul E).toMonoidHom ((ContinuousMonoidHom.prod_map f g).toMonoidHom a)

@[simp]

theorem ContinuousAddMonoidHom.coprod_toFun {A : Type u_2} {B : Type u_3} {E : Type u_6} [AddMonoid A] [AddMonoid B] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace E] [TopologicalAddGroup E] (f : ContinuousAddMonoidHom A E) (g : ContinuousAddMonoidHom B E) : ∀ (a : A × B), (ContinuousAddMonoidHom.coprod f g) a = (ContinuousAddMonoidHom.add E).toAddMonoidHom ((ContinuousAddMonoidHom.sum_map f g).toAddMonoidHom a)

def ContinuousMonoidHom.coprod {A : Type u_2} {B : Type u_3} {E : Type u_6} [Monoid A] [Monoid B] [CommGroup E] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace E] [TopologicalGroup E] (f : ContinuousMonoidHom A E) (g : ContinuousMonoidHom B E) : ContinuousMonoidHom (A × B) E

Coproduct of two continuous homomorphisms to the same space.

Equations

• ContinuousMonoidHom.coprod f g = ContinuousMonoidHom.comp (ContinuousMonoidHom.mul E) (ContinuousMonoidHom.prod_map f g)

instance ContinuousAddMonoidHom.instAddCommGroupContinuousAddMonoidHomToAddMonoidToSubNegAddMonoidToAddGroup {A : Type u_2} {E : Type u_6} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] : AddCommGroup (ContinuousAddMonoidHom A E)

Equations

• ContinuousAddMonoidHom.instAddCommGroupContinuousAddMonoidHomToAddMonoidToSubNegAddMonoidToAddGroup = AddCommGroup.mk (_ : ∀ (f g : ContinuousAddMonoidHom A E), f + g = g + f)

theorem ContinuousAddMonoidHom.instAddCommGroupContinuousAddMonoidHomToAddMonoidToSubNegAddMonoidToAddGroup.proof_13 {A : Type u_2} {E : Type u_1} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] (f : ContinuousAddMonoidHom A E) : -f + f = 0

theorem ContinuousAddMonoidHom.instAddCommGroupContinuousAddMonoidHomToAddMonoidToSubNegAddMonoidToAddGroup.proof_6 {A : Type u_2} {E : Type u_1} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] (f : ContinuousAddMonoidHom A E) (g : ContinuousAddMonoidHom A E) (h : ContinuousAddMonoidHom A E) : f + g + h = f + (g + h)

theorem ContinuousAddMonoidHom.instAddCommGroupContinuousAddMonoidHomToAddMonoidToSubNegAddMonoidToAddGroup.proof_14 {A : Type u_2} {E : Type u_1} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] (f : ContinuousAddMonoidHom A E) (g : ContinuousAddMonoidHom A E) : f + g = g + f

theorem ContinuousAddMonoidHom.instAddCommGroupContinuousAddMonoidHomToAddMonoidToSubNegAddMonoidToAddGroup.proof_12 {A : Type u_2} {E : Type u_1} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] : ∀ (n : ℕ) (a : ContinuousAddMonoidHom A E), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a

theorem ContinuousAddMonoidHom.instAddCommGroupContinuousAddMonoidHomToAddMonoidToSubNegAddMonoidToAddGroup.proof_9 {A : Type u_2} {E : Type u_1} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] : ∀ (a b : ContinuousAddMonoidHom A E), a - b = a - b

theorem ContinuousAddMonoidHom.instAddCommGroupContinuousAddMonoidHomToAddMonoidToSubNegAddMonoidToAddGroup.proof_2 {A : Type u_2} {E : Type u_1} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] (f : ContinuousAddMonoidHom A E) : 0 + f = f

theorem ContinuousAddMonoidHom.instAddCommGroupContinuousAddMonoidHomToAddMonoidToSubNegAddMonoidToAddGroup.proof_7 {A : Type u_2} {E : Type u_1} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] (f : ContinuousAddMonoidHom A E) : 0 + f = f

theorem ContinuousAddMonoidHom.instAddCommGroupContinuousAddMonoidHomToAddMonoidToSubNegAddMonoidToAddGroup.proof_4 {A : Type u_2} {E : Type u_1} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] : ∀ (x : ContinuousAddMonoidHom A E), nsmulRec 0 x = nsmulRec 0 x

theorem ContinuousAddMonoidHom.instAddCommGroupContinuousAddMonoidHomToAddMonoidToSubNegAddMonoidToAddGroup.proof_3 {A : Type u_2} {E : Type u_1} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] (f : ContinuousAddMonoidHom A E) : f + 0 = f

theorem ContinuousAddMonoidHom.instAddCommGroupContinuousAddMonoidHomToAddMonoidToSubNegAddMonoidToAddGroup.proof_10 {A : Type u_2} {E : Type u_1} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] : ∀ (a : ContinuousAddMonoidHom A E), zsmulRec 0 a = zsmulRec 0 a

theorem ContinuousAddMonoidHom.instAddCommGroupContinuousAddMonoidHomToAddMonoidToSubNegAddMonoidToAddGroup.proof_11 {A : Type u_2} {E : Type u_1} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] : ∀ (n : ℕ) (a : ContinuousAddMonoidHom A E), zsmulRec (Int.ofNat (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) a

theorem ContinuousAddMonoidHom.instAddCommGroupContinuousAddMonoidHomToAddMonoidToSubNegAddMonoidToAddGroup.proof_5 {A : Type u_2} {E : Type u_1} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] : ∀ (n : ℕ) (x : ContinuousAddMonoidHom A E), nsmulRec (n + 1) x = nsmulRec (n + 1) x

theorem ContinuousAddMonoidHom.instAddCommGroupContinuousAddMonoidHomToAddMonoidToSubNegAddMonoidToAddGroup.proof_8 {A : Type u_2} {E : Type u_1} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] (f : ContinuousAddMonoidHom A E) : f + 0 = f

theorem ContinuousAddMonoidHom.instAddCommGroupContinuousAddMonoidHomToAddMonoidToSubNegAddMonoidToAddGroup.proof_1 {A : Type u_2} {E : Type u_1} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] (f : ContinuousAddMonoidHom A E) (g : ContinuousAddMonoidHom A E) (h : ContinuousAddMonoidHom A E) : f + g + h = f + (g + h)

instance ContinuousMonoidHom.instCommGroupContinuousMonoidHomToMonoidToDivInvMonoidToGroup {A : Type u_2} {E : Type u_6} [Monoid A] [CommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalGroup E] : CommGroup (ContinuousMonoidHom A E)

Equations

• ContinuousMonoidHom.instCommGroupContinuousMonoidHomToMonoidToDivInvMonoidToGroup = CommGroup.mk (_ : ∀ (f g : ContinuousMonoidHom A E), f * g = g * f)

instance ContinuousAddMonoidHom.instTopologicalSpaceContinuousAddMonoidHom {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : TopologicalSpace (ContinuousAddMonoidHom A B)

Equations

• ContinuousAddMonoidHom.instTopologicalSpaceContinuousAddMonoidHom = TopologicalSpace.induced ContinuousAddMonoidHom.toContinuousMap ContinuousMap.compactOpen

instance ContinuousMonoidHom.instTopologicalSpaceContinuousMonoidHom {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : TopologicalSpace (ContinuousMonoidHom A B)

Equations

• ContinuousMonoidHom.instTopologicalSpaceContinuousMonoidHom = TopologicalSpace.induced ContinuousMonoidHom.toContinuousMap ContinuousMap.compactOpen

theorem ContinuousAddMonoidHom.inducing_toContinuousMap (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : Inducing ContinuousAddMonoidHom.toContinuousMap

theorem ContinuousMonoidHom.inducing_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : Inducing ContinuousMonoidHom.toContinuousMap

theorem ContinuousAddMonoidHom.embedding_toContinuousMap (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : Embedding ContinuousAddMonoidHom.toContinuousMap

theorem ContinuousMonoidHom.embedding_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : Embedding ContinuousMonoidHom.toContinuousMap

theorem ContinuousAddMonoidHom.range_toContinuousMap (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : Set.range ContinuousAddMonoidHom.toContinuousMap = {f : C(A, B) | f 0 = 0 ∧ ∀ (x y : A), f (x + y) = f x + f y}

theorem ContinuousMonoidHom.range_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : Set.range ContinuousMonoidHom.toContinuousMap = {f : C(A, B) | f 1 = 1 ∧ ∀ (x y : A), f (x * y) = f x * f y}

theorem ContinuousAddMonoidHom.closedEmbedding_toContinuousMap (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] [ContinuousAdd B] [T2Space B] : ClosedEmbedding ContinuousAddMonoidHom.toContinuousMap

theorem ContinuousMonoidHom.closedEmbedding_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [ContinuousMul B] [T2Space B] : ClosedEmbedding ContinuousMonoidHom.toContinuousMap

instance ContinuousAddMonoidHom.instT2SpaceContinuousAddMonoidHomInstTopologicalSpaceContinuousAddMonoidHom {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] [T2Space B] : T2Space (ContinuousAddMonoidHom A B)

Equations

• (_ : T2Space (ContinuousAddMonoidHom A B)) = (_ : T2Space (ContinuousAddMonoidHom A B))

instance ContinuousMonoidHom.instT2SpaceContinuousMonoidHomInstTopologicalSpaceContinuousMonoidHom {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [T2Space B] : T2Space (ContinuousMonoidHom A B)

Equations

• (_ : T2Space (ContinuousMonoidHom A B)) = (_ : T2Space (ContinuousMonoidHom A B))

instance ContinuousAddMonoidHom.instTopologicalAddGroupContinuousAddMonoidHomToAddMonoidToSubNegAddMonoidToAddGroupInstTopologicalSpaceContinuousAddMonoidHomToAddGroupInstAddCommGroupContinuousAddMonoidHomToAddMonoidToSubNegAddMonoidToAddGroup {A : Type u_2} {E : Type u_6} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] : TopologicalAddGroup (ContinuousAddMonoidHom A E)

Equations

• (_ : TopologicalAddGroup (ContinuousAddMonoidHom A E)) = (_ : TopologicalAddGroup (ContinuousAddMonoidHom A E))

instance ContinuousMonoidHom.instTopologicalGroupContinuousMonoidHomToMonoidToDivInvMonoidToGroupInstTopologicalSpaceContinuousMonoidHomToGroupInstCommGroupContinuousMonoidHomToMonoidToDivInvMonoidToGroup {A : Type u_2} {E : Type u_6} [Monoid A] [CommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalGroup E] : TopologicalGroup (ContinuousMonoidHom A E)

Equations

• (_ : TopologicalGroup (ContinuousMonoidHom A E)) = (_ : TopologicalGroup (ContinuousMonoidHom A E))

theorem ContinuousAddMonoidHom.continuous_of_continuous_uncurry {B : Type u_3} {C : Type u_4} [AddMonoid B] [AddMonoid C] [TopologicalSpace B] [TopologicalSpace C] {A : Type u_7} [TopologicalSpace A] (f : A → ContinuousAddMonoidHom B C) (h : Continuous (Function.uncurry fun (x : A) (y : B) => (f x) y)) : Continuous f

theorem ContinuousMonoidHom.continuous_of_continuous_uncurry {B : Type u_3} {C : Type u_4} [Monoid B] [Monoid C] [TopologicalSpace B] [TopologicalSpace C] {A : Type u_7} [TopologicalSpace A] (f : A → ContinuousMonoidHom B C) (h : Continuous (Function.uncurry fun (x : A) (y : B) => (f x) y)) : Continuous f

theorem ContinuousAddMonoidHom.continuous_comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [LocallyCompactSpace B] : Continuous fun (f : ContinuousAddMonoidHom A B × ContinuousAddMonoidHom B C) => ContinuousAddMonoidHom.comp f.2 f.1

theorem ContinuousMonoidHom.continuous_comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [LocallyCompactSpace B] : Continuous fun (f : ContinuousMonoidHom A B × ContinuousMonoidHom B C) => ContinuousMonoidHom.comp f.2 f.1

theorem ContinuousAddMonoidHom.continuous_comp_left {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : ContinuousAddMonoidHom A B) : Continuous fun (g : ContinuousAddMonoidHom B C) => ContinuousAddMonoidHom.comp g f

theorem ContinuousMonoidHom.continuous_comp_left {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : ContinuousMonoidHom A B) : Continuous fun (g : ContinuousMonoidHom B C) => ContinuousMonoidHom.comp g f

theorem ContinuousAddMonoidHom.continuous_comp_right {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : ContinuousAddMonoidHom B C) : Continuous fun (g : ContinuousAddMonoidHom A B) => ContinuousAddMonoidHom.comp f g

theorem ContinuousMonoidHom.continuous_comp_right {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : ContinuousMonoidHom B C) : Continuous fun (g : ContinuousMonoidHom A B) => ContinuousMonoidHom.comp f g

theorem ContinuousAddMonoidHom.compLeft.proof_3 {A : Type u_3} {B : Type u_1} (E : Type u_2) [AddMonoid A] [AddMonoid B] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace E] (f : ContinuousAddMonoidHom A B) : Continuous fun (g : ContinuousAddMonoidHom B E) => ContinuousAddMonoidHom.comp g f

theorem ContinuousAddMonoidHom.compLeft.proof_1 {A : Type u_1} {B : Type u_3} (E : Type u_2) [AddMonoid A] [AddMonoid B] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace E] [TopologicalAddGroup E] (f : ContinuousAddMonoidHom A B) : (fun (g : ContinuousAddMonoidHom B E) => ContinuousAddMonoidHom.comp g f) 0 = (fun (g : ContinuousAddMonoidHom B E) => ContinuousAddMonoidHom.comp g f) 0

theorem ContinuousAddMonoidHom.compLeft.proof_2 {A : Type u_3} {B : Type u_2} (E : Type u_1) [AddMonoid A] [AddMonoid B] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace E] [TopologicalAddGroup E] (f : ContinuousAddMonoidHom A B) (_g : ContinuousAddMonoidHom B E) (_h : ContinuousAddMonoidHom B E) : { toFun := fun (g : ContinuousAddMonoidHom B E) => ContinuousAddMonoidHom.comp g f, map_zero' := (_ : (fun (g : ContinuousAddMonoidHom B E) => ContinuousAddMonoidHom.comp g f) 0 = (fun (g : ContinuousAddMonoidHom B E) => ContinuousAddMonoidHom.comp g f) 0) }.toFun (_g + _h) = { toFun := fun (g : ContinuousAddMonoidHom B E) => ContinuousAddMonoidHom.comp g f, map_zero' := (_ : (fun (g : ContinuousAddMonoidHom B E) => ContinuousAddMonoidHom.comp g f) 0 = (fun (g : ContinuousAddMonoidHom B E) => ContinuousAddMonoidHom.comp g f) 0) }.toFun (_g + _h)

def ContinuousAddMonoidHom.compLeft {A : Type u_2} {B : Type u_3} (E : Type u_6) [AddMonoid A] [AddMonoid B] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace E] [TopologicalAddGroup E] (f : ContinuousAddMonoidHom A B) : ContinuousAddMonoidHom (ContinuousAddMonoidHom B E) (ContinuousAddMonoidHom A E)

ContinuousAddMonoidHom _ f is a functor.

Equations

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

def ContinuousMonoidHom.compLeft {A : Type u_2} {B : Type u_3} (E : Type u_6) [Monoid A] [Monoid B] [CommGroup E] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace E] [TopologicalGroup E] (f : ContinuousMonoidHom A B) : ContinuousMonoidHom (ContinuousMonoidHom B E) (ContinuousMonoidHom A E)

ContinuousMonoidHom _ f is a functor.

Equations

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

theorem ContinuousAddMonoidHom.compRight.proof_3 (A : Type u_1) {E : Type u_3} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] {B : Type u_2} [AddCommGroup B] [TopologicalSpace B] (f : ContinuousAddMonoidHom B E) : Continuous fun (g : ContinuousAddMonoidHom A B) => ContinuousAddMonoidHom.comp f g

theorem ContinuousAddMonoidHom.compRight.proof_2 (A : Type u_2) {E : Type u_3} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] {B : Type u_1} [AddCommGroup B] [TopologicalSpace B] [TopologicalAddGroup B] (f : ContinuousAddMonoidHom B E) (g : ContinuousAddMonoidHom A B) (h : ContinuousAddMonoidHom A B) : { toFun := fun (g : ContinuousAddMonoidHom A B) => ContinuousAddMonoidHom.comp f g, map_zero' := (_ : (fun (g : ContinuousAddMonoidHom A B) => ContinuousAddMonoidHom.comp f g) 0 = 0) }.toFun (g + h) = { toFun := fun (g : ContinuousAddMonoidHom A B) => ContinuousAddMonoidHom.comp f g, map_zero' := (_ : (fun (g : ContinuousAddMonoidHom A B) => ContinuousAddMonoidHom.comp f g) 0 = 0) }.toFun g + { toFun := fun (g : ContinuousAddMonoidHom A B) => ContinuousAddMonoidHom.comp f g, map_zero' := (_ : (fun (g : ContinuousAddMonoidHom A B) => ContinuousAddMonoidHom.comp f g) 0 = 0) }.toFun h

theorem ContinuousAddMonoidHom.compRight.proof_1 (A : Type u_1) {E : Type u_2} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] {B : Type u_3} [AddCommGroup B] [TopologicalSpace B] [TopologicalAddGroup B] (f : ContinuousAddMonoidHom B E) : (fun (g : ContinuousAddMonoidHom A B) => ContinuousAddMonoidHom.comp f g) 0 = 0

def ContinuousAddMonoidHom.compRight (A : Type u_2) {E : Type u_6} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] {B : Type u_7} [AddCommGroup B] [TopologicalSpace B] [TopologicalAddGroup B] (f : ContinuousAddMonoidHom B E) : ContinuousAddMonoidHom (ContinuousAddMonoidHom A B) (ContinuousAddMonoidHom A E)

ContinuousAddMonoidHom f _ is a functor.

Equations

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

def ContinuousMonoidHom.compRight (A : Type u_2) {E : Type u_6} [Monoid A] [CommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalGroup E] {B : Type u_7} [CommGroup B] [TopologicalSpace B] [TopologicalGroup B] (f : ContinuousMonoidHom B E) : ContinuousMonoidHom (ContinuousMonoidHom A B) (ContinuousMonoidHom A E)

ContinuousMonoidHom f _ is a functor.

Equations

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

def PontryaginDual (A : Type u_2) [Monoid A] [TopologicalSpace A] : Type u_2

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

Equations

• PontryaginDual A = ContinuousMonoidHom A ↥circle

instance instTopologicalSpacePontryaginDual (A : Type u_2) [Monoid A] [TopologicalSpace A] : TopologicalSpace (PontryaginDual A)

Equations

• instTopologicalSpacePontryaginDual A = inferInstance

instance instT2SpacePontryaginDualInstTopologicalSpacePontryaginDual (A : Type u_2) [Monoid A] [TopologicalSpace A] : T2Space (PontryaginDual A)

Equations

• (_ : T2Space (PontryaginDual A)) = (_ : T2Space (ContinuousMonoidHom A ↥circle))

noncomputable instance instCommGroupPontryaginDual (A : Type u_2) [Monoid A] [TopologicalSpace A] : CommGroup (PontryaginDual A)

Equations

• instCommGroupPontryaginDual A = inferInstance

instance instTopologicalGroupPontryaginDualInstTopologicalSpacePontryaginDualToGroupInstCommGroupPontryaginDual (A : Type u_2) [Monoid A] [TopologicalSpace A] : TopologicalGroup (PontryaginDual A)

Equations

• (_ : TopologicalGroup (PontryaginDual A)) = (_ : TopologicalGroup (ContinuousMonoidHom A ↥circle))

noncomputable instance instInhabitedPontryaginDual (A : Type u_2) [Monoid A] [TopologicalSpace A] : Inhabited (PontryaginDual A)

Equations

• instInhabitedPontryaginDual A = inferInstance

instance PontryaginDual.instFunLikePontryaginDualSubtypeComplexMemSubmonoidToMulOneClassToMulZeroOneClassToNonAssocSemiringInstSemiringComplexInstMembershipInstSetLikeSubmonoidCircle {A : Type u_2} [Monoid A] [TopologicalSpace A] : FunLike (PontryaginDual A) A ↥circle

Equations

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

noncomputable instance PontryaginDual.instContinuousMonoidHomClassPontryaginDualSubtypeComplexMemSubmonoidToMulOneClassToMulZeroOneClassToNonAssocSemiringInstSemiringComplexInstMembershipInstSetLikeSubmonoidCircleToMonoidToMonoidToMonoidWithZeroInstTopologicalSpaceSubtypeToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingInstNormedFieldComplexInstFunLikePontryaginDualSubtypeComplexMemSubmonoidToMulOneClassToMulZeroOneClassToNonAssocSemiringInstSemiringComplexInstMembershipInstSetLikeSubmonoidCircle {A : Type u_2} [Monoid A] [TopologicalSpace A] : ContinuousMonoidHomClass (PontryaginDual A) A ↥circle

Equations

• (_ : ContinuousMonoidHomClass (PontryaginDual A) A ↥circle) = (_ : ContinuousMonoidHomClass (ContinuousMonoidHom A ↥circle) A ↥circle)

noncomputable def PontryaginDual.map {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (f : ContinuousMonoidHom A B) : ContinuousMonoidHom (PontryaginDual B) (PontryaginDual A)

PontryaginDual is a functor.

Equations

• PontryaginDual.map f = ContinuousMonoidHom.compLeft (↥circle) f

@[simp]

theorem PontryaginDual.map_apply {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (f : ContinuousMonoidHom A B) (x : PontryaginDual B) (y : A) : ((PontryaginDual.map f) x) y = x (f y)

@[simp]

theorem PontryaginDual.map_one {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : PontryaginDual.map (ContinuousMonoidHom.one A B) = ContinuousMonoidHom.one (PontryaginDual B) (PontryaginDual A)

@[simp]

theorem PontryaginDual.map_comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (g : ContinuousMonoidHom B C) (f : ContinuousMonoidHom A B) : PontryaginDual.map (ContinuousMonoidHom.comp g f) = ContinuousMonoidHom.comp (PontryaginDual.map f) (PontryaginDual.map g)

@[simp]

theorem PontryaginDual.map_mul {A : Type u_2} {E : Type u_6} [Monoid A] [CommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalGroup E] (f : ContinuousMonoidHom A E) (g : ContinuousMonoidHom A E) : PontryaginDual.map (f * g) = PontryaginDual.map f * PontryaginDual.map g

noncomputable def PontryaginDual.mapHom (A : Type u_2) (E : Type u_6) [Monoid A] [CommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalGroup E] [LocallyCompactSpace E] : ContinuousMonoidHom (ContinuousMonoidHom A E) (ContinuousMonoidHom (PontryaginDual E) (PontryaginDual A))

ContinuousMonoidHom.dual as a ContinuousMonoidHom.

Equations

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