## Stream: maths

#### Adam Topaz (Feb 22 2021 at 16:31):

How bad is it if I tag add_map_spec with simp in the following code? (see examples)

import category_theory.preadditive

namespace category_theory

class functor.additive {C D : Type*} [category C] [category D]
[preadditive C] [preadditive D] (F : C ⥤ D) : Prop :=
(exists_hom' : ∀ (X Y : C), ∃ f : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y),
∀ g : X ⟶ Y, F.map g = f g)

variables {C D : Type*} [category C] [category D] [preadditive C]

lemma exists_hom (X Y : C) : ∃ f : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y),
∀ g : X ⟶ Y, F.map g = f g := functor.additive.exists_hom' _ _

namespace functor

noncomputable
def add_map {X Y : C} : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y) :=
classical.some \$ functor.additive.exists_hom F X Y

@[simp]
lemma add_map_spec {X Y : C} {f : X ⟶ Y} : F.map f = F.add_map f :=

example {X Y : C} : F.map (0 : X ⟶ Y) = 0 := by simp

example {X Y : C} {f g : X ⟶ Y} : F.map (f + g) = F.map f + F.map g := by simp

end functor

end category_theory


#### Yakov Pechersky (Feb 22 2021 at 16:34):

Why not have the F.map 0 = 0 and F.map (f + g) = F.map f + F.map g as the API lemmas instead?

#### Yakov Pechersky (Feb 22 2021 at 16:34):

And, which direction would you want the distribution lemma to simplify in?

#### Adam Topaz (Feb 22 2021 at 16:35):

Sure I can do that, but presumably there are 1000 other lemmas about morphisms of abelian groups which I would like to use eventually.

#### Yakov Pechersky (Feb 22 2021 at 16:36):

This might be a case where some sort of meta code to transfer over the lemmas could work.

#### Adam Topaz (Feb 22 2021 at 16:40):

This would all be a lot easier if we didn't depricate is_hom/is_add_hom, etc.

#### Kevin Buzzard (Feb 22 2021 at 16:44):

I am confused about this. My current understanding is that the problem with is_add_hom is not that it exists, but that it is a class. I think. If I'm right and if a refactor with these changes would get files like deprecated.group out of deprecated then I might well be motivated to take this on. I totally agree that there are times when is_add_hom is useful, but I also very much believe that for group homomorphisms in Lean 3 you're better off using ->+ in general.

#### Adam Topaz (Feb 22 2021 at 16:47):

@Kevin Buzzard do you have any thoughts about the simp tag in the code above?

#### Eric Wieser (Feb 22 2021 at 16:48):

You should be able to define add_map computably I think?

#### Kevin Buzzard (Feb 22 2021 at 16:48):

I am not really a computer scientist, I don't have much of an understanding of simp. If the linter is happy then why not just try it?

#### Eric Wieser (Feb 22 2021 at 16:48):

Since you only need to unpack the existential inside the proof obligations

#### Kevin Buzzard (Feb 22 2021 at 16:48):

In practice I guess I would try and stick to add_map as much as possible, so hopefully I'd not need the simp lemma much.

#### Adam Topaz (Feb 22 2021 at 16:49):

@Eric Wieser yeah I can make it computable.

#### Eric Wieser (Feb 22 2021 at 16:50):

We have this type of things with docs#pi.single too, where we have the regular version, and a separate bundled version docs#add_monoid_hom.single. We copy across the really obvious lemmas like docs#pi.single_add, but for the more niche ones the user is expected to write "backwards" along docs#add_monoid_hom.single_apply or similar.

#### Adam Topaz (Feb 22 2021 at 16:50):

import category_theory.preadditive

namespace category_theory

class functor.additive {C D : Type*} [category C] [category D]
[preadditive C] [preadditive D] (F : C ⥤ D) : Prop :=
(exists_hom' : ∀ (X Y : C), ∃ f : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y),
∀ g : X ⟶ Y, F.map g = f g)

variables {C D : Type*} [category C] [category D] [preadditive C]

lemma exists_hom (X Y : C) : ∃ f : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y),
∀ g : X ⟶ Y, F.map g = f g := functor.additive.exists_hom' _ _

namespace functor

def add_map {X Y : C} : (X ⟶ Y) →+ (F.obj X ⟶ F.obj Y) :=
{ to_fun := λ f, F.map f,
map_zero' := begin
rcases functor.additive.exists_hom F X Y with ⟨f,hf⟩,
simp [hf],
end,
rcases functor.additive.exists_hom F X Y with ⟨f,hf⟩,
simp [hf],
end }

