English
If there is a uniform equicontinuity at 1 for a family of monoid homomorphisms on a pair of spaces with compactness data, then the space of continuous monoid homomorphisms is locally compact.
Русский
Если имеется равномерная эквиконтинуальность в точке 1 для семейства моноидных гомоморфизмов при наличии данных о компактности, то пространство непрерывных моноидных гомоморфизмов локально компактно.
LaTeX
$$$\text{EquicontinuousAt}\; (\cdot)\ 1 \Rightarrow \text{LocallyCompactSpace}(\mathrm{ContinuousMonoidHom}(X,Y)).$$$
Lean4
@[to_additive]
theorem locallyCompactSpace_of_equicontinuousAt (U : Set X) (V : Set Y) (hU : IsCompact U) (hV : V ∈ nhds (1 : Y))
(h : EquicontinuousAt (fun f : {f : X →* Y | Set.MapsTo f U V} ↦ (f : X → Y)) 1) :
LocallyCompactSpace (ContinuousMonoidHom X Y) :=
by
replace h := equicontinuous_of_equicontinuousAt_one _ h
obtain ⟨W, hWo, hWV, hWc⟩ := local_compact_nhds hV
let S1 : Set (X →* Y) := {f | Set.MapsTo f U W}
let S2 : Set (ContinuousMonoidHom X Y) := {f | Set.MapsTo f U W}
let S3 : Set C(X, Y) := (↑) '' S2
let S4 : Set (X → Y) := (↑) '' S3
replace h : Equicontinuous ((↑) : S1 → X → Y) := h.comp (Subtype.map _root_.id fun f hf ↦ hf.mono_right hWV)
have hS4 : S4 = (↑) '' S1 := by
ext
constructor
· rintro ⟨-, ⟨f, hf, rfl⟩, rfl⟩
exact ⟨f, hf, rfl⟩
· rintro ⟨f, hf, rfl⟩
exact ⟨⟨f, h.continuous ⟨f, hf⟩⟩, ⟨⟨f, h.continuous ⟨f, hf⟩⟩, hf, rfl⟩, rfl⟩
replace h : Equicontinuous ((↑) : S3 → X → Y) :=
by
rw [equicontinuous_iff_range, ← Set.image_eq_range] at h ⊢
rwa [← hS4] at h
replace hS4 : S4 = Set.pi U (fun _ ↦ W) ∩ Set.range ((↑) : (X →* Y) → (X → Y)) :=
by
simp_rw [hS4, Set.ext_iff, Set.mem_image, S1, Set.mem_setOf_eq]
exact fun f ↦ ⟨fun ⟨g, hg, hf⟩ ↦ hf ▸ ⟨hg, g, rfl⟩, fun ⟨hg, g, hf⟩ ↦ ⟨g, hf ▸ hg, hf⟩⟩
replace hS4 : IsClosed S4 :=
hS4.symm ▸ (isClosed_set_pi (fun _ _ ↦ hWc.isClosed)).inter (MonoidHom.isClosed_range_coe X Y)
have hS2 : (interior S2).Nonempty :=
by
let T : Set (ContinuousMonoidHom X Y) := {f | Set.MapsTo f U (interior W)}
have h1 : T.Nonempty := ⟨1, fun _ _ ↦ mem_interior_iff_mem_nhds.mpr hWo⟩
have h2 : T ⊆ S2 := fun f hf ↦ hf.mono_right interior_subset
have h3 : IsOpen T := isOpen_induced (ContinuousMap.isOpen_setOf_mapsTo hU isOpen_interior)
exact h1.mono (interior_maximal h2 h3)
exact
TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group
⟨⟨S2,
(isInducing_toContinuousMap X Y).isCompact_iff.mpr
(ArzelaAscoli.isCompact_of_equicontinuous S3 hS4.isCompact h)⟩,
hS2⟩
