Zulip Chat Archive

Stream: maths

Topic: continuous group actions

Bernd Losert (Dec 14 2021 at 14:12):

Is there any theory in mathlib about continuous group actions on topological spaces?

Yaël Dillies (Dec 14 2021 at 14:14):

docs#has_continuous_smul :wink:

Eric Rodriguez (Dec 14 2021 at 14:26):

There's also #10465, adding has_continuous_smul₂

Bernd Losert (Dec 14 2021 at 14:34):

Ah, OK. What about continuous partial actions?

Bernd Losert (Dec 14 2021 at 14:35):

Actually, I don't see anything about partial actions. Speaking of which, how does mathlib deal with partial functions in general?

Bernd Losert (Dec 14 2021 at 14:35):

If I want to define a partial function a -> b, do I define it as a -> option b?

Yakov Pechersky (Dec 14 2021 at 14:38):

Often, mathlib defines partial functions as a total function, sending things outside of the domain to a junk value. One that is often useful for proofs. Otherwise repeated application of the partial function require constant proofs that you're in the range you expect

Yakov Pechersky (Dec 14 2021 at 14:39):

For example, division by 0 is defined in your usual number systems as 0.

Yakov Pechersky (Dec 14 2021 at 14:39):

Or the derivative of nondifferentiable functions is the 0 function (I think)

Bernd Losert (Dec 14 2021 at 14:40):

I see.

Bernd Losert (Dec 14 2021 at 14:41):

Since I'm working abstractly, I won't have junk values available.

Yakov Pechersky (Dec 14 2021 at 14:44):

If you have a group, you always have the unit available for junk

Yury G. Kudryashov (Dec 14 2021 at 14:44):

You'll have junk values when you'll want to apply general results.

Yury G. Kudryashov (Dec 14 2021 at 14:45):

When you formulate them, you assume that you have a total function and it has good properties on some set.

Yury G. Kudryashov (Dec 14 2021 at 14:46):

If you want true partial functions, then have a look at docs#pfun

Bernd Losert (Dec 14 2021 at 14:46):

Ah, didn't know about pfun. Nice.

Bernd Losert (Dec 14 2021 at 14:50):

Yury G. Kudryashov said:

When you formulate them, you assume that you have a total function and it has good properties on some set.

Yeah. This sounds like the way to go.

Bernd Losert (Dec 14 2021 at 14:50):

Thanks.

Yury G. Kudryashov (Dec 14 2021 at 14:59):

We usually work with total functions because you can't, e.g., rewrite on h : a = b in (f : α →. β) a (ha : (f a).dom).

Kevin Buzzard (Dec 14 2021 at 16:25):

Can you simp_rw?

Yury G. Kudryashov (Dec 14 2021 at 18:21):

I'm not sure. For some reasons I don't fully understand, simp only (used by simp_rw) sometimes fails to apply @[congr] lemmas.

Yury G. Kudryashov (Dec 14 2021 at 18:21):

tl;dr: it's easier to try

Last updated: Dec 20 2023 at 11:08 UTC