Thursday afternoon

Stream: Lean for the curious mathematician 2020

[Rob Lewis]

We'll start again in 6 minutes with @Anne Baanen on linear algebra!

[Johan Commelin]

Hey everyone! We're starting again

[Johan Commelin]

Category theory in mathlib

[Johan Commelin]

Join Zoom Meeting
https://vu-live.zoom.us/j/95402085900

Meeting ID: 954 0208 5900
Password: 333537

[Sophie Morel]

Did anybody solve exercise 4 of the category theory exercises ? It's the one the asks to prove that the forgetful functor from commutative rings to sets is corepresentable. I was able to construct the corepresenting object (it's Z[t]) and the transformations between coYoneda of this and the forgetful functor, and I tried to automate everything else, including naturality of the natural transformations, but Lean doesn't want to automate naturality of the first natural transformation (the one from the forgetful functor to coYoneda of Z[t], sending an element r of a commutative ring R to the evaluation at r morphism, that I constructed using polynomial.eval₂_ring_hom). So I tried and it comes down to the fact that a morphism of rings is a morphism of Z-algebras, but I couldn't convince Lean of that. I got frustrated and looked at the hints, they only gave me hints to do the stuff I already done, so I got extra frustrated and looked at the solution, but it doesn't prove naturality and has the same error message as my file in the same place. :sad:

[Johan Commelin]

@Sophie Morel I haven't looked at that particular exercise or the solutions. But are you looking for something like

import ring_theory.algebra

variables (R S : Type*) [ring R] [ring S]

def ring_hom.to_alg_hom (f : R →+* S) : R →ₐ[ℤ] S :=
{ commutes' := λ n, f.map_int_cast n, .. f}

I guess the issue is more complicated?

[Scott Morrison]

oops, sorry, the solutions were meant to be complete -- I'm pretty sure at some point they were! I'll go look at that.

[Scott Morrison]

Hmm... the solution is working for me. Perhaps try leanproject get-mathlib-cache to make sure you're running with the same version of mathlib?

[Scott Morrison]

In any case, here's a copy of the solution with the naturality field filled in.

import algebra.category.CommRing

open category_theory
open opposite
open polynomial

noncomputable theory

def CommRing_forget_representable : Σ (R : CommRing), (forget CommRing) ≅ coyoneda.obj (op R) :=
⟨CommRing.of (polynomial ℤ),
 { hom :=
   { app := λ R r, polynomial.eval₂_ring_hom (algebra_map ℤ R) r,
     naturality' :=
     begin
       intros X Y f, ext x p,
       simp only [ring_hom_eval₂_algebra_map_int, forget_map_eq_coe, coyoneda_obj_map,
         coe_eval₂_ring_hom, types_comp_apply, coe_comp]
      end },
   inv :=
   { app := λ R f, by { dsimp at f, exact f X, }, }, }⟩

[Scott Morrison]

I first wrote naturality' := by tidy?, then massaged the output from tidy into this form. The simp only invocation just does the same as what simp would do.

[Sophie Morel]

Hi @Scott Morrison, I did a git pull and a leanproject get-mathlib-cache before I started working on the exercises this morning, and I just tried doing that again, just in case. But when I type leanproject get-mathlib-cache, the answer I get is

Looking for local mathlib oleans
Found local mathlib oleans

and nothing gets downloaded. I don't know if that's the expected behaviour.

Anyway, your solution still doesn't work here. The opening brace on line 41 is underlined, and the corresponding error message (same as the one I get for my solution) is :

tactic failed, there are unsolved goals
state:
X Y : CommRing,
f : X ⟶ Y,
x : ↥X,
x_1 : polynomial ℤ
⊢ eval₂ (algebra_map ℤ ↥Y) (has_coe_to_fun.coe f x) x_1 =
    has_coe_to_fun.coe f (eval₂ (algebra_map ℤ ↥X) x x_1)

[Sophie Morel]

which I interpret as "hey you, you forgot to prove naturality !".

[Sophie Morel]

But given that the tidy tactic also fails here (I had tried it before, I just tried again), maybe the problem is with my local installation. I'll try re-leanprojecting lftcm2020 to see what happens.

[Scott Morrison]

Okay, I've just checked that

import algebra.category.CommRing
import data.polynomial.algebra_map

open category_theory
open opposite
open polynomial

noncomputable theory

def CommRing_forget_representable : Σ (R : CommRing), (forget CommRing) ≅ coyoneda.obj (op R) :=
⟨CommRing.of (polynomial ℤ),
 { hom :=
   { app := λ R r, polynomial.eval₂_ring_hom (algebra_map ℤ R) r,
     naturality' :=
     begin
       intros X Y f, ext x p,
       simp only [ring_hom_eval₂_algebra_map_int, forget_map_eq_coe, coyoneda_obj_map,
         coe_eval₂_ring_hom, types_comp_apply, coe_comp]
      end },
   inv :=
   { app := λ R f, by { dsimp at f, exact f X, }, }, }⟩

succeeds on the master branch of mathlib.

[Scott Morrison]

(Note it has one additional import beyond the previous version I posted higher up this thread!)

[Scott Morrison]

Hopefully git pull and leanproject get-mathlib-cache will get you to that same state of lftcm2020 as I'm in.

[Scott Morrison]

And I've also checked that lean src/solutions/thursday/afternoon/category_theory/exercise4.lean works okay in the master branch of lftcm2020

[Sophie Morel]

@Scott Morrison The extra import did the trick, it made the mistake disappear in my solution too ! (Without trying to fill out the naturality field.) So it wasn't my local mathlib installation, whew. Thanks !

[Scott Morrison]

Oops, sorry! mathlib moves fast... Sebastien is working on moving the tutorials and exercises directly into mathlib, so they don't break in future.

[Sophie Morel]

Well, I'm not a patient person so I'll still try to do the other exercises and complain if I can't make them work. :wink: