additive group homs

Stream: maths

[Johan Commelin]

This has come up before. I need additive group homs. I can duplicate Patrick's work on group homs, but I also saw @[to_additive finsupp.sum_map_range_index] in data/finsupp.lean. Can someone explain to me how that magic works? Would it be enough to sprinkle some @[to_additive ...]'s into algebra/group.lean to have everything work?

[Kevin Buzzard]

There are additive group homs in the scheme stuff

[Kevin Buzzard]

Kenny wrote them

[Kevin Buzzard]

you could cut and paste for some basic stuff

[Kevin Buzzard]

if you just want a solution

[Johan Commelin]

Sure, but I'm also interested in the long-term approach

[Kevin Buzzard]

lines 47 onwards at https://github.com/kbuzzard/lean-stacks-project/blob/master/src/canonical_isomorphism_nonsense.lean

[Kevin Buzzard]

already there is a little magic going on

[Andrew Ashworth]

the long term approach would be to learn a bit about tactics and understand how to_additive works, which is for automatically moving theorems from multiplicative groups to additive groups... unfortunately, learning tactics in Lean is a bit of a chore right now since Programming in Lean is unfinished

[Andrew Ashworth]

well, actually, now that I'm looking at algebra/group.lean, you don't need to know much about tactics to understand what's going on there

[Johan Commelin]

But then... I know next to nothing...

[Andrew Ashworth]

hmm, have you worked through TPIL by chance?

[Andrew Ashworth]

The first eleven chapters of Software Foundations is in Coq, but also quite good

[Andrew Ashworth]

I am the kind of person who learns by grabbing a textbook and doing the exercises...

[Johan Commelin]

Yes, maybe I should do that as well... but trying to define singular homology seems like a lot more fun...

[Johan Commelin]

I am the kind of person who learns by cargo cult hacking

[Andrew Ashworth]

this is also valid, but unfortunately if you get stuck there is no solutions manual available to unstuck you, whereas such a thing exists for Software Foundations... the solutions manual known as Mario is asleep right now

[Johannes Hölzl]

the magic of to_additive is a search and replace of all to_additive constants in the definition of the constant. Afterwards the additive, multiplicative constant pair is added to the to_additive database. By using attribute [to_additive a_c] m_c you add a new relation. The requirement is that the additive constants are an exact mirror of the multiplicative ones.

[Johan Commelin]

So, if I understand you correctly, it shouldn't be too complicated to sprinkle @to_additive in algebra/group.lean. Is that right?

[Johan Commelin]

Ok, so here is something that I am a bit worried about: in mathematics the notion of an "additive" group is really just notation (though pretty useful!). In Lean we have "groups" and "additive groups" and now we have is_group_hom and is_add_group_hom. But we also need mixed homomorphisms (from a multiplicative group to an additive group, and vice versa). For example, exp and log are such mixed homomorphisms. So all of a sudden, we have 4 notions of group homomorphisms. And now we want to compose these guys. So we need 8 composition lemmas. And I proved the 5 lemma some time ago: it has 10 groups in its statements. But any of those can be an "additive" group (and this occurs in nature!). Does that mean we need 1024 statements of the Five Lemma?

[Mario Carneiro]

Use multiplicative to do these kind of things

[Johan Commelin]

But, doesn't that mean we should use multiplicative all the time?

[Mario Carneiro]

The additive / multiplicative group thing has a long history, and we are still debating the best way to do it

[Johan Commelin]

Ok, I see. I can understand that it might be delicate to pick the correct approach

[Mario Carneiro]

multiplicative is useful for post hoc fitting a multiplicative theorem in an additive or mixed-additive use case

[Johan Commelin]

I feel like I would rather just remove add_group entirely. But I don't see through all the ramifications

[Mario Carneiro]

to_additive is useful for preparing theorems up front with new names and statements

[Mario Carneiro]

It's very confusing to apply mul_one when you want to simplify x + 0 = x

[Johan Commelin]

Yes, but I think that that to_additive magic will replace all occurences of mul with add

[Mario Carneiro]

yes, that's the idea

[Johan Commelin]

Or can you also use it to create mixed statements?

[Mario Carneiro]

it's not very smart, it usually fails on mixed statements

[Mario Carneiro]

like gpow, which has an interplay between the additive semiring N and the group in question

[Mario Carneiro]

those translations had to be done manually, and in that case usually multiplicative is easier

