Stream: maths

Topic: (anti)-monotone

Johan Commelin (Oct 20 2020 at 05:48):

@Damiano Testa needs non-increasing maps: https://github.com/leanprover-community/mathlib/pull/4707/files#diff-7988ec8f11293ebdbc60170c32d15458910725a0f10ee3333b5b60134e745ccaR23

We've talked a lot about this before. I think we should find some definitive solution, and implement it. (Either code, or guidelines on what to do.) Options that I see:

1. Define a predicate for non-increasing maps
2. Use the dual order.
3. Use some rel_hom.

@Yury G. Kudryashov @Mario Carneiro @Aaron Anderson
(I think Aaron did something with (3) recently, but I'm not up to speed with what's there and what works.)

Mario Carneiro (Oct 20 2020 at 05:49):

I would like 2 to at least be usable

Damiano Testa (Oct 20 2020 at 05:50):

I tried 2, but was unable to get Lean to accept that the same type (\N in my case) had two different orders... This is my inability and it can probably be done already, but I do not know how...

Johan Commelin (Oct 20 2020 at 05:51):

@Damiano Testa I think there is a dual_order type synonym. Or maybe it is called order_dual?

Damiano Testa (Oct 20 2020 at 05:51):

I got to the stage where I realized, I think, that order_dual X (or something similar) was simply a type synonym for X but I was not able to give it the opposite order...

Damiano Testa (Oct 20 2020 at 06:09):

src/order/basic.lean

As far as I understand, order_dual X is a type synonym for X. How do I produce an X' that is "X with the dual order"? I believe that this is simply a question of what command to give Lean, since in the cited file dual_le seems to exactly be the mathematical "dual order".

Mario Carneiro (Oct 20 2020 at 06:10):

There should be a to_dual function that is a synonym for the identity function

Mario Carneiro (Oct 20 2020 at 06:11):

Er, wait are you asking how to make a type that is "X with the dual order"? That's order_dual X

Mario Carneiro (Oct 20 2020 at 06:11):

it is a type synonym for X but it's order is the dual order

Damiano Testa (Oct 20 2020 at 06:12):

Ok, maybe this is not literally what I meant. I would like to "use the dual order on X", but Lean keeps using the "usual" order on X, even if I call it order_dual X. Is this clearer?

Mario Carneiro (Oct 20 2020 at 06:13):

If you have a b : order_dual X and write a <= b, that will come out the same as b <= a in the order on X

Damiano Testa (Oct 20 2020 at 06:13):

I will try again: maybe I got confused and Lean was doing the right thing, but I did not have it straight in my mind.

Damiano Testa (Oct 20 2020 at 06:13):

Mario Carneiro said:

If you have a b : order_dual X and write a <= b, that will come out the same as b <= a in the order on X

Ok, this is exactly what I want: I will try again!

Mario Carneiro (Oct 20 2020 at 06:14):

If you have a b : X and write (a : order_dual X) <= b though, it will still come out as a <= b

Mario Carneiro (Oct 20 2020 at 06:14):

which is why it's useful to have an identity function here: if you write @id (order_dual X) a <= @id (order_dual X) b then that comes out as b <= a

Damiano Testa (Oct 20 2020 at 06:16):

Mario Carneiro said:

which is why it's useful to have an identity function here: if you write @id (order_dual X) a <= @id (order_dual X) b then that comes out as b <= a

I believe that this is exactly the command that I was missing!

Mario Carneiro (Oct 20 2020 at 06:17):

Usually we define to_dual : X -> order_dual X := id and then use to_dual instead of that @id application

Mario Carneiro (Oct 20 2020 at 06:17):

but I don't know if that's in the library

Damiano Testa (Oct 20 2020 at 06:17):

I had produced a new type with an order and defined an "order reversing function". Now I should be able to use the order_dual type and this @id (order_dual X)

Damiano Testa (Oct 20 2020 at 06:18):

Mario Carneiro said:

Usually we define to_dual : X -> order_dual X := id and then use to_dual instead of that @id application

I searched for "to_dual" and it was not in the file above.

Mario Carneiro (Oct 20 2020 at 06:18):

Our practices in defining type synonyms have changed over the years

