bundling mul_homs

Stream: maths

[Kevin Buzzard]

Mathlib has the unbundled is_mul_hom class (a Prop), and then it has mul_equiv which references this unbundled is_mul_hom. If we were to bundle mul_homs, how would we define mul_equiv?

import data.equiv.basic algebra.group
import data.equiv.algebra

variables {α : Type*} {β : Type*} {γ : Type*}
[has_mul α] [has_mul β] [has_mul γ]
(M : Type*) (N : Type*) (P : Type*)
[has_mul M] [has_mul N] [has_mul P]

/- Mathlib:

class is_mul_hom {α β : Type*} [has_mul α] [has_mul β] (f : α → β) : Prop :=
(map_mul : ∀ x y, f (x * y) = f x * f y)

structure mul_equiv (α β : Type*) [has_mul α] [has_mul β] extends α ≃ β :=
(hom : is_mul_hom to_fun)

notation ≃* for mul_equiv, proved to be reflexive, symmetric and transitive

-- not yet found a use for this instance. Should `is_mul_hom` be a structure?
instance (h : α ≃* β) : is_mul_hom h.to_equiv := h.hom

-/

namespace mul

/-- bundled homs FTW -/
structure hom (M N : Type*) [has_mul M] [has_mul N] :=
(f : M → N)
(map_mul : ∀ x y, f (x * y) = f x * f y)

-- but now if I delete `is_mul_hom`, how do I define `mul_equiv`?
-- notation for homs
infix ` →* `:25 := hom

[Mario Carneiro]

mul_equiv A B extends equiv A B, mul_hom A B

[Kevin Buzzard]

Should I be using old or new structures for these things?

[Mario Carneiro]

old structures FTW

[Kevin Buzzard]

Is what you call mul_hom what I called mul.hom?

[Kevin Buzzard]

Did I name it wrong?

[Mario Carneiro]

I don't think so

[Mario Carneiro]

mul_hom A B for me is the type of augmented functions from A to B

[Kevin Buzzard]

but mul.hom has got a field f and equiv has got a field to_fun and these are supposed to be defeq and have the same name.

[Mario Carneiro]

I don't see mul.hom in the example

[Mario Carneiro]

Oh there it is

[Kevin Buzzard]

I'm talking about my attempt to bundle homs.

[Mario Carneiro]

I think that should be mul_hom

[Mario Carneiro]

mul isn't a namespace

[Mario Carneiro]

mul_hom should have a field called to_fun

[Mario Carneiro]

so that mul_equiv works

[Kevin Buzzard]

to_fun is such a horrible name for a function. I guess its canonical name is the coercion so maybe it doesn't matter. Wait -- the map from mul_equiv X Y to mul_hom X Y -- that is no longer an instance, because mul_hom isn't a class. Is this still done with coercions somehow?

[Mario Carneiro]

it's a function called to_mul_hom

[Mario Carneiro]

You can try using a coercion but this one tends to trigger rarely

[Mario Carneiro]

given that the parent functions are always called to_*, to_fun seems to match that naming convention

[Kevin Buzzard]

structure mul_hom (M N : Type*) [has_mul M] [has_mul N] :=
(to_fun : M → N)
(map_mul : ∀ x y, to_fun (x * y) = to_fun x * to_fun y)

Should this have a coercion to fun?

[Mario Carneiro]

yes

[Kevin Buzzard]

My map_mul is crappy:

set_option old_structure_cmd true

/-- bundled homs FTW -/
structure mul_hom (M N : Type*) [has_mul M] [has_mul N] :=
(to_fun : M → N)
(map_mul : ∀ x y, to_fun (x * y) = to_fun x * to_fun y)

-- notation for homs
infix ` →* `:25 := mul_hom

instance : has_coe_to_fun (M →* N) :=
{ F := λ _, M → N,
  coe := mul_hom.to_fun }

#check mul_hom.map_mul
/-
mul_hom.map_mul : ∀ (c : ?M_1 →* ?M_2) (x y : ?M_1), c.to_fun (x * y) = c.to_fun x * c.to_fun y
-- yeah but I want it to be the coercion, not `c.to_fun`
-/

It has come out non-canonically. Am I supposed to be doing this:

def mul_hom.map_mul' : ∀ (f : M →* N) (x y : M), f (x * y) = f x * f y := mul_hom.map_mul

?

[Mario Carneiro]

with the primes inverted

[Kevin Buzzard]

So you're saying I need to change mathlib

[Kevin Buzzard]

no

[Kevin Buzzard]

you're saying I need to change my structure field's name.

[Mario Carneiro]

yes

[Kevin Buzzard]

Should this

structure mul_equiv' (A B) [has_mul A] [has_mul B] extends equiv A B, mul_hom A B

have a coercion to fun?

[Mario Carneiro]

yes

[Kevin Buzzard]

import data.equiv.basic algebra.group
import data.equiv.algebra

variables {α : Type*} {β : Type*} {γ : Type*}
[has_mul α] [has_mul β] [has_mul γ]
(M : Type*) (N : Type*) (P : Type*)
[has_mul M] [has_mul N] [has_mul P]

-- Recall that the unbundled definition of a mul_hom
-- and the definition of a mul_equiv, with notation ≃*, are in mathlib.

/- Mathlib:

-- in root namespace
class is_mul_hom {α β : Type*} [has_mul α] [has_mul β] (f : α → β) : Prop :=
(map_mul : ∀ x y, f (x * y) = f x * f y)

-- root namespace
structure mul_equiv (α β : Type*) [has_mul α] [has_mul β] extends α ≃ β :=
(hom : is_mul_hom to_fun)

notation ≃*, proved to be reflexive, symmetric and transitive (note: it is not a Prop)
-/


--. We will define
-- bundled homomorphisms of muls, with notation →*, and bundled
-- equivs, with notation ≃*'


set_option old_structure_cmd true

