## Stream: general

### Topic: cerw

#### Johan Commelin (Nov 18 2018 at 18:23):

I am a complete newbie when it comes to tactic writing. Here is a request for a tactic, and I have no idea how realistic it is. Suppose I have an isomorphism h : X ≅ Y in some category C. And suppose I have some other term foo : bar X, then I would like to have a tactic cerw (category-erw) that tries to figure out if bar is some sort of category_theory.functor.obj and if so, replaces X with Y.
I realise this request is a bit vague. I would be happy to flesh out the details.

HI Johan,

#### Scott Morrison (Nov 18 2018 at 20:13):

I started writing this, as iso_induction.

#### Scott Morrison (Nov 18 2018 at 20:14):

This is intended as my start of an answer to all our questions about transport of structure.

#### Scott Morrison (Nov 18 2018 at 20:14):

It is not at all done, but it is certainly doable, and I would love to do it!

for the idea

#### Scott Morrison (Nov 18 2018 at 20:18):

It is not quite that same as iso_rw, but the same tooling would be required to make that work.

#### Scott Morrison (Nov 18 2018 at 20:20):

iso_induction takes a hypotheses X \iso Y, and tries to replace all appearances of X with Y, by writing everything in a form where X appears as the argument of a functor.

#### Johan Commelin (Nov 19 2018 at 05:40):

Cool. That's going to be very useful!

#### Johan Commelin (Nov 19 2018 at 05:43):

I am afraid that monoid.ext will be considered intollerable abuse of the type class system.

#### Scott Morrison (Nov 19 2018 at 08:17):

@Johan Commelin, what's wrong with monoid.ext?

@[extensionality] lemma monoid.ext {α : Type u} (m n : monoid α)
(mul : ∀ x y : α, (by haveI := m; exact x * y) = (by haveI := n; exact x * y)) : m = n :=


looks good to me

#### Scott Morrison (Nov 19 2018 at 08:18):

Is it the two different uses of haveI that you're worried about?

#### Johan Commelin (Nov 19 2018 at 08:18):

Aah, wait. You aren't actually asking that there are two instances of monoid α

I read to fast.

#### Scott Morrison (Nov 19 2018 at 08:18):

No, no square brackets for this lemma!

#### Mario Carneiro (Nov 19 2018 at 08:21):

do you have groupoids? that's an obvious thing to prove about isos

#### Mario Carneiro (Nov 19 2018 at 08:24):

also it's not clear to me why monoid_transport isn't proven directly and it becomes the map part of monoid_type_constructor

#### Scott Morrison (Mar 19 2019 at 01:03):

@Kevin Buzzard, @Johan Commelin, resuming an old thread about transport of structure along isomorphisms, I wonder if you could have a look at tests/iso_induction.lean on the iso_induction branch. In particular, my idea is that it may be possible to synthesise things like submodule_functor, ideal_functor, and is_local_functor, stubbed out in the file, completely automatically.

If that's the case, then being able to prove is_local_ring S given hypotheses h : is_local_ring R and f : R \iso S should be pretty doable via tactics that look like iso_subst f; exact h.

Really the question becomes --- if you look in the partial proofs of submodule_functor I've been writing, can you write down _exactly_ why every mathematician knows exactly what to do at every step? :-) This is the sort of thing tidy is aimed at, but it's not up to the task quite yet.

#### Kevin Buzzard (Mar 19 2019 at 01:08):

Did you see Mario's effort on this question? My lean time has been 100% taken up with perfectoids recently so I didn't look at it

#### Scott Morrison (Mar 19 2019 at 01:09):

No, maybe I didn't... @Mario Carneiro, could you give me a pointer?

#### Scott Morrison (Mar 19 2019 at 01:09):

(Have to disappear for a few hours, but I'll read up afterwards.)

#### Mario Carneiro (Mar 19 2019 at 01:10):

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

#### Scott Morrison (Mar 19 2019 at 01:16):

Okay, that is cool. :-)

#### Scott Morrison (Mar 19 2019 at 01:17):

A lot of automation is going to be needed still, before the mathematicians can cope with this. :-)

#### Mario Carneiro (Mar 19 2019 at 01:19):

right, this was really an exercise in finding out what major infrastructure components were missing in the automation we all expect

#### Mario Carneiro (Mar 19 2019 at 01:19):

equiv.rel in particular turned out to be important

#### Mario Carneiro (Mar 19 2019 at 01:20):

eventually, transfer should be able to do the job of proving the last few theorems, although stuff about transferring ideals and other things will all need to be explicitly stated, at least, and marked for use with transfer

#### Johan Commelin (Mar 19 2019 at 07:09):

@Scott Morrison I'll try to write up the kind of proofs that I expect tidy to generate

#### Scott Morrison (Mar 19 2019 at 08:31):

@Johan Commelin, maybe it's not worth doing any now. The functoriality argument for submodule needs to rely on deeper layers of functoriality, anyway. May I should try writing the actual iso_subst and iso_rwtactic, because they'll in turn be used by the [derive] handler for functoriality and iso_functoriality instances...