Mario Carneiro (Oct 20 2020 at 06:19):

see for example src#opposite.op

Mario Carneiro (Oct 20 2020 at 06:20):

It's possible to avoid using these identity functions, but you have to assert a lot more type annotations and you get more "leakage" of the instance from X instead of order_dual X

Damiano Testa (Oct 20 2020 at 06:22):

I was not expecting to find a to_dual, since I am not sure yet what to expect with Lean! However, what you mentioned is highly likely to solve my problems!

Damiano Testa (Oct 20 2020 at 06:40):

I seem to have the same problem: I would like the min' to be computed using the dual order, but it seems to be still the old order...

import data.finsupp.basic

def to_dual (α : Type*) [linear_order α] : α -> order_dual α := id

lemma monotone_max'_min' {α : Type*} [decidable_linear_order α] {s : finset α} (hs : s.nonempty) :
max' s hs = (min' (image (to_dual α) s) (nonempty.image hs (to_dual α))) :=
begin
sorry,
end


Johan Commelin (Oct 20 2020 at 06:45):

You probably want

import data.finsupp.basic

open finset

variables {α : Type*}

def to_dual : α → order_dual α := id

def of_dual : order_dual α → α := id

lemma monotone_max'_min' [decidable_linear_order α] {s : finset α} (hs : s.nonempty) :
max' s hs = of_dual (min' (image to_dual s) (nonempty.image hs to_dual)) :=
begin

end


Damiano Testa (Oct 20 2020 at 06:45):

(In case it is helpful, this is my earlier question on the topic:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/monotone.20decreasing.20.60.60.60.E2.84.95.20.E2.86.92.20.E2.84.95.60.60.60)

Johan Commelin (Oct 20 2020 at 06:46):

@Damiano Testa In your example, Lean was looking at the =, and thinking

hmmm, where does this = live? Let's look at the LHS: max' s hs. Ok, that's in \alpha. So then the RHS must also live in \alpha, so I'm going to take that min' in \alpha with the order coming from \alpha.
Aah, I see that the user wrote to_dual, but I'm going to ignore that.

Damiano Testa (Oct 20 2020 at 06:47):

@Johan Commelin thanks for the explanation! I will use your code!

Johan Commelin (Oct 20 2020 at 06:47):

Because I added the of_dual in front of the RHS, Lean will think

Ok, so the RHS has to live in \alpha. That means that the argument to of_dual must live in order_dual \alpha. Let me take the min' in the order dual of \alpha.

Scott Morrison (Oct 20 2020 at 07:06):

Yes, please define, if they don't exist already, explicit to_dual and of_dual functions, and use those. Ideally after defining those you can mark order_dual as [irreducible], which will guard against "accidentally" changing between the type and its order_dual.

Johan Commelin (Oct 20 2020 at 07:07):

This still breaks through a little bit of abstraction. But it is a start.

import data.finsupp.basic

open finset

variables {α : Type*}

def to_dual : α → order_dual α := id

def of_dual : order_dual α → α := id

@[simp] lemma to_dual_of_dual (a : order_dual α) : to_dual (of_dual a) = a := rfl
@[simp] lemma of_dual_to_dual (a : α) : of_dual (to_dual a) = a := rfl

section

lemma to_dual_injective : function.injective (to_dual : α → order_dual α) :=
function.injective_id

@[simp] lemma to_dual_inj {a b : α} :
to_dual a = to_dual b ↔ a = b := iff.rfl

@[simp] lemma to_dual_le_to_dual [has_le α] {a b : α} :
to_dual a ≤ to_dual b ↔ b ≤ a := iff.rfl

@[simp] lemma to_dual_lt_to_dual [has_lt α] {a b : α} :
to_dual a < to_dual b ↔ b < a := iff.rfl

lemma of_dual_injective : function.injective (of_dual : order_dual α → α) :=
function.injective_id

@[simp] lemma of_dual_inj {a b : order_dual α} :
of_dual a = of_dual b ↔ a = b := iff.rfl

@[simp] lemma of_dual_le_of_dual [has_le α] {a b : order_dual α} :
of_dual a ≤ of_dual b ↔ b ≤ a := iff.rfl

