## Stream: maths

### Topic: bundling mul_homs

#### Kevin Buzzard (Jul 18 2019 at 04:21):

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 (Jul 18 2019 at 04:22):

mul_equiv A B extends equiv A B, mul_hom A B

#### Kevin Buzzard (Jul 18 2019 at 04:23):

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

#### Mario Carneiro (Jul 18 2019 at 04:23):

old structures FTW

#### Kevin Buzzard (Jul 18 2019 at 04:23):

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

#### Kevin Buzzard (Jul 18 2019 at 04:23):

Did I name it wrong?

I don't think so

#### Mario Carneiro (Jul 18 2019 at 04:24):

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

#### Kevin Buzzard (Jul 18 2019 at 04:24):

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 (Jul 18 2019 at 04:24):

I don't see mul.hom in the example

Oh there it is

#### Kevin Buzzard (Jul 18 2019 at 04:25):

I'm talking about my attempt to bundle homs.

#### Mario Carneiro (Jul 18 2019 at 04:25):

I think that should be mul_hom

#### Mario Carneiro (Jul 18 2019 at 04:25):

mul isn't a namespace

#### Mario Carneiro (Jul 18 2019 at 04:26):

mul_hom should have a field called to_fun

#### Mario Carneiro (Jul 18 2019 at 04:26):

so that mul_equiv works

#### Kevin Buzzard (Jul 18 2019 at 04:31):

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 (Jul 18 2019 at 04:32):

it's a function called to_mul_hom

#### Mario Carneiro (Jul 18 2019 at 04:32):

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

#### Mario Carneiro (Jul 18 2019 at 04:34):

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

#### Kevin Buzzard (Jul 18 2019 at 04:55):

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?

yes

#### Kevin Buzzard (Jul 18 2019 at 05:03):

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 (Jul 18 2019 at 05:04):

with the primes inverted

#### Kevin Buzzard (Jul 18 2019 at 05:04):

So you're saying I need to change mathlib

no

#### Kevin Buzzard (Jul 18 2019 at 05:05):

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

yes

#### Kevin Buzzard (Jul 18 2019 at 05:25):

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?

yes

#### Kevin Buzzard (Jul 18 2019 at 05:56):

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 (Jul 18 2019 at 06:00):

People will complain about the order of arguments to comp

#### Johan Commelin (Jul 18 2019 at 06:01):

@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 (Jul 18 2019 at 06:01):

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

#### Johan Commelin (Jul 18 2019 at 06:02):

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 (Jul 18 2019 at 06:02):

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

#### Kevin Buzzard (Jul 18 2019 at 06:25):

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 (Jul 18 2019 at 11:49):

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 (Jul 18 2019 at 11:50):

Note that we can define group.hom to be mul_hom

#### Chris Hughes (Jul 18 2019 at 12:08):

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 (Jul 18 2019 at 12:16):

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

#### Kevin Buzzard (Jul 18 2019 at 12:16):

What should the custom constructor be called?

#### Chris Hughes (Jul 18 2019 at 12:26):

Yes @[reducible] def group_hom := monoid_hom.

group_hom.mk

#### Chris Hughes (Jul 18 2019 at 12:27):

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

#### Kevin Buzzard (Jul 18 2019 at 18:15):

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 (Jul 18 2019 at 18:18):

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

#### Kevin Buzzard (Jul 18 2019 at 18:19):

I am just experimenting. I will certainly report back.

#### Johan Commelin (Jul 18 2019 at 18:21):

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 (Jul 18 2019 at 18:22):

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

#### Johan Commelin (Jul 18 2019 at 18:22):

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 (Jul 18 2019 at 18:22):

Nope, that's not true.

#### Kevin Buzzard (Jul 18 2019 at 18:22):

and making it reducible

#### Johan Commelin (Jul 18 2019 at 18:22):

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

#### Johan Commelin (Jul 18 2019 at 18:23):

Even if vector_space is reducibly defined to be a module.

#### Johan Commelin (Jul 18 2019 at 18:23):

This has bitten me several times.

#### Kevin Buzzard (Jul 18 2019 at 18:24):

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 (Jul 18 2019 at 18:24):

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

#### Johan Commelin (Jul 18 2019 at 18:24):

I want to propose/discuss just ditching group_hom altogether.

#### Johan Commelin (Jul 18 2019 at 18:25):

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

#### Johan Commelin (Jul 18 2019 at 18:25):

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

#### Kevin Buzzard (Jul 18 2019 at 18:26):

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 (Jul 18 2019 at 18:27):

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

#### Johan Commelin (Jul 18 2019 at 18:27):

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

#### Johan Commelin (Jul 18 2019 at 18:28):

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

#### Chris Hughes (Jul 18 2019 at 18:28):

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 (Jul 18 2019 at 18:29):

For the same reason that vector_space shouldn't exist?

#### Kevin Buzzard (Jul 18 2019 at 18:34):

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 (Jul 18 2019 at 18:35):

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 (Jul 18 2019 at 18:37):

We tell them to use M1 =* M2.

#### Johan Commelin (Jul 18 2019 at 18:37):

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

#### Johan Commelin (Jul 18 2019 at 18:37):

Or whatever the notation for monoid homs will be.

#### Chris Hughes (Jul 18 2019 at 18:41):

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

#### Kevin Buzzard (Jul 18 2019 at 19:11):

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 (Jul 18 2019 at 19:16):

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

#### Kevin Buzzard (Jul 18 2019 at 20:12):

then what term is ->* notation for?

#### Kevin Buzzard (Jul 18 2019 at 20:12):

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 (Jul 18 2019 at 20:13):

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

monoid homs

#### Kevin Buzzard (Jul 18 2019 at 20:14):

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 (Jul 18 2019 at 20:15):

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

#### Kevin Buzzard (Jul 18 2019 at 20:15):

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 (Jul 18 2019 at 20:15):

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

#### Kevin Buzzard (Jul 18 2019 at 20:16):

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 (Jul 18 2019 at 20:17):

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

#### Johan Commelin (Jul 18 2019 at 20:17):

I think this is quite a nice solution.

#### Kevin Buzzard (Jul 18 2019 at 20:19):

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

#### Johan Commelin (Jul 18 2019 at 20:19):

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 (Jul 18 2019 at 20:20):

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 (Jul 18 2019 at 20:20):

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

#### Kevin Buzzard (Jul 18 2019 at 20:21):

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

#### Johan Commelin (Jul 18 2019 at 20:21):

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

#### Kevin Buzzard (Jul 18 2019 at 20:22):

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

#### Johan Commelin (Jul 18 2019 at 20:22):

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

#### Johan Commelin (Jul 18 2019 at 20:22):

But people don't really seem to care.

#### Kevin Buzzard (Jul 18 2019 at 20:26):

@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 (Jul 18 2019 at 20:41):

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 (Jul 18 2019 at 20:44):

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 (Jul 18 2019 at 20:44):

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 (Jul 18 2019 at 20:44):

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

#### Kevin Buzzard (Jul 18 2019 at 20:45):

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 (Jul 18 2019 at 20:47):

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 (Jul 18 2019 at 20:50):

I heartily disagree

#### Kevin Buzzard (Jul 18 2019 at 20:50):

"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 (Jul 18 2019 at 20:50):

that one is not proving trivial to implement

#### Mario Carneiro (Jul 18 2019 at 20:50):

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

#### Mario Carneiro (Jul 18 2019 at 20:51):

which is setting yourself up for failure

#### Kevin Buzzard (Jul 18 2019 at 20:51):

You guys worry too much about these tedious implementation issues

#### Mario Carneiro (Jul 18 2019 at 20:52):

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

#### Kevin Buzzard (Jul 18 2019 at 20:52):

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

#### Kevin Buzzard (Jul 18 2019 at 20:52):

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

#### Mario Carneiro (Jul 18 2019 at 20:52):

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 (Jul 18 2019 at 20:56):

implementing transfer is hard because type theory is big and complicated

#### Kevin Buzzard (Jul 18 2019 at 20:57):

You should just solve it with pointers or something

:expressionless:

#### Mario Carneiro (Jul 18 2019 at 21:05):

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 (Jul 18 2019 at 21:08):

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 (Jul 18 2019 at 21:09):

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

#### Mario Carneiro (Jul 18 2019 at 21:11):

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

#### Mario Carneiro (Jul 18 2019 at 21:13):

