Zulip Chat Archive

Stream: maths

Topic: additive group homs


view this post on Zulip Johan Commelin (May 23 2018 at 18:36):

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?

view this post on Zulip Kevin Buzzard (May 23 2018 at 18:53):

There are additive group homs in the scheme stuff

view this post on Zulip Kevin Buzzard (May 23 2018 at 18:53):

Kenny wrote them

view this post on Zulip Kevin Buzzard (May 23 2018 at 18:53):

you could cut and paste for some basic stuff

view this post on Zulip Kevin Buzzard (May 23 2018 at 18:53):

if you just want a solution

view this post on Zulip Johan Commelin (May 23 2018 at 18:54):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 18:54):

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

view this post on Zulip Kevin Buzzard (May 23 2018 at 18:55):

already there is a little magic going on

view this post on Zulip Andrew Ashworth (May 23 2018 at 19:04):

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

view this post on Zulip Andrew Ashworth (May 23 2018 at 19:07):

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

view this post on Zulip Johan Commelin (May 23 2018 at 19:11):

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

view this post on Zulip Andrew Ashworth (May 23 2018 at 19:25):

hmm, have you worked through TPIL by chance?

view this post on Zulip Andrew Ashworth (May 23 2018 at 19:26):

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

view this post on Zulip Andrew Ashworth (May 23 2018 at 19:26):

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

view this post on Zulip Johan Commelin (May 23 2018 at 19:34):

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

view this post on Zulip Johan Commelin (May 23 2018 at 19:35):

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

view this post on Zulip Andrew Ashworth (May 23 2018 at 19:40):

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

view this post on Zulip Johannes Hölzl (May 23 2018 at 19:41):

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.

view this post on Zulip Johan Commelin (May 23 2018 at 19:43):

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

view this post on Zulip Johan Commelin (May 25 2018 at 04:07):

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?

view this post on Zulip Mario Carneiro (May 25 2018 at 04:41):

Use multiplicative to do these kind of things

view this post on Zulip Johan Commelin (May 25 2018 at 04:42):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 04:42):

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

view this post on Zulip Johan Commelin (May 25 2018 at 04:43):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 04:45):

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

view this post on Zulip Johan Commelin (May 25 2018 at 04:45):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 04:45):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 04:46):

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

view this post on Zulip Johan Commelin (May 25 2018 at 04:46):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 04:46):

yes, that's the idea

view this post on Zulip Johan Commelin (May 25 2018 at 04:46):

Or can you also use it to create mixed statements?

view this post on Zulip Mario Carneiro (May 25 2018 at 04:47):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 04:48):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 04:48):

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

view this post on Zulip Johan Commelin (May 25 2018 at 04:50):

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?

view this post on Zulip Mario Carneiro (May 25 2018 at 04:50):

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

view this post on Zulip Johan Commelin (May 25 2018 at 04:51):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 04:51):

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

view this post on Zulip Johan Commelin (May 25 2018 at 04:51):

But why do you think it is worse?

view this post on Zulip Mario Carneiro (May 25 2018 at 04:51):

It's less mnemonic than either add_zero or mul_one

view this post on Zulip Mario Carneiro (May 25 2018 at 04:52):

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

view this post on Zulip Johan Commelin (May 25 2018 at 04:52):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 04:52):

but then it gets into extending lean, which gets messy

view this post on Zulip Mario Carneiro (May 25 2018 at 04:53):

What do you mean?

view this post on Zulip Johan Commelin (May 25 2018 at 04:53):

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

view this post on Zulip Johan Commelin (May 25 2018 at 04:54):

But maybe I just used it wrong

view this post on Zulip Johan Commelin (May 25 2018 at 04:56):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 04:57):

What are you trying to do exactly?

view this post on Zulip Johan Commelin (May 25 2018 at 04:57):

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?

view this post on Zulip Mario Carneiro (May 25 2018 at 04:58):

yes

view this post on Zulip Johan Commelin (May 25 2018 at 04:58):

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.

view this post on Zulip Mario Carneiro (May 25 2018 at 04:58):

we don't

view this post on Zulip Johan Commelin (May 25 2018 at 04:59):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 05:00):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 05:00):

