Zulip Chat Archive

Stream: maths

Topic: Additive functors


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Yakov Pechersky (Feb 22 2021 at 16:34):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Feb 22 2021 at 16:47):

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

view this post on Zulip Eric Wieser (Feb 22 2021 at 16:48):

You should be able to define add_map computably I think?

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Feb 22 2021 at 16:48):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Feb 22 2021 at 16:49):

@Eric Wieser yeah I can make it computable.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 16:51):

Looks good so far :-)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Adam Topaz (Feb 22 2021 at 16:52):

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

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 16:53):

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

view this post on Zulip Adam Topaz (Feb 22 2021 at 16:53):

Same here :(

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Feb 22 2021 at 17:01):

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

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Feb 22 2021 at 17:02):

Maybe a push_comp and a pull_comp tactic?

view this post on Zulip 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

view this post on Zulip Adam Topaz (Feb 22 2021 at 17:04):

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

view this post on Zulip Adam Topaz (Feb 22 2021 at 17:08):

LONG

view this post on Zulip Adam Topaz (Feb 22 2021 at 17:09):

@Johan Commelin see the of_is_hom in the code above.

view this post on Zulip 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

view this post on Zulip Adam Topaz (Feb 22 2021 at 17:09):

I think this is probably good enough, no?

view this post on Zulip 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

view this post on Zulip Adam Topaz (Feb 22 2021 at 17:14):

They're defeq if you apply them :)

view this post on Zulip Eric Wieser (Feb 22 2021 at 17:14):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Feb 22 2021 at 17:16):

See LONG above

view this post on Zulip Eric Wieser (Feb 22 2021 at 17:17):

Yeah, my comment was in response to that

view this post on Zulip Adam Topaz (Feb 22 2021 at 17:18):

What's the issue with add_map_spec then?

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 22 2021 at 17:18):

It's not as general as it could be

view this post on Zulip Adam Topaz (Feb 22 2021 at 17:18):

Oh I see.

view this post on Zulip Eric Wieser (Feb 22 2021 at 17:19):

Sometimes you might need to replace it even when not applied

view this post on Zulip Adam Topaz (Feb 22 2021 at 18:08):

#6367

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 22 2021 at 19:46):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Feb 22 2021 at 19:52):

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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Feb 22 2021 at 20:17):

Just to be clear, that works?

view this post on Zulip Adam Topaz (Feb 22 2021 at 20:17):

yes

view this post on Zulip Eric Wieser (Feb 22 2021 at 20:18):

That might be a big discovery

view this post on Zulip Adam Topaz (Feb 22 2021 at 20:21):

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

view this post on Zulip 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?)

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Feb 22 2021 at 22:58):

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

view this post on Zulip Eric Wieser (Feb 22 2021 at 22:59):

Agreed on the existential not being better than the simpler solution

view this post on Zulip Adam Topaz (Feb 22 2021 at 23:23):

Okay, I pushed this change to #6367


Last updated: May 14 2021 at 20:13 UTC