will you be our tutor?

Stream: general

[Johan Commelin]

Hi everyone, here's another post about the LftCM 2020 workshop that takes place next week. Right now, 33 people have signed up for the workshop!

This post is directed to people in the community with ample experience in Lean. Ideally, you will worked with Lean for at least a couple of months, and maybe have several PRs to mathlib under your belt.

We are looking for tutors that will assist during the exercise sessions. These will take place in a Zoom meeting. We will have several breakout rooms per session. Please indicate for which sessions you could help us by leading a breakout room.
Your task will be to help participants get unstuck while they are working on Lean exercises.
See https://leanprover-community.github.io/lftcm2020/schedule.html for the schedule.

If you are a speaker for some session, please do not sign up as tutor for that same session.

The poll where you can sign up can be found here: https://cloud.commelin.net/apps/polls/s/VwIVXMDDtSUBxtRI

P.s.: You can answer with three options:

• green checkmark — yes, I'll be there
• yellow checkmark — maybe, if necessary
• red cross — unavailable

[Johan Commelin]

Thanks to everyone who has offered help so far. We're still looking for a couple more.
@Sebastien Gouezel @Heather Macbeth @Yury G. Kudryashov @Kevin Buzzard @Amelia Livingston @Jeremy Avigad @Markus Himmel
Do any of you want to help with some of the sessions?

[Yury G. Kudryashov]

I'll reply tonight.

[Heather Macbeth]

Thanks, just replied.

[Sebastien Gouezel]

It's gonna be hard for me, because I have to take care of the kids at home. I'll try to show up when I can...

[Johan Commelin]

Thanks! I completely understand!

[Patrick Massot]

No worries Sébastien! We're getting a little nervous because the participant list has grown quite a bit, but we'll manage.

[Markus Himmel]

Where do the exercises come from? Are they set by the speaker?

[Alex J. Best]

Yes, thats the plan.

[Kevin Buzzard]

Sure I can do it, I'm just not really on top of all the other things I'm doing right now so was holding back

[Scott Morrison]

@Markus Himmel, I should have the category theory exercises up soon. My first attempts were mostly too hard, so I'm writing some easier ones now. If you want to contribute any, please feel free! :-)

[Scott Morrison]

@Bhavik Mehta, if you'd be interested/able to join at least for the category theory exercise session that would be great!

[Bhavik Mehta]

Do you know how much time/effort it involves?

[Scott Morrison]

I think the idea is that we're going to split the zoom session into breakout rooms for the exercise session.

[Scott Morrison]

So the idea would be to be available to join one of those rooms for the hour or so after the "lecture", to discuss problems with whatever fraction of the participants we end up.

[Bhavik Mehta]

Ah I see, I'll put my name down

[Jeremy Avigad]

Sorry, I answered this on the wrong thread.... I can do any of the 13:00 or later sessions. I'll show up for Kevin's session tomorrow morning and stick around as long as needed.

[Johan Commelin]

Thanks for the help, @ everyone

[Bhavik Mehta]

Scott Morrison said:

Markus Himmel, I should have the category theory exercises up soon. My first attempts were mostly too hard, so I'm writing some easier ones now. If you want to contribute any, please feel free! :-)

If you're still working on this, there might be some helpful ones from Markus or my kata on codewars, I also probably have some standalone lemmas floating about if you still need things

[Scott Morrison]

I still need easy (including really easy) exercises, if you want to suggest any!

[Kevin Buzzard]

is Yoneda from first principles easy?

[Bhavik Mehta]

Yeah one nice thing could be constructing the iso between b and c given a natural (in a) bijection from (a -> b) to (a -> c)

[Bhavik Mehta]

I'm not sure if these are appropriate for what you're looking for but:

lemma equiv_reflects_mono {D : Type u₂} [category.{v} D] {X Y : C} (f : X ⟶ Y) (e : C ≌ D)
  (hef : mono (e.functor.map f)) : mono f := sorry

lemma equiv_preserves_mono {D : Type u₂} [category.{v} D] {X Y : C} (f : X ⟶ Y) [mono f] (e : C ≌ D) :
  mono (e.functor.map f) := sorry

[Bhavik Mehta]

def over_terminal [has_terminal.{v} C] : over (⊤_ C) ≌ C :=

perhaps

[Bhavik Mehta]

def real_pullback [has_pullbacks C] {A B : C} (f : A ⟶ B) : over B ⥤ over A :=

[Bhavik Mehta]

instance reflects_iso_of_reflects_limits_of_shape_punit [reflects_limits_of_shape (discrete punit) F] :
  reflects_isomorphisms F :=

I probably should PR this to mathlib but I haven't yet so might be a good exercise

[Markus Himmel]

As a completely trivial very first exercise, how about reproving some basic facts about monomorphisms?

import tactic
import category_theory.isomorphism

open category_theory

universes v u

variables {C : Type u} [category.{v} C]

example {X : C} : mono (𝟙 X) :=
{ right_cancellation := λ Z g h hgh, by convert hgh; rw category.comp_id }

example {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [mono f] [mono g] : mono (f ≫ g) :=
{ right_cancellation := λ W x y hxy,
  begin
    refine (cancel_mono f).1 ((cancel_mono g).1 _),
    simpa only [category.assoc] using hxy
  end }

example {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [mono (f ≫ g)] : mono f :=
{ right_cancellation := λ W x y hxy,
  begin
    apply (cancel_mono (f ≫ g)).1,
    rw reassoc_of hxy
  end }

example {X Y : C} (f : X ⟶ Y) [is_iso f] : mono f :=
{ right_cancellation := λ Z g h hgh,
    by rw [←category.comp_id g, ←category.comp_id h, ←is_iso.hom_inv_id f,
        ←category.assoc, hgh, category.assoc] }

[Scott Morrison]

Thanks, both, these are good easy exercises. I think I'll have enough shortly, just getting everything in order.

[Scott Morrison]

I keep writing exercises and discovering things that are just horrible in mathlib, and get distracted fixing them. :-)

[Kevin Buzzard]

Fixing mathlib is always a good and important thing