I think that statement showed up in one of the answers

#### Kevin Buzzard (Jul 18 2019 at 21:13):

Was it the one I accepted?

#### Mario Carneiro (Jul 18 2019 at 21:15):

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

#### Mario Carneiro (Jul 18 2019 at 21:16):

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 (Jul 18 2019 at 21:16):

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

#### Mario Carneiro (Jul 18 2019 at 21:17):

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

#### Mario Carneiro (Jul 18 2019 at 21:17):

Andrej usually has interesting things to say

#### Mario Carneiro (Jul 18 2019 at 21:20):

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 (Jul 18 2019 at 21:22):

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 (Jul 18 2019 at 21:22):

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

#### Kevin Buzzard (Jul 18 2019 at 21:32):

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 (Jul 18 2019 at 21:34):

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

#### Mario Carneiro (Jul 18 2019 at 21:34):

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 (Jul 18 2019 at 21:34):

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

#### Kevin Buzzard (Jul 18 2019 at 21:34):

So tell me again what transfer specifically means?

#### Mario Carneiro (Jul 18 2019 at 21:35):

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 (Jul 18 2019 at 21:36):

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 (Jul 18 2019 at 21:36):

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

not particularly

#### Kevin Buzzard (Jul 18 2019 at 21:36):

So we may as well start right away :-)

#### Mario Carneiro (Jul 18 2019 at 21:37):

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

#### Kevin Buzzard (Jul 18 2019 at 21:37):

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

#### Mario Carneiro (Jul 18 2019 at 21:37):

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

no

#### Mario Carneiro (Jul 18 2019 at 21:37):

meta code comes later

#### Mario Carneiro (Jul 18 2019 at 21:38):

proofs come first

#### Mario Carneiro (Jul 18 2019 at 21:40):

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 (Jul 18 2019 at 21:40):

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 (Jul 18 2019 at 21:40):

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

#### Mario Carneiro (Jul 18 2019 at 21:41):

You don't, that's the problem

#### Kevin Buzzard (Jul 18 2019 at 21:41):

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

#### Kevin Buzzard (Jul 18 2019 at 21:42):

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

#### Kevin Buzzard (Jul 18 2019 at 21:42):

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

#### Mario Carneiro (Jul 18 2019 at 21:42):

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

#### Kevin Buzzard (Jul 18 2019 at 21:42):

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 (Jul 18 2019 at 21:43):

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

#### Kevin Buzzard (Jul 18 2019 at 21:43):

So what formally is the problem?

#### Mario Carneiro (Jul 18 2019 at 21:43):

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 (Jul 18 2019 at 21:43):

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

#### Kevin Buzzard (Jul 18 2019 at 21:44):

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

It is

#### Kevin Buzzard (Jul 18 2019 at 21:44):

You just peel P apart and do it by induction

Yes, so do it

#### Kevin Buzzard (Jul 18 2019 at 21:44):

You mean it's hard to implement?

No, it's easy

but it's work

#### Kevin Buzzard (Jul 18 2019 at 21:45):

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

#### Mario Carneiro (Jul 18 2019 at 21:45):

and it needs to actually be in mathlib

It's not maths.

#### Mario Carneiro (Jul 18 2019 at 21:45):

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

#### Kevin Buzzard (Jul 18 2019 at 21:45):

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 (Jul 18 2019 at 21:46):

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

#### Kevin Buzzard (Jul 18 2019 at 21:46):

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

#### Mario Carneiro (Jul 18 2019 at 21:46):

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

#### Mario Carneiro (Jul 18 2019 at 21:46):

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

#### Kevin Buzzard (Jul 18 2019 at 21:46):

So what needs doing in practice?

#### Kevin Buzzard (Jul 18 2019 at 21:47):

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

#### Mario Carneiro (Jul 18 2019 at 21:47):

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

#### Kevin Buzzard (Jul 18 2019 at 21:47):

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

#### Kevin Buzzard (Jul 18 2019 at 21:47):

So what is the type of equiv.rel?

#### Mario Carneiro (Jul 18 2019 at 21:48):

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

#### Mario Carneiro (Jul 18 2019 at 21:49):

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 (Jul 18 2019 at 21:49):

oh so that one's done now, right?

