[Merged by Bors] - feat: define ProperConstSMul
#6675
Conversation
urkud
added
awaiting-review
|
I don't like This is really a technical condition that would never be talked about in usual maths (since everyone just talks about group actions) so I think it's best if the name is a bit technical 😅 but I have no good suggestion. By the way, do you have a use case for the |
| theorem IsCompact.preimage_continuous [CompactSpace α] [T2Space β] {f : α → β} {s : Set β} | ||
| (hs : IsCompact s) (hf : Continuous f) : IsCompact (f ⁻¹' s) := | ||
| (hs.isClosed.preimage hf).isCompact |
There was a problem hiding this comment.
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.
BTW, we have IsProperMap and CocompactMap.
There was a problem hiding this comment.
I know, I added IsProperMap recently. I claim that it is the right concept mathematically, so I think we should expand this API rather than that of CocompactMap.
There was a problem hiding this comment.
... right concept mathematically
I wouldn't be surprised if both are useful (or even all 3 if you add isCompact_preimage). BTW, I didn't look closely at the definitions; which one is weaker?
There was a problem hiding this comment.
In general spaces (and for continuous functions of course), IsProperMap -> isCompact_preimage -> CocompactMap . The equivalence between isCompact_preimage and CocompactMap works as soon as the codomain is Hausdorff, and everything is equivalent when the codomain is Hausdorff and locally compact.
Regarding isCompact_preimage vs CocompactMap, I think we can safely redefine CocompactMap in terms of compact preimages, the tendsto definition was a nice trick but I don't think it's mathematically meaningful.
IsProperMap on the other hand is indeed significantly stronger than CocompactMap, so I'm not suggesting removing the latter, but I know that some key results that are usually proved for isCompact_preimage maps only work in locally compact space unless you assume the stronger IsProperMap. I don't have a good example in mathlib of such a theorem about CocompactMap, but we have some in the context of group actions. For example you can remove the locally compactness assumption in t2Space_of_properlyDiscontinuousSMul_of_t2Space if you strengthen the definition of ProperlyDiscontinuousSMul to use IsProperMap.
There was a problem hiding this comment.
Done. I also added a version of isProperMap_iff_ultrafilter for a T₂ codomain.
There was a problem hiding this comment.
Do you think I should use IsProperMap instead of IsCompact s → IsCompact (f ⁻¹' s)? UPD: done.
ADedecker
added
awaiting-author
Yes, |
urkud
added
awaiting-review
|
|
||
| /-- 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`). -/ |
There was a problem hiding this comment.
Could you add the same comment on the multiplicative version?
|
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
|
bors merge |
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
ProperConstSMulProperConstSMul
I need this as a technical assumption in an upcoming PR about continuity of the action of
DomMulAct MonLp.