The compact-open topology on continuous monoid morphisms.

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

Equations

• ContinuousMonoidHom.instTopologicalSpace A B = TopologicalSpace.induced ContinuousMonoidHom.toContinuousMap ContinuousMap.compactOpen

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

Equations

• ContinuousAddMonoidHom.instTopologicalSpace A B = TopologicalSpace.induced ContinuousAddMonoidHom.toContinuousMap ContinuousMap.compactOpen

theorem ContinuousMonoidHom.isInducing_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : Topology.IsInducing toContinuousMap

theorem ContinuousAddMonoidHom.isInducing_toContinuousMap (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : Topology.IsInducing toContinuousMap

@[deprecated ContinuousMonoidHom.isInducing_toContinuousMap (since := "2024-10-28")]

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

Alias of ContinuousMonoidHom.isInducing_toContinuousMap.

theorem ContinuousMonoidHom.isEmbedding_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : Topology.IsEmbedding toContinuousMap

theorem ContinuousAddMonoidHom.isEmbedding_toContinuousMap (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : Topology.IsEmbedding toContinuousMap

@[deprecated ContinuousMonoidHom.isEmbedding_toContinuousMap (since := "2024-10-26")]

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

Alias of ContinuousMonoidHom.isEmbedding_toContinuousMap.

instance ContinuousMonoidHom.instContinuousEvalConst (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousEvalConst (ContinuousMonoidHom A B) A B

instance ContinuousAddMonoidHom.instContinuousEvalConst (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousEvalConst (ContinuousAddMonoidHom A B) A B

instance ContinuousMonoidHom.instContinuousEval (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [LocallyCompactPair A B] : ContinuousEval (ContinuousMonoidHom A B) A B

instance ContinuousAddMonoidHom.instContinuousEval (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] [LocallyCompactPair A B] : ContinuousEval (ContinuousAddMonoidHom A B) A B

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

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

theorem ContinuousMonoidHom.isClosedEmbedding_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [ContinuousMul B] [T2Space B] : Topology.IsClosedEmbedding toContinuousMap

theorem ContinuousAddMonoidHom.isClosedEmbedding_toContinuousMap (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] [ContinuousAdd B] [T2Space B] : Topology.IsClosedEmbedding toContinuousMap

@[deprecated ContinuousMonoidHom.isClosedEmbedding_toContinuousMap (since := "2024-10-20")]

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

Alias of ContinuousMonoidHom.isClosedEmbedding_toContinuousMap.

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

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

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

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

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_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_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) => f.2.comp f.1

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) => f.2.comp f.1

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) => g.comp f

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) => g.comp f

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) => f.comp g

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) => f.comp g

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] [IsTopologicalGroup E] (f : ContinuousMonoidHom A B) : ContinuousMonoidHom (ContinuousMonoidHom B E) (ContinuousMonoidHom A E)

ContinuousMonoidHom _ f is a functor.

Equations

• ContinuousMonoidHom.compLeft E f = { toFun := fun (g : ContinuousMonoidHom B E) => g.comp f, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }

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] [IsTopologicalAddGroup E] (f : ContinuousAddMonoidHom A B) : ContinuousAddMonoidHom (ContinuousAddMonoidHom B E) (ContinuousAddMonoidHom A E)

ContinuousAddMonoidHom _ f is a functor.

Equations

• ContinuousAddMonoidHom.compLeft E f = { toFun := fun (g : ContinuousAddMonoidHom B E) => g.comp f, map_zero' := ⋯, map_add' := ⋯, continuous_toFun := ⋯ }

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

ContinuousMonoidHom f _ is a functor.

Equations

• ContinuousMonoidHom.compRight A f = { toFun := fun (g : ContinuousMonoidHom A B) => f.comp g, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }

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

ContinuousAddMonoidHom f _ is a functor.

Equations

• ContinuousAddMonoidHom.compRight A f = { toFun := fun (g : ContinuousAddMonoidHom A B) => f.comp g, map_zero' := ⋯, map_add' := ⋯, continuous_toFun := ⋯ }

theorem ContinuousMonoidHom.locallyCompactSpace_of_equicontinuousAt {X : Type u_7} {Y : Type u_8} [TopologicalSpace X] [Group X] [IsTopologicalGroup X] [UniformSpace Y] [CommGroup Y] [UniformGroup Y] [T0Space Y] [CompactSpace Y] (U : Set X) (V : Set Y) (hU : IsCompact U) (hV : V ∈ nhds 1) (h : EquicontinuousAt (fun (f : ↑{f : X →* Y | Set.MapsTo (⇑f) U V}) => ⇑↑f) 1) : LocallyCompactSpace (ContinuousMonoidHom X Y)

theorem ContinuousAddMonoidHom.locallyCompactSpace_of_equicontinuousAt {X : Type u_7} {Y : Type u_8} [TopologicalSpace X] [AddGroup X] [IsTopologicalAddGroup X] [UniformSpace Y] [AddCommGroup Y] [UniformAddGroup Y] [T0Space Y] [CompactSpace Y] (U : Set X) (V : Set Y) (hU : IsCompact U) (hV : V ∈ nhds 0) (h : EquicontinuousAt (fun (f : ↑{f : X →+ Y | Set.MapsTo (⇑f) U V}) => ⇑↑f) 0) : LocallyCompactSpace (ContinuousAddMonoidHom X Y)

theorem ContinuousMonoidHom.locallyCompactSpace_of_hasBasis {X : Type u_7} {Y : Type u_8} [TopologicalSpace X] [Group X] [IsTopologicalGroup X] [UniformSpace Y] [CommGroup Y] [UniformGroup Y] [T0Space Y] [CompactSpace Y] [LocallyCompactSpace X] (V : ℕ → Set Y) (hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)) (hVo : (nhds 1).HasBasis (fun (x : ℕ) => True) V) : LocallyCompactSpace (ContinuousMonoidHom X Y)

theorem ContinuousAddMonoidHom.locallyCompactSpace_of_hasBasis {X : Type u_7} {Y : Type u_8} [TopologicalSpace X] [AddGroup X] [IsTopologicalAddGroup X] [UniformSpace Y] [AddCommGroup Y] [UniformAddGroup Y] [T0Space Y] [CompactSpace Y] [LocallyCompactSpace X] (V : ℕ → Set Y) (hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x + x ∈ V n → x ∈ V (n + 1)) (hVo : (nhds 0).HasBasis (fun (x : ℕ) => True) V) : LocallyCompactSpace (ContinuousAddMonoidHom X Y)