@[simp] lemma of_dual_lt_of_dual [has_lt α] {a b : order_dual α} :
of_dual a < of_dual b ↔ b < a := iff.rfl

lemma le_to_dual [has_le α] {a : order_dual α} {b : α} :
a ≤ to_dual b ↔ b ≤ of_dual a := iff.rfl

lemma lt_to_dual [has_lt α] {a : order_dual α} {b : α} :
a < to_dual b ↔ b < of_dual a := iff.rfl

lemma to_dual_le [has_le α] {a : α} {b : order_dual α} :
to_dual a ≤ b ↔ of_dual b ≤ a := iff.rfl

lemma to_dual_lt [has_lt α] {a : α} {b : order_dual α} :
to_dual a < b ↔ of_dual b < a := iff.rfl

end

lemma monotone_max'_min' [decidable_linear_order α] {s : finset α} (hs : s.nonempty) :
max' s hs = of_dual (min' (image to_dual s) (nonempty.image hs to_dual)) :=
begin
apply le_antisymm,
{ apply max'_le,
intros,
rw [← le_to_dual],
apply min'_le,
rw [mem_image],
refine ⟨_, H, rfl⟩ },
{ rw [← to_dual_le],
apply le_min',
intros,
rw [to_dual_le],
apply le_max',
rw mem_image at H,
rcases H with ⟨x, H, rfl⟩,
exact H }
end


Mario Carneiro (Oct 20 2020 at 07:09):

the last proof would be simpler if you prove of_dual (min' x y) = max' (of_dual x) (of_dual y) and variations

Mario Carneiro (Oct 20 2020 at 07:11):

well, I guess that's already what it is

Damiano Testa (Oct 20 2020 at 07:42):

@Johan Commelin
Thank you for spelling everything out for me!

What I needed indeed was the statement that max' and min' are exchanged after going through the order dual! I was going to prove as an exercise the analogous statement about max and min of individual elements, but I had to leave and left all for later!

Yury G. Kudryashov (Oct 20 2020 at 10:48):

@Damiano Testa max and min are defined so that max a b = min (to_dual a) (to_dual b) is a rfl.

Yury G. Kudryashov (Oct 20 2020 at 10:48):

I think that we should rename monotone to mono_incr and define mono_decr.

Yury G. Kudryashov (Oct 20 2020 at 10:49):

mono_decr α β should be defeq mono_incr α (order_dual β)

Yury G. Kudryashov (Oct 20 2020 at 10:49):

def mono_decr f := ∀ {{x y}}, x ≤ y → f y ≤ f x


Yury G. Kudryashov (Oct 20 2020 at 10:50):

Most proofs about mono_decr should be := @(thm_about_mono_incr) _ (order_dual _) _ _ _

Yury G. Kudryashov (Oct 20 2020 at 10:50):

See strict_mono_decr_on for an example.

Kevin Buzzard (Oct 20 2020 at 11:00):

In general mathlib has got a very long way with its philosophy that the nicest structures and ideas are the ones which preserve notation. For example we have a gigantic theory about functions satisfying f(a+b)=f(a)+f(b). On the other hand it seems we have essentially nothing about functions satisfying f(a*b)=f(a)+f(b), because we have noticed that the mathematician's conventions for addition and multiplication often seem to be going on in some kind of consistent and compatible way (surprise surprise) -- but not always (see e.g. additive valuations, which don't exist in mathlib yet). There is some kind of "exponential / log" bridge which takes you from the multiplicative to the additive structure and back, but we don't have a general class of functions with this property, we just have multiplicative.to_add and are expected to build everything upon that.

The argument against adding some kind of +→* notation is that "it won't scale". Fortunately, in the 2000 years since we've known about + and * we've not invented any more fundamental operations which are valid in vast generality, so these things won't have to scale much. The ever-increasing pile of -> and \equiv notation is of course a bit disturbing (and makes mathlib harder to read for mathematicians with no background), but this is perhaps a different question.

