-
Notifications
You must be signed in to change notification settings - Fork 256
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: define ProperConstSMul
#6675
Changes from all commits
42c8d83
0725c5a
6b6493f
9c15766
e108562
e8f9c1d
79a2047
74f8ea4
c8c7696
b94e690
444260e
4a04c8b
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,69 @@ | ||
/- | ||
Copyright (c) 2023 Yury Kudryashov. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Yury Kudryashov | ||
-/ | ||
import Mathlib.Topology.Algebra.ConstMulAction | ||
import Mathlib.Topology.ProperMap | ||
/-! | ||
# Actions by proper maps | ||
|
||
In this file we define `ProperConstSMul M X` to be a mixin `Prop`-value class | ||
stating that `(c • ·)` is a proper map for all `c`. | ||
|
||
Note that this is **not** the same as a proper action (not yet in `Mathlib`) | ||
which requires `(c, x) ↦ (c • x, x)` to be a proper map. | ||
|
||
We also provide 4 instances: | ||
- for a continuous action on a compact Hausdorff space, | ||
- and for a continuous group action on a general space; | ||
- for the action on `X × Y`; | ||
- for the action on `∀ i, X i`. | ||
-/ | ||
|
||
/-- A mixin typeclass saying that the `(c +ᵥ ·)` is a proper map for all `c`. | ||
|
||
Note that this is **not** the same as a proper additive action (not yet in `Mathlib`). -/ | ||
class ProperConstVAdd (M X : Type*) [VAdd M X] [TopologicalSpace X] : Prop where | ||
/-- `(c +ᵥ ·)` is a proper map. -/ | ||
isProperMap_vadd (c : M) : IsProperMap ((c +ᵥ ·) : X → X) | ||
|
||
/-- A mixin typeclass saying that `(c • ·)` is a proper map for all `c`. | ||
|
||
Note that this is **not** the same as a proper multiplicative action (not yet in `Mathlib`). -/ | ||
@[to_additive] | ||
class ProperConstSMul (M X : Type*) [SMul M X] [TopologicalSpace X] : Prop where | ||
/-- `(c • ·)` is a proper map. -/ | ||
isProperMap_smul (c : M) : IsProperMap ((c • ·) : X → X) | ||
|
||
/-- `(c • ·)` is a proper map. -/ | ||
@[to_additive "`(c +ᵥ ·)` is a proper map."] | ||
theorem isProperMap_smul {M : Type*} (c : M) (X : Type*) [SMul M X] [TopologicalSpace X] | ||
[h : ProperConstSMul M X] : IsProperMap ((c • ·) : X → X) := h.1 c | ||
|
||
/-- The preimage of a compact set under `(c • ·)` is a compact set. -/ | ||
@[to_additive "The preimage of a compact set under `(c +ᵥ ·)` is a compact set."] | ||
theorem IsCompact.preimage_smul {M X : Type*} [SMul M X] [TopologicalSpace X] | ||
[ProperConstSMul M X] {s : Set X} (hs : IsCompact s) (c : M) : IsCompact ((c • ·) ⁻¹' s) := | ||
(isProperMap_smul c X).isCompact_preimage hs | ||
|
||
@[to_additive] | ||
instance (priority := 100) {M X : Type*} [SMul M X] [TopologicalSpace X] [ContinuousConstSMul M X] | ||
[T2Space X] [CompactSpace X] : ProperConstSMul M X := | ||
⟨fun c ↦ (continuous_const_smul c).isProperMap⟩ | ||
|
||
@[to_additive] | ||
instance (priority := 100) {G X : Type*} [Group G] [MulAction G X] [TopologicalSpace X] | ||
[ContinuousConstSMul G X] : ProperConstSMul G X := | ||
⟨fun c ↦ (Homeomorph.smul c).isProperMap⟩ | ||
|
||
instance {M X Y : Type*} | ||
[SMul M X] [TopologicalSpace X] [ProperConstSMul M X] | ||
[SMul M Y] [TopologicalSpace Y] [ProperConstSMul M Y] : | ||
ProperConstSMul M (X × Y) := | ||
⟨fun c ↦ (isProperMap_smul c X).prod_map (isProperMap_smul c Y)⟩ | ||
|
||
instance {M ι : Type*} {X : ι → Type*} | ||
[∀ i, SMul M (X i)] [∀ i, TopologicalSpace (X i)] [∀ i, ProperConstSMul M (X i)] : | ||
ProperConstSMul M (∀ i, X i) := | ||
⟨fun c ↦ .pi_map fun i ↦ isProperMap_smul c (X i)⟩ |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -1311,6 +1311,10 @@ theorem Bornology.relativelyCompact_eq_inCompact [T2Space α] : | |
Bornology.ext _ _ Filter.coclosedCompact_eq_cocompact | ||
#align bornology.relatively_compact_eq_in_compact Bornology.relativelyCompact_eq_inCompact | ||
|
||
theorem IsCompact.preimage_continuous [CompactSpace α] [T2Space β] {f : α → β} {s : Set β} | ||
(hs : IsCompact s) (hf : Continuous f) : IsCompact (f ⁻¹' s) := | ||
(hs.isClosed.preimage hf).isCompact | ||
Comment on lines
+1314
to
+1316
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. While you're at it, could you link this to the IsProperMap API by showing that any map from a compact space to a Hausdorff space is proper? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. BTW, we have There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I know, I added There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
I wouldn't be surprised if both are useful (or even all 3 if you add There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. In general spaces (and for continuous functions of course), Regarding
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Done. I also added a version of There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Do you think I should use |
||
|
||
/-- If `V : ι → Set α` is a decreasing family of compact sets then any neighborhood of | ||
`⋂ i, V i` contains some `V i`. This is a version of `exists_subset_nhds_of_isCompact'` where we | ||
don't need to assume each `V i` closed because it follows from compactness since `α` is | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could you add the same comment on the multiplicative version?