The compact-open topology on continuous monoid morphisms.

@[instance_reducible]

instance ContinuousMonoidHom.instTopologicalSpace (A : Type u_1) (B : Type u_2) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : TopologicalSpace (A →ₜ* B)

Equations

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

@[instance_reducible]

instance ContinuousAddMonoidHom.instTopologicalSpace (A : Type u_1) (B : Type u_2) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : TopologicalSpace (A →ₜ+ B)

Equations

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

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

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

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

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

instance ContinuousMonoidHom.instContinuousEvalConst (A : Type u_1) (B : Type u_2) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousEvalConst (A →ₜ* B) A B

instance ContinuousAddMonoidHom.instContinuousEvalConst (A : Type u_1) (B : Type u_2) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] : ContinuousEvalConst (A →ₜ+ B) A B

instance ContinuousMonoidHom.instContinuousEval (A : Type u_1) (B : Type u_2) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [LocallyCompactPair A B] : ContinuousEval (A →ₜ* B) A B

instance ContinuousAddMonoidHom.instContinuousEval (A : Type u_1) (B : Type u_2) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] [LocallyCompactPair A B] : ContinuousEval (A →ₜ+ B) A B

theorem ContinuousMonoidHom.range_toContinuousMap (A : Type u_1) (B : Type u_2) [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_1) (B : Type u_2) [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_1) (B : Type u_2) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [ContinuousMul B] [T2Space B] : Topology.IsClosedEmbedding toContinuousMap

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

instance ContinuousMonoidHom.instT2Space {A : Type u_1} {B : Type u_2} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [T2Space B] : T2Space (A →ₜ* B)

instance ContinuousAddMonoidHom.instT2Space {A : Type u_1} {B : Type u_2} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] [T2Space B] : T2Space (A →ₜ+ B)

instance ContinuousMonoidHom.instIsTopologicalGroup {A : Type u_1} {E : Type u_4} [Monoid A] [CommGroup E] [TopologicalSpace A] [TopologicalSpace E] [IsTopologicalGroup E] : IsTopologicalGroup (A →ₜ* E)

instance ContinuousAddMonoidHom.instIsTopologicalAddGroup {A : Type u_1} {E : Type u_4} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [IsTopologicalAddGroup E] : IsTopologicalAddGroup (A →ₜ+ E)

theorem ContinuousMonoidHom.continuous_of_continuous_uncurry {B : Type u_2} {C : Type u_3} [Monoid B] [Monoid C] [TopologicalSpace B] [TopologicalSpace C] {A : Type u_5} [TopologicalSpace A] (f : A → 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_2} {C : Type u_3} [AddMonoid B] [AddMonoid C] [TopologicalSpace B] [TopologicalSpace C] {A : Type u_5} [TopologicalSpace A] (f : A → B →ₜ+ C) (h : Continuous (Function.uncurry fun (x : A) (y : B) => (f x) y)) : Continuous f

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

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

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

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

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

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

def ContinuousMonoidHom.compLeft {A : Type u_1} {B : Type u_2} (E : Type u_4) [Monoid A] [Monoid B] [CommGroup E] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace E] [IsTopologicalGroup E] (f : A →ₜ* B) : (B →ₜ* E) →ₜ* A →ₜ* E

ContinuousMonoidHom _ f is a functor.

Equations

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

def ContinuousAddMonoidHom.compLeft {A : Type u_1} {B : Type u_2} (E : Type u_4) [AddMonoid A] [AddMonoid B] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace E] [IsTopologicalAddGroup E] (f : A →ₜ+ B) : (B →ₜ+ E) →ₜ+ A →ₜ+ E

ContinuousAddMonoidHom _ f is a functor.

Equations

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

def ContinuousMonoidHom.compRight (A : Type u_1) {E : Type u_4} [Monoid A] [CommGroup E] [TopologicalSpace A] [TopologicalSpace E] [IsTopologicalGroup E] {B : Type u_5} [CommGroup B] [TopologicalSpace B] [IsTopologicalGroup B] (f : B →ₜ* E) : (A →ₜ* B) →ₜ* A →ₜ* E

ContinuousMonoidHom f _ is a functor.

Equations

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

def ContinuousAddMonoidHom.compRight (A : Type u_1) {E : Type u_4} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [IsTopologicalAddGroup E] {B : Type u_5} [AddCommGroup B] [TopologicalSpace B] [IsTopologicalAddGroup B] (f : B →ₜ+ E) : (A →ₜ+ B) →ₜ+ A →ₜ+ E

ContinuousAddMonoidHom f _ is a functor.

Equations

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

theorem ContinuousMonoidHom.isClosedEmbedding_coe {A : Type u_1} {B : Type u_2} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [DiscreteTopology A] [ContinuousMul B] [T2Space B] : Topology.IsClosedEmbedding DFunLike.coe

theorem ContinuousAddMonoidHom.isClosedEmbedding_coe {A : Type u_1} {B : Type u_2} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] [DiscreteTopology A] [ContinuousAdd B] [T2Space B] : Topology.IsClosedEmbedding DFunLike.coe

instance ContinuousMonoidHom.instCompactSpace {A : Type u_1} {B : Type u_2} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [DiscreteTopology A] [ContinuousMul B] [T2Space B] [CompactSpace B] : CompactSpace (A →ₜ* B)

instance ContinuousAddMonoidHom.instCompactSpace {A : Type u_1} {B : Type u_2} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] [DiscreteTopology A] [ContinuousAdd B] [T2Space B] [CompactSpace B] : CompactSpace (A →ₜ+ B)

theorem ContinuousMonoidHom.locallyCompactSpace_of_equicontinuousAt {X : Type u_5} {Y : Type u_6} [TopologicalSpace X] [Group X] [IsTopologicalGroup X] [UniformSpace Y] [CommGroup Y] [IsUniformGroup 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 (X →ₜ* Y)

theorem ContinuousAddMonoidHom.locallyCompactSpace_of_equicontinuousAt {X : Type u_5} {Y : Type u_6} [TopologicalSpace X] [AddGroup X] [IsTopologicalAddGroup X] [UniformSpace Y] [AddCommGroup Y] [IsUniformAddGroup 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 (X →ₜ+ Y)

theorem ContinuousMonoidHom.locallyCompactSpace_of_hasBasis {X : Type u_5} {Y : Type u_6} [TopologicalSpace X] [Group X] [IsTopologicalGroup X] [UniformSpace Y] [CommGroup Y] [IsUniformGroup 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 (X →ₜ* Y)

theorem ContinuousAddMonoidHom.locallyCompactSpace_of_hasBasis {X : Type u_5} {Y : Type u_6} [TopologicalSpace X] [AddGroup X] [IsTopologicalAddGroup X] [UniformSpace Y] [AddCommGroup Y] [IsUniformAddGroup 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 (X →ₜ+ Y)