English
Under a HasBasis for nhds(1) and a compatible basis V, the space of ContinuousMonoidHom with the compact-open topology is locally compact.
Русский
При наличии базы nhds(1) и совместимой базиса V пространство ContinuousMonoidHom с компактно-открытой топологией локально компактно.
LaTeX
$$$\text{HasBasis}(nhds(1))\,V \Rightarrow \mathrm{LocallyCompactSpace}(\mathrm{ContinuousMonoidHom} X Y).$$$
Lean4
@[to_additive]
theorem locallyCompactSpace_of_hasBasis (V : ℕ → Set Y) (hV : ∀ {n x}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1))
(hVo : Filter.HasBasis (nhds 1) (fun _ ↦ True) V) : LocallyCompactSpace (ContinuousMonoidHom X Y) :=
by
obtain ⟨U0, hU0c, hU0o⟩ := exists_compact_mem_nhds (1 : X)
let U_aux : ℕ → {S : Set X | S ∈ nhds 1} :=
Nat.rec ⟨U0, hU0o⟩ <| fun _ S ↦
let h := exists_closed_nhds_one_inv_eq_mul_subset S.2
⟨Classical.choose h, (Classical.choose_spec h).1⟩
let U : ℕ → Set X := fun n ↦ (U_aux n).1
have hU1 : ∀ n, U n ∈ nhds 1 := fun n ↦ (U_aux n).2
have hU2 : ∀ n, U (n + 1) * U (n + 1) ⊆ U n := fun n ↦
(Classical.choose_spec (exists_closed_nhds_one_inv_eq_mul_subset (U_aux n).2)).2.2.2
have hU3 : ∀ n, U (n + 1) ⊆ U n := fun n x hx ↦ hU2 n (mul_one x ▸ Set.mul_mem_mul hx (mem_of_mem_nhds (hU1 (n + 1))))
have hU4 : ∀ f : X →* Y, Set.MapsTo f (U 0) (V 0) → ∀ n, Set.MapsTo f (U n) (V n) :=
by
intro f hf n
induction n with
| zero => exact hf
| succ n ih => exact fun x hx ↦ hV (ih (hU3 n hx)) (map_mul f x x ▸ ih (hU2 n (Set.mul_mem_mul hx hx)))
apply locallyCompactSpace_of_equicontinuousAt (U 0) (V 0) hU0c (hVo.mem_of_mem trivial)
rw [hVo.uniformity_of_nhds_one.equicontinuousAt_iff_right]
refine fun n _ ↦ Filter.eventually_iff_exists_mem.mpr ⟨U n, hU1 n, fun x hx ⟨f, hf⟩ ↦ ?_⟩
rw [Set.mem_setOf_eq, map_one, div_one]
exact hU4 f hf n hx