#### Mario Carneiro (Jul 18 2019 at 21:50):

You need a few theorems about it

#### Mario Carneiro (Jul 18 2019 at 21:50):

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

#### Kevin Buzzard (Jul 18 2019 at 21:50):

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

#### Mario Carneiro (Jul 18 2019 at 21:50):

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

#### Mario Carneiro (Jul 18 2019 at 21:51):

I think left_unique and right_unique are typeclasses

#### Mario Carneiro (Jul 18 2019 at 21:52):

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

#### Kevin Buzzard (Jul 18 2019 at 21:57):

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 (Jul 18 2019 at 21:58):

e is an equiv

#### Mario Carneiro (Jul 18 2019 at 21:59):

not a fancy equiv, just an equiv

#### Mario Carneiro (Jul 18 2019 at 22:00):

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

#### Jeremy Avigad (Jul 18 2019 at 22:00):

@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 (Jul 18 2019 at 22:11):

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

#### Kevin Buzzard (Jul 18 2019 at 23:10):

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

#### Kevin Buzzard (Jul 18 2019 at 23:10):

Everything is already there, in Dedekind.

#### Andrew Ashworth (Jul 19 2019 at 10:57):

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 (Jul 19 2019 at 18:22):

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 (Jul 19 2019 at 18:24): pick a simple predicate or construction and try to prove its isomorphism theorem #### Kevin Buzzard (Jul 19 2019 at 19:02): 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 (Jul 19 2019 at 19:02): the lemma below looks like some experimental new one way traffic system #### Kevin Buzzard (Jul 19 2019 at 19:02): lemma rel_iff : ((↔) ⇒ (↔) ⇒ (↔)) (↔) (↔) := ...  #### Mario Carneiro (Jul 19 2019 at 19:03): It's a new way to write *_congr lemmas #### Mario Carneiro (Jul 19 2019 at 19:04): 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 (Jul 19 2019 at 19:06): https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/how.20to.20use.20transfer/near/135299706 #### Kevin Buzzard (Jul 19 2019 at 19:07): 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 (Jul 19 2019 at 19:08): There's another old post where I prove isomorphism theorem for maximal ideals this way #### Mario Carneiro (Jul 19 2019 at 19:08): https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Perfectoid.20spaces/near/159808751 #### Kevin Buzzard (Jul 19 2019 at 19:09): 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 (Jul 19 2019 at 19:10): At the time I just remember not understanding the issues well enough, and hence being unable to understand the code properly #### Kevin Buzzard (Jul 19 2019 at 19:11): 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 (Jul 19 2019 at 19:12): 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 (Jul 19 2019 at 19:12): oh that's right there was a respects_isomorphism typeclass IIRC #### Mario Carneiro (Jul 19 2019 at 19:13): I forget the actual name #### Kevin Buzzard (Jul 19 2019 at 19:13): Each time this transfer conversation occurs I learn quite a lot about the idea, but I still have work to do. #### Kevin Buzzard (Jul 19 2019 at 23:55): 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 (Jul 20 2019 at 00:02): 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 (Jul 20 2019 at 00:22): 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 (Jul 20 2019 at 00:23): This is necessary for making the "proof by induction" go through #### Mario Carneiro (Jul 20 2019 at 00:23): which is why I'm not supportive of the typeclass approach #### Mario Carneiro (Jul 20 2019 at 00:25): The relator way to write platonist_friendly P is (e.rel => iff) P P where e is an ordered field equiv #### Mario Carneiro (Jul 20 2019 at 00:28): 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 (Jul 20 2019 at 08:55): 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 (Jul 21 2019 at 02:25): 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 (Jul 21 2019 at 02:31):

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

@Sian Carey

#### Kevin Buzzard (Jul 21 2019 at 04:14):

@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 (Jul 21 2019 at 04:45):

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 (Jul 21 2019 at 04:47):

Are semiring_hom, ring_hom and field_hom all the same?

#### Kevin Buzzard (Jul 21 2019 at 04:47):

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

#### Mario Carneiro (Jul 21 2019 at 04:48):

Of those ring_hom is my favorite

#### Kevin Buzzard (Jul 21 2019 at 04:49):

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 (Jul 21 2019 at 04:50):

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 (Jul 21 2019 at 04:50):

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