/-- bundled homs -/
structure mul_hom (M N : Type*) [has_mul M] [has_mul N] :=
(to_fun : M → N)
(map_mul' : ∀ x y, to_fun (x * y) = to_fun x * to_fun y)

-- notation for homs
infix ` →* `:25 := mul_hom

-- I want to think of a hom as a function sometimes
instance : has_coe_to_fun (M →* N) :=
{ F := λ _, M → N,
  coe := mul_hom.to_fun }

/-- the statement that mul_homs preserve mul, in its canonical form -/
def mul_hom.map_mul : ∀ (f : α →* β) (x y : α), f (x * y) = f x * f y := mul_hom.map_mul'

-- for structures like this you need to prove `id` and `comp` next.
namespace mul_hom

/-- the identity is a mul_hom-/
def id : M →* M := {to_fun := id, map_mul' := λ _ _, rfl}

/-- composite of mul_homs is a mul_hom -/
def comp (f : α →* β) (g : β →* γ) : α →* γ :=
{ to_fun := λ m, g (f m),
  map_mul' := λ x y, by rw [map_mul f, map_mul g] }

end mul_hom

/-- mul_equiv' (bundled mul_equiv -- the name mul_equiv is currently nicked by unbundled mul_equiv) -/
structure mul_equiv' (A B) [has_mul A] [has_mul B] extends equiv A B, mul_hom A B

-- notation for mul_equiv'
infix ` ≃*' `:25 := mul_equiv'

instance : has_coe_to_fun (M ≃*' N) := { F := _,
  coe := mul_equiv'.to_fun }

def mul_equiv'.map_mul : ∀ (f : α ≃*' β) (x y : α), f (x * y) = f x * f y
:= mul_equiv'.map_mul'

-- now need reflexive, symmetric and transitive

namespace mul_equiv'

@[refl] def refl (α : Type*) [has_mul α] : α ≃*' α :=
{ map_mul' := λ x y, rfl,
..equiv.refl α}

-- this one did not go so well.
@[symm] def symm (h : α ≃*' β) : β ≃*' α :=
{ map_mul' := λ n₁ n₂, function.injective_of_left_inverse h.left_inv begin
    show h.to_fun (h.inv_fun (n₁ * n₂)) =
    h (h.inv_fun n₁ * h.inv_fun n₂), -- annoying to have to `show`
    rw h.right_inv,
    rw h.map_mul,
    convert rfl, -- annoying to have to `convert`. This should surely just be rewrites.
      exact h.right_inv _,
    exact h.right_inv _,
  end,
  ..h.to_equiv.symm}

@[trans] def trans (h1 : α ≃*' β) (h2 : β ≃*' γ) : (α ≃*' γ) :=
{ map_mul' := λ x y,
    show h2 (h1 (x * y)) = h2 (h1 x) * h2 (h1 y),
    by rw [h1.map_mul, h2.map_mul],
  ..equiv.trans h1.to_equiv h2.to_equiv }

-- an ≃*' is a hom
def equiv'.to_hom (h : M ≃*' N) : M →* N :=
  { to_fun := h.to_equiv,
    map_mul' := h.map_mul'
  }

def equiv'.inv_hom (h : M ≃*' N) : N →* M :=
  { to_fun := h.symm.to_equiv,
  map_mul' := h.symm.map_mul
  }

end mul_equiv'

equiv'.symm didn't go well but most of the other stuff looks OK to me

[Mario Carneiro]

People will complain about the order of arguments to comp

[Johan Commelin]

@Kevin Buzzard You probably know this but mul_hom.map_mul should be a lemma, and it is a very good simp-lemma.

[Mario Carneiro]

What's wrong with symm? It looks like that's the sort of thing that is mathematically substantive anyway

[Johan Commelin]

In fact, that's the most important reason for bundling in the first place. That this is a simp-lemma that actually triggers.

[Johan Commelin]

Also, we'll want simp-lemmas id_apply and comp_apply.

[Kevin Buzzard]

Kevin Buzzard You probably know this but mul_hom.map_mul should be a lemma, and it is a very good simp-lemma.

I'm not very good at simp still.

[Kevin Buzzard]

So anyway, there is a bunch of structure most of which is correctly named, and hopefully defined sensibly. Do we want all all of this in mathlib? And then there's the equivalent stuff for semigroup, for monoid and for group. I don't care about the mul stuff really, I was just practicing. I do care about equivs of monoids and of groups and would like some students to prepare a mathlib PR.

What are we looking for in such a PR? Should the students try and define everything for semigroup when we don't really need it? Is a PR of this nature for group welcome? @Chris Hughes do you have any opinions on this? I've talked to you before about it and you seem to have a clear head about what should be there.

[Kevin Buzzard]

Note that we can define group.hom to be mul_hom

[Kevin Buzzard]

I think the last time we talked about this, you liked that idea.

[Chris Hughes]

Don't bother with semigroup stuff unless it's virtually no effort. I'd actually prefer group_hom and monoid_hom to be the same, since these are the two that are actually used. You could write a custom constructor without the unnecessary axiom.

Same idea goes for ring_hom and semiring_hom

[Kevin Buzzard]

so you're saying you want group.hom to be called group_hom and to demand that f(1)=1?

[Kevin Buzzard]

What should the custom constructor be called?

[Chris Hughes]

Yes @[reducible] def group_hom := monoid_hom.

group_hom.mk

[Chris Hughes]

That way, simp lemmas you prove about monoid_homs will work with group homs.

[Kevin Buzzard]

And should this be reducible too? [sorry for prime on mul_equiv, mathlib has a slightly more unbundled one]

def monoid_equiv (M N) [monoid M] [monoid N] := mul_equiv' M N

[Johan Commelin]

Is it clear that making some of these definitions does not create leakage?

[Kevin Buzzard]

I am just experimenting. I will certainly report back.

[Johan Commelin]

Also, I think Lean is quite bad at dealing with situations like this:
I have M1 M2 : Type and [monoid M1] [monoid M2]
I also have f : monoid_hom M1 M2.
Then, for some reason, it happens that I can actually prove that M1 and M2 are groups.
Now I need to work to turn f into a group hom. And if I don't do that, certain lemma's can't be applied, and simp gets stuck etc...

[Kevin Buzzard]

This won't happen with Chris' suggesting of defining group_hom to be equal to monoid_hom

[Johan Commelin]

I know it is not very beginner-friendly. But I'm becoming more and more of the opinion that we shouldn't have these "shadowing" classes. Like vector_space (and even module). And so, maybe we should also just get rid of group_homs

[Johan Commelin]

Nope, that's not true.

[Kevin Buzzard]

and making it reducible

[Johan Commelin]

If I have a module over a field, I can't apply linear algebra results.

[Johan Commelin]

Even if vector_space is reducibly defined to be a module.

[Johan Commelin]

This has bitten me several times.

[Kevin Buzzard]

We need some way of being able to talk about group homomorphisms. What is your suggestion? Unbundled homs? I thought this had problems too?

[Johan Commelin]

No, it's somewhat orthogonal to bundling, but it's very much related to refactoring.

[Johan Commelin]

I want to propose/discuss just ditching group_hom altogether.

[Johan Commelin]

Just write monoid_hom.mk' for the case that you construct monoid homs between groups.

[Johan Commelin]

It doesn't look nice... but it is more flexible.

[Kevin Buzzard]

This has bitten me several times.

If you try to fix it by making the actual object you want from the object you have (e.g. the vector space over the field from the module), then you then have two objects which mathematicians find completely indistinguishable, but for which Lean finds it hard to port results about one object to results from the other. This sounds like a good place to try out a transfer tactic, no?

[Johan Commelin]

Meh... I would rather let the problem go away.

[Johan Commelin]

Maybe group_hom can be an abbreviation?? I still don't know what this does exactly.

[Johan Commelin]

But it seems to be something like hyper-super-duper-reducible.

[Chris Hughes]

And should this be reducible too? [sorry for prime on mul_equiv, mathlib has a slightly more unbundled one]

def monoid_equiv (M N) [monoid M] [monoid N] := mul_equiv' M N

That shouldn't exist

[Johan Commelin]

For the same reason that vector_space shouldn't exist?

[Kevin Buzzard]

I want to propose/discuss just ditching group_hom altogether.

If we ditch group_hom altogether, what will be the canonical way of representing the concept of $f:G\to H$ with $f(xy)=f(x)f(y)$ with $G$, $H$ groups?

[Kevin Buzzard]

def monoid_equiv (M N) [monoid M] [monoid N] := mul_equiv' M N

That shouldn't exist

If that doesn't exist at all, then what happens to the poor newbie who shows up with their two monoids and wants to know where the equiv is?

[Johan Commelin]

We tell them to use M1 =* M2.

[Johan Commelin]

If we ditch group_hom you just write f : G →m H

[Johan Commelin]

Or whatever the notation for monoid homs will be.

[Chris Hughes]

I started on ->1*, but I propose ->*, and screw mul homs notation.

[Kevin Buzzard]

So notation can attempt to solve the issue. Chris are you proposing the notation with no 1 to be overloaded? I am mostly interested in group homs and isoms because a student of mine needs them asap

[Chris Hughes]

I'm proposing no notation for mul homs, since they're rarely used.

[Kevin Buzzard]

then what term is ->* notation for?

[Kevin Buzzard]

I am happy to implement your idea but I don't understand it yet. I would just like isomorphisms and bundled homomorphisms of groups sooner rather than later.

[Kevin Buzzard]

I want to do more experiments with the bundled morphisms approach.

[Chris Hughes]

monoid homs

[Kevin Buzzard]

A monoid hom has this extra condition that 1 goes to 1. So we define monoid_hom, and we can make \equiv\_g be notation for monoid_hom.

[Johan Commelin]

Sure, so Chris is saying →* for monoid homs and group homs. No notation for mul_hom.

[Kevin Buzzard]

and we could also make \equiv\_m be notation for monoid_hom for when we're working with moniods, and then Lean's prettyprinter would have an impossible notation problem to solve.

[Johan Commelin]

And \equiv* might be a nice fit for mul_equiv (and we don't need monoid_equiv or group_equiv).

[Kevin Buzzard]

So we just tell the user in comments in the group section: "the notation for group homomorphisms is ->* and the notation for group isomorphisms is \equiv*"

[Johan Commelin]

Sure... and because the notation is somewhat natural it is even avoiding the awkard f : monoid_hom G H for group homs.

[Johan Commelin]

I think this is quite a nice solution.

[Kevin Buzzard]

That's quite interesting that the force of the mathematical interpretation ->* is "I preserve everything relevant to multiplication that is present"

[Johan Commelin]

The special constructor could be

def group_hom {G H : Type} [group G] [group H] (h : f (x*y) = f x * f y) : G →* H := sorry

[Kevin Buzzard]

If you defined monoids to mathematicians and then said "OK now what do you think $M\to^*N$ means?" they'd be like "monoid hom I guess"

[Johan Commelin]

(That example didn't type check, but you get the idea.)

[Kevin Buzzard]

But Chris seems to be explictly suggesting that the name group_hom is never assigned. Is this what you think @Chris Hughes ?

[Johan Commelin]

What I'm saying is that monoid_hom.mk is a bad name for constructing monoid homs between groups.

[Kevin Buzzard]

These are all such irrelevances, there must be some solution with automation or something. Mathematically we are doing absolutely nothing at all.

[Johan Commelin]

I've been saying time and again that Fabian can auto-generate all of these.

[Johan Commelin]

But people don't really seem to care.

[Kevin Buzzard]

@Mario Carneiro we need computer science help. We have a very rigorous notion of "the same" here -- this seems to me like this is type class inference in a tangle. Do you understand why we are struggling? Why can't Johan do linear algebra with a module over a field? @Johan Commelin can you give a MWE? We need to get good at this.

[Mario Carneiro]

I think that more names for the same thing is bad for formalization, although I understand why it is mathematically desirable. I am on board with Chris's suggestions

[Kevin Buzzard]

We also need the additive version of everything, I suppose? That entire process can be automated. Can you literally to a regex on the file to generate its additive version? And then you can look observe the funny fact that there are two olean files which are exactly the same

[Mario Carneiro]

While I don't want to minimize Fabian's work, the proofs are not the hard part here. This is all API design questions

[Kevin Buzzard]

Right. I'm trying really hard to make a mathematician's API.

[Kevin Buzzard]

I now have a much better understanding of the issues here and I think it's a really important question for drawing mathematicians in. We want to make it look easy.

[Kevin Buzzard]

I think we might be losing half our audience at

inductive nat
| zero : what does all this weird stuff mean

We just want to say "The naturals are $\mathbb{N}$, typed \N and they work exactly as you would expect them to". Implementing this is not a trivial thing at all!

[Mario Carneiro]

I heartily disagree

[Kevin Buzzard]

"It goes without saying that if $A$ and $B$ are isomorphic comm_rings then $A$ is Gorenstein iff $B$ is. It does not need a proof. "

[Kevin Buzzard]

that one is not proving trivial to implement

[Mario Carneiro]

hardcoding what "they work exactly as you would expect" means is just making lean more "magical" and less comprehensible

[Mario Carneiro]

which is setting yourself up for failure

[Kevin Buzzard]

You guys worry too much about these tedious implementation issues

[Mario Carneiro]

That's not an implementation issue, it's a pedagogy issue

[Kevin Buzzard]

We're never going to run the code we're making, you don't need to optimise it

[Kevin Buzzard]

We just want to eat every proposition and every proof bit by bit

[Mario Carneiro]

if lean has tons of special cases then it's big and complicated to learn. This is not an exaggeration, it's already the case

[Mario Carneiro]

implementing transfer is hard because type theory is big and complicated

[Kevin Buzzard]

You should just solve it with pointers or something

[Mario Carneiro]

:expressionless:

[Mario Carneiro]

That said, transfer is already implemented and mostly works. As I've said many times, what is needed is not a tactic but lemmas for it to use

[Kevin Buzzard]

So mathematicians have a gigantic list of abstract mathematical ideas. And for each of these ideas computer scientists have developed some term in type theory, or perhaps some token (the mathematical symbol of isomorphism comes to mind), and said "look here it is", and then we say "Thanks. Does it do this, this, that and this?" and you guys go "Yes of course. And it does a gazillion other things too like look you can see inside it and you can do that if you want" and we say "no thanks, we just need this this that and this. We will now promise that any future terms will be built using that interface. In return, you must understand our notion of equality, which you can work out from the interface I suppose"

Examples: the real numbers, a group, the localisation of a ring, the module of one-forms for an algebra over a ring, or a sheaf on a space.

[Mario Carneiro]

Except that sometimes you break the interface and pretend you didn't

[Mario Carneiro]

Reading the MO question I was amused that no one noticed that $\Bbb R\subseteq\Bbb C$ is not an isomorphism-invariant statement. They say "we know isomorphisms don't matter so we may as well assume it's the case" but then it's not isomorphism invariant anymore

[Kevin Buzzard]

I find those endless comments very hard to read.

[Mario Carneiro]

I think that statement showed up in one of the answers

[Kevin Buzzard]

Was it the one I accepted?

[Mario Carneiro]

https://mathoverflow.net/a/336233/34444

[Mario Carneiro]

Relatedly, we can assume that $\Bbb R\subseteq\Bbb C$ because we only care about the axiomatized properties of $\Bbb R$, which are preserved under isomorphism. One could manually preserve the original $\Bbb R$ as an actual subset of its quadratic extension, but that is unnecessary for the reason I just stated.

This reasoning fails to take into account that by taking advantage of isomorphism invariance you break it

[Kevin Buzzard]

There are also two deleted answers with positive scores which degenerated into flamewars resulting in the OP just deleting everything

[Mario Carneiro]

I saw the comment but I'm not high rep on MO so I can't read it :(

[Mario Carneiro]

Andrej usually has interesting things to say

[Mario Carneiro]

To me the process is tedious but straightforward. We need equiv.rel in mathlib, and then a bunch of isomorphism builders, and a bunch of isomorphism statements, and then this will be easy

[Mario Carneiro]

Don't come to me about making a tactic to do it until you've already done it 10 times and know what it looks like

[Kevin Buzzard]

I think Andrej and I follow each other on Twitter; I'll prod him.

[Kevin Buzzard]

What is the role that this predicate should play? We define the Cauchy reals, and we prove that they are a complete arch field, and then we prove that any two complete arch fields are uniquely isomorphic as ordered fields. We then have this type real and this promise that we will only use complete_archimedean_ordered_field real or whatever. We have given you a precise interface here. What you now need to do somehow is to make this a primitive object -- I would quite happily be in an environment where the real type and its instance as a complete archimedean ordered field was some structure and a bunch of axioms. Why can't we use this abstraction for the reals and only have access to this interface?

[Kevin Buzzard]

It would presumably be easier to reason about proof transportability if you knew the proof had stuck to the interface.

[Mario Carneiro]

I'm talking about transfer specifically. This is independent of any interface to the reals you may or may not be adhering to

[Kevin Buzzard]

I want a little bit of HoTT magic at exactly this point

[Kevin Buzzard]

So tell me again what transfer specifically means?

[Mario Carneiro]

To me the process is tedious but straightforward. We need equiv.rel in mathlib, and then a bunch of isomorphism builders, and a bunch of isomorphism statements, and then this will be easy

[Mario Carneiro]

The only way to get, provably in lean, invariance from syntax generically is if you have a deeply embedded language and express all your properties in that language. I'm sure we don't want to do that

[Kevin Buzzard]

Will this tedious but straightforward process be easier to do in Lean 4?

[Mario Carneiro]

not particularly

[Kevin Buzzard]

So we may as well start right away :-)

[Mario Carneiro]

like I said, stop thinking of tactics and start thinking about the problem

[Kevin Buzzard]

Isn't the immediate problem that someone has to write some meta code?

[Mario Carneiro]

Once you know what the problem is and what the solution is the tactic writes itself

[Mario Carneiro]

no

[Mario Carneiro]

meta code comes later

[Mario Carneiro]

proofs come first

[Mario Carneiro]

Tactics never allow you to prove something you couldn't prove before. They just make it easier to do things you already knew how to do

[Kevin Buzzard]

So maybe a tactic which does this would be interesting: I will define the Dedekind reals in Lean, prove they're a complete arch ordered field, and then demand from you a copy of the Bochner integral but all with Dedekind reals instead of Cauchy reals.

[Kevin Buzzard]

Do I "know how to do that"? Is this one we're going to solve with tags?

[Mario Carneiro]

You don't, that's the problem

[Kevin Buzzard]

the idea is that any PR to mathlib which didn't use the allowable interface would not be accepted.

[Kevin Buzzard]

So you just have to write some regex to check that people aren't fiddling with the real's privates

[Kevin Buzzard]

and run all PR's through the regex to check for safety

[Mario Carneiro]

The safety check is not the problem, the equivalence proofs are

[Kevin Buzzard]

and if they pass you can accept the PR and then some Lean code generates a proof that all the stuff in mathlib is still "safe"

[Mario Carneiro]

Even if we know everything is safe that doesn't provide a proof of equivalence

[Kevin Buzzard]

So what formally is the problem?

[Mario Carneiro]

You have already stated it: Given a concrete predicate P on rings prove that if A and B are isomorphic rings then P(A) iff P(B)

[Kevin Buzzard]

Surely it provides a proof that the term exists, it just doesn't actually make the term.

[Kevin Buzzard]

Why isn't that P(A) iff P(B) thing easy?

[Mario Carneiro]

It is

[Kevin Buzzard]

You just peel P apart and do it by induction

[Mario Carneiro]

Yes, so do it

[Kevin Buzzard]

You mean it's hard to implement?

[Mario Carneiro]

No, it's easy

[Mario Carneiro]

but it's work

[Kevin Buzzard]

I can't do it, I have my decency.

[Mario Carneiro]

and it needs to actually be in mathlib

[Kevin Buzzard]

It's not maths.

[Mario Carneiro]

transfer will not work until mathlib is full of theorems like that

[Kevin Buzzard]

that's an axiom, you guys have to do that one :-) I would have no idea how to do it. Is it the sort of thing a novice tactic-writer could try?

[Mario Carneiro]

If you don't know how to do it, how would a novice know?

[Kevin Buzzard]

I mean maybe they can just read Programming In Lean and then just do it

[Mario Carneiro]

A novice tactic writer can generalize from examples, but we have none

[Mario Carneiro]

once we have done it by hand 10 times a novice tactic writer can do the rest

[Kevin Buzzard]

So what needs doing in practice?

[Kevin Buzzard]

What's the first thing that needs to be done?

[Mario Carneiro]

equiv.rel, isomorphism builders, and theorems of the form A ~= B -> P(A) <-> P(B)

[Kevin Buzzard]

Are there some sorts of milestones which you can see to making this transfer tactic?

[Kevin Buzzard]

So what is the type of equiv.rel?

[Mario Carneiro]

equiv.rel (e : A ~= B) : A -> B -> Prop := \lam a b, e a = b

[Mario Carneiro]

This allows you to state a theorem of the form A ~= B -> P(A) <-> P(B) as e.rel => iff where => is that funny relator operation

[Kevin Buzzard]

oh so that one's done now, right?

[Mario Carneiro]

You need a few theorems about it

[Mario Carneiro]

the most important ones for transfer is that it is left and right unique

[Kevin Buzzard]

OK so is there some structure I need to make on equiv.rel?

[Mario Carneiro]

and the converse is given by equiv.rel of the inverse equiv

[Mario Carneiro]

I think left_unique and right_unique are typeclasses

[Mario Carneiro]

If you look at logic.relator there are several functions related to this sort of thing

[Kevin Buzzard]

Just to be clear -- the e : A =~ B notation -- the type of e is just some random type T A B, or does it have to have some sort of equivalence relation properties?

[Mario Carneiro]

e is an equiv

[Mario Carneiro]

not a fancy equiv, just an equiv

[Mario Carneiro]

More complicated things would have something like (e.to_equiv.rel => iff) Gorenstein Gorenstein where e is a ring equiv

[Jeremy Avigad]

@Kevin Buzzard I can't resist a bit of history here. Read Dedekind's Was sind und was sollen die Zahlen (1888), roughly "What are the [natural] numbers and what should they be." See especially the introduction. (It is the second essay here: http://www.gutenberg.org/files/21016/21016-pdf.pdf.) The answer to the question posed in the title is expressed more clearly in his letter to Keferstein: http://www.bris.ac.uk/media-library/sites/structuralism/migrated/documents/kerfstein.pdf. It is as you say: We don't care what they are, as long as they satisfy the properties we want. We only need to construct one to show that the notion is coherent. Then, if as long as we respect the interface, anything we say about one will be true of the other. (The part about respecting the interface is in Section 134 on page 48 of the essay.) In modern terms, he gave an axiomatic characterization of the natural numbers, a set theoretic construction (from the assumption that there exists an infinite set), and a proof that any two systems satisfying the axioms are isomorphic.

Dedekind was an early proponent of a modern, structural view of mathematics, at a time when the subject had a much more calculational style. According to van der Waerden, Emmy Noether used to say "Es steht alles schon bei Dedekind," i.e. everything is already there, in Dedekind.

[Kevin Buzzard]

I have seen all this stuff before but I just never really understood its depth until recently

[Kevin Buzzard]

But in some sense it really is not mathematics. This whole thing is just a tedious implementation issue.

[Kevin Buzzard]

Everything is already there, in Dedekind.

[Andrew Ashworth]

Maybe the old usage of transfer to prove properties about ints-as-pairs-of-naturals should be the in mathlib docs, i.e. https://github.com/leanprover/lean/blob/6ab792733d09878d82ce98d88f6f476c8e0f34d8/library/init/data/int/basic.lean

[Kevin Buzzard]

import data.equiv.basic
import logic.relator

def equiv.rel {A B : Type*} (e : A ≃ B) : A → B → Prop := λ a b, e a = b

variables {A : Type*} {B : Type*} (e : A ≃ B)

instance : relator.left_unique (equiv.rel e) := λ a₁ b a₂ h1 h2, equiv.injective e $ eq.trans h1 h2.symm
instance : relator.right_unique (equiv.rel e) := λ a b₁ b₂ h1 h2, eq.trans h1.symm h2

What next?

[Mario Carneiro]

pick a simple predicate or construction and try to prove its isomorphism theorem

[Kevin Buzzard]

lemma rel_imp : (iff ⇒ (iff  ⇒ iff)) implies implies :=

this logic.relator file is pretty cool :-)

But didn't @Scott Morrison and/or @Simon Hudon write a bunch of this sort of code years ago?

[Kevin Buzzard]

the lemma below looks like some experimental new one way traffic system

[Kevin Buzzard]

lemma rel_iff : ((↔) ⇒ (↔) ⇒ (↔)) (↔) (↔) := ...

[Mario Carneiro]

It's a new way to write *_congr lemmas

[Mario Carneiro]

For the proof, I would just unfold the notations straight away until I know what I'm doing. The transfer tactic knows how to put the lemmas together without unfolding them

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/how.20to.20use.20transfer/near/135299706

[Kevin Buzzard]

We've talked about this stuff before and I have just about enough control of Zulip search to be able to find some of it.

[Mario Carneiro]

There's another old post where I prove isomorphism theorem for maximal ideals this way

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Perfectoid.20spaces/near/159808751

[Kevin Buzzard]

And there was definitely one where I started talking about this sort of thing and was asking how to make a transfer tactic, and Simon and Scott just talked about it for a while and then I think Scott wrote a tonne of code, and there was quite an active period during which you (Mario) were asleep, and then you woke up and checked Zulip and were like "wooah you guys have moved fast" or something. I'd really like to find that thread.

[Kevin Buzzard]

At the time I just remember not understanding the issues well enough, and hence being unable to understand the code properly

[Kevin Buzzard]

It was some code which went through a fair few primitives and proved a lemma about each of them, and then started proving lemmas about other things all hands-on.

[Kevin Buzzard]

Maybe there was also talk about using tags for transfer, and using typeclass resolution to tag more and more stuff as "still OK if replaced by isomorphic thing"

[Mario Carneiro]

oh that's right there was a respects_isomorphism typeclass IIRC

[Mario Carneiro]

I forget the actual name

[Kevin Buzzard]

Each time this transfer conversation occurs I learn quite a lot about the idea, but I still have work to do.

[Kevin Buzzard]

import data.real.basic

instance notation.sub_eq_add_neg (X : Type) [has_add X] [has_neg X] :
has_sub X := ⟨λ a b, a + -b⟩

class has_field_notation (X : Type) extends has_zero X, has_one X,
has_mul X, has_add X, has_neg X -- note: don't use has_sub
-- because it might cause a diamond now

instance : has_field_notation ℝ := by refine {};apply_instance

class complete_ordered_archimedean_field (X : Type) [has_field_notation X] : Prop :=
(all_the_axioms : ∀ x y : X, x + y = y + x) -- ...
(etc : ∀ x : X, 1 * x = 1)

-- boring proof omitted
instance cauchy_reals_are_complete : complete_ordered_archimedean_field ℝ := sorry

structure Reals :=
(X : Type)
[h : has_field_notation X]
(e : complete_ordered_archimedean_field X)

def CauchyReals : Reals :=
{ X := ℝ,
  h := by apply_instance,
  e := cauchy_reals_are_complete
}

structure ordered_field_equiv (X Y : Type) [has_field_notation X] [has_field_notation Y]
  [complete_ordered_archimedean_field X] [complete_ordered_archimedean_field Y]
  extends equiv X Y -- add extra axioms here

theorem all_reals_are_the_same (X : Type) [has_field_notation X]
  [complete_ordered_archimedean_field X] :
∃ e : ordered_field_equiv X ℝ, true := sorry -- boring proof omitted

class platonist_friendly (P : set Reals) : Prop :=
(e : ∀ X : Reals, P X ↔ P CauchyReals)

instance (P Q : set Reals) [platonist_friendly P] [platonist_friendly Q] :
platonist_friendly (P ∩ Q) := ⟨λ X, begin
  show P X ∧ Q X ↔ P CauchyReals ∧ Q CauchyReals,
  rw [_inst_1.e, _inst_2.e]
end⟩

I didn't look at your work yet, I just thought I'd try and work out some concepts with this Cauchy / Dedekind reals thing.

One could even play the same game with the Lau Rationals (the field of fractions of $\mathbb{Z}$) vs the computer science rationals in mathlib.

[Kevin Buzzard]

Is the idea that a tactic can generate instances of the platonist_friendly class, by induction on P somehow? There are no relators above so they are also clearly offering something which I've not yet understood. And finally there is this question which does not appear to be addressed by the above -- if I prove some theorem about some Bochner integral of some function being equal to pi, how do I mark this theorem with the "there is a version of me for Dedekind reals and indeed for all terms of type Reals" tag?

[Mario Carneiro]

What relators bring to the table is the ability to deal with n-ary predicates, with a variety of equivalences on the inputs (one type might be in bijection, the other is a module and there's a module iso, and then relative to the first equiv some elements a and b are related)

[Mario Carneiro]

This is necessary for making the "proof by induction" go through

[Mario Carneiro]

which is why I'm not supportive of the typeclass approach

[Mario Carneiro]

The relator way to write platonist_friendly P is (e.rel => iff) P P where e is an ordered field equiv

[Mario Carneiro]

well that's not quite accurate since you bundled Reals. Normally you would use some relation R : Reals -> Reals -> Prop asserting that the two elements of Reals are isomorphic, but in the case of Reals that's the trivially true relation

[Kevin Buzzard]

Yes, the reals are somehow an easier case, the universal predicate applies to types with field notation and is just the assertion that they're complete ordered Archimedean fields which is enough to make them "the same as" the platonic reals

[Kevin Buzzard]

I bundled subthings and morphisms of things!

import data.equiv.basic

class thing (α : Type) : Type. -- insert data here (usually notation and some axioms)

variables {α β γ: Type} [thing α] [thing β] [thing γ]

class is_subthing (s : set α) : Prop := true -- this class should not exist. Sometimes you see it in mathlib though.

set_option old_structure_cmd true

structure subthing (α : Type) [thing α] :=
(carrier : set α)
(proof : is_subthing carrier) -- replace with notation closure axioms e.g. one_mem, mul_mem etc. Note that is_subthing is never used again.

instance : has_coe_to_sort (subthing α) := ⟨_, subthing.carrier⟩

instance : has_coe (subthing α) (set α) := ⟨subthing.carrier⟩

-- another deprecated class
def is_thing_morphism (f : α → β) : Prop := true -- this class should not exist. Sometimes you see it in mathlib though.
-- I won't bother making it into a class. It's deprecated.

structure thing_morphism α β [thing α] [thing β]:=
(to_fun : α → β)
(h : is_thing_morphism to_fun) -- replace with notation-preserving axioms e.g. map_one, map_mul.... Note that `is_thing_morphism`  never occurs again

infixr ` →t `:25 := thing_morphism

instance : has_coe_to_fun (α →t β) :=
{ F := λ _, α → β,
  coe := thing_morphism.to_fun}

lemma thing_morphism.ext (f g : α →t β) : (f : α → β) = g → f = g := begin
  intro h,
  cases f,
  cases g,
  rwa thing_morphism.mk.inj_eq,
end

-- bundled equivs using old structure command so no `to_fun` problems
structure thing_equiv α β [thing α] [thing β] extends equiv α β, thing_morphism α β

infix ` ≃t `:25 := thing_equiv

namespace thing_equiv

instance : has_coe_to_fun (thing_equiv α β) := { F := λ _, α → β, coe := to_fun}

theorem ext {f g : thing_equiv α β} (h : (f : α → β) = g) : f = g :=
begin
  cases f, cases g,
  rw thing_equiv.mk.inj_eq,
  refine equiv.mk.inj _;try {assumption},
  change f_to_fun = g_to_fun at h,
  refine equiv.ext _ _ _,
  exact congr_fun h,
end

lemma coe_inj : function.injective (thing_equiv.to_equiv : thing_equiv α β → equiv α β) := begin
  intros f g h,
  apply ext,
  -- is this idiomatic?
  show ⇑(to_equiv f) = _,
  rw h,
  refl,
end

@[refl] protected def refl (α : Type) [thing α] : α ≃t α := { h := trivial,..equiv.refl α}
@[symm] protected def symm (e : α ≃t β) : β ≃t α := { h := trivial,..e.to_equiv.symm}
@[trans] protected def trans (e1 : β ≃t γ) (e2 : α ≃t β) : α ≃t γ := { h := trivial,..e2.to_equiv.trans e1.to_equiv}

-- perms
def perm (α : Type) [thing α] := thing_equiv α α

instance : has_one (perm α) := ⟨thing_equiv.refl α⟩
instance : has_mul (perm α) := ⟨thing_equiv.trans⟩ -- goodness knows if this is "right" or whether I should swap
instance : has_inv (perm α) := ⟨thing_equiv.symm⟩

instance : group (perm α) :=
{ mul := (*),
  one := 1,
  inv := λ x, x⁻¹,
  mul_assoc := λ _ _ _, ext rfl,
  one_mul := λ _, ext rfl,
  mul_one := λ _, ext rfl,
  mul_left_inv := λ f, ext $ begin funext x, exact f.left_inv x end}

end thing_equiv

I got as far as the automorphism group of a thing.

[Kevin Buzzard]

Now someone can knock off a tactic and we can just bundle everything instantly.

[Kevin Buzzard]

@Sian Carey

[Kevin Buzzard]

@Chris Hughes my understanding is that you want bundled monoid_hom but no definition of group_hom. Could there still be a group_hom namespace though?

[Kevin Buzzard]

I want to define field homomorphisms between $fields$ which I guess are called discrete_field. Chris / @Mario Carneiro -- what do you people want the bundled class to be called (discrete_field_hom, field_hom, ring_hom, semiring_hom...) and exactly what instances to you want Lean to ask for in the actual definition of the structure? (e.g. map_zero follows from map_add because everything is a field in my case of interest, so we don't need it, but I don't care if map_zero is a field or not, I just want to do it right).

[Mario Carneiro]

Are semiring_hom, ring_hom and field_hom all the same?

[Kevin Buzzard]

yes but I thought Chris was arguing that some of these things shouldn't even be tokens.

[Mario Carneiro]

Of those ring_hom is my favorite

[Kevin Buzzard]

I thought he suggested that group_hom be not defined, ->* be notation for monoid_hom which also demands map_one and just tell the user to use the right notation for group homs which happens to coincide with the notation for monoid homs. They will never have to make one with their bare hands hopefully :-)

[Mario Carneiro]

We can do the same thing with field homs - call it ring_hom, but it's really a semiring hom and you use it for semirings and fields too

[Kevin Buzzard]

If field_hom is not even defined, can there still be a field_hom namespace? Does that ever happen in mathlib?

[Mario Carneiro]

There can be a namespace

[Mario Carneiro]

Although you will miss out on dot notation

[Kevin Buzzard]

but theorems which are specific for fields, such as injectivity of the underlying map, naturally live there I think...oh, I see your point.

[Kevin Buzzard]

Is ->*+ horrible notation for a ring hom?

[Mario Carneiro]

lgtm

[Kevin Buzzard]

I want a LaTeX right-arrow with a + and a * floating over it when we're doing the controlled natural language thing; this notation is just a temporary thing

[Mario Carneiro]

You don't have to convince me, I find this kind of notation more palatable than random selections from the unicode arrow palette

[Kevin Buzzard]

@Kenny Lau what is the categorification of subring R?

[Kenny Lau]

mathematically?

[Kevin Buzzard]

Is it ring_hom A R or injective_ring_hom A R?

[Kevin Buzzard]

Is the question mathematically meaningful?

[Kenny Lau]

https://ncatlab.org/nlab/show/subobject

[Kenny Lau]

it's an isomorphism class of monomorphisms

[Kevin Buzzard]

Thanks.

[Kevin Buzzard]

So I think you're saying it's injective_ring_hom.

[Kevin Buzzard]

injective is a predicate on ring_hom.

[Kevin Buzzard]

which implies monic

[Kevin Buzzard]

Is this something to do with topologies on categories?

[Kevin Buzzard]

These categories -- lattices -- are the best categories in Lean. Do we have topologies on these categories?

[Kevin Buzzard]

structure ring_equiv (R S : Type) [ring R] [ring S] extends (R ≃ S), (R →+* S)

[Kevin Buzzard]

end of definition

[Kenny Lau]

These categories -- lattices -- are the best categories in Lean. Do we have topologies on these categories?

we have... Groethendieck topologies

[Kevin Buzzard]

Is monic an example?

[Kenny Lau]

of what?

[Kevin Buzzard]

Something that satisfies the axioms for the admissible morphisms in a grothendieck topology

[Kenny Lau]

grothendieck topology needs admissible families of morphisms right

[Kenny Lau]

I can say that { A_i -> A } is admissible if the images generate the whole ring

[Scott Morrison]

abbreviation ring_equiv (R S : Type) [ring R] [ring S] := Ring.of R ≅ Ring.of S

[Yury G. Kudryashov]

@Scott Morrison The definition with ≅ has two drawbacks.
1. It only works for R and S in the same universe.
2. It's harder to define elements of this type. Currently, ≃* etc ask for a proof of to_fun being a hom, and automatically deduce that inv is a hom.

[Kevin Buzzard]

2 can be solved with a constructor. 1 I personally don't care about because I am a mathematician

[Kevin Buzzard]

Can we use function composition notation with bundled homs? If f : thing_hom A B and g : thing_hom B C then can we have f \circ g : thing_hom A C or whichever way round you want it? Does one just overload notation in this situation?

[Yury G. Kudryashov]

Possibly, we can have something like has_comp and use it.

[Yury G. Kudryashov]

Though it means overriding notation from core.

[Yury G. Kudryashov]

(of course, we can use some other symbol)

[Scott Morrison]

... Kevin, is bring able to talk about things in different universes so important to you that you're willing to give up the completely uniform notation for morphisms, composition, isomorphism, tensor product, etc, notation that the category theory API provides?

[Kevin Buzzard]

I know I know, but the category theory API bundles objects which makes it scary. I don't know how to glue sheaves using the category theory version of sheaves.

[Kevin Buzzard]

linear_equiv is defined with the old structure command, and mul_equiv with the new one. In practice this means that mul_equiv just has a field to_equiv and then all the equiv stuff like left_inv comes off that:

import linear_algebra.basic

#print linear_equiv -- long
#print mul_equiv -- short

#check linear_equiv.left_inv -- works
#check mul_equiv.left_inv -- fails

Which is best?

[Chris Hughes]

Old structures are the best.

[Andrew Ashworth]

So the disadvantage with the new structure command is that if you want to use properties of equiv, you have to explicitly write to_equiv. The advantage of new structures is that they are faster.

[Andrew Ashworth]

My rule of thumb is: use old structures if the thing you are describing is a genuine mathematical object. Use a new structure if it's just a universal property.

[Kevin Buzzard]

So all the structures we built in the perfectoid project -- for example adic spaces -- should all be using the old structure command?

[Kevin Buzzard]

@Chris Hughes it's about time we started calling them "good old structures" and "the good old structure command".

[Andrew Ashworth]

well, they're equivalent, in a sense, so no need to rewrite things that don't need to be rewritten

[Andrew Ashworth]

in fact, if you've already done it using new structures

[Andrew Ashworth]

you should keep them that way. after all, they are faster

[Andrew Ashworth]

maybe a better rule of thumb is: use a new structure, unless you get annoyed with always having to write to_equiv

[Andrew Ashworth]

the most important difference is new structures can't have duplicate fields

[Chris Hughes]

It's just a pain to use the constructor for new structures.

[Andrew Ashworth]

yes, in the original description of new structures, Leo assumed a bunch of the tactics would be updated to transparently handle it all. Well, it didn't

[Kevin Buzzard]

We never really ran into these issues as far as I remember -- our main goal was a definition, and our structures just got bigger and bigger but we were lucky not to ever run into duplicate substructures.

[Kevin Buzzard]

The tactics didn't get updated, or they couldn't be updated?

[Andrew Ashworth]

didn't get updated

[Andrew Ashworth]

I guess also since we have no idea what's happening in Lean 4, maybe prefer and start with new structures and hope they are easier to work with whenever the new version gets released

[Andrew Ashworth]

ahh, so you see, in my last three paras I've given completely contradictory advise

[Andrew Ashworth]

I suppose I don't know which one to prefer either :)

[Kevin Buzzard]

Here's a question about mul_equivs. I really don't know how to set these up. So far I have gone for the old structure command, extending equiv and adding a field map_mul. The problem is with proving things like symmetry. I have goals like

h.to_fun ((equiv.symm (to_equiv h)).to_fun (n₁ * n₂)) =
    h.to_fun ((equiv.symm (to_equiv h)).to_fun n₁ * (equiv.symm (to_equiv h)).to_fun n₂)

which I really just want to put into a canonical form and then rewrite/simp to death. But the problem is that the canonical form of h.inv_fun seems to be h.symm when h is an equiv, and if I define symm on mul_equiv then I have to reprove stuff like symm_apply_apply in this situation.

[Kenny Lau]

yeah but the proof is just equiv.symm_apply_apply

[Kevin Buzzard]

but I can't rewrite it

[Kevin Buzzard]

In fact my first question is what the canonical notation for the inverse bijection should be with h : mul_equiv G H

[Chris Hughes]

Prove that f.symm.to_equiv = f.to_equiv.symm and make it simp

[Kevin Buzzard]

I think my issue is that I am in the middle of defining mul_equiv.symm and I am complaining about not being able to use the canonical notation h.symm when stating some intermediate result, but this is spurious because h.symm is in the process of being defined.

[Yury G. Kudryashov]

Hi, I was away for some time. It seems that monoid_hom and add_monoid_hom are already bundled. I have a few questions about the implementation:
1. Why do we repeat all the proofs instead of using to_additive? My guess is “to provide docstrings” but we can use tactic.add_doc_string. Actually, the new docstring can be turned into the second optional argument to to_additive.
2. I see that M, N, G, H is used for monoids/groups. Doesn't it break the naming conventions? I'm trying to understand how strict is the style guide w.r.t. naming convention.
3. If I want to migrate, say, polynomial.C to monoid_hom, the definition will look like def C {α} ... : α →* polynomial α, and C (1 : α) fails to coerce C to a function. It works, if I make α a mandatory argument but this is not convenient.

[Kevin Buzzard]

1. because I only really worked out the full power of to_additive today (see a thread in #general).
2. Yes it breaks the naming conventions. Computer scientists get a lot of things right about names, but I believe that one of very few exceptions is here. If a computer scientist wants to a call a group alpha and a normal subgroup beta and then some auxiliary set gamma then that's fine by me, but if we call the group G and the normal subgroup N and the auxiliary set S then it is much easier to see at a glance what is happening, especially if variables are being used and the definitions of alpha and beta are 150 lines up.
3. Probably @Chris Hughes will have something to say on the matter.

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/to_additive.20and.20tags

[Kevin Buzzard]

See https://github.com/leanprover-community/mathlib/blob/659533e1dc63074d3386ffb8b2fbed50151dd34c/src/group_theory/submonoid.lean#L344 for the kind of code I am writing now. I think this is better -- I repeat almost nothing.

[Yury G. Kudryashov]

@Kevin Buzzard Thanks for explanations. I'd like to help with migrating to bundled hom. What can I work on to avoid duplication of effort?

[Kevin Buzzard]

You would be more than welcome to help @Amelia Livingston and me with all the to_additive stuff. As you can see we got up to line 569. Amelia also refactored localisation.lean in that branch, to see how things look with the changes, and they seemed fine. We did not think about polynomials though.

[Yury G. Kudryashov]

E.g., I can rewrite algebra/group/hom using to_additive. Is it OK?

[Kevin Buzzard]

Here's a message I sent Amelia earlier today:

So what I currently believe is this. Say you have made 10 definitions and proved 20 lemmas in the namespace submonoid and you want to get additive versions in add_submonoid. The one thing which can almost always be avoided is having to write out a proof twice, once in the multiplicative and once in the additive case.

The best possible scenario is when defining a lemma; in this case you can use @[to_additive add_submonoid.foo] and that might be almost all you need to do; this will hopefully generate the proof automatically. Unfortunately it doesn't generate the docstring automatically and you have to add it with this run_cmd which which I don't really understand. There are plenty of examples in the commit I pushed today (all in this bundled_submonoids branch of mathlib).

More complicated is a definition. I have been writing definition submonoid.foo ..., getting it working, and then writing #print prefix submonoid.foo (note that you need submonoid even if you're in the submonoid namespace). You then see submonoid.foo but also perhaps submonoid.foo.match_1 or submonoid.foo.equations_eqn3 or something. For structures you see loads of things. After the definition you can write to_additive [add_submonoid.foo.proof_3] submonoid.foo.proof_3 and this needs to be done for everything in the output. However it all has to be done in the right order. If you get red squiggles under a to_additive then look at the error, see if it mentions add_submonoid.foo.equation_2 and then move the corresponding to_additive line above the line with the error. In all cases I got this to work. And don't forget the docstring. Note that in one case the errors I got were errors involving functions which I had not defined -- other people had missed out the to_additive tags on other functions, so I had to add those in (they should probably be moved to the correct part of mathlib at some point).

Even more complicated is a structure. I have been defining the additive ones by hand. And there are some lemmas or definitions which don't port, for example those involving powers x^n turn into ones involving smultiples n \bub x and because the order got switched to_additive sometimes can't handle it. In these cases I leave the submonoid namespace immediately, define the additive one by hand (i.e. write the same code again), do all the to_additive tags and the docstring, and then go back into the submonoid namespace. You then have to re-input all the variables which you had open in that namespace. Variables outside a namespace survive inside it, but variables inside a namespace die once the namespace is closed, even if you go back in.

[Kevin Buzzard]

Everything we have done is in the bundled_submonoids branch of mathlib and our plan was to finish submonoid.lean and then make a PR.

[Kevin Buzzard]

We didn't touch the hom file so it will be OK.

[Yury G. Kudryashov]

Probably, one of us should learn more about Lean tactic language, and let to_additive handle mydef._proof_n and all those mystruct.cases_on etc.
Another idea is to have @[bundled_hom] user attr that defines has_coe_to_fun and restates all axioms using coe instead of f.to_fun.

[Yury G. Kudryashov]

OK, then I'll go through hom, then I'll try to migrate concrete categories (Mon etc.) to bundled homs.

[Kevin Buzzard]

Bundling group and monoid and ring stuff (subthings, homs and isomorphisms) is just a one-off job which needs to be done once. The reason I am motivated to do it now is because I think it makes it easier for mathematicians -- but I am not sure about this. Other people also believe it's best to do things like bundle homs and subobjects, for other reasons. What became clear to me was that the task of actually removing unbundled homs and replacing them with bundled ones is a vast task, because is_submonoid appears 200 times in the library and one of the appearances is in the definition of is_subgroup which appears 200 more times, and then is_subring uses both of these etc etc.

[Kevin Buzzard]

Furthermore, the switch would be one huge PR which would take a very long time to write and would have to constantly be playing catch-up with the library. This sounded very unappealing. So my plan is to bundle stuff, leave the unbundled stuff in for now (but mention that it is deprecated in docstrings) and then start changing leaf nodes to see if things work. Amelia changed localisation.lean and it worked fine. But changing stuff deeper in mathlib is painful. So our plan is to work from the outside in. The disadvantage of our approach is that ultimately it will in some sense be more work, probably. The advantage is that we can access bundled homs immediately, which is what I wanted really.

[Patrick Massot]

I'm very worried about this thread. For the sensitivity conjecture project, I worked seriously with linear maps for the first time. They are bundled, and it simply does not work. The coercion to function works completely randomly, and there are instance search timeout all over the place. It's extremely time-consuming and frustrating to fight that

[Mario Carneiro]

Bundled maps have much lower pressure on the typeclass system, because you aren't inferring the fact that the function is a hom anymore

[Mario Carneiro]

I can believe that the coercion is problematic sometimes though. The alternative is to write .to_fun

[Patrick Massot]

but coercions are part of the type class system

[Patrick Massot]

The alternative doesn't work, because lemmas are stated without .to_fun

[Mario Carneiro]

Personally, I would happily live with to_fun everywhere. I put the coercions in because you guys are always going on about nice looking notation and lean 3 provides few other opportunities for this kind of thing

[Patrick Massot]

This is really sad

[Yury G. Kudryashov]

/me prefers Python-style obj.__call__ convention over typeclass resolution

[Mario Carneiro]

I agree completely (to both statements)

[Yury G. Kudryashov]

@Mario Carneiro What's are the other opportunities in Lean 3 for this kind of thing?

[Mario Carneiro]

for zero-notation functions, nothing, but if you are willing to accept a character or two you can use a notation

[Yury G. Kudryashov]

BTW, what's wrong with dropping has_coe_to_fun and using f.1?

[Yury G. Kudryashov]

Forgot to tag @Kevin Buzzard

[Patrick Massot]

This is really not how we think about maps

[Yury G. Kudryashov]

@Patrick Massot I see the following options:
1. the old way; pros: already implemented; easy to say that the same map can be is_mul_hom or is_monoid_hom under different assumptions; cons: need to find is_*_hom instances here and there; what else?
2. bundled homs, implicit coercion; pros: map_mul and map_one are right there; M →* N is exactly Mon.of M \--> Mon.of N (not yet); cons: need to find has_coe_to_fun every time; sometimes this coercion fails;
3. bundled homs, f.1; pros: see 2 + no class instance resolution at all; cons: unnatural notation.
What do I miss?

[Patrick Massot]

I don't see what I could add here. Type class inference doesn't work in Lean 3, and it doesn't provide error messages

[Patrick Massot]

2. Yes it breaks the naming conventions. Computer scientists get a lot of things right about names, but I believe that one of very few exceptions is here. If a computer scientist wants to a call a group alpha and a normal subgroup beta and then some auxiliary set gamma then that's fine by me, but if we call the group G and the normal subgroup N and the auxiliary set S then it is much easier to see at a glance what is happening, especially if variables are being used and the definitions of alpha and beta are 150 lines up.

I also wanted to comment on that. The linear algebra library uses the random greek letter convention, and it's really a nightmare. They are lots of type involved, and not knowing which one is meant to be a base field, an indexing type or a vector space is really awful. They are tons of lemmas whose statements are very hard to parse, and would be very easy with reasonable type naming conventions.

[Yury G. Kudryashov]

Then maybe docs/contribute/naming.md should be adjusted.

[Yury G. Kudryashov]

With some sensible theory-specific naming conventions.

[Patrick Massot]

I'd love that

[Kevin Buzzard]

+1 from me.

[Kevin Buzzard]

@Yury G. Kudryashov the reason I'm bundling is because the community seems to think it's the best idea. To a certain extent it might just be about experimenting to find out what works best. I have seen coercions fail before and you can just write (f : G -> H) to make them happen; I quite like that notation

[Kevin Buzzard]

The one place where I feel that the alpha beta notation is natural is when dealing with types that really are that -- just types. For example equiv alpha beta seems fine to me because for all I know this is what computer scientists really call types. But types which are playing a mathematical role such as groups have got such a history of notation behind them and it's used to guide readers, and I don't see the point of throwing it away. Sure some people use $k$ for a number field and some use $K$, but nobody uses $\alpha$. The number field library that will one day be written will need to choose a notation, but it should, in my opinion, use one which is already in use.

[Andrew Ashworth]

morally speaking isn't it [G : group alpha]?

[Scott Morrison]

It is really unfortunate the coercions to function types barely work. I think this is the main pain point with bundling.

[Yury G. Kudryashov]

@Andrew Ashworth Groups are not bundled, so after [G : group α] you still have to say x : α, and this is not very readable, especially if you have, e.g., a group acting on a space.

[Kevin Buzzard]

Mathematicians read x : α as $x\in\alpha$ and they are far more used to $g\in G$. In fact this is in some sense exactly the point -- if I see $g\in G$ in the middle of a maths paper without any context then I would be likely to guess that $G$ was a group and $g$ an element. If I see x : α in a library file then I have no clue.

[Yury G. Kudryashov]

@Kevin Buzzard I rewrote to_additive to automatically take care of many things. I'll try to PR it tonight or tomorrow. Current state (no docs, WIP) is available at https://github.com/urkud/mathlib/blob/to_additive/src/algebra/group/to_additive.lean

[Yury G. Kudryashov]

Namely, (1) it automatically adds to_additive attribute to structure fields; (2) it looks for prefixes in dict instead of full names; (3) it automatically transfers decl._proof_1, decl._match_1 etc . With (2), we don't need to have attribute [to_additive add_monoid_hom.cases_on] monoid_hom.cases_on etc.

[Kevin Buzzard]

I'm away from Lean until Monday (camping)

[Kevin Buzzard]

Feel free to take a look at the bundled submonoids branch

[Yury G. Kudryashov]

@Kevin Buzzard Good luck with camping!

[Kevin Buzzard]

@Amelia Livingston did you push everything you have? The submonoid.lean file is half toadditiveised

[Amelia Livingston]

Not yet, I'm tidying things up a bit but I will push today. I've not toadditiveised anything yet.

[Yury G. Kudryashov]

@Amelia Livingston It should be easier to use @[to_additive] with my changes, so you should probably postpone to_additiveisation for a day or two. I'll try to tidy my patch tonight.

[Amelia Livingston]

Okay. Thank you for working on it!

[Yury G. Kudryashov]

@Amelia Livingston I pushed a new version of @[to_additive] to the to_additive branch of urkud/mathlib.
It automates:

• mapping of structure fields;
• mapping of hidden defs like name._proof_1, name._match_1;
• mapping of projections like semigroup.to_has_mul (relies on @[ancestor] attributes);
• mapping of name.cases_on by mapping prefixes instead of names.

[Yury G. Kudryashov]

Other items I want to add before making a PR:

• take docstring as an optional argument; alternative is to use run_cmd add_doc_string after each definition;
• autogenerate target namespace using to_additive_attr.get_param src.get_prefix; ask for the suffix only;
• make “target name” argument optional;
  • simple: use the same suffix as in the source name, e.g. monoid_hom.comp → add_monoid_hom.comp;
  • advanced: parse suffix replacing mul→add, one→zero, prod→sum (what else?).
• automatically create target.equations._eqn_1.

[Yury G. Kudryashov]

@Mario Carneiro what is responsible for creating my_name.equations._eqn_1? Is it intentional that this thing is called after normal defs but not after add_decls?

[Floris van Doorn]

I think it's the equation compiler who adds those equalities. add_decl (and its relatives, like add_inductive) indeed doesn't have the same side effects (like creating auxiliary definitions) as adding a declaration normally. It's probably useful to have both the version with and without side-effects, and it was suggested previously to expose versions with side effects in the community fork of Lean.

[Yury G. Kudryashov]

@Floris van Doorn Then I'll postpone automatic handling of equations till we have add_decl_with_side_effects.

[Mario Carneiro]

it's already available in community lean

[Yury G. Kudryashov]

See https://github.com/leanprover-community/mathlib/pull/1345 for the new to_additive. It seems that I've broken compilation in one of the last commits. I'll fix it tonight.