Zulip Chat Archive

Stream: new members

Topic: notation for isomorphisms


Alex Meiburg (Oct 12 2021 at 20:38):

I've got a def convert_a_into_b (sa : struct_a M) : struct_b (option M) and a def convert_b_into_a (sb : struct_b M) : struct_a (units M). I want to show that these are meaningfully inverses, so I tried writing something like

def a_b_iso [a_inst : struct_a M]: convert_b_into_a (convert_a_into_b a_inst) ≃ a_inst := begin sorry end

but that doesn't compile, it says that

type mismatch at application equiv (convert_a_into_b inst_a).convert_b_into_a term (convert_a_into_b inst_a).convert_b_into_a has type struct_a (option (units M)) : Type u but is expected to have type Sort ? : Type ?
and
type mismatch at application ⁇ ≃ a_inst term a_inst has type struct_a M : Type u but is expected to have type Sort ? : Type ?

Alex Meiburg (Oct 12 2021 at 20:39):

I tried following a few different examples in mathlib to see how to use def turning one structure into another, but, I couldn't figure it out. Help with the syntax? :upside_down:

Adam Topaz (Oct 12 2021 at 20:43):

#backticks <-- some info about making your posts more readable if they contain code

Adam Topaz (Oct 12 2021 at 20:45):

Also, a #mwe would be helpful

Eric Wieser (Oct 12 2021 at 20:45):

What do you mean by "meaningfully inverses" as opposed to "inverses"?

Alex Meiburg (Oct 12 2021 at 20:51):

Well, that I guess they aren't literally inverses because the types option (units M) and M are different. (I think?) Even though here they'll end up corresponding exactly one-to-one.

Patrick Massot (Oct 12 2021 at 20:51):

equiv a b need a and b to be types.

Alex Meiburg (Oct 12 2021 at 20:51):

I'll make an mwe later today

Yaël Dillies (Oct 12 2021 at 21:03):

You probably rather want to make convert_a_into_b the first field of M ≃ option M (an equivalence is data) and massage convert_b_into_a option M → Mto to make it the second field.

Yaël Dillies (Oct 12 2021 at 21:04):

However I doubt you actually want an equivalence because you only wanted to show that they compose to the identity one way.

Yaël Dillies (Oct 12 2021 at 21:05):

If that's really the case, you can't much more than "They compose to the identity".

anton_shrdlu (Oct 12 2021 at 21:20):

Hi, I am trying to get the quickstart at https://leanprover.github.io/lean4/doc/quickstart.html going.
I ran it with standard options and everything runs fine, but when I check for version lean is still at 3.xx.
Is there some action I need to take first, if I previously installed lean 3?

anton_shrdlu (Oct 12 2021 at 21:21):

I am also new to zulip, so sorry if this is the wrong place for questions like this.

Alex Meiburg (Oct 12 2021 at 21:24):

They compose to the identity both ways, actually, I was planning to show it each way separately. If there's a better notation / code / class for that I'm all ears!

Alex Meiburg (Oct 12 2021 at 21:38):

notably I do not haveM ≃ option M, that would be false, in fact the injection from M into option M isn't even natural. It's only when I go back through units (option M) that it's isomorphic.

For a concrete example, units and with_zero are inverse operations when beginning with a group G or group_with_zero G0. There is an isomorphism between units (with_zero G) and G, as well as between with_zero (units G0) and G0. In that case the isomorphisms are pretty trivial since the with_zero and units instances directly inherit multiplication from the parent G or G0.

In my case, the multiplication operation is not the same, so I was advised that instead of declaring [struct_a M] option M as an instance of struct_b M, I should def the mappings, which I've done in convert_a_into_b and vv. But now I'm not sure how to use those definitions.

How do I write down the equivalence that I'm trying to state?

Alex Meiburg (Oct 13 2021 at 06:04):

I made a MWE. It's not that small, but I think it's pretty quick to read, and it's self-contained... https://gist.github.com/Timeroot/65e4e8a5b7a4216251f425c0e1cd1da1

Help appreciated!

Yakov Pechersky (Oct 13 2021 at 12:27):

Like Patrick said above, equivs or mul_equivs etc are between types, not between terms. While here, you're trying to state an equivalence between structures, which are terms. I would imagine that the type of your equiv could be between option (units S) and units (option S). The term of an equiv type is a structure, comprising two functions and proofs that they are inverses of each other on both sides.

Yakov Pechersky (Oct 13 2021 at 12:28):

Then, if you can define that, you have a bundled function, that is, bundled directly with its inverses and with the proofs of that inverse-fact.

Yakov Pechersky (Oct 13 2021 at 12:29):

My types suggested above won't work btw I don't think.

Yakov Pechersky (Oct 13 2021 at 12:30):

Perhaps in this case it is between add_group S and add_group (units (option S))

Yakov Pechersky (Oct 13 2021 at 12:31):

But that's really talking about the equiv between S and units (option S)

Eric Wieser (Oct 13 2021 at 12:40):

Does just writing = work for your mwe?

Alex Meiburg (Oct 13 2021 at 15:41):