[Johan Commelin]

So, if we didn't have all the "multiplicative" connotations with our groups... but just op_neu instead of mul_one. Would that be helpful?

[Mario Carneiro]

Jeremy likes this idea. I think it's the worst of both worlds

[Johan Commelin]

If you could somehow have some magic that infers whether you use * or + notation, I feel like it would give a very nice fusion.

[Mario Carneiro]

(Jeremy Avigad has been testing out a bunch of solutions in this space the past few months)

[Johan Commelin]

But why do you think it is worse?

[Mario Carneiro]

It's less mnemonic than either add_zero or mul_one

[Mario Carneiro]

some of that magic goes beyond what lean will currently do on its own

[Johan Commelin]

Yes, but having a lot of gsmul sprinkled through your goal is also not very helpful

[Mario Carneiro]

but then it gets into extending lean, which gets messy

[Mario Carneiro]

What do you mean?

[Johan Commelin]

Well, I was playing around with multiplicative a bit. And I think it gave me those gsmul's

[Johan Commelin]

But maybe I just used it wrong

[Johan Commelin]

I think I will just wait to see what you and Jeremy work out.

[Mario Carneiro]

What are you trying to do exactly?

[Johan Commelin]

If I understand you correctly, you say that a class is_add_group_hom is fine. But we shouldn't have classes for mixed homomorphisms. If one of those pops up, just turn it into an is_group_homwith multiplicative. Is that correct?

[Mario Carneiro]

yes

[Johan Commelin]

Because if we also have classes for the mixed homomorphisms, then you do need 8 composition rules. And I feel like you run head first into some cambrian explosion.

[Mario Carneiro]

we don't

[Johan Commelin]

So, shouldn't I just get rid of is_add_group_hom as well? And just use multiplicative immediately?

[Mario Carneiro]

I should hope there isn't too much theory on is_add_group_hom

[Mario Carneiro]

seeing as it can usually be rephrased in terms of is_group_hom

[Johan Commelin]

But still, I don't see why you draw the line there...

[Mario Carneiro]

two is manageable, 2^n isn't?

[Johan Commelin]

Anyway, what I am trying to do, is to prove that the boundary operator on the simplicial complex satisfies d \circ d = 0

[Johan Commelin]