#### Mario Carneiro (Jul 21 2019 at 04:50):

There can be a namespace

#### Mario Carneiro (Jul 21 2019 at 04:51):

Although you will miss out on dot notation

#### Kevin Buzzard (Jul 21 2019 at 04:52):

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 (Jul 21 2019 at 04:53):

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

lgtm

#### Kevin Buzzard (Jul 21 2019 at 04:54):

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 (Jul 21 2019 at 04:56):

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 (Jul 21 2019 at 04:56):

@Kenny Lau what is the categorification of subring R?

mathematically?

#### Kevin Buzzard (Jul 21 2019 at 04:57):

Is it ring_hom A R or injective_ring_hom A R?

#### Kevin Buzzard (Jul 21 2019 at 04:57):

Is the question mathematically meaningful?

#### Kenny Lau (Jul 21 2019 at 04:57):

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

#### Kenny Lau (Jul 21 2019 at 04:57):

it's an isomorphism class of monomorphisms

Thanks.

#### Kevin Buzzard (Jul 21 2019 at 05:03):

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

#### Kevin Buzzard (Jul 21 2019 at 05:04):

injective is a predicate on ring_hom.

#### Kevin Buzzard (Jul 21 2019 at 05:04):

which implies monic

#### Kevin Buzzard (Jul 21 2019 at 05:05):

Is this something to do with topologies on categories?

#### Kevin Buzzard (Jul 21 2019 at 05:07):

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

#### Kevin Buzzard (Jul 21 2019 at 05:23):

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


#### Kevin Buzzard (Jul 21 2019 at 05:24):

end of definition

#### Kenny Lau (Jul 21 2019 at 05:41):

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

we have... Groethendieck topologies

#### Kevin Buzzard (Jul 21 2019 at 06:47):

Is monic an example?

of what?

#### Kevin Buzzard (Jul 21 2019 at 06:58):

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

#### Kenny Lau (Jul 21 2019 at 07:01):

grothendieck topology needs admissible families of morphisms right

#### Kenny Lau (Jul 21 2019 at 07:01):

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

#### Scott Morrison (Jul 21 2019 at 08:14):

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

#### Yury G. Kudryashov (Jul 21 2019 at 09:10):

@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 (Jul 21 2019 at 12:10):

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

#### Kevin Buzzard (Jul 21 2019 at 15:43):

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 (Jul 21 2019 at 18:42):

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

#### Yury G. Kudryashov (Jul 21 2019 at 18:43):

Though it means overriding notation from core.

#### Yury G. Kudryashov (Jul 21 2019 at 18:44):

(of course, we can use some other symbol)

#### Scott Morrison (Jul 21 2019 at 20:13):

... 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 (Jul 21 2019 at 21:04):

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 (Jul 28 2019 at 18:42):

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 (Jul 28 2019 at 19:51):

Old structures are the best.

#### Andrew Ashworth (Jul 28 2019 at 19:51):

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 (Jul 28 2019 at 19:53):

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 (Jul 28 2019 at 19:56):

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

#### Kevin Buzzard (Jul 28 2019 at 19:57):

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

#### Andrew Ashworth (Jul 28 2019 at 19:57):

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

#### Andrew Ashworth (Jul 28 2019 at 19:57):

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

#### Andrew Ashworth (Jul 28 2019 at 19:57):

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

#### Andrew Ashworth (Jul 28 2019 at 20:01):

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

#### Andrew Ashworth (Jul 28 2019 at 20:03):

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

#### Chris Hughes (Jul 28 2019 at 20:05):

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

#### Andrew Ashworth (Jul 28 2019 at 20:06):

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 (Jul 28 2019 at 20:07):

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 (Jul 28 2019 at 20:07):

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

#### Andrew Ashworth (Jul 28 2019 at 20:07):

didn't get updated

#### Andrew Ashworth (Jul 28 2019 at 20:09):

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 (Jul 28 2019 at 20:10):

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

#### Andrew Ashworth (Jul 28 2019 at 20:11):

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

#### Kevin Buzzard (Jul 29 2019 at 15:46):

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 (Jul 29 2019 at 15:48):

yeah but the proof is just equiv.symm_apply_apply

