filter.has_scalar missing?

Stream: Is there code for X?

[Bernd Losert]

I was surprised that this does not exists yet, given that we have filter.has_mul, filter.has_add and so on. Or maybe it's hidden somewhere where I can't find it? Should I make a PR?

[Bernd Losert]

filter.has_inv also seems to be missing.

[Yury G. Kudryashov]

If you're going to edit this file, then please add missing docstrings as well.

[Yaël Dillies]

I'm filling in similar gaps in file#algebra/pointwise in #12694 if that draws inspiration. I can also just do it if you do not feel like it.

[Bernd Losert]

Yaël Dillies said:

I'm filling in similar gaps in file#algebra/pointwise in #12694 if that draws inspiration. I can also just do it if you do not feel like it.

Pretty please.

[Yaël Dillies]

Preliminatory work in #12789

[Yaël Dillies]

It looks like we can streamline the definitions. Having a think...

[Bernd Losert]

So I see that your PR was merged with a TODO. Are you still working on it? If not, I could make a PR with stuff that I have already regarding smul and inv.

[Yaël Dillies]

Yes I am :)

[Yaël Dillies]

I figured that we could significantly shorten the API by writing constructors in terms of docs#sup_bot_hom.

[Bernd Losert]

Alright, thanks. Can you elaborate on how you plan to use sup_bot_hom?

[Yaël Dillies]

If you have a look at docs#filter.has_mul, you see that the reason the definition works is that (s₁ ∪ s₂) * t = s₁ * t ∪ s₂ * t, s * (t₁ ∪ t₂) = s * t₁ ∪ s * t₂, ∅ * s = ∅, s * ∅ = ∅. Hence you can replace (*) by any f : sup_bot_hom (set α) (sup_bot_hom (set β) (set γ)) and it will just work.

[Bernd Losert]

Interesting. So it should also work in the case of smul since smul is supremum-preserving?

[Yaël Dillies]

Exactly! And neg, and inv (with a unary variant)...

[Bernd Losert]

Great. Looking forward to it.

[Yaël Dillies]

@Bernd Losert, is there anything that you want which is not on branch#more_filter_pointwise? For example, more stuff analogous to file#data/set/pointwise

[Bernd Losert]

Great work! You have a lot of stuff that I need. Here's one I don't see:

lemma set.smul_subset_smul_left [has_scalar M α] {t t' : set M}
  (s : set α) (hsub : t ⊆ t') : t • s ⊆ t' • s

but I guess we can get that one using set.image2_subset_left? Here's another, which actually took me a while to prove:

lemma filter.inv_smul_of_smul [group G] [mul_action G α] {g : filter G} {f f' : filter α}
  (hle : f' ≤ g • f) [hf' : f'.ne_bot] : ((g⁻¹ • f') ⊓ f).ne_bot :=

[Yaël Dillies]

Oh I can add that first one real quick.

[Yaël Dillies]

I am not quite sure the second one should be a lemma. I feel like we could split it down. Also, it weirdly mixes instance and explicit ne_bot arguments.

[Bernd Losert]

Yeah, I guess I am confused about whether ne_bot should be instance arguments or regular arguments since mathlib sometimes does one or the other or both.

[Bernd Losert]

In any case, the second lemma is a very peculiar result that I needed for proving another more interesting result.

[Yaël Dillies]

#13062 for the first half

[Yaël Dillies]

#13170 for the second half

[Bernd Losert]

I was just looking at that. Looks really nice.

[Yaël Dillies]

Glad you like it!

[Adam Topaz]

Can't you use docs#filter.bind for these map constructions?

[Yaël Dillies]

I would be eager to know how, because #13170 was all about adding seminontrivial API.

[Adam Topaz]

Can't you use docs#filter.bind for these map constructions?

[Adam Topaz]

(sorry for the duplication. I'm on mobile with my university's "very good" wifi)

[Yaël Dillies]

Note that we care about definitional equality. My filter.map₂ allows you to get the basically simplest condition.

[Yaël Dillies]

@Bernd Losert, there you have it!

[Bernd Losert]

Awesome. Thank you so much. I will update my code.

[Yaël Dillies]

Sorry it took near a month. mathlib do be like that.

[Bernd Losert]

No worries. I'm having a some trouble using lemmas like filter.mem_inv. The lemma that I was using was this:

lemma filter.mem_inv_iff [has_inv α] {s : set α} {f : filter α} :
  s ∈ f⁻¹ ↔ ∃ t ∈ f, t⁻¹ ⊆ s

What's the easiest way to get this result from filter.mem_inv?

[Yaël Dillies]

You can instantiate t to be s⁻¹.

[Bernd Losert]

Sorry, I don't follow.

[Bernd Losert]

Also, I'm getting this error in one of my proofs:

invalid type ascription, term has type
  (map (uncurry has_scalar.smul) (map has_inv.inv g ×ᶠ ↑k')).ne_bot
but is expected to have type
  (g⁻¹ • ↑k').ne_bot

Are these things not definitionally equal?

[Yaël Dillies]

I mean that the t in ∃ t ∈ f, t⁻¹ ⊆ s can always be taken as s⁻¹.

[Yaël Dillies]

I believe not, because I defined docs#filter.map₂, without referring to docs#filter.map. So defeq breaking isn't that surprising. This should be a lemma about map₂ and uncurry, though, and I can try writing it down if you show me your code.

[Bernd Losert]

I mean that the t in ∃ t ∈ f, t⁻¹ ⊆ s can always be taken as s⁻¹.

Ah, you're right. I will still need to create a lemma for this though. I thought I could get away with a oneliner conversion.

Here's the snippet from the proof:

  set k : filter α := g⁻¹ • ↑k' with hdef,
  haveI : k.ne_bot := filter.ne_bot.map (filter.ne_bot.prod (filter.ne_bot.map hnb has_inv.inv) k'.ne_bot) (uncurry (•))

[Yaël Dillies]

Why not use docs#filter.ne_bot.smul?

[Bernd Losert]

Ah, cool. Let me try it with that.

[Bernd Losert]

Yep, that worked.

[Yaël Dillies]

Sorry, docs#smul_ne_bot_iff

[Yaël Dillies]

Oh misread twice. That cancelled out

[Bernd Losert]

Ah shucks. There are other parts of the code showing the "invalid type ascription" issue. I guess I'll have to rethink some of these proofs.