Zulip Chat Archive

Stream: general

Topic: algebra.pointwise

Floris van Doorn (Jun 27 2020 at 18:42):

@Johan Commelin pointed me to this file: https://github.com/leanprover-community/mathlib/blob/master/src/algebra/pointwise.lean
I didn't know that we had it, probably partly because all the instances are local, which means it's not used that often.

Is there a reason these instances shouldn't be global? Can we add simp lemmas simplifying has_inv.inv '' s and has_inv.inv ⁻¹' s to these operations?

Johan Commelin (Jun 27 2020 at 18:43):

I think it's because sometimes there are other things you can do. Eg, set X is also a boolean algebra...

Floris van Doorn (Jun 27 2020 at 18:45):

Hmm, do you want to use the boolean algebra operations as mul and add? In that case I'm wondering whether my approach was better, just writing s.mul t instead of s * t for pointwise multiplication.

Johan Commelin (Jun 27 2020 at 18:48):

Well, the pointwise file also sets up semimodule instances etc... so you would need to duplicate a lot of api

Johan Commelin (Jun 27 2020 at 18:48):

Maybe all the instances can be global, I don't know. I made them local because I was cautious.

Floris van Doorn (Jun 27 2020 at 19:26):

Does anyone see any issue with making these instances global?

Yury G. Kudryashov (Jun 28 2020 at 05:08):

I propose to change boolean algebras and sets to use ∁ for complement and \ for difference.

Yury G. Kudryashov (Jun 28 2020 at 05:08):

Then use +, -, * for pointwise operations on sets.

Jalex Stark (Jun 28 2020 at 06:20):

I agree with Yury; when writing informal math I'm likely to use pointwise operations on sets without comment, but would be pretty explicit if i were using + and * to mean set operations

Floris van Doorn (Jun 29 2020 at 15:41):

Please vote: for s : set α what should - s mean:
:one: the complement of s
:two: the pointwise negation of s, i.e. {x∣−x∈s}\{x \mid -x \in s\} or {−x∣x∈s}\{-x \mid x \in s\}

Mario Carneiro (Jun 29 2020 at 15:43):

what's the notation for the complement under :two: ?

Gabriel Ebner (Jun 29 2020 at 15:44):

I thought we've already moved away from negation for set complements to C?

Patrick Massot (Jun 29 2020 at 15:44):

Floris is fighting back.

Floris van Doorn (Jun 29 2020 at 15:45):

Wait, when did this happen? (I want option 2)

Mario Carneiro (Jun 29 2020 at 15:46):

Also related is what the notation should be for the complement operation in a boolean algebra

Floris van Doorn (Jun 29 2020 at 15:46):

Currently it's 1: https://github.com/leanprover-community/lean/blob/6830e10f2dd24b23aaa50b2ab93d957f6d8559b5/library/init/data/set.lean#L69

Patrick Massot (Jun 29 2020 at 15:48):

Mario Carneiro said:

what's the notation for the complement under :two: ?

image.png

Patrick Massot (Jun 29 2020 at 15:48):

It's a bit annoying that this discussion is spread over two streams.

Bryan Gin-ge Chen (Jun 29 2020 at 15:49):

See: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/3212.20compl.20notation

Floris van Doorn (Jun 29 2020 at 15:49):

@Mario Carneiro: for sets we already have s.compl. We could do something like a postfix ᶜ (superscript c)

Patrick Massot (Jun 29 2020 at 15:49):

But Mario's question is actually the relevant one. Nobody in his right mind would use -s to denote the complement of s.

Floris van Doorn (Jun 29 2020 at 15:51):

Thanks for the link to #3212. I did not see that PR yet.

Floris van Doorn (Jun 30 2020 at 03:32):

I just saw pointwise_mul_semiring, which has union as "addition", and pointwise multiplication as "multiplication". This instance directly conflicts with having addition mean pointwise addition on sets.

Is this an appropriate place to define foo α := set α and have pointwise_mul_semiring [monoid α] : semiring (foo α)?

Johan Commelin (Jun 30 2020 at 04:23):

Aah, you are right. This is in fact a useful notion, we used it in the perfectoid project. Certainly a type synonym would solve it. But I don't have a good name suggestion at the moment.

Floris van Doorn (Jun 30 2020 at 04:25):

If we would add the type synonym, that would still be annoying to work with, right?
For s : foo \a we still would get f '' s : set \a. Do we have to duplicate set operations and instances? (has_union (foo \a), ...)

Johan Commelin (Jun 30 2020 at 04:33):

Hmm...

Johan Commelin (Jun 30 2020 at 04:33):

I guess this is one reason why I kept all the instances as defs. Just let the user choose locally what they want to do.

Floris van Doorn (Jun 30 2020 at 04:34):

You can still do it with enough type annotations, (f '' s + g ''t : foo \a) or something.

Floris van Doorn (Jun 30 2020 at 04:34):

Do we ever want to use pointwise_add and pointwise_semiring in the same declaration?

Johan Commelin (Jun 30 2020 at 04:39):

I don't know what the future will bring...
But I can't think of such a situation right now.

Kevin Buzzard (Jun 30 2020 at 06:02):

I made the integers as a quotient of nat^2 the other day and with algebra.pi_instances imported it gave nat^2 a 1 which corresponded to (1,1)=0 in Z

Johan Commelin (Jun 30 2020 at 06:05):

That's a different pointwise though

Johan Commelin (Jun 30 2020 at 06:06):

Floris is talking about pointwise addition of subsets of some additive monoid/group

Last updated: Dec 20 2023 at 11:08 UTC