Changing the order

Stream: new members

[Antoine Chambert-Loir]

I want to define a Galois connection, but the usual ordering (given by an instance) is the opposite of the one that works… How to have the other one?

[Patrick Massot]

You can use docs#order_dual and a bunch of @

[Patrick Massot]

If there are too many @ it can be worth the trouble of wrapping the offending type in a synonym.

[Johan Commelin]

@Antoine Chambert-Loir is it by chance a docs#galois_coinsertion? Of course I don't know your context.

[Antoine Chambert-Loir]

I don't think so. It is the duality between fixing_submonoid and fixed_points. As in Galois theory, it reverses inclusion (it is antitone) while Galois connections are monotone (see docs#galois_connection.monotone_u and docs#galois_connection.monotone_l).
That means that formulating the result that Galois theory is given by a Galois connection will require some tweeks.

[Kevin Buzzard]

It's like defining contravariant functors though -- do you do the op on the first variable or the second? There is no answer which works well for everything. We need Heather et al's semilinear maps to compose them.

[Kevin Buzzard]

I guess you could make an API for the structure you want by just porting it over directly from the covariant case. What did people do in Galois theory? I'm assuming they proved _something_ was a Galois connection!

[Riccardo Brasca]

Galois insertions and Galois coinsertions are both Galois connections. Maybe we need a Galois coconnection

[Antoine Chambert-Loir]

It's probably simpler to have it contravariant in the first variable (subgroups). But that's OK, I would be fine with saying that my ordered set is that of subgroups with opposite order, except that I can't for the moment.

[Johan Commelin]

docs#is_galois.galois_coinsertion_intermediate_field_subgroup

[Antoine Chambert-Loir]

Cool, that shows how to use it! Thank you! (I was browsing for connectionsthere and did not find that one…)

[Yaël Dillies]

But what is the galois_insertion of galois_coconnection, Riccardo?

[Yaël Dillies]

I'm half joking, because it does come up all the time (look for galois.*dual in VScode).

[Reid Barton]

Wait how do both directions involve to_dual?

[Riccardo Brasca]

I have no idea, I am always confused by insertion/coinsertion :D

[Reid Barton]

I mean both to_dual and of_dual are the identity, so I understand why it typechecks, but I don't understand which two types are supposedly involved in galois_coinsertion_intermediate_field_subgroup

[Kevin Buzzard]

I guess it's because you have maps in both directions that you need two duals. You have two contravariant functors. Oh I see your point! There's some abuse right?

[Reid Barton]

But logically shouldn't it be

  galois_coinsertion
    (⇑order_dual.to_dual ∘ intermediate_field.fixing_subgroup)
    (intermediate_field.fixed_field ∘ ⇑order_dual.of_dual)   -- not to_dual!

[Johan Commelin]

It is abusing order_dual (order_dual X) = X, I guess. But that is idiomatic in the order-theory library.

[Kevin Buzzard]

Reid's version looks better to me. There is no definitional abuse there. It will I suspect make Lean generally happier.

[Yaël Dillies]

Oh indeed that's fishy.

[Riccardo Brasca]

of_dual seems to work, at least in that file

[Riccardo Brasca]

And it is definitely more readable

[Antoine Chambert-Loir]

I wrote this:

example : @galois_connection (set α) (order_dual (submonoid M)) _ (order_dual.preorder (_))
  (λ s : set α, (fixing_submonoid M s))
  (λ P : submonoid M, mul_action.fixed_points P α) := sorry

and

example : galois_connection
  (λ s : set α, order_dual.to_dual (fixing_submonoid M s))
  (λ P : submonoid M, mul_action.fixed_points P α) := sorry

worked, and I could write proofs for both. They are identical except that in the second case, I needed to change p ∈ ⇑order_dual.to_dual (fixing_submonoid M s) to p ∈ fixing_submonoid M s by hand.

[Riccardo Brasca]

(deleted)

[Antoine Chambert-Loir]

And

example : galois_connection
  (λ s : set α, order_dual.to_dual (fixing_submonoid M s))
  (λ P : submonoid M, mul_action.fixed_points (order_dual.of_dual P) α) :=  sorry

follows Reid's convention (with the same proof)

[Antoine Chambert-Loir]

(A seemingly unrelated question: if there are fixing_submonoidlemmas for actions of monoids, should there be fixing_subgrouplemmas as well, for group actions ?
Should their proof be repeated or should one made use of the one for monoids?)

[Riccardo Brasca]

It's better to prove as much as possible for monoid actions (I mean, without doing anything exotic, if the "usual" proof works we're happy, otherwise let's just do it for groups). Then we need that the monoid associated to the subgroup stabilizer is the same as the monoid stabilizer of the action of the underlying monoid.

[Riccardo Brasca]

If at some point you can't deduce a result about the subgroup stabilizer from the corresponding result about the monoid stabilizer it means there is an hole in the API subgroup.to_submonoid.

[Eric Wieser]

This is docs#galois_connection.dual we're talking about, right? nevermind

[Antoine Chambert-Loir]

@Eric Wieser I thought so for a minute, but no : it seems that one reverts both preorders (Galois connections are monotone).
As @Riccardo Brasca said, maybe a galois.coconnectionwould be useful, without theorems, just a reformulation into galois.connection.

[Yaël Dillies]

I've thought about this but couldn't convince myself it was worth the code duplication. And we still need to find a name for the corresponding insertion/coinsertion. Maybe the three could be cogalois_connection, cogalois_insertion, cogalois_coinsertion?

[Riccardo Brasca]

There is PR about subsemigroup. In analysis semigroup actions are important, so we may even want consider a basic API in this generality

[Antoine Chambert-Loir]

@Yaël Dillies , would something like this be useful?

lemma antitone.dual_left_iff : antitone f ↔ monotone (f ∘ of_dual) :=
begin
  split; exact λ hf a b h, hf h
end

For the moment, there's docs#antitone.dual_left that does one direction.
Possibly the other one can be obtained by rewriting, I'm not sure.

[Yaël Dillies]

That shouldn't be necessary, but if we do want it, it should be a simp lemma in the other direction.

[Moritz Doll]

Sorry for being late, but I feel like the answer is do the same as in docs#linear_map.polar_gc (which is the same as Reid Barton's answer)