I've always thought of this <= v >= thing as being a similar sort of thing. Thus far we have stuck with the order-preserving concept monotone, and because the universe is in some sort of harmony we've been able to get a long way with it. However there is this fundamental fact that if <= is a partial order then so is >=, and furthermore in the kind of MSc level stuff we're doing now we do see this duality showing up; many natural constructions relating algebra and geometry e.g. the contravariant Galois connection between subsets of affine n-space and subsets of polynomial rings (subspace goes to functions vanishing on the subspace; set of functions goes to subset where they all vanish) (edit: perhaps it's also worth mentioning Galois' original Galois connection! An order-reversing one between subsets of a field and subsets of a Galois group, a very natural example of a mono_decr and one which we will be needing very soon in mathlib). Thus far we've been expected to rely on order_dual and do everything by hand, but one wonders whether now it is time to experiment with these classes which don't preserve a notation but instead map it to another notation. I'm definitely for the experiment.

Damiano Testa (Oct 20 2020 at 11:05):

I have read your suggestions, and I am happy with them! I just do not trust my understanding of Lean enough to actually perform such a major revision of monotone. What I needed was really just the proof above. I will try to see @Johan Commelin's solution using order_duals but already the comment about irreducible is very opaque to me...

Kevin Buzzard (Oct 20 2020 at 11:06):

Those of us who don't want these hybrid functions will end up having to ask for the monoid hom exp' : multiplicative(real) -> real because they will be restricted to the classes that we currently have. Similarly if we don't inroduce this then we'll end up with subfields -> order_dual (subgroups) in Galois theory, and perhaps order_dual(subgroups) -> subfields as well (even moving between those two "identical" maps will be a slight pain, and of course we have the same question for the inverses). With this proposal we just get one mono_decr.

Kevin Buzzard (Oct 20 2020 at 11:12):

@Damiano Testa Mathlib is "weird" when it comes to groups. The founders decided to set up the entire theory twice, once with group for group law * and once with add_group with group law +. On the face of it, this sounds like a terrible idea! I think it came out of the way notation is used in typeclasses. But actually it seems to work fine in practice. However it does mean that the concept of an isomorphism between a multiplicative and an additive group is a new concept, different to isomorphisms of multiplicative groups (which we have already). We have sort of been resisting making these bridges and this is what has held up valuations on a DVR (that and the fact that I had to make a whole bunch of vlogs for the new Imperial students, something which has taken me 6 weeks of solid work). I now know what I'm doing (I'm just going to mimic what Rob did for p-adic valuations) but this doesn't mean that that questions go away in general. A lot of stuff is order-reversing once you start doing algebraic geometry. Yury is just suggesting hard coding some special case of a contravariant functor to see if it makes life better -- instead of being a covariant functor to the dual category (or is it from the dual category? Same thing to us, different thing to Lean), it's perhaps time to experiment directly. This stuff has all come up before, and people have just been playing with what to do about it in general.

Damiano Testa (Oct 20 2020 at 11:19):

I am perfectly happy with having commands for monotone_decreasing! Most of the PRs that I put in were to deal with trailing_coefficients which is simply the leading_coefficients for the opposite order!! So I am all in favour of making this a simpler procedure! I just had no idea where to start. Now, I think that I know where to start, but do not feel that I am able to produce code like the one that @Johan Commelin produced as quickly and efficiently...

Kevin Buzzard (Oct 20 2020 at 11:20):

yes, setting up the foundations should perhaps be done by an expert.

Damiano Testa (Oct 20 2020 at 14:05):

Could I suggest making a PR with the code that @Johan Commelin wrote above in a separate file in the order folder, maybe in a file called mon_decr.lean, so that #4707 can then proceed? The lemma there is the only "monotone-decreasing" information that I need...

Johan Commelin (Oct 20 2020 at 14:36):

I think that apart from the min-max lemma, all the stuff that I wrote should be close to the definition of order_dual

Johan Commelin (Oct 20 2020 at 14:36):

The min-max lemma can probably go close to the definition of min' and max'

Damiano Testa (Oct 20 2020 at 15:03):

In case you are interested, I created this PR: #4715. I simply merged @Johan Commelin 's code where it seemed appropriate!

Johan Commelin (Oct 20 2020 at 15:06):

@Damiano Testa I think the monotone_max'_min' should get a different name, though

Johan Commelin (Oct 20 2020 at 15:07):

And we need a different reviewer, because I wrote too much of this PR

Johan Commelin (Oct 20 2020 at 15:07):