Yes, but one is even more manageable... (-;

[Mario Carneiro]

so use is_group_hom and call it a day

[Johan Commelin]

And this complex consists of an additive group for each n : nat. And an additive hom between succesive groups.

[Mario Carneiro]

what makes them additive?

[Johan Commelin]

Those groups are all finsupp (X n) int

[Johan Commelin]

where X n is a Type; depending on n (duh)

[Mario Carneiro]

okay, so where is the mixed group hom?

[Johan Commelin]

And the homomorphisms between them are somehow a bit involved... You take an alternating sum of (n+1) maps from X (n+1) to X n, and those induce maps between those additive groups.

[Johan Commelin]

Aah, there is no mixed group hom in this picture yet.

[Johan Commelin]

But I was thinking about other stuff in maths, where they do pop up.

[Johan Commelin]

In all sorts of exponential sequences

[Mario Carneiro]

So you can use is_group_hom + multiplicative to define is_add_group_hom, and then most of the theorems will defeq carry over (although they may need to be restated)

[Johan Commelin]

Ok, but I think I will try to just use multiplicative directly.

[Johan Commelin]

So instead of proving is_add_group_hom d I prove @is_group_hom (multiplicate _) (multiplicative _) d

[Johan Commelin]

Or something like that.

[Mario Carneiro]

they should be the same, but yes unfold if necessary

[Johan Commelin]

Ok, thanks for this discussion! I learned something (-;

[Johan Commelin]

Ooh, and if I locally make every instance of add_group into an instance of group, I think I run into the same trouble with ugly notation and names, right?

[Mario Carneiro]

Oh don't do that

[Mario Carneiro]

that's a recipe for disaster because the notations get all mixed up

[Johan Commelin]

ok

[Mario Carneiro]

next you know it you write 1 + 1 : nat and get 0 :/

[Johan Commelin]

got it

[Johan Commelin]

Ok, so here is another ignorant question:
The reason we have infix notation * for every group is because they are instances of has_mul, right?

[Johan Commelin]

So what if we made abstract groups, with op and neu etc...

[Johan Commelin]

And we don't have infix notation for those

[Johan Commelin]

And then we have concrete groups (like the units in rat, or int) and we make those instances of has_mul resp. has_add

[Johan Commelin]

Then we still have our beloved infix notation.

[Johan Commelin]

And then we can have some to_multiplicate resp. to_additive magic, that will turn op_neu into mul_one resp. add_zero

[Johan Commelin]

So the proofs remain readable and intuitive

[Johan Commelin]

If you want to prove something about an abstract group, and you would like to use infix * notation, then inside the proof you can make the group into an instance of has_mul (I hope) and voila, you have your *. But the statement that you proved is all of a sudden also valid in the context of additive notation.

[Johan Commelin]

Does this idea make any sense at all?

[Mario Carneiro]

If you use has_mul then it gets involved in the statements of the theorems you prove, so there is some unfolding to apply it in a given context

[Johan Commelin]

Well, I hope to keep it out of the statements.

[Mario Carneiro]

then you can't use notation with abstract group theory

[Mario Carneiro]

which is a thing people want

[Johan Commelin]

So you would have some statement theorem {G : Type} [group G] : blabla := begin ... end

[Johan Commelin]

and between the begin and end you do some sort of have_instance : has_mul G := { mul := op }

[Johan Commelin]

and then you can use multiplicative notation in the rest of the proof.

[Johan Commelin]

But it does not affect the statement

[Mario Carneiro]

so blabla there has no notation?

[Johan Commelin]

Yes, that is correct

[Johan Commelin]

Unless we can somehow sugar that in... but I guess then we run into trouble again (which was your point)

[Mario Carneiro]

right

[Mario Carneiro]

Also, without mul constants in that statement simp gets lost in higher order unification

[Johan Commelin]

I think there is quite a lot of interesting blabla that does not have very much notation

[Mario Carneiro]

for example if you have the theorem op x id = x where op and id are variables, simp can't use it

[Mario Carneiro]

but if the theorem is x + 0 = x then it can

[Johan Commelin]

You could wrap the statement with local notation x' \bullet 'y := op x y

[Johan Commelin]

If you really want infix notation in the statement

[Mario Carneiro]

that doesn't solve the problem I just mentioned though

[Johan Commelin]

Hmmm, so why can't simp use the former? (Newbie alert!)

[Mario Carneiro]

the expression ?M1 x ?M2 matches almost anything

[Mario Carneiro]

because you can have some lambda term for ?M1

[Mario Carneiro]

unification up to beta reduction is called higher order unification and it's undecidable

[Mario Carneiro]

and lean only does a very limited subset of it

[Johan Commelin]

Ok, so then we don't have simp for abstract groups.

[Mario Carneiro]

sad face

[Johan Commelin]

But as soon as you are in a multiplicate of additive setting, you have it back

[Mario Carneiro]

then I always want to be in a multiplicative or additive setting

[Johan Commelin]

and if inside the proof you do the have instance thing that I suggested above, then you also have it back (I hope)

[Johan Commelin]

So (I hope, once again) inside proofs you can always assume that you are inside the multiplicative setting

[Johan Commelin]

even if you prove something for an abstract group

[Mario Carneiro]

no, you still have that simp can only use groups with notation regardless of whether the goal uses notation

[Johan Commelin]

Yes, but you will have a group with notation. Because the first thing you prove inside your proof is that you have notation. And then you continue with the actual proof.

[Johan Commelin]

I really hope something like that is possible

[Mario Carneiro]

I mean, if you have a theorem whose statement is neutral but whose proof uses notation, it can't be used with simp

[Johan Commelin]

Hmmz, that is very sad

[Mario Carneiro]

because only the statement matters for simp

[Johan Commelin]

But you can change the statement inside the proof, right? By some apply to_multiplicative, or something

[Mario Carneiro]

So I just use multiplicative notation for "generic" group theory, and use multiplicative for transferring to additive

[Mario Carneiro]

I don't see any reason to avoid some kind of primacy between the notations

[Johan Commelin]

Ok, maybe I just need to get used to that (-;

[Johan Commelin]

But let me try to understand Lean better: if I have a "generic" statement, and I start my proof with apply multiplicative. Would I be able to use simp after that?

[Mario Carneiro]

simp can be used on any statement, but it can only use simp lemmas that are stated with notation

[Mario Carneiro]

I guess if you want to use simp on a generic statement you will need to change your goal to one that uses notation for the lemmas to match though

[Johan Commelin]

Right, and I think a tactic could do that change for me

[Mario Carneiro]

yes

[Mario Carneiro]

no such tactic exists, but it could be done

[Johan Commelin]

Great. Then I prefer that approach to group theory. But I respect your choice.

[Johan Commelin]

It would solve all the group_hom hassle

[Johan Commelin]

I think in the end, the code would be shorter, less duplication, and less multiplicative for end users.

[Mario Carneiro]

but it would still have the problem of not being registerable with simp, as a lemma on its own right

[Johan Commelin]

True, but I believe that the bulk of generic group theory is not simp lemmas

[Johan Commelin]

So we would need to state a couple of simp lemmas for groups with notation.

[Johan Commelin]

We don't want the five lemma to be a simp lemma, right?

[Mario Carneiro]

more complicated theorems, proving existence of things or what not, can often be opened up to defeq anyway so it doesn't matter

[Johan Commelin]

But I wouldn't mind if end users could use it, without figuring out to which of the 10 groups they first need to apply multiplicative

[Mario Carneiro]

Why don't you just state a version where everything is group, and another where everything is add_group, and let users deal with it themselves if they have mixed groups

[Johan Commelin]

Because I really think that means I won't have many users...

[Johan Commelin]

The conversion between group and add_group should be completely transparent

[Johan Commelin]

Otherwise we won't convert much mathematicians to formalisation

[Mario Carneiro]

Not completely transparent, if it's too transparent then * and + become the same and that's bad

[Mario Carneiro]

it's really not an easy problem

[Mario Carneiro]

I think multiplicative strikes the right balance, you have to explicitly state what you want but otherwise lean does the proof for free

[Johan Commelin]

Hmmm, would still like to have groups without notation

[Mario Carneiro]

why?

[Mario Carneiro]

it's not easier to read

[Mario Carneiro]

it's not easier to use

[Mario Carneiro]

the names are less obvious

[Johan Commelin]

For the generic theorems. Because those can be applied transparently to both settings

[Mario Carneiro]

I see no advantages

[Mario Carneiro]

it can't be applied transparently though

[Johan Commelin]

I think they are just as easy to use (or easier, in the mixed setting).

[Mario Carneiro]

it is as easy to apply a neutral theorem to an additive setting as it is to apply a multiplicative theorem in an additive setting

[Johan Commelin]

If every add_group is an instance of generic_group, and I prove the five lemma for generic groups, then I can just apply it to additive groups, right?

[Johan Commelin]

Without any multiplicative stuff

[Johan Commelin]

You see, when I have my mathematician hat on I never think about whether my group is additive or multiplicative. I just use it. And I just use theorems. And it works.

[Mario Carneiro]

I never had to deal with this in metamath either

[Johan Commelin]

So I don't want end users to have to figure out themselves where they need to use multiplicative to make some generic theorem work

[Kenny Lau]

You see, when I have my mathematician hat on I never think about whether my group is additive or multiplicative. I just use it. And I just use theorems. And it works.

hear hear

[Mario Carneiro]

it was all local notation

[Kenny Lau]

we do have an algebra hierarchy that mario doesn't use though

[Kenny Lau]

in that hierarchy this problem is avoided, I think

[Mario Carneiro]

Leo has his own ideas about generic groups. Like I said, this issue has a long history

[Mario Carneiro]

The core lean impl is unfinished though, maybe lean 4 will have something workable

[Mario Carneiro]

Honestly I have had more conversations on this topic than I would like, and things have not changed as a result

[Mario Carneiro]

I just want to prove theorems and use what's there

[Johan Commelin]

Ok. Got that.

[Johan Commelin]

I really don't want to start any fights of course. I really love what you have done so far.

[Mario Carneiro]

I don't mean to be short with you, but everyone has an idea and every solution has pros and cons

[Mario Carneiro]

I would suggest not entering the ring unless you have a large amount of testing to support your claims

[Johan Commelin]

Yeah, that's good advice.

[Kevin Buzzard]

I don't see any reason to avoid some kind of primacy between the notations

This is a concept alien to mathematicians, that's why Johan is talking about it. But, like division by zero, it's just something we have to learn.

[Kevin Buzzard]

They have different customs here.

[Patrick Massot]

Did we get anywhere with this additive group homs thread? @Mario Carneiro what is the definition you recommend in the end?