option.map_comp

Stream: general

[Kevin Buzzard]

What is option.map_comp called? I can't find it :-/ Oh! Is it something to do with monads?

[Sebastian Ullrich]

Yes, it's comp_map (of class is_lawful_functor)

[Kevin Buzzard]

Can I get this cheaply?

def with_zero (α) := option α

instance : monad with_zero := option.monad

namespace with_zero

def map {α β : Type*} (f : α → β) : with_zero α → with_zero β := option.map f

lemma map_id {α : Type*} : map (id : α → α) = id := option.map_id

lemma map_comp {α : Type*} {β : Type*} {γ : Type*} (f : α → β) (g : β → γ) (r : with_zero α) :
  with_zero.map (g ∘ f) r = (with_zero.map g) ((with_zero.map f) r) :=
is_lawful_functor.comp_map f g r -- error involving <$>
/-
  type mismatch, term
    comp_map ?m_7 ?m_8 ?m_9
  has type
    (?m_6 ∘ ?m_7) <$> ?m_8 = ?m_6 <$> ?m_7 <$> ?m_8
  but is expected to have type
    map (g ∘ f) r = map g (map f r)
-/

end with_zero

I have never had to deal with <$> before.

[Chris Hughes]

Have you proved it's a lawful monad?

[Kevin Buzzard]

def map {α β : Type*} (f : α → β) : with_zero α → with_zero β := functor.map f

This fixes it.

[Kevin Buzzard]

I've proved it's a functor:

example : functor with_zero := by apply_instance

[Kevin Buzzard]

Or at least, someone did...

[Chris Hughes]

Don't you need to prove it's a lawful functor?

[Kevin Buzzard]

def with_zero (α) := option α

instance : monad with_zero := option.monad

namespace with_zero

def map {α β : Type*} (f : α → β) : with_zero α → with_zero β := functor.map f

lemma map_id {α : Type*} : map (id : α → α) = id := option.map_id

lemma map_comp {α : Type*} {β : Type*} {γ : Type*} (f : α → β) (g : β → γ) (r : with_zero α) :
  with_zero.map (g ∘ f) r = (with_zero.map g) ((with_zero.map f) r) :=
is_lawful_functor.comp_map f g r -- compiles fine

example : is_lawful_functor with_zero := by apply_instance -- fails!

end with_zero

Apparently not :P

[Kevin Buzzard]

I've never played with this stuff before.

[Kevin Buzzard]

example : is_lawful_functor option := by apply_instance -- works!

[Kevin Buzzard]

I am surprised things work out like this. Type class inference found an instance for is_lawful_functor with_zero when using is_lawful_functor.comp_map but not when I asked it explicitly.

[Kevin Buzzard]

Am I supposed to be writing code like this in a library:

def with_zero (α) := option α

instance : monad with_zero := option.monad

example : is_lawful_functor with_zero := show is_lawful_functor option, by apply_instance

example : is_lawful_monad with_zero := show is_lawful_monad option, by apply_instance

namespace with_zero

def map {α β : Type*} (f : α → β) : with_zero α → with_zero β := functor.map f

lemma map_id {α : Type*} : map (id : α → α) = id := option.map_id

lemma map_comp {α : Type*} {β : Type*} {γ : Type*} (f : α → β) (g : β → γ) (r : with_zero α) :
  with_zero.map (g ∘ f) r = (with_zero.map g) ((with_zero.map f) r) :=
is_lawful_functor.comp_map f g r

end with_zero

Or am I just supposed to use is_lawful_functor.comp_map whenever I want with_zero.comp_map?

[Kevin Buzzard]

It's the same question Johan asked earlier with vector_subspace.zero_mem just equalling submodule.zero_mem.

[Patrick Massot]

What about using open is_lawful_functor and stop worrying?

[Kevin Buzzard]

Is that what I'm supposed to do?

[Kevin Buzzard]

aargh functor is rubbish

class functor (f : Type u → Type v) : Type (max (u+1) v) :=
(map : Π {α β : Type u}, (α → β) → f α → f β)
(map_const : Π {α β : Type u}, α → f β → f α := λ α β, map ∘ const β)

functor.map will only eat f : alpha -> beta if alpha and beta live in the same universe :-(

[Kevin Buzzard]

I don't think this is general enough for me after all

[Kevin Buzzard]

So I'm back to the start.

universes u₁ u₂ u₃

def option.map_comp {α : Type u₁} {β : Type u₂} {γ : Type u₃}
  (f : α → β) (g : β → γ) (r : option α) :
option.map (g ∘ f) r = option.map g (option.map f r) := sorry

Is this in Lean or mathlib somewhere?

[Mario Carneiro]

I don't think it is, it should be in data.option.basic

[Kevin Buzzard]

You can't prove it using lawful functors, or at least I can't, because then the universes have to be the same.

[Mario Carneiro]

This is a known limitation of functor

[Mario Carneiro]

this is why many monads have map functions separate from the notation

[Kevin Buzzard]

You want this sort of thing to construct an equiv of monoids (with_zero G) from an equiv of groups (G)

[Mario Carneiro]

I guess it's just a semigroup equiv?

[Kevin Buzzard]

A semigroup equiv of monoids is a monoid equiv, if I've understood this statement correctly

[Mario Carneiro]

with_zero makes a semigroup into a monoid

[Kevin Buzzard]

Aah I see. Yes.

[Mario Carneiro]

so the congr theorem should turn semigroup equivs into monoid equivs

[Kevin Buzzard]

Right.

[Kevin Buzzard]

Oh this is more congr?

[Mario Carneiro]

yeah, if you squint

[Kevin Buzzard]

I'm learning to squint at congr.

[Mario Carneiro]

G ~= H -> with_zero G ~= with_zero H

[Kevin Buzzard]

yes, that's a congr alright.

[Kevin Buzzard]

So what's the function called?

[Mario Carneiro]

with_zero_congr?

[Kevin Buzzard]

I don't think I'll tell you what I was going to call it.

[Mario Carneiro]

or maybe something with projection notation

[Kevin Buzzard]

semigroup_equiv.with_zero_congr?

[Mario Carneiro]

semigroup_equiv.with_zero_congr doesn't buy much

[Kevin Buzzard]

Ohohoh I just sat down to code this and noticed that it is from groups to monoids -- the group law is *, so this extra zero isn't the monoid identity. Maybe it's from monoids to monoids.

[Kevin Buzzard]

def to_with_zero_monoid_equiv (h : monoid_equiv α β) : monoid_equiv (with_zero α) (with_zero β) :=
{ to_fun := with_zero.map (h.to_equiv),
  inv_fun := with_zero.map (h.to_equiv.symm),
  left_inv := λ x, begin cases x, refl, show some _ = some _, congr, exact h.left_inv x end,
  right_inv := λ x, begin cases x, refl, show some _ = some _, congr, exact h.right_inv x end,
  mul_hom := λ x y, begin cases x; cases y,
  { refl},
  { refl},
  { refl},
  { show some _ = some _, congr, exact h.mul_hom x y}
  end}

My plan for the proof of left_inv was to use with_zero.map_comp and with_zero.map_id but there's barely any point.