Also, I think you don't need the linear order assumption, right?

Johan Commelin (Oct 20 2020 at 15:08):

Under which assumptions are min' and max' defined? I dunno

Damiano Testa (Oct 20 2020 at 15:20):

Johan Commelin said:

Damiano Testa I think the monotone_max'_min' should get a different name, though

max'_eq_dual_min'?

Johan Commelin (Oct 20 2020 at 15:25):

I think that's better

Damiano Testa (Oct 20 2020 at 15:32):

Maybe we can reverse the equality and think of it as a simp lemma?

Damiano Testa (Oct 20 2020 at 15:33):

(and call it dual_min'_eq_max')

Mario Carneiro (Oct 20 2020 at 15:34):

@Kevin Buzzard I agree that antitone functions or whatever we call them are important and on a fairly short list of permutations on the symbols we have available so there isn't too much risk of combinatorial growth, but I would still like to see it grow "organically", waiting until we have a critical mass of theorems about order_dual homs so that we know what's important

Mario Carneiro (Oct 20 2020 at 15:35):

I think the max/min simp lemmas should be of_dual (max a b) = min (of_dual a) (of_dual b) and the four variations on this with min/max swapped and to_dual instead of of_dual

Yury G. Kudryashov (Oct 20 2020 at 15:58):

@Johan Commelin If you carefully define max' and min', then the duality is a rfl.

Johan Commelin (Oct 20 2020 at 16:24):

But then we need to redefine them, I guess?

Yury G. Kudryashov (Oct 20 2020 at 16:36):

Where are they defined? I'm on the phone.

Yury G. Kudryashov (Oct 20 2020 at 16:39):

I've redefined min and max in stdlib to get rfl some time ago

Heather Macbeth (Oct 20 2020 at 16:39):

I would like to flag an analogy: working with anti-monotone functions as monotone functions for the order-dual (defined via a type synonym) on one of the sets, is quite similar to what @Frédéric Dupuis is currently working on in #4379, working with conjugate-linear maps as linear maps for the conjugate-space (defined via a type synonym) of one of the two vector spaces.

Heather Macbeth (Oct 20 2020 at 16:41):

I haven't had time to read this thread and think through whether there are any lessons that can be taken from it for @Frédéric Dupuis ' situation (or vice versa). But I'll try later (or maybe someone more experienced can do so immediately).

Frédéric Dupuis (Oct 20 2020 at 20:51):

To add a bit more details: #4379 basically introduces the dual of a Hilbert space, and we want to show that the map that takes a vector to its dual is semilinear. Since we don't have semilinear maps, we can instead view it as a linear map from the conjugate vector space to the dual, so conjugate vector spaces are also defined there as a type synonym with the right instances.

Frédéric Dupuis (Oct 20 2020 at 21:00):

As for order_dual, my experience with it has been that it's a great way to get one-line proofs, for example see all the lemmas about concave_on in analysis/convex/basic.

Frédéric Dupuis (Oct 20 2020 at 21:02):

But when one has to convert back and forth all the time between a type and its synonym it's quite painful.

Damiano Testa (Nov 20 2020 at 10:49):

Dear All,

I have been struggling to use the new version of monotone, using order_dual and I am ready to give up! I find it incredibly difficult to even understand if max' is using the "natural order" or the order_dual. In proofs, I constantly face goals of the form a=a where a : ℕ and a : order_dual ℕ. Almost never I am able to get Lean to realize that they are the same, since then rw, simp_rw, congr, convert ... all appear to fail.

It would be nice to have orders and their duals to work, but I am unable to understand how. In particular, I no longer know how to prove that nat_degree (reverse f) equals nat_degree f - nat_trailing_degree f.

If someone is willing to give it a try, I would be happy to see this method succeed! Otherwise, I would prefer to go back to the clunky-but-workable strategy of not introducing order_dual and instead using max and min on the same order.

Johan Commelin (Nov 20 2020 at 10:53):

Thanks a lot for trying. And I'm sorry to hear that the experiment failed.

Johan Commelin (Nov 20 2020 at 10:54):

Would you mind posting the file with your experiment?

Damiano Testa (Nov 20 2020 at 10:54):

sure, I will clean up the junk and produce a template to try out!

