notation for isomorphisms

Stream: new members

[Alex Meiburg]

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]

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]

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

[Adam Topaz]

Also, a #mwe would be helpful

[Eric Wieser]

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

[Alex Meiburg]

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]

equiv a b need a and b to be types.

[Alex Meiburg]

I'll make an mwe later today

[Yaël Dillies]

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]

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]

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

[anton_shrdlu]

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]

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

[Alex Meiburg]

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]

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]

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]

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]

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]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Eric Wieser]

Does just writing = work for your mwe?

[Alex Meiburg]

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

[Alex Meiburg]

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]

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]

@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]

Maybe that's okay, I don't know

[Yakov Pechersky]

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

[Yakov Pechersky]

Yes, docs#units.group

[Yaël Dillies]

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

[Yaël Dillies]

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

[Alex Meiburg]

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]

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]

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]

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

[Yaël Dillies]

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]

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

[Yaël Dillies]

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]

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

[Yaël Dillies]

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]

I mean

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

[Yaël Dillies]

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]

Does that make sense?

[Eric Wieser]

Are you aware of docs#with_zero?

[Alex Meiburg]

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]

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?