change order on `pfilter`

Stream: maths

[Kevin Buzzard]

When making #14759 (in relation to a student project on filters) I discovered that principal was antitone for pfilter, unlike for filter when it is monotone. The reason is that the order on pfilter is not the "backwards" one which we use on filter. This caused me a bit of pain in #14759; to my surprise

lemma Inf_gc' : galois_connection (principal: P → (pfilter P)ᵒᵈ) (λ (F : (pfilter P)ᵒᵈ), Inf (id F : pfilter P)) :=

is false, because unification for galois_connection seems to ignore the order dual and the incorrect order is inherited.

Should we change the order on pfilter to be the op of the current one?

[Yaël Dillies]

Note that I have a big refactor of pfilter coming up so if we do decide on it I will probably include it in.

[Yaël Dillies]

Also, this change also concerns docs#upper_set and for the record I'm in favor of it.

[Kevin Buzzard]

I'm happy if you want to close #14759, I was basically just making it to teach myself a bit about pfilters.

[Eric Wieser]

Note that the way to prevent unification failing you in your example is to explicitly compose with to_dual as appropriate