#### Scott Morrison (Mar 19 2019 at 08:32):

Also, I need to understand Mario's approach properly. I haven't understood yet how general it will be. (I'm initially a little worried taking about ring equivalences, and monoid equivalences, and .... all separately, rather than building the machinery abstractly at the level of isomorphisms in some category, but maybe I don't know what I'm talking about here. :-)

#### Kevin Buzzard (Mar 19 2019 at 09:32):

I wanted to do some linear_ordered_comm_group equivalences for the perfectoid project and I've been slowly but surely writing monoid_equiv, group_equiv, le_equiv, mul_equiv, add_group_equiv, ...

#### Scott Morrison (Mar 19 2019 at 10:07):

Hmmm... use bundled objects, bundled morphisms, set up the category instances, and get for free uniform notation and lemmas for all these notions of equivalence. I'm not really sure how plausible it is, but it seems a desirable goal.

#### Johan Commelin (Mar 19 2019 at 10:17):

@Scott Morrison I've documented my attempt in a copy of your file. Pushed to the branch.

#### Johan Commelin (Mar 19 2019 at 10:17):

It stops halfway because things got annoying.

#### Johan Commelin (Mar 19 2019 at 10:17):

And because you said that I maybe shouldn't do it anyway :lol:

#### Kevin Buzzard (Mar 19 2019 at 10:34):

...has_zero_equiv, has_one_equiv, ...

#### Kevin Buzzard (Mar 21 2019 at 11:34):

I had an issue with transferring information along an isomorphism which took me two days of hard work to solve. During this time I learnt what I think might be a valuable lesson, so I'll just document it here.

If $G$ and $H$ are isomorphic groups, and $J$ is a normal subgroup of $G$ with corresponding normal subgroups $K$ of $H$, then $G/J$ and $H/K$ are isomorphic.

I proved this in Lean. I set up group_equiv and proved, amongst other things, group_equiv.trans. I then proved that if $\phi:G\to H$ was a group isomorphism and $K$ was a normal subgroup of $H$ then $G/\phi^{-1}(K)$ was isomorphic to $H/K$. This seemed to me like a good idea at the time, but in retrospect I think it was my mistake. I then proved the moronic theorem that if $G$ was a group and $J_1$, $J_2$ were two subgroups which were equal, then $G/J_1$ was isomorphic to $G/J_2$. I proved this theorem because I know that ridiculous theorems of this form are sometimes what needs to be done. I then used transitivity to prove the $G/J\cong H/K$ result and things were fine, until I wanted to start transporting things along the corresponding isomorphism and nothing seemed to unfold nicely and it was a nightmare.

Independently of working on this quotient issue we were working on another isomorphism issue -- if two integral domains are isomorphic then their fields of fractions are isomorphic. In fact Johan was working on this a couple of weeks ago, and he wrote equiv_of_equiv. This is a much better approach! This does the entire job in one go -- he has a hypothesis the analogue of which would be $\phi(J)=K$. But preimages are slightly easier to work with than images, because image involves an existence statement which is not there with preimage. In summary then, I think this is the sort of theorem one should prove (and indeed I have proved in the perfectoid project):

def group_equiv.quotient {G : Type*} {H : Type*} [group G] [group H]
(he : group_equiv G H) (J : set G) [normal_subgroup J] (K : set H) [normal_subgroup K]
(h2 : he.to_equiv ⁻¹' K = J) :
group_equiv (quotient_group.quotient J) (quotient_group.quotient K) :=


It's interesting to note that all these thoughts about exactly what statements should be proved here are perhaps evidence for mathematicians that things are not quite as simple as they might seem when it comes to transfer or cerw or whatever we're calling it now. "If $G$ and $H$ are isomorphic, with normal subgroups $J$ and $K$ identified with each other, then obviously $G/J=H/K$". Yeah but I've just found out the hard way that formalising this statement and proof the wrong way can cause a lot of pain later down the line.

#### Mario Carneiro (Mar 21 2019 at 11:36):

I actually suggest neither preimages nor images, but rather a relation equiv.rel(phi) J K

#### Mario Carneiro (Mar 21 2019 at 11:37):

it can be defined to be the preimage equality though

#### Mario Carneiro (Mar 21 2019 at 11:38):

or rather, it is the equiv.rel of the map set J -> set K induced by phi

#### Kevin Buzzard (Mar 21 2019 at 11:39):

In practice the thing which was crucial for me was that the actual map can be defined "all in one go" using lift, rather than the way I had built it. This opens the door to things unfolding nicely.

#### Mario Carneiro (Mar 21 2019 at 11:39):

The advantage of the relation is you get something more symmetric, which you can prove theorems about swaps and such

#### Mario Carneiro (Mar 21 2019 at 11:40):

and it will fold nicely into future work on getting transfer to automate this stuff

#### Kevin Buzzard (Mar 21 2019 at 11:40):

Right -- this is why I'm posting this in the cerw thread. I'd like to have a transfer thread really.

#### Kevin Buzzard (Mar 21 2019 at 11:41):

Writing the perfectoid project has really taught me a lot about Lean's type theory, it has been a wonderful experience; I am now finally beginning to understand, and sometimes even solve myself, issues where what I want is trivial in maths but Lean won't buy it. These are, to me at least, the most frustrating things about using Lean.

#### Kevin Buzzard (Mar 21 2019 at 11:42):

In particular I am beginning to understand more about the difficulties of transferring the things which transfer so naturally in mathematics, like this statement that if R and S are isomorphic rings and R is local then S is.

#### Mario Carneiro (Mar 21 2019 at 11:43):

Do you follow the general strategy I tried to outline in that earlier stuff with is_maximal_ideal? For types, you want to define an equiv mapping (i.e. A ~=r B implies ideal A ~= ideal B), and for predicates you want to prove stuff about preserving equiv.rel on the component types

#### Mario Carneiro (Mar 21 2019 at 11:45):

If done correctly these should be compositional, in that if you have some complicated definition and you have the appropriate transfer lemmas for all the pieces of the definition then there is a straightforward way to put them all together to get the analogous transfer lemma for your definition

#### Mario Carneiro (Mar 21 2019 at 11:47):

You have the right idea with that lemma but to fit the mold h2 should have the type (equiv_set he).rel J K where equiv_set : A ~= B -> set A ~= set B

#### Kevin Buzzard (Mar 21 2019 at 11:48):

No I still did not sit down and look at the is_maximal_ideal stuff. Maybe this was an error. I am just highly focussed on the perfectoid project at the minute and am being ruthless. We're nearly there -- I can see the light at the end of the tunnel and the incentive to just keep working on it is very strong. I was up until 3am last night working on it and then up again at 7am doing more.

#### Mario Carneiro (Mar 21 2019 at 11:50):

no problem, indeed if you have already proven your version of the statement then that's great. I'm thinking more in terms of how to link it up into a general theory, where you don't need any creativity to put the lemmas together

#### Mario Carneiro (Mar 21 2019 at 11:51):

because we can't write a tactic to do the work for us until it's an utterly routine exercise

#### Kevin Buzzard (Mar 21 2019 at 11:51):

I'm looking at it now.

instance (α β) [ring α] [ring β] : has_coe_to_fun (α ≃r β) :=
⟨λ_, α → β, λe, e.to_equiv⟩


I did not put coe_to_fun instances for group_equiv and monoid_equiv and preorder_equiv and mul_equiv and add_equiv and all the other equivs, because there was not one for ring_equiv. Now I see you've put one in. Shall I put coercions in for all the other ones?

#789

#### Kevin Buzzard (Mar 21 2019 at 11:52):

https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.23789.20extensions.20of.20equiv

#### Kevin Buzzard (Mar 21 2019 at 11:53):

Fancy a review of what I've PR'ed so far? ;-)

#### Johan Commelin (Mar 22 2019 at 05:51):

I actually suggest neither preimages nor images, but rather a relation equiv.rel(phi) J K

If we take this idea seriously (which is I guess the main claim of "Theorems for free") should we then also define add_equiv in terms of equiv.rel (has_add.add A) (has_add.add B)?

#### Johan Commelin (Mar 22 2019 at 05:53):

After all, the equiv.rel between A and B induces an equiv.rel between A → A → A and B → B → B.

#### Mario Carneiro (Mar 22 2019 at 06:08):

you don't need to define this specifically, it is f.rel => f.rel => f.rel if f : A ~= B

#### Johan Commelin (Mar 22 2019 at 06:45):

Sure... my question is: should we use those facts in the definition of add_equiv, mul_equiv, le_equiv, etc...

#### Johan Commelin (Mar 22 2019 at 06:46):

If we use rel in their definitions, does that help down the line with inferring equivs, or transporting stuff?

#### Mario Carneiro (Mar 22 2019 at 06:56):

the definition of add_equiv et al doesn't use any of this

#### Mario Carneiro (Mar 22 2019 at 06:57):

rather, add_equiv et al are used to define the relations at the base case

(deleted)

#### Kevin Buzzard (Apr 05 2019 at 14:50):

Hey @Assia Mahboubi . A commutative ring is called _local_ if it has a unique maximal ideal. If you find a mathematician and ask them the following question: "if $R$ and $S$ are isomorphic rings, and $R$ is local, is $S$ local?", then I think they will struggle to say anything useful other than "the answer is obviously yes". This is because "local", like every other predicate on rings that a mathematician uses, is constant on isomorphism classes. Unfortunately it turns out that there are completely valid predicates which no mathematician cares about but which do not have this property (e.g. P X := X = R). If you had to prove this statement about local rings in Coq, how would it go? Can you get it for free, or cheaply? The people here are trying to make a tactic which does it, and progress is being made, but I think we're not there yet.

Last updated: May 12 2021 at 05:19 UTC