Additive functors

Stream: maths

[Adam Topaz]

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]

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]

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

[Adam Topaz]

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]

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

[Adam Topaz]

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

[Kevin Buzzard]

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]

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

[Eric Wieser]

You should be able to define add_map computably I think?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

@Eric Wieser yeah I can make it computable.

[Eric Wieser]

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]

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]

Looks good so far :-)

[Adam Topaz]

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]

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]

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

[Kevin Buzzard]

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

[Adam Topaz]

Same here :(

[Eric Wieser]

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]

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]

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

[Yakov Pechersky]

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]

Maybe a push_comp and a pull_comp tactic?

[Johan Commelin]

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]

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

[Adam Topaz]

LONG

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' _ _

def of_is_hom (G : C ⥤ D)
  (map_zero : ∀ X Y : C, G.map (0 : X ⟶ Y) = 0)
  (map_add : ∀ (X Y : C) (f g : X ⟶ Y), G.map (f + g) = G.map f + G.map g) :
  functor.additive G := functor.additive.mk $ λ X Y,
⟨⟨λ f, G.map f, map_zero _ _, map_add _ _⟩, λ g, rfl⟩

end functor.additive

namespace functor

@[simps]
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 }

lemma add_map_spec {X Y : C} {f : X ⟶ Y} : F.add_map f = F.map f := rfl

@[simp]
lemma map_zero {X Y : C} : F.map (0 : X ⟶ Y) = 0 :=
by simp only [← add_map_spec, add_monoid_hom.map_zero]

@[simp]
lemma map_add {X Y : C} {f g : X ⟶ Y} : F.map (f + g) = F.map f + F.map g :=
by simp only [← add_map_spec, add_monoid_hom.map_add]

@[simp]
lemma map_neg {X Y : C} {f : X ⟶ Y} : F.map (-f) = - F.map f :=
by simp only [← add_map_spec, add_monoid_hom.map_neg]

@[simp]
lemma map_sub {X Y : C} {f g : X ⟶ Y} : F.map (f - g) = F.map f - F.map g :=
by simp [sub_eq_neg_add]

end functor

end category_theory

[Adam Topaz]

@Johan Commelin see the of_is_hom in the code above.

[Johan Commelin]

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

[Adam Topaz]

I think this is probably good enough, no?

[Eric Wieser]

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

[Adam Topaz]

They're defeq if you apply them :)

[Eric Wieser]

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

[Eric Wieser]

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

[Adam Topaz]

See LONG above

[Eric Wieser]

Yeah, my comment was in response to that

[Adam Topaz]

What's the issue with add_map_spec then?

[Eric Wieser]

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]

It's not as general as it could be

[Adam Topaz]

Oh I see.

[Eric Wieser]

Sometimes you might need to replace it even when not applied

[Adam Topaz]

#6367

[Adam Topaz]

@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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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

[Adam Topaz]

@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]

Just to be clear, that works?

[Adam Topaz]

yes

[Eric Wieser]

That might be a big discovery

[Adam Topaz]

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

[Scott Morrison]

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]

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]

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

[Eric Wieser]

Agreed on the existential not being better than the simpler solution

[Adam Topaz]

Okay, I pushed this change to #6367