Transporting across an isomorphism

Stream: new members

[Devon Tuma]

I've been trying to start learning Lean by formalizing Jacobson rings, and one theorem I wanted to use was along the lines of is_jacobson_iff_iso (e : S ≃+* R) : is_jacobson S ↔ is_jacobson R where S and R are two commutative rings. I ended up just writing out a a direct proof using the definitions with maps and comaps of ideals, but I was wondering if there was a nicer way to do a proof like this in Lean? Or is a ring equivalence not "strong" enough for this?

[Kyle Miller]

I wonder if this is because this is the statement that being a Jacobson ring is an invariant of rings up to isomorphism, and that needs proof. It would be cool if there were a tactic to automatically construct a proof for you if you only used the ring axioms in the statement of some property.

[Alex J. Best]

This is a big open problem in lean really, there are some tactics like tactic#equiv_rw and tactic#transport but they aren't at the stage where they can handle these goals with no input from the user as far as I can tell.
You can't just rewrite along an equiv so in that sense an equiv is not strong enough in lean (compared to equality), but as the proof steps should all be somewhat automatic a lot of us hope that there does exist a tactic to finish these goals easily, just nobody has written a bulletproof one yet!

[Kevin Buzzard]

This should be solvable by a tactic yes, and we'll get there in the end :-)

[Kevin Buzzard]

In this particular case, Mario's law applies I think. A homomorphic image of a Jacobson ring is a Jacobson ring I guess, and probably this needs a proof. The isomorphism statement follows from this.

[Kevin Buzzard]

Mario argues that many cases of this rewriting along equivalence principle follow from stronger results which aren't tautological to a mathematician and need to be proved anyway. This breaks down for various 1-dimensional properties such as PID though

[Kevin Buzzard]

Aah but not for PIR, interestingly enough

[Devon Tuma]

Yes in this case the actual proof isn't too bad to just write so its not a huge issue, but thanks for this info on the general state of things like this. Using tactics for proofs like this is new to me coming from a background in just Agda, and I hadn't considered they could prove bigger things like this.

I hadn't thought about proving this for the homomorphic image first and then specializing that to the isomorphic case, that seems like a nice way to make the proof cleaner.

[Kyle Miller]

My rough understanding of an underlying issue is that you need some sort of coherence law to be able to do rewrites. For example, you might have some loop of equivalences whose composition is some nontrivial automorphism, and if you rewrite only portions of a term using an equivalence, you're liable to obtain absurd conclusions. Equality in lean has the property that any such loop gives the trivial automorphism, due to proof irrelevance in Prop.

There's a nonconstructive way to rewrite across isomorphisms, I think. You can choose (probably by the axiom of choice somehow) a canonical isomorphism between every pair of objects in an isomorphism class in such a way that any loop of compositions is the identity, and then you should be able to do rewrites with respect to these specific isomorphisms for terms involving only the axioms of the objects under question. I have no intuition about whether you can actually do anything useful with this, though. But, at least for the is_jacobson example, all the terms are in the theory of rings so the isomorphism implies there is a canonical isomorphism, and so you would be able to rewrite is_jacobson S to is_jacobson R to get a tautology.

[Kevin Buzzard]

What if R=S and e isn't the identity?

[Kyle Miller]

You wouldn't rewrite using e itself. You'd use the fact it exists to nonconstructively obtain the canonical isomorphism R to S (and these isomorphisms are chosen so that any loop of compositions is the identity). If R = S, then this canonical automorphism is the identity.

[Devon Tuma]

@Kyle Miller Ah, I assume that means Lean does not have any sort of UIP axiom or axiom K for types? So outside of Prop there can be multiple different equivalences between two types, which gives these "nontrivial automorphisms" between types?

[Johan Commelin]

There certainly can be multiple different equivs between two types.

[Kyle Miller]

I don't know these axioms, but at least the way equiv is defined in Lean, which is a pair of maps that are left and right inverses to each other, there can certainly be many equivalences between non-Prop types.

[Johan Commelin]

@Kyle Miller I have no idea what you would mean with choosing a canonical isomorphism...

[Johan Commelin]

Is it just whatever classical.choice spits out?

[Johan Commelin]

I don't think you can prove that it is the identity in the case of R = S.

[Johan Commelin]

Equality of types is an extremely awkard notion to prove things about.

[Kyle Miller]

You'd have to set up your statement carefully, which I'm not sure how to do right now. It's "canonical" in the same sense that every module has a "canonical" projective resolution.

[Johan Commelin]

I'm only more confused now...

[Johan Commelin]

If I have two isomorphic rings R and S, I don't have any idea what could be meant be the "canonical" isomorphism between R and S...

[Kyle Miller]

Informally, I was imagining taking a representative object from each isomorphism class, and for every other object choose some isomorphism to the representative object. Then, every pair of objects in the isomorphism class would have a "canonical" isomorphism between them by the unique composition of chosen isomorphisms.

[Kyle Miller]

It's a similar sort of solution to the problem of defining derived functors, with a solution being to fix specific projective resolutions for every module. Sorry, I'm severely misusing the word "canonical."

[Devon Tuma]

@Johan Commelin I can see that there are certainly multiple equivalences between types, but in Lean can you apply univalence to them to also get distinct equalities between types? Or do all type equalities get squashed down to being equal in Lean (or is univalence not even a thing in Lean)?

[Kyle Miller]

@Johan Commelin But, since you're saying proving things about equalities of types is extremely awkward, this might be completely unworkable.

[Andrew Ashworth]

univalence is not a thing in lean

[Andrew Ashworth]

UIP and axiom K everywhere

[Kyle Miller]

@Devon Tuma Oh, it looks like "equivalence" has meant two things in this conversation. Sorry to mislead you that Lean had nontrivial homotopy equivalences between types.

[Devon Tuma]

@Kyle Miller No worries, I think that was part of what was tripping me up in the first place with a ring equivalence being very different than a homotopy style equivalence between the actual types

[Mario Carneiro]

I believe that what lean calls R ≃+* S is equivalent to what a HoTT system would call an equivalence (or via univalence, equality) of elements of the type Ring

[Mario Carneiro]

so calling them "ring equivalences" is not a misrepresentation