Skip to content

Commit

Permalink
refactor(CompactOpen): redefine in terms of Set.image2 and `Set.Map…
Browse files Browse the repository at this point in the history 
…sTo` (#11053)
  • Loading branch information
@urkud @kbuzzard
urkud authored and kbuzzard committed Mar 12, 2024
1 parent 4c3d752 commit b4eac21
Showing 1 changed file with 82 additions and 126 deletions.
208 changes: 82 additions & 126 deletions Mathlib/Topology/CompactOpen.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,61 +43,27 @@ section CompactOpen
variable {α X Y Z : Type*}
variable [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {K : Set X} {U : Set Y}

/-- A generating set for the compact-open topology (when `s` is compact and `u` is open). -/
def CompactOpen.gen (s : Set X) (u : Set Y) : Set C(X, Y) :=
{ f | f '' s ⊆ u }
#align continuous_map.compact_open.gen ContinuousMap.CompactOpen.gen

@[simp]
theorem gen_empty (u : Set Y) : CompactOpen.gen (∅ : Set X) u = Set.univ :=
Set.ext fun f => iff_true_intro ((congr_arg (· ⊆ u) (image_empty f)).mpr u.empty_subset)
#align continuous_map.gen_empty ContinuousMap.gen_empty

@[simp]
theorem gen_univ (s : Set X) : CompactOpen.gen s (Set.univ : Set Y) = Set.univ :=
Set.ext fun f => iff_true_intro (f '' s).subset_univ
#align continuous_map.gen_univ ContinuousMap.gen_univ

@[simp]
theorem gen_inter (s : Set X) (u v : Set Y) :
CompactOpen.gen s (u ∩ v) = CompactOpen.gen s u ∩ CompactOpen.gen s v :=
Set.ext fun _ => subset_inter_iff
#align continuous_map.gen_inter ContinuousMap.gen_inter

@[simp]
theorem gen_union (s t : Set X) (u : Set Y) :
CompactOpen.gen (s ∪ t) u = CompactOpen.gen s u ∩ CompactOpen.gen t u :=
Set.ext fun f => (iff_of_eq (congr_arg (· ⊆ u) (image_union f s t))).trans union_subset_iff
#align continuous_map.gen_union ContinuousMap.gen_union

theorem gen_empty_right {s : Set X} (h : s.Nonempty) : CompactOpen.gen s (∅ : Set Y) = ∅ :=
eq_empty_of_forall_not_mem fun _ => (h.image _).not_subset_empty
#align continuous_map.gen_empty_right ContinuousMap.gen_empty_right

-- The compact-open topology on the space of continuous maps X → Y.
#noalign continuous_map.compact_open.gen
#noalign continuous_map.gen_empty
#noalign continuous_map.gen_univ
#noalign continuous_map.gen_inter
#noalign continuous_map.gen_union
#noalign continuous_map.gen_empty_right

/-- The compact-open topology on the space of continuous maps `C(X, Y)`. -/
instance compactOpen : TopologicalSpace C(X, Y) :=
TopologicalSpace.generateFrom
{ m | ∃ (s : Set X) (_ : IsCompact s) (u : Set Y) (_ : IsOpen u), m = CompactOpen.gen s u }
.generateFrom <| image2 (fun K U ↦ {f | MapsTo f K U}) {K | IsCompact K} {U | IsOpen U}
#align continuous_map.compact_open ContinuousMap.compactOpen

/-- Definition of `ContinuousMap.compactOpen` in terms of `Set.image2`. -/
/-- Definition of `ContinuousMap.compactOpen`. -/
theorem compactOpen_eq : @compactOpen X Y _ _ =
.generateFrom (Set.image2 CompactOpen.gen {s | IsCompact s} {t | IsOpen t}) :=
congr_arg TopologicalSpace.generateFrom <| Set.ext fun _ ↦ by simp [eq_comm]

/-- Definition of `ContinuousMap.compactOpen` in terms of `Set.image2` and `Set.MapsTo`. -/
theorem compactOpen_eq_mapsTo : @compactOpen X Y _ _ =
.generateFrom (Set.image2 (fun K U ↦ {f | MapsTo f K U}) {K | IsCompact K} {U | IsOpen U}) := by
simp only [mapsTo', compactOpen_eq]; rfl

protected theorem isOpen_gen {s : Set X} (hs : IsCompact s) {u : Set Y} (hu : IsOpen u) :
IsOpen (CompactOpen.gen s u) :=
TopologicalSpace.GenerateOpen.basic _ (by dsimp [mem_setOf_eq]; tauto)
#align continuous_map.is_open_gen ContinuousMap.isOpen_gen
.generateFrom (image2 (fun K U ↦ {f | MapsTo f K U}) {K | IsCompact K} {t | IsOpen t}) :=
rfl

lemma isOpen_setOf_mapsTo (hK : IsCompact K) (hU : IsOpen U) :
IsOpen {f : C(X, Y) | MapsTo f K U} := by
rw [compactOpen_eq_mapsTo]; exact .basic _ (mem_image2_of_mem hK hU)
theorem isOpen_setOf_mapsTo (hK : IsCompact K) (hU : IsOpen U) :
IsOpen {f : C(X, Y) | MapsTo f K U} :=
isOpen_generateFrom_of_mem <| mem_image2_of_mem hK hU
#align continuous_map.is_open_gen ContinuousMap.isOpen_setOf_mapsTo

lemma eventually_mapsTo {f : C(X, Y)} (hK : IsCompact K) (hU : IsOpen U) (h : MapsTo f K U) :
∀ᶠ g : C(X, Y) in 𝓝 f, MapsTo g K U :=
Expand All @@ -106,7 +72,7 @@ lemma eventually_mapsTo {f : C(X, Y)} (hK : IsCompact K) (hU : IsOpen U) (h : Ma
lemma nhds_compactOpen (f : C(X, Y)) :
𝓝 f = ⨅ (K : Set X) (_ : IsCompact K) (U : Set Y) (_ : IsOpen U) (_ : MapsTo f K U),
𝓟 {g : C(X, Y) | MapsTo g K U} := by
simp_rw [compactOpen_eq_mapsTo, nhds_generateFrom, mem_setOf_eq, @and_comm (f ∈ _), iInf_and,
simp_rw [compactOpen_eq, nhds_generateFrom, mem_setOf_eq, @and_comm (f ∈ _), iInf_and,
← image_prod, iInf_image, biInf_prod, mem_setOf_eq]

lemma tendsto_nhds_compactOpen {l : Filter α} {f : α → C(Y, Z)} {g : C(Y, Z)} :
Expand All @@ -115,9 +81,8 @@ lemma tendsto_nhds_compactOpen {l : Filter α} {f : α → C(Y, Z)} {g : C(Y, Z)
simp [nhds_compactOpen]

lemma continuous_compactOpen {f : X → C(Y, Z)} :
Continuous f ↔ ∀ K, IsCompact K → ∀ U, IsOpen U → IsOpen {x | MapsTo (f x) K U} := by
simp_rw [compactOpen_eq, continuous_generateFrom_iff, forall_image2_iff, mapsTo',
CompactOpen.gen, image_subset_iff, preimage_setOf_eq, mem_setOf]
Continuous f ↔ ∀ K, IsCompact K → ∀ U, IsOpen U → IsOpen {x | MapsTo (f x) K U} :=
continuous_generateFrom_iff.trans forall_image2_iff

section Functorial

Expand All @@ -130,7 +95,7 @@ theorem continuous_comp (g : C(Y, Z)) : Continuous (ContinuousMap.comp g : C(X,
then the composition `ContinuousMap.comp g : C(X, Y) → C(X, Z)` is a topology inducing map too. -/
theorem inducing_comp (g : C(Y, Z)) (hg : Inducing g) : Inducing (g.comp : C(X, Y) → C(X, Z)) where
induced := by
simp only [compactOpen_eq_mapsTo, induced_generateFrom_eq, image_image2, hg.setOf_isOpen,
simp only [compactOpen_eq, induced_generateFrom_eq, image_image2, hg.setOf_isOpen,
image2_image_right, MapsTo, mem_preimage, preimage_setOf_eq, comp_apply]

/-- If `g : C(Y, Z)` is a topological embedding,
Expand Down Expand Up @@ -260,52 +225,50 @@ theorem compactOpen_le_induced (s : Set X) :
(continuous_restrict s).le_induced
#align continuous_map.compact_open_le_induced ContinuousMap.compactOpen_le_induced

/-- The compact-open topology on `C(X, Y)` is equal to the infimum of the compact-open topologies
on `C(s, Y)` for `s` a compact subset of `X`. The key point of the proof is that the union of the
compact subsets of `X` is equal to the union of compact subsets of the compact subsets of `X`. -/
theorem compactOpen_eq_sInf_induced :
/-- The compact-open topology on `C(X, Y)`
is equal to the infimum of the compact-open topologies on `C(s, Y)` for `s` a compact subset of `X`.
The key point of the proof is that for every compact set `K`,
the universal set `Set.univ : Set K` is a compact set as well. -/
theorem compactOpen_eq_iInf_induced :
(ContinuousMap.compactOpen : TopologicalSpace C(X, Y)) =
⨅ (s : Set X) (_ : IsCompact s),
TopologicalSpace.induced (ContinuousMap.restrict s) ContinuousMap.compactOpen := by
refine' le_antisymm _ _
· refine' le_iInf₂ _
exact fun s _ => compactOpen_le_induced s
simp only [← generateFrom_iUnion, induced_generateFrom_eq, ContinuousMap.compactOpen]
apply TopologicalSpace.generateFrom_anti
rintro _ ⟨s, hs, u, hu, rfl⟩
rw [mem_iUnion₂]
refine' ⟨s, hs, _, ⟨univ, isCompact_iff_isCompact_univ.mp hs, u, hu, rfl⟩, _⟩
ext f
simp only [CompactOpen.gen, mem_setOf_eq, mem_preimage, ContinuousMap.coe_restrict]
rw [image_comp f ((↑) : s → X)]
simp
#align continuous_map.compact_open_eq_Inf_induced ContinuousMap.compactOpen_eq_sInf_induced

theorem nhds_compactOpen_eq_sInf_nhds_induced (f : C(X, Y)) :
⨅ (K : Set X) (_ : IsCompact K), .induced (.restrict K) ContinuousMap.compactOpen := by
refine le_antisymm (le_iInf₂ fun s _ ↦ compactOpen_le_induced s) ?_
refine le_generateFrom <| forall_image2_iff.2 fun K (hK : IsCompact K) U hU ↦ ?_
refine TopologicalSpace.le_def.1 (iInf₂_le K hK) _ ?_
convert isOpen_induced (isOpen_setOf_mapsTo (isCompact_iff_isCompact_univ.1 hK) hU)
simp only [mapsTo_univ_iff, Subtype.forall]
rfl
#align continuous_map.compact_open_eq_Inf_induced ContinuousMap.compactOpen_eq_iInf_induced

@[deprecated] alias compactOpen_eq_sInf_induced := compactOpen_eq_iInf_induced

theorem nhds_compactOpen_eq_iInf_nhds_induced (f : C(X, Y)) :
𝓝 f = ⨅ (s) (hs : IsCompact s), (𝓝 (f.restrict s)).comap (ContinuousMap.restrict s) := by
rw [compactOpen_eq_sInf_induced]
simp [nhds_iInf, nhds_induced]
#align continuous_map.nhds_compact_open_eq_Inf_nhds_induced ContinuousMap.nhds_compactOpen_eq_sInf_nhds_induced
rw [compactOpen_eq_iInf_induced]
simp only [nhds_iInf, nhds_induced]
#align continuous_map.nhds_compact_open_eq_Inf_nhds_induced ContinuousMap.nhds_compactOpen_eq_iInf_nhds_induced

@[deprecated] alias nhds_compactOpen_eq_sInf_nhds_induced := nhds_compactOpen_eq_iInf_nhds_induced

theorem tendsto_compactOpen_restrict {ι : Type*} {l : Filter ι} {F : ι → C(X, Y)} {f : C(X, Y)}
(hFf : Filter.Tendsto F l (𝓝 f)) (s : Set X) :
Filter.Tendsto (fun i => (F i).restrict s) l (𝓝 (f.restrict s)) :=
Tendsto (fun i => (F i).restrict s) l (𝓝 (f.restrict s)) :=
(continuous_restrict s).continuousAt.tendsto.comp hFf
#align continuous_map.tendsto_compact_open_restrict ContinuousMap.tendsto_compactOpen_restrict

theorem tendsto_compactOpen_iff_forall {ι : Type*} {l : Filter ι} (F : ι → C(X, Y)) (f : C(X, Y)) :
Filter.Tendsto F l (𝓝 f) ↔
∀ (s) (hs : IsCompact s), Filter.Tendsto (fun i => (F i).restrict s) l (𝓝 (f.restrict s)) := by
rw [compactOpen_eq_sInf_induced]
simp [nhds_iInf, nhds_induced, Filter.tendsto_comap_iff, Function.comp]
Tendsto F l (𝓝 f) ↔
∀ K, IsCompact K → Tendsto (fun i => (F i).restrict K) l (𝓝 (f.restrict K)) := by
rw [compactOpen_eq_iInf_induced]
simp [nhds_iInf, nhds_induced, Filter.tendsto_comap_iff, Function.comp]
#align continuous_map.tendsto_compact_open_iff_forall ContinuousMap.tendsto_compactOpen_iff_forall

/-- A family `F` of functions in `C(X, Y)` converges in the compact-open topology, if and only if
it converges in the compact-open topology on each compact subset of `X`. -/
theorem exists_tendsto_compactOpen_iff_forall [WeaklyLocallyCompactSpace X] [T2Space Y]
{ι : Type*} {l : Filter ι} [Filter.NeBot l] (F : ι → C(X, Y)) :
(∃ f, Filter.Tendsto F l (𝓝 f)) ↔
∀ (s : Set X) (hs : IsCompact s), ∃ f, Filter.Tendsto (fun i => (F i).restrict s) l (𝓝 f) := by
∀ s : Set X, IsCompact s → ∃ f, Filter.Tendsto (fun i => (F i).restrict s) l (𝓝 f) := by
constructor
· rintro ⟨f, hf⟩ s _
exact ⟨f.restrict s, tendsto_compactOpen_restrict hf s⟩
Expand Down Expand Up @@ -339,68 +302,61 @@ variable (X Y)

/-- The coevaluation map `Y → C(X, Y × X)` sending a point `x : Y` to the continuous function
on `X` sending `y` to `(x, y)`. -/
def coev (y : Y) : C(X, Y × X) :=
{ toFun := Prod.mk y }
@[simps (config := .asFn)]
def coev (b : Y) : C(X, Y × X) :=
{ toFun := Prod.mk b }
#align continuous_map.coev ContinuousMap.coev

variable {X Y}

theorem image_coev {y : Y} (s : Set X) : coev X Y y '' s = ({y} : Set Y) ×ˢ s := by
aesop
theorem image_coev {y : Y} (s : Set X) : coev X Y y '' s = {y} ×ˢ s := by simp
#align continuous_map.image_coev ContinuousMap.image_coev

-- The coevaluation map Y → C(X, Y × X) is continuous (always).
theorem continuous_coev : Continuous (coev X Y) :=
continuous_generateFrom_iff.2 <| by
rintro _ ⟨s, sc, u, uo, rfl⟩
rw [isOpen_iff_forall_mem_open]
intro y hy
have hy' : (↑(coev X Y y) '' s ⊆ u) := hy
-- Porting note: was below
--change coev X Y y '' s ⊆ u at hy
rw [image_coev s] at hy'
rcases generalized_tube_lemma isCompact_singleton sc uo hy' with ⟨v, w, vo, _, yv, sw, vwu⟩
refine' ⟨v, _, vo, singleton_subset_iff.mp yv⟩
intro y' hy'
change coev X Y y' '' s ⊆ u
rw [image_coev s]
exact (prod_mono (singleton_subset_iff.mpr hy') sw).trans vwu
/-- The coevaluation map `Y → C(X, Y × X)` is continuous (always). -/
theorem continuous_coev : Continuous (coev X Y) := by
have : ∀ {a K U}, MapsTo (coev X Y a) K U ↔ {a} ×ˢ K ⊆ U := by simp [mapsTo']
simp only [continuous_iff_continuousAt, ContinuousAt, tendsto_nhds_compactOpen, this]
intro x K hK U hU hKU
rcases generalized_tube_lemma isCompact_singleton hK hU hKU with ⟨V, W, hV, -, hxV, hKW, hVWU⟩
filter_upwards [hV.mem_nhds (hxV rfl)] with a ha
exact (prod_mono (singleton_subset_iff.mpr ha) hKW).trans hVWU
#align continuous_map.continuous_coev ContinuousMap.continuous_coev

end Coev

section Curry

/-- The curried form of a continuous map `α × β → γ` as a continuous map `α → C(β, γ)`.
If `a × β` is locally compact, this is continuous. If `α` and `β` are both locally
compact, then this is a homeomorphism, see `Homeomorph.curry`. -/
def curry (f : C(X × Y, Z)) : C(X, C(Y, Z)) where
toFun a := ⟨Function.curry f a, f.continuous.comp <| by continuity⟩
continuous_toFun := (continuous_comp f).comp continuous_coev
#align continuous_map.curry ContinuousMap.curry

@[simp]
theorem curry_apply (f : C(X × Y, Z)) (a : X) (b : Y) : f.curry a b = f (a, b) :=
rfl
#align continuous_map.curry_apply ContinuousMap.curry_apply

/-- Auxiliary definition, see `ContinuousMap.curry` and `Homeomorph.curry`. -/
def curry' (f : C(X × Y, Z)) (x : X) : C(Y, Z) :=
⟨Function.curry f x, Continuous.comp f.2 (continuous_const.prod_mk continuous_id)⟩
-- Porting note: proof was `by continuity`
@[deprecated ContinuousMap.curry]
def curry' (f : C(X × Y, Z)) (a : X) : C(Y, Z) := curry f a
#align continuous_map.curry' ContinuousMap.curry'

/-- If a map `X × Y → Z` is continuous, then its curried form `X → C(Y, Z)` is continuous. -/
theorem continuous_curry' (f : C(X × Y, Z)) : Continuous (curry' f) :=
Continuous.comp (continuous_comp f) continuous_coev
set_option linter.deprecated false in
/-- If a map `α × β → γ` is continuous, then its curried form `α → C(β, γ)` is continuous. -/
@[deprecated ContinuousMap.curry]
theorem continuous_curry' (f : C(X × Y, Z)) : Continuous (curry' f) := (curry f).continuous
#align continuous_map.continuous_curry' ContinuousMap.continuous_curry'

/-- To show continuity of a map `X → C(Y, Z)`, it suffices to show that its uncurried form
`X × Y → Z` is continuous. -/
/-- To show continuity of a map `α → C(β, γ)`, it suffices to show that its uncurried form
`α × β → γ` is continuous. -/
theorem continuous_of_continuous_uncurry (f : X → C(Y, Z))
(h : Continuous (Function.uncurry fun x y => f x y)) : Continuous f :=
continuous_curry' ⟨_, h⟩
(curry ⟨_, h⟩).2
#align continuous_map.continuous_of_continuous_uncurry ContinuousMap.continuous_of_continuous_uncurry

/-- The curried form of a continuous map `X × Y → Z` as a continuous map `X → C(Y, Z)`.
If `X × Y` is locally compact, this is continuous. If `X` and `Y` are both locally
compact, then this is a homeomorphism, see `Homeomorph.curry`. -/
def curry (f : C(X × Y, Z)) : C(X, C(Y, Z)) :=
⟨_, continuous_curry' f⟩
#align continuous_map.curry ContinuousMap.curry

@[simp]
theorem curry_apply (f : C(X × Y, Z)) (x : X) (y : Y) : f.curry x y = f (x, y) :=
rfl
#align continuous_map.curry_apply ContinuousMap.curry_apply

/-- The currying process is a continuous map between function spaces. -/
theorem continuous_curry [LocallyCompactSpace (X × Y)] :
Continuous (curry : C(X × Y, Z) → C(X, C(Y, Z))) := by
Expand Down

0 comments on commit b4eac21

Please sign in to comment.