# Zulip Chat Archive

## Stream: maths

### Topic: Additive functors

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

I'm working on additive functors.

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]
[preadditive D] (F : C ⥤ D) [functor.additive F]
namespace functor.additive
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' _ _
end functor.additive
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 :=
by {unfold add_map, rw classical.some_spec (functor.additive.exists_hom F X Y)}
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]
[preadditive D] (F : C ⥤ D) [functor.additive F]
namespace functor.additive
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' _ _
end functor.additive
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,
map_add' := begin
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 :-(

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

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...

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

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 :=
F.add_map.map_sub f g
```

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

It's not as general as it could be

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

Oh I see.

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

Sometimes you might need to replace it even when not applied

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

#### 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)
restate_axiom additive_functor.add_map_eq'
attribute [simp] additive_functor.add_map_eq
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)
restate_axiom additive_functor.add_map_eq'
attribute [simp, priority 100] additive_functor.add_map_eq
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} :
F.add_map (f ≫ g) = F.add_map f ≫ F.add_map g := by simp
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?

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

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?

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

Perhaps worth a new thread in general about this odd bundling behavior

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

Agreed on the existential not being better than the simpler solution

#### Adam Topaz (Feb 22 2021 at 23:23):

Okay, I pushed this change to #6367

Last updated: May 14 2021 at 20:13 UTC