#### Kevin Buzzard (Jul 29 2019 at 15:48):

but I can't rewrite it

#### Kevin Buzzard (Jul 29 2019 at 15:49):

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

#### Chris Hughes (Jul 29 2019 at 15:51):

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

#### Kevin Buzzard (Jul 29 2019 at 15:51):

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 (Aug 09 2019 at 18:40):

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 (Aug 09 2019 at 18:43):

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 (Aug 09 2019 at 18:45):

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 (Aug 09 2019 at 18:48):

@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 (Aug 09 2019 at 18:50):

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 (Aug 09 2019 at 18:51):

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

#### Kevin Buzzard (Aug 09 2019 at 18:51):

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).

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 (Aug 09 2019 at 18:53):

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 (Aug 09 2019 at 18:55):

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

#### Yury G. Kudryashov (Aug 09 2019 at 18:55):

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 (Aug 09 2019 at 18:57):

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

#### Kevin Buzzard (Aug 09 2019 at 18:58):

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 (Aug 09 2019 at 19:01):

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 (Aug 09 2019 at 19:54):

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 (Aug 09 2019 at 19:57):

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 (Aug 09 2019 at 19:58):

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

#### Patrick Massot (Aug 09 2019 at 19:58):

but coercions are part of the type class system

#### Patrick Massot (Aug 09 2019 at 19:58):

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

#### Mario Carneiro (Aug 09 2019 at 19:59):

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

#### Yury G. Kudryashov (Aug 09 2019 at 20:00):

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

#### Mario Carneiro (Aug 09 2019 at 20:01):

I agree completely (to both statements)

#### Yury G. Kudryashov (Aug 09 2019 at 20:09):

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

#### Mario Carneiro (Aug 09 2019 at 20:10):

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

#### Yury G. Kudryashov (Aug 09 2019 at 20:12):

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

#### Yury G. Kudryashov (Aug 09 2019 at 20:13):

Forgot to tag @Kevin Buzzard

#### Patrick Massot (Aug 09 2019 at 20:13):

This is really not how we think about maps

#### Yury G. Kudryashov (Aug 09 2019 at 20:22):

@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 (Aug 09 2019 at 20:55):

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 (Aug 09 2019 at 21:02):

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 (Aug 09 2019 at 21:10):

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

#### Yury G. Kudryashov (Aug 09 2019 at 21:10):

With some sensible theory-specific naming conventions.

I'd love that

+1 from me.

#### Kevin Buzzard (Aug 09 2019 at 22:12):

@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 (Aug 09 2019 at 23:03):

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 (Aug 10 2019 at 00:50):

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

#### Scott Morrison (Aug 10 2019 at 01:07):

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

#### Yury G. Kudryashov (Aug 10 2019 at 08:44):

@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 (Aug 10 2019 at 09:12):

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 (Aug 15 2019 at 17:48):

@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 (Aug 15 2019 at 17:51):

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 (Aug 15 2019 at 17:52):

I'm away from Lean until Monday (camping)

#### Kevin Buzzard (Aug 15 2019 at 17:52):

Feel free to take a look at the bundled submonoids branch

#### Yury G. Kudryashov (Aug 15 2019 at 17:53):

@Kevin Buzzard Good luck with camping!

#### Kevin Buzzard (Aug 15 2019 at 17:53):

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

#### Amelia Livingston (Aug 15 2019 at 17:55):

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

#### Yury G. Kudryashov (Aug 15 2019 at 18:09):

@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 (Aug 15 2019 at 18:10):

Okay. Thank you for working on it!

#### Yury G. Kudryashov (Aug 16 2019 at 14:49):

@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 (Aug 16 2019 at 15:03):

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.compadd_monoid_hom.comp;
• advanced: parse suffix replacing mul→add, one→zero, prod→sum (what else?).
• automatically create target.equations._eqn_1.

#### Yury G. Kudryashov (Aug 16 2019 at 15:16):

@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 (Aug 16 2019 at 15:35):

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 (Aug 16 2019 at 15:51):

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

#### Mario Carneiro (Aug 16 2019 at 16:58):

it's already available in community lean

#### Yury G. Kudryashov (Aug 18 2019 at 15:42):

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.

Last updated: May 11 2021 at 15:12 UTC