English
Under equicontinuity, UniformFun.ofFun ∘ F induces the same topology as F in the compact setting.
Русский
При равномерной ограниченности UniformFun.ofFun ∘ F индуктивно задает ту же топологию, что и F, в компактной обстановке.
LaTeX
$$$ [TopologicalSpace ι] [CompactSpace X] (F\_eqcont : Equicontinuous F) : IsInducing (UniformFun.ofFun ∘ F) \leftrightarrow IsInducing F $$$
Lean4
/-- Let `X` be a topological space, `𝔖` a family of compact subsets of `X`, `α` a uniform space,
and `F : ι → (X → α)` a family which is equicontinuous on each `K ∈ 𝔖`. Then, the uniform
structures of uniform convergence on `𝔖` and pointwise convergence on `⋃₀ 𝔖` induce the same
uniform structure on `ι`.
In particular, pointwise convergence and compact convergence coincide on an equicontinuous
subset of `X → α`.
Consider using `EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi'` and
`EquicontinuousOn.inducing_uniformOnFun_iff_pi'` instead to avoid rewriting instances,
as well as their unprimed versions in case `𝔖` covers `X`. -/
theorem comap_uniformOnFun_eq {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K)
(F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) :
(UniformOnFun.uniformSpace X α 𝔖).comap F = (Pi.uniformSpace _).comap ((⋃₀ 𝔖).restrict ∘ F) := by
-- Recall that the uniform structure on `X →ᵤ[𝔖] α` is the one induced by all the maps
-- `K.restrict : (X →ᵤ[𝔖] α) → (K →ᵤ α)` for `K ∈ 𝔖`. Its pullback along `F`, which is
-- the LHS of our goal, is thus the uniform structure induced by the maps
-- `K.restrict ∘ F : ι → (K →ᵤ α)` for `K ∈ 𝔖`.
have H1 :
(UniformOnFun.uniformSpace X α 𝔖).comap F = ⨅ (K ∈ 𝔖), (UniformFun.uniformSpace _ _).comap (K.restrict ∘ F) := by
simp_rw [UniformOnFun.uniformSpace, UniformSpace.comap_iInf, ← UniformSpace.comap_comap, UniformFun.ofFun,
Equiv.coe_fn_mk, UniformOnFun.toFun, UniformOnFun.ofFun, Function.comp_def, UniformFun, Equiv.coe_fn_symm_mk]
-- Now, note that a similar fact is true for the uniform structure on `X → α` induced by
-- the map `(⋃₀ 𝔖).restrict : (X → α) → ((⋃₀ 𝔖) → α)`: it is equal to the one induced by
-- all maps `K.restrict : (X → α) → (K → α)` for `K ∈ 𝔖`, which means that the RHS of our
-- goal is the uniform structure induced by the maps `K.restrict ∘ F : ι → (K → α)` for `K ∈ 𝔖`.
have H2 : (Pi.uniformSpace _).comap ((⋃₀ 𝔖).restrict ∘ F) = ⨅ (K ∈ 𝔖), (Pi.uniformSpace _).comap (K.restrict ∘ F) :=
by
simp_rw [UniformSpace.comap_comap, Pi.uniformSpace_comap_restrict_sUnion (fun _ ↦ α) 𝔖, UniformSpace.comap_iInf]
-- But, for `K ∈ 𝔖` fixed, we know that the uniform structures of `K →ᵤ α` and `K → α`
-- induce, via the equicontinuous family `K.restrict ∘ F`, the same uniform structure on `ι`.
have H3 :
∀ K ∈ 𝔖, (UniformFun.uniformSpace K α).comap (K.restrict ∘ F) = (Pi.uniformSpace _).comap (K.restrict ∘ F) :=
fun K hK ↦ by
have : CompactSpace K := isCompact_iff_compactSpace.mp (𝔖_compact K hK)
exact (equicontinuous_restrict_iff _ |>.mpr <| F_eqcont K hK).comap_uniformFun_eq
simp_rw [H1, H2, iInf_congr fun K ↦ iInf_congr fun hK ↦ H3 K hK]
