## 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 \mid -x \in s\}$ or $\{-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

#### 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.

#### 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), ...)

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