cerw

Stream: general

[Johan Commelin]

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.

[Scott Morrison]

HI Johan,

[Scott Morrison]

I started writing this, as iso_induction.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

Have a look at https://github.com/semorrison/lean-category-theory/blob/master/src/category_theory/iso_induction.lean

[Scott Morrison]

for the idea

[Scott Morrison]

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

[Scott Morrison]

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]

Cool. That's going to be very useful!

[Johan Commelin]

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

[Scott Morrison]

@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 :=

[Mario Carneiro]

looks good to me

[Scott Morrison]

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

[Johan Commelin]

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

[Johan Commelin]

I read to fast.

[Scott Morrison]

No, no square brackets for this lemma!

[Mario Carneiro]

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

[Mario Carneiro]

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]

@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]

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]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Scott Morrison]

Okay, that is cool. :-)

[Scott Morrison]

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

[Mario Carneiro]

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

[Mario Carneiro]

equiv.rel in particular turned out to be important

[Mario Carneiro]

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]

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

[Scott Morrison]

@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]

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]

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]

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]

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

[Johan Commelin]

It stops halfway because things got annoying.

[Johan Commelin]

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

[Kevin Buzzard]

...has_zero_equiv, has_one_equiv, ...

[Kevin Buzzard]

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]

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

[Mario Carneiro]

it can be defined to be the preimage equality though

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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?

[Kevin Buzzard]

#789

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Johan Commelin]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Alexander Bentkamp]

(deleted)

[Kevin Buzzard]

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.