@[simp]
lemma add_map_spec {X Y : C} {f : X ⟶ Y} : F.map f = F.add_map f := by simp [add_map]

example {X Y : C} : F.map (0 : X ⟶ Y) = 0 := by simp

example {X Y : C} {f g : X ⟶ Y} : F.map (f + g) = F.map f + F.map g := by simp

end functor

end category_theory


#### Kevin Buzzard (Feb 22 2021 at 16:51):

Looks good so far :-)

#### Adam Topaz (Feb 22 2021 at 16:52):

Kevin, that was exactly my thought too -- when I know my functor is additive, I will always use add_map instead of map. So why not add that simp lemma :)? Maybe @Mario Carneiro can convince me otherwise.

#### Eric Wieser (Feb 22 2021 at 16:52):

I guess you're forced to choose between:

• You want the lemmas about functor.map to apply automatically, and force the user to do a bit of a dance to get the lemmas about add_monoid_hom
• You want the lemmas about add_monoid_hom to apply automatically, and force the user to do a bit of a dance to get the lemmas about functor.map

#### Adam Topaz (Feb 22 2021 at 16:52):

Hmm.... yeah that's a good point.

#### Kevin Buzzard (Feb 22 2021 at 16:53):

I am a naive mathematician and want both to happen at once :-(

Same here :(

#### Eric Wieser (Feb 22 2021 at 16:55):

One argument goes "bundled homs are ubiquitous, users will recognize when they have a goal that needs them to try and turn map into add_map via manual rewrites, but are less likely to recognize when they need to do the reverse". But I only make that argument because I'm used to having to do it with things like finsupp.lsingle which would be way too bundled for it to match lots of lemmas about finsupp.single were it not for the fact that simp put it in that form for me

#### Yakov Pechersky (Feb 22 2021 at 17:00):

This is a contrast the category theory part of the library has from other parts of the library. Which direction is the simplifying one here?

lemma prod.map_comp_map : prod.map g g' ∘ prod.map f f' = prod.map (g ∘ f) (g' ∘ f') := sorry


That is, which one of

lemma list.comp_map : list.map (h ∘ g) l = list.map h (list.map g l) := sorry


or

lemma list.map_map : list.map g (list.map f l) = list.map (g ∘ f) l := sorry


In list, the choice in map_map. In category theory portions of the library, I've seen that comp_map is the direction preferred.

#### Adam Topaz (Feb 22 2021 at 17:01):

I think @Eric Wieser 's comment convinced me against this simp lemma.

#### Yakov Pechersky (Feb 22 2021 at 17:01):

The thought likely being, anything which would have simplified list.map f l will also simplify list.map (g ∘ f), and moreover, you'll get possible simplifcations once g ∘ f exists as a term.

#### Yakov Pechersky (Feb 22 2021 at 17:02):

Maybe a push_comp and a pull_comp tactic?

#### Johan Commelin (Feb 22 2021 at 17:03):

Can't we have axioms map_add' and map_zero', and have a bundled version map_hom defined afterwards? I think that you don't need exists_hom then

#### Adam Topaz (Feb 22 2021 at 17:04):

@Johan Commelin Does it matter? I'm making a small api anyway...

LONG

#### Adam Topaz (Feb 22 2021 at 17:09):

@Johan Commelin see the of_is_hom in the code above.

#### Johan Commelin (Feb 22 2021 at 17:09):

I don't think it matters too much. But proving map_add' etc might be shorter proofs than exists_hom

#### Adam Topaz (Feb 22 2021 at 17:09):

I think this is probably good enough, no?

#### Eric Wieser (Feb 22 2021 at 17:14):

Oh, an annoying thing about your case vs pi.single is that map is not defeq to map_add

#### Adam Topaz (Feb 22 2021 at 17:14):

They're defeq if you apply them :)

#### Eric Wieser (Feb 22 2021 at 17:14):

I'd recommend exploiting the defeq-ness in your proofs then!

#### Eric Wieser (Feb 22 2021 at 17:15):

And change to lemma add_map_spec {X Y : C} {f : X ⟶ Y} : ⇑F.add_map = F.map := rfl too

#### Adam Topaz (Feb 22 2021 at 17:16):

See LONG above

#### Eric Wieser (Feb 22 2021 at 17:17):

Yeah, my comment was in response to that

#### Adam Topaz (Feb 22 2021 at 17:18):

What's the issue with add_map_spec then?

#### Eric Wieser (Feb 22 2021 at 17:18):

I'm suggesting the proofs be akin to

lemma map_sub {X Y : C} {f g : X ⟶ Y} : F.map (f - g) = F.map f - F.map g :=


#### Eric Wieser (Feb 22 2021 at 17:18):

It's not as general as it could be

Oh I see.

#### Eric Wieser (Feb 22 2021 at 17:19):

Sometimes you might need to replace it even when not applied

#6367

#### Adam Topaz (Feb 22 2021 at 19:38):

@Eric Wieser concerning your comment on github. Would this be better in your opinion?

import category_theory.preadditive
namespace category_theory

variables (C D : Type*) [category C] [category D] [preadditive C] [preadditive D]

structure additive_functor extends C ⥤ D :=
(add_map : Π {X Y : C}, (X ⟶ Y) →+ ((obj X) ⟶ (obj Y)))
(add_map_eq' : Π {X Y : C} {f : X ⟶ Y}, add_map f = map f . obviously)

infixr  ⥤+ :26 := additive_functor

end category_theory


#### Adam Topaz (Feb 22 2021 at 19:42):

I guess I can play with priorities to get something that sort of works:

import category_theory.preadditive

namespace category_theory

variables (C D : Type*) [category C] [category D] [preadditive C] [preadditive D]

structure additive_functor extends C ⥤ D :=
(add_map : Π {X Y : C}, (X ⟶ Y) →+ ((obj X) ⟶ (obj Y)))
(add_map_eq' : Π {X Y : C} {f : X ⟶ Y}, add_map f = map f . obviously)

infixr  ⥤+ :26 := additive_functor

variables {C D} {F : C ⥤+ D}

example {X Y : C} : F.add_map (0 : X ⟶ Y) = 0 := by simp

example {X Y : C} {f g : X ⟶ Y} : F.add_map (f + g) = F.add_map f + F.add_map g := by simp

example {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} :

end category_theory


#### Eric Wieser (Feb 22 2021 at 19:45):

The argument that I thought justified my suggestion is moot for reasons I don't quite understand

#### Eric Wieser (Feb 22 2021 at 19:46):

So I have no opinion on whether that's better or worse

#### Eric Wieser (Feb 22 2021 at 19:47):

But I'd like to understand why your case works when the is_add_monoid_hom case doesn't, in case it informs us about how to fix the is_add_monoid_hom case

#### Adam Topaz (Feb 22 2021 at 19:52):

The answer is, of course, to just redefine groups as one-object groupoids! (joking, of course)

#### Adam Topaz (Feb 22 2021 at 20:08):

@Eric Wieser

import algebra

structure bundled_function (α β : Type*) :=
(to_fun : α → β)

variables {α β : Type*}

instance foo : has_coe_to_fun (bundled_function α β) :=
{ F := λ _, α → β,
coe := λ f, f.to_fun }

class is_monoid_hom_foo [monoid α] [monoid β] (f : bundled_function α β) : Prop :=
(map_one : f 1 = 1)
(map_mul {x y} : f (x * y) = f x * f y)

attribute [simp] is_monoid_hom_foo.map_one is_monoid_hom_foo.map_mul

example {M N : Type*} [monoid M] [monoid N] (f : bundled_function M N)
[is_monoid_hom_foo f] {x y : M} : f (x * y) = f x * f y := by simp

example {M N : Type*} [monoid M] [monoid N] (f : bundled_function M N)
[is_monoid_hom_foo f] : f 1 = 1 := by simp


I'm confused.

#### Eric Wieser (Feb 22 2021 at 20:17):

Just to be clear, that works?

yes

#### Eric Wieser (Feb 22 2021 at 20:18):

That might be a big discovery

#### Adam Topaz (Feb 22 2021 at 20:21):

But I still have no idea why this works but it doesn't for plain functions...

#### Scott Morrison (Feb 22 2021 at 22:47):

For plain functions the simp lemma can't match, because the head of the left-hand-side is a metavariable (any function f). For bundled_function the head is some constant (I guess the coercion?)

#### Scott Morrison (Feb 22 2021 at 22:49):

Going back up a bit, I'm dubious about using the existential exists_hom'. As Johan says above, why not just have fields map_zero' and map_add', and construct the bundled F.map_add after the fact?