= doesn't work, because one side has type has option S, and the other has type add_group (units (option S)).

Alex Meiburg (Oct 13 2021 at 15:45):

It sounds like equiv / mul_equiv are maybe not the right relation then.

I'm a bit confused because in e.g. all the ring theory stuff, it says R ≃+* S where {R : Type*}{S : Type*} with [ring R] [ring S]. So I guess there, R is the type, and [ring R] is stating there there is an instance of ring structure on R available to use? And I want to explicitly provide the ring structure to use, which is not an "obvious" one

Yaël Dillies (Oct 13 2021 at 16:40):

Another option is to provide the ring structure (or your case, add_group and group?) through instance and then provide the equivalence you want as a group isomorphism (although they mix additive and multiplicative notation, so I don't know how that's supposed to work).

Alex Meiburg (Oct 13 2021 at 17:31):

@Yaël Dillies let's suppose they both used multiplicative notation -- if I put an instance on it, that would be something like instance [group G] : group_with_zero (option G) and instance [group_with_zero G] : group (units G), right?

Wouldn't that make things a little bit 'polluted'? Now any discussion of an option of a group is "also" about a group_with_zero, right?

Alex Meiburg (Oct 13 2021 at 17:31):

Maybe that's okay, I don't know

Yakov Pechersky (Oct 13 2021 at 17:39):

I think units G is a group for any monoid G, by definition. And group_with_zero G implies monoid G.

Yakov Pechersky (Oct 13 2021 at 17:40):

Yes, docs#units.group

Yaël Dillies (Oct 13 2021 at 17:49):

Actually I'm afraid this will lead to typeclass loops.

Yaël Dillies (Oct 13 2021 at 17:49):

because that's precisely the point of what you're doing: to loop.

Alex Meiburg (Oct 13 2021 at 17:49):

Yes, but I'm trying to understand the notation. The actual goal is I would like to write some Lean to show the canonical isomorphism between squags and sloops. :) And while units G can directly inherit the same mul operation from the monoid G, the same is not true between squags and sloops: the isomorphism is "fairly" natural, but using an instance would mean that I now have a * operation that doesn't actually lift! And that would be pretty awful. Hence me trying to make an example here where I'm defining units G to have the opposite multiplication (a*b -> b*a), to suggest the nontriviality of the lift.

Yaël Dillies (Oct 13 2021 at 17:52):

I really don't know how to get around the fact that you're transforming G into option G into units (option G).

Alex Meiburg (Oct 13 2021 at 17:52):

Good news is I figured out how to actually get the type signature I wanted, but manually feeding all the type arguments. Unfortunately, that is so awful that it comes out to a good thirty lines of code. I've added it as a comment on the MWE: https://gist.github.com/Timeroot/65e4e8a5b7a4216251f425c0e1cd1da1

Suggestions for how to make this more legible? For instance, it would be nice if I could name (@@units (option S) (@@monoid_with_zero.to_monoid (option S) (@@group_with_zero.to_monoid_with_zero (option S) (convert_g_into_g₀_op g) ) ) ) as one type and re-use that.

Yaël Dillies (Oct 13 2021 at 17:53):

What about you define the "obvious" equivalences G ≃ units (option G) and G ≃ option (units G) first?

Yaël Dillies (Oct 13 2021 at 17:54):

Alex Meiburg said:

Unfortunately, that is so awful that it comes out to a good thirty lines of code.

Okay, this is what horrendous means :rofl:

Yaël Dillies (Oct 13 2021 at 17:57):

Then you can show that your convert_whatevers compose into one direction of the equivalence.

Yaël Dillies (Oct 13 2021 at 17:58):

I doubt there is anything more Lean-meaningful you can say about it because your begin and end types don't match. Else an group iso would have done the trick.

Yaël Dillies (Oct 13 2021 at 17:59):

Basically, your operations only add complexity, even though they are morally inverses to each other.

Yaël Dillies (Oct 13 2021 at 18:00):

One thing you could try, though, is to define four conversions: the two you already have + the two that you get by making the former two simplifying.

Yaël Dillies (Oct 13 2021 at 18:01):

I mean

  • G → units G
  • G → option G
  • units G → G
  • option G → G

Yaël Dillies (Oct 13 2021 at 18:02):

Of course, for the latter two you'll have to assume that the group structure on units G/option Gis somehow what you would get from the former two. Typically, you must assume none = 0.

Yaël Dillies (Oct 13 2021 at 18:02):

Does that make sense?

Eric Wieser (Oct 13 2021 at 20:05):

Are you aware of docs#with_zero?

Alex Meiburg (Oct 13 2021 at 21:03):

Yes, I am, I was avoiding that because it just gives the definitions one more layer to unfold, and my "minimal" example was already bigger than I preferred

Alex Meiburg (Oct 13 2021 at 21:04):

Yaël Dillies said:

I mean

  • G → units G
  • G → option G
  • units G → G
  • option G → G

This is interesting, what would be the equivalence I actually end up proving then?


Last updated: Dec 20 2023 at 11:08 UTC