# Zulip Chat Archive

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

- Define a predicate for non-increasing maps
- Use the dual order.
- 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):

Thanks for the thread!

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

#### Mario Carneiro (Oct 20 2020 at 05:52):

it should already exist

#### 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_dual`

s 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_coefficient`

s 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!

#### Johan Commelin (Nov 20 2020 at 10:56):

Merci!

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

you should be able to find the file here:

https://gist.github.com/adomani/6f82a36069e60b318741bdf8d3bcbf76

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