Merci!

Damiano Testa (Nov 20 2020 at 11:08):

you should be able to find the file here:

The file is quite long, but everything up to line 290 is essentially already in mathlib. My first change has been on line 291, with the introduction of order_dual and to_dual. After that, it has been a lot of pain to make progress. Lemma typ on line 349 is an extracted goal to see if things work out: you can safely ignore it! However, those are the kind of issues that sometimes I was able to overcome, but often stumped me!

Do ask questions: I am more than happy to learn from them!

Damiano Testa (Nov 20 2020 at 11:10):

I suspect that things might be easier if reverse and reflect were also defined using order_dual, but I am not sure that this would really be an improvement: I find it very hard to "switch on and off" order instances in Lean.

Eric Wieser (Nov 20 2020 at 11:11):

I'm confused - isn't to_dual already in mathlib? If so, why do you redefine it in your gist?

Damiano Testa (Nov 20 2020 at 11:12):

It is already in mathlib, but since not all the statements that follow are in mathlib, I included all that I knew was needed in order to produce a working (highly non-minimal) example!

Damiano Testa (Nov 20 2020 at 11:14):

(You will find other definitions and lemmas that are already in mathlib, but if you use this file with its imports, it seems to compile with no problems on my version of lean, up to line 360. In fact, up to 366, but I am not sure that my attempt really leads in a good direction.)

Johan Commelin (Nov 27 2020 at 08:03):

I just found out that we have strict_mono_decr_on in mathlib.
It seems really weird that we have that specific special case, but not mono_decr or strict_mono_decr in general.

Johan Commelin (Nov 27 2020 at 08:03):

I think that we are coming to the conclusion that order_dual is useful, but doesn't scale as a solution.

Johan Commelin (Nov 27 2020 at 08:05):

I'm starting to lean (no pun) towards the position that we should refactor to have separate notions of mono_incr and mono_decr with solid APIs for both of them. (One can be defined using order_dual, in terms of the other. I don't care.)

Damiano Testa (Nov 27 2020 at 08:35):

After a conversation with @Kevin Buzzard in this thread, I think that the suggestion was to prove a bunch of results with a "flabby" order_dual, so as to have a solid API. Eventually, though, making order_dual irreducible (something that I do not understand, so this might be nonsense) should give a workable setup.

To be honest, I am not entirely sure how this would work. For instance, I am very happy to have both min and max defined on ℕ and I would rather not have to switch to order_dual twice to convert a min to a max or vice-versa.

Also, if I have been following the various "galois connection" discussions, I suspect that this might be one, right?

Kevin Buzzard (Nov 27 2020 at 08:38):

Galois connections are all covariant in Lean! So in particular none of the ones I knew about before coming here (subsets of $\mathbb{A}^n$ and subsets of $k[X_1,\ldots,X_n]$, and, erm, Galois theory) are in Lean :-)

Kevin Buzzard (Nov 27 2020 at 08:38):

The ones in Lean right now are things like subsets of a group and subgroups of a group

Damiano Testa (Nov 27 2020 at 08:40):

Ahhhh!!! It had not clicked in me the issue with covariance/contravariance! In my mind, affine schemes "were essentially" in Lean, since there is a lot of commutative algebra!! Now that I had so much trouble getting results about leading coefficients imply results on trailing coefficients, I appreciate better the chasm that still exists!

Damiano Testa (Nov 27 2020 at 08:52):

Now that I am slightly more Lean-versed, I have a question.

When using the same type with different relations, I can see that this might cause confusion and introducing a type-synonym might make things worse: having two types for the natural numbers, one called ℕ and the other called order_dual ℕ is not so useful when you want to talk about max and min simultaneously.

However, when the relations are on "really" different types, like homomorphisms of comm_rings and morphisms of affine schemes, why is it a problem to set up the relations at the beginning, so that they match?

In the specific case of Galois theory, I might even go further and say that in Lean it might therefore be simpler to establish the Galois connection between subgroups and spectra of fields!!

Kevin Buzzard (Nov 27 2020 at 09:00):

Galois connection: that's an interesting idea :-) The issue with contravariant Galois connections is literally that the definition is not there.

Damiano Testa (Nov 27 2020 at 09:00):

Still, I am not sure that I understand this issue with covariance/contravariance too well. (The discussion below is likely a rambling based on a misconception.)

"In set theory", by construction, given any two mathematical objects A and B, they are sets and at least the question "is A a subset of B makes sense. Thus, the proper class of all mathematical objects is a poset (!). This is then abused and moved around identifications, but everyone always has a lingering feeling of what "containment" means, at least in local contexts. For instance, subgroups of Galois group are ordered by inclusion, fields are ordered by inclusion, these two natural orders, clash.

However, "in type theory", the poset structure needs to be provided externally. So, what is the problem with covariance/contravariance, if we get to choose which way the arrows point?

Kevin Buzzard (Nov 27 2020 at 09:02):

The computer scientists are always scared about the way things scale, at least this is my impression. If we define contravariant Galois connections then we have to define contravariant poset maps (a <= b -> f(a) >= f(b)) etc etc, and they say "we can just use order_dual and that's only one function so it scales". But it also makes things more complicated.

Damiano Testa (Nov 27 2020 at 09:03):

Ok, but then whichever one of min or max you define first, already implies the other, right?

Damiano Testa (Nov 27 2020 at 09:03):

(I am trying to undestand the basic principles, I am not trying to be snappy, in case the chat gives a wrong impression!)

Kevin Buzzard (Nov 27 2020 at 09:05):

min and max are still both defined on one type, they didn't go that far :-)

Damiano Testa (Nov 27 2020 at 09:05):

Would it then be the case that there should be an "orderless" bijection between ℕ and order_dual ℕ?

Kevin Buzzard (Nov 27 2020 at 09:06):

Sure, and that map should even have a name. If order_dual is semireducible then people might even use id for that name, but if it's irreducible then it would have an explicit name like to_dual or whatever.

Damiano Testa (Nov 27 2020 at 09:07):

Kevin Buzzard said:

min and max are still both defined on one type, they didn't go that far :-)

To be fair, I think that this is the right choice! But then, I would like to be able to say that a linear function is monotone increasing/decreasing, rather than having to define it from the correctly ordered type so that it is always monotone increasing!

Kevin Buzzard (Nov 27 2020 at 11:29):

I guess some people are defining antimono functions, but we don't have contravariant Galois connections or insertions yet, like we don't have functions from A to B such that $f(xy)=f(x)+f(y)$. People look at definitions like this and are scared that such a definition will lead to some chaos, but I'm not convinced it will. Another example is contravariant functors. You have to decide which category to put the "op" on and there is no canonical answer. Another way of doing it would just to have been to define contravariant_functor to be a map between the categories and write down the axioms rather than opping something. The disadvantage with this approach is that then there's a risk you have to develop the entire functor API again in the contravariant setting. Perhaps a solution to this would be to write a tactic using a @[to_contravariant] tag, but this would be hard work.

Damiano Testa (Nov 27 2020 at 11:39):

It is a little frustrating that the innocent-looking assertion "reverse all the arrows in your category" causes so much trouble in formalization

Damiano Testa (Nov 27 2020 at 11:41):

However, even the consequences for intuition of such a change are huge: no one had realized that commutative rings with 1 are affine schemes, until Grothendieck, I think!

Kevin Buzzard (Nov 27 2020 at 11:41):

Think about it this way. Is a contravariant functor actually equal to (a) a covariant functor $C\to D^{op}$ (b) a covariant functor $C^{op}\to D$ (c) a map $C\to D$ with some properties? All of these are "the same" but in fact none of them are the same. Machinery should be able to cover this up, whether it's a good API or good tactics, but this machinery needs to be made.

Damiano Testa (Nov 27 2020 at 11:44):

I agree: I personally like to have the opposite and place it on the category that I am less familiar with! I can see how this is somewhat difficult to formalize... :grinning:

Joseph Myers (Nov 28 2020 at 02:23):

There's a galois_connection using order_dual in analysis.normed_space.inner_product for orthogonal complements of subspaces. (Immediately followed by a series of lemmas with one-line proofs, so that you don't need to think about two different orders on subspaces at the same time in order to use those properties of orthogonal subspaces.)

Last updated: May 14 2021 at 19:21 UTC