seeing as it can usually be rephrased in terms of is_group_hom

view this post on Zulip Johan Commelin (May 25 2018 at 05:01):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 05:02):

two is manageable, 2^n isn't?

view this post on Zulip Johan Commelin (May 25 2018 at 05:02):

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

view this post on Zulip Johan Commelin (May 25 2018 at 05:02):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 05:02):

so use is_group_hom and call it a day

view this post on Zulip Johan Commelin (May 25 2018 at 05:03):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 05:03):

what makes them additive?

view this post on Zulip Johan Commelin (May 25 2018 at 05:03):

Those groups are all finsupp (X n) int

view this post on Zulip Johan Commelin (May 25 2018 at 05:03):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 05:04):

okay, so where is the mixed group hom?

view this post on Zulip Johan Commelin (May 25 2018 at 05:05):

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.

view this post on Zulip Johan Commelin (May 25 2018 at 05:05):

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

view this post on Zulip Johan Commelin (May 25 2018 at 05:05):

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

view this post on Zulip Johan Commelin (May 25 2018 at 05:05):

In all sorts of exponential sequences

view this post on Zulip Mario Carneiro (May 25 2018 at 05:06):

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)

view this post on Zulip Johan Commelin (May 25 2018 at 05:07):

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

view this post on Zulip Johan Commelin (May 25 2018 at 05:08):

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

view this post on Zulip Johan Commelin (May 25 2018 at 05:08):

Or something like that.

view this post on Zulip Mario Carneiro (May 25 2018 at 05:10):

they should be the same, but yes unfold if necessary

view this post on Zulip Johan Commelin (May 25 2018 at 05:10):

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

view this post on Zulip Johan Commelin (May 25 2018 at 05:11):

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?

view this post on Zulip Mario Carneiro (May 25 2018 at 05:12):

Oh don't do that

view this post on Zulip Mario Carneiro (May 25 2018 at 05:12):

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

view this post on Zulip Johan Commelin (May 25 2018 at 05:12):

ok

view this post on Zulip Mario Carneiro (May 25 2018 at 05:12):

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

view this post on Zulip Johan Commelin (May 25 2018 at 05:13):

got it

view this post on Zulip Johan Commelin (May 25 2018 at 06:32):

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?

view this post on Zulip Johan Commelin (May 25 2018 at 06:32):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:33):

And we don't have infix notation for those

view this post on Zulip Johan Commelin (May 25 2018 at 06:33):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:33):

Then we still have our beloved infix notation.

view this post on Zulip Johan Commelin (May 25 2018 at 06:34):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:34):

So the proofs remain readable and intuitive

view this post on Zulip Johan Commelin (May 25 2018 at 06:36):

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.

view this post on Zulip Johan Commelin (May 25 2018 at 06:36):

Does this idea make any sense at all?

view this post on Zulip Mario Carneiro (May 25 2018 at 06:37):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:37):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 06:37):

then you can't use notation with abstract group theory

view this post on Zulip Mario Carneiro (May 25 2018 at 06:38):

which is a thing people want

view this post on Zulip Johan Commelin (May 25 2018 at 06:38):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:38):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:39):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:39):

But it does not affect the statement

view this post on Zulip Mario Carneiro (May 25 2018 at 06:39):

so blabla there has no notation?

view this post on Zulip Johan Commelin (May 25 2018 at 06:40):

Yes, that is correct

view this post on Zulip Johan Commelin (May 25 2018 at 06:40):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 06:40):

right

view this post on Zulip Mario Carneiro (May 25 2018 at 06:41):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:41):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 06:41):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 06:41):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:42):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:42):

If you really want infix notation in the statement

view this post on Zulip Mario Carneiro (May 25 2018 at 06:42):

that doesn't solve the problem I just mentioned though

view this post on Zulip Johan Commelin (May 25 2018 at 06:43):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 06:43):

the expression ?M1 x ?M2 matches almost anything

view this post on Zulip Mario Carneiro (May 25 2018 at 06:44):

because you can have some lambda term for ?M1

view this post on Zulip Mario Carneiro (May 25 2018 at 06:44):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 06:44):

and lean only does a very limited subset of it

view this post on Zulip Johan Commelin (May 25 2018 at 06:45):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 06:45):

sad face

view this post on Zulip Johan Commelin (May 25 2018 at 06:45):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 06:45):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:45):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:46):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:46):

even if you prove something for an abstract group

view this post on Zulip Mario Carneiro (May 25 2018 at 06:47):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:48):

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.

view this post on Zulip Johan Commelin (May 25 2018 at 06:48):

I really hope something like that is possible

view this post on Zulip Mario Carneiro (May 25 2018 at 06:48):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:48):

Hmmz, that is very sad

view this post on Zulip Mario Carneiro (May 25 2018 at 06:48):

because only the statement matters for simp

view this post on Zulip Johan Commelin (May 25 2018 at 06:49):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 06:49):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 06:50):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:50):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:52):

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?

view this post on Zulip Mario Carneiro (May 25 2018 at 06:53):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 06:54):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:54):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 06:54):

yes

view this post on Zulip Mario Carneiro (May 25 2018 at 06:54):

no such tactic exists, but it could be done

view this post on Zulip Johan Commelin (May 25 2018 at 06:55):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:55):

It would solve all the group_hom hassle

view this post on Zulip Johan Commelin (May 25 2018 at 06:55):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 06:55):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:56):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:56):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:57):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 06:57):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:58):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 06:58):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:59):

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

view this post on Zulip Johan Commelin (May 25 2018 at 06:59):

The conversion between group and add_group should be completely transparent

view this post on Zulip Johan Commelin (May 25 2018 at 06:59):

Otherwise we won't convert much mathematicians to formalisation

view this post on Zulip Mario Carneiro (May 25 2018 at 07:00):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 07:00):

it's really not an easy problem

view this post on Zulip Mario Carneiro (May 25 2018 at 07:00):

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

view this post on Zulip Johan Commelin (May 25 2018 at 07:01):

Hmmm, would still like to have groups without notation

view this post on Zulip Mario Carneiro (May 25 2018 at 07:01):

why?

view this post on Zulip Mario Carneiro (May 25 2018 at 07:02):

it's not easier to read

view this post on Zulip Mario Carneiro (May 25 2018 at 07:02):

it's not easier to use

view this post on Zulip Mario Carneiro (May 25 2018 at 07:02):

the names are less obvious

view this post on Zulip Johan Commelin (May 25 2018 at 07:02):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 07:02):

I see no advantages

view this post on Zulip Mario Carneiro (May 25 2018 at 07:02):

it can't be applied transparently though

view this post on Zulip Johan Commelin (May 25 2018 at 07:02):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 07:03):

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

view this post on Zulip Johan Commelin (May 25 2018 at 07:03):

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?

view this post on Zulip Johan Commelin (May 25 2018 at 07:03):

Without any multiplicative stuff

view this post on Zulip Johan Commelin (May 25 2018 at 07:04):

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.

view this post on Zulip Mario Carneiro (May 25 2018 at 07:05):

I never had to deal with this in metamath either

view this post on Zulip Johan Commelin (May 25 2018 at 07:05):

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

view this post on Zulip Kenny Lau (May 25 2018 at 07:05):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 07:05):

it was all local notation

view this post on Zulip Kenny Lau (May 25 2018 at 07:05):

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

view this post on Zulip Kenny Lau (May 25 2018 at 07:05):

in that hierarchy this problem is avoided, I think

view this post on Zulip Mario Carneiro (May 25 2018 at 07:06):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 07:07):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 07:08):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 07:08):

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

view this post on Zulip Johan Commelin (May 25 2018 at 07:09):

Ok. Got that.

view this post on Zulip Johan Commelin (May 25 2018 at 07:09):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 07:10):

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

view this post on Zulip Mario Carneiro (May 25 2018 at 07:11):

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

view this post on Zulip Johan Commelin (May 25 2018 at 07:15):

Yeah, that's good advice.

view this post on Zulip Kevin Buzzard (May 25 2018 at 22:18):

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.

view this post on Zulip Kevin Buzzard (May 25 2018 at 22:20):

They have different customs here.

view this post on Zulip Patrick Massot (Jul 10 2018 at 08:42):

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


Last updated: May 18 2021 at 07:19 UTC