# Zulip Chat Archive

## Stream: general

### Topic: option.map_comp

#### Kevin Buzzard (Mar 23 2019 at 20:45):

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

#### Sebastian Ullrich (Mar 23 2019 at 20:59):

Yes, it's `comp_map`

(of class `is_lawful_functor`

)

#### Kevin Buzzard (Mar 23 2019 at 22:51):

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 (Mar 23 2019 at 22:57):

Have you proved it's a lawful monad?

#### Kevin Buzzard (Mar 23 2019 at 22:57):

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

This fixes it.

#### Kevin Buzzard (Mar 23 2019 at 22:58):

I've proved it's a functor:

example : functor with_zero := by apply_instance

#### Kevin Buzzard (Mar 23 2019 at 22:58):

Or at least, someone did...

#### Chris Hughes (Mar 23 2019 at 22:59):

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

#### Kevin Buzzard (Mar 23 2019 at 23:01):

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 (Mar 23 2019 at 23:02):

I've never played with this stuff before.

#### Kevin Buzzard (Mar 23 2019 at 23:10):

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

#### Kevin Buzzard (Mar 23 2019 at 23:11):

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 (Mar 23 2019 at 23:17):

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 (Mar 23 2019 at 23:18):

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

#### Patrick Massot (Mar 24 2019 at 08:13):

What about using `open is_lawful_functor`

and stop worrying?

#### Kevin Buzzard (Mar 24 2019 at 08:43):

Is that what I'm supposed to do?

#### Kevin Buzzard (Mar 24 2019 at 09:05):

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 (Mar 24 2019 at 09:05):

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

#### Kevin Buzzard (Mar 24 2019 at 09:13):

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 (Mar 24 2019 at 09:24):

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

#### Kevin Buzzard (Mar 24 2019 at 09:25):

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 (Mar 24 2019 at 09:25):

This is a known limitation of `functor`

#### Mario Carneiro (Mar 24 2019 at 09:26):

this is why many monads have `map`

functions separate from the notation

#### Kevin Buzzard (Mar 24 2019 at 09:26):

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

#### Mario Carneiro (Mar 24 2019 at 09:26):

I guess it's just a semigroup equiv?

#### Kevin Buzzard (Mar 24 2019 at 09:27):

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

#### Mario Carneiro (Mar 24 2019 at 09:27):

`with_zero`

makes a semigroup into a monoid

#### Kevin Buzzard (Mar 24 2019 at 09:28):

Aah I see. Yes.

#### Mario Carneiro (Mar 24 2019 at 09:28):

so the congr theorem should turn semigroup equivs into monoid equivs

#### Kevin Buzzard (Mar 24 2019 at 09:28):

Right.

#### Kevin Buzzard (Mar 24 2019 at 09:28):

Oh this is more congr?

#### Mario Carneiro (Mar 24 2019 at 09:28):

yeah, if you squint

#### Kevin Buzzard (Mar 24 2019 at 09:28):

I'm learning to squint at congr.

#### Mario Carneiro (Mar 24 2019 at 09:29):

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

#### Kevin Buzzard (Mar 24 2019 at 09:29):

yes, that's a congr alright.

#### Kevin Buzzard (Mar 24 2019 at 09:29):

So what's the function called?

#### Mario Carneiro (Mar 24 2019 at 09:29):

`with_zero_congr`

?

#### Kevin Buzzard (Mar 24 2019 at 09:29):

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

#### Mario Carneiro (Mar 24 2019 at 09:29):

or maybe something with projection notation

#### Kevin Buzzard (Mar 24 2019 at 09:30):

semigroup_equiv.with_zero_congr?

#### Mario Carneiro (Mar 24 2019 at 09:30):

`semigroup_equiv.with_zero_congr`

doesn't buy much

#### Kevin Buzzard (Mar 24 2019 at 15:29):

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 (Mar 24 2019 at 15:36):

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.

Last updated: Dec 20 2023 at 11:08 UTC