Zulip Chat Archive

Stream: maths

Topic: Bundled homs


view this post on Zulip Chris Hughes (May 26 2019 at 12:48):

I think it's time to bundle homs. I'm doing algebraic closure, and unbundled homs are causing some problems.

1) It is difficult to compose them, particularly if there are more than two.
2) Lemmas that contain bundled homs in their statements tend to be slow to use. Examples are polynomial.map_map and polynomial.eval₂_map This lemma is also causing me problems.

lemma algebraic_comp' {L M : Type*} [discrete_field L] [discrete_field M]
  (i : K  L) (j : L  M) [is_field_hom i] [is_field_hom j] :
  ( x, algebraic i x)  ( x, algebraic j x)   x, algebraic (j  i) x

3) All the simp lemmas will work.

How should this be done? In particular should it be done in some sort of category theory framework?

view this post on Zulip Kenny Lau (May 26 2019 at 12:51):

https://github.com/leanprover-community/mathlib/pull/717

view this post on Zulip Chris Hughes (May 26 2019 at 12:52):

I want to bundle all of them at once. No good only bundling field homs, because I use ring hom lemmas.

view this post on Zulip Keeley Hoek (May 26 2019 at 13:08):

Maybe you could use this business? https://github.com/leanprover-community/mathlib/blob/c6a7f300ea43cfc0478e3ee81a141d5288d90df6/src/category_theory/instances/CommRing/basic.lean#L31
Then the \hom arrow gives ring homs

view this post on Zulip Mario Carneiro (May 26 2019 at 13:24):

I am of course in favor of this. I would suggest something like linear_map: the types are still unbundled in the usual way, but the map types are fully bundled and have the types as explicit args

view this post on Zulip Mario Carneiro (May 26 2019 at 13:25):

So explicit reference to category theory is not necessary and I think not all that useful for this. Rather, I think that category theory stands to gain from bundled maps since it makes it easy to define the hom-sets

view this post on Zulip Mario Carneiro (May 26 2019 at 13:28):

The experts can weigh in but I don't really see how category theory can be leveraged to reduce duplication here. Sure we can say "these maps and types form a category" but that doesn't make the definition of the maps any easier, and for defeq reasons we want a bespoke definition anyway

view this post on Zulip Mario Carneiro (May 26 2019 at 13:28):

same for group/ring/linear isomorphisms

view this post on Zulip Kevin Buzzard (May 26 2019 at 13:44):

Update the issue. Have this conversation there maybe?

view this post on Zulip Kevin Buzzard (May 26 2019 at 13:45):

Or link to this.

view this post on Zulip Keeley Hoek (May 26 2019 at 13:47):

@Scott Morrison should weigh in and not me (and I've no idea how much he cares), but there are some things to say for the category theory machinery; no new notation like f' ∘ᶠ f would need to exist, for example

view this post on Zulip Chris Hughes (May 26 2019 at 13:55):

I wasn't really suggesting any advanced category theory, just basically using the same notation as we do for the category theory version, and making a hom in the category of groups the same thing as a group hom.

view this post on Zulip Keeley Hoek (May 26 2019 at 14:01):

Sorry, I just copied that from a random comment on the issue Kevin mentioned

view this post on Zulip Johan Commelin (May 27 2019 at 11:21):

@Chris Hughes Can't we just leave the library as is, and use the category CommRing whenever you need bundled homs?

view this post on Zulip Johan Commelin (May 27 2019 at 11:22):

That we we don't need →_am, →_m, →_ag, →_g, →_sr, →_r notations for all the different algebraic structures. :smiley:

view this post on Zulip Johan Commelin (May 27 2019 at 11:23):

Don't forget that I didn't even mention topological (add) groups, topological rings, etc...

view this post on Zulip Kenny Lau (May 27 2019 at 11:23):

the category library is... well... at times hard to use

view this post on Zulip Kenny Lau (May 27 2019 at 11:23):

but that's the me 3 months ago speaking; the library might have changed a lot

view this post on Zulip Johan Commelin (May 27 2019 at 11:24):

Please complain on the chat with MWE's... (-; Then we can work to improve it.

view this post on Zulip Kenny Lau (May 27 2019 at 11:26):

I remember that time when I couldn't construct the "shift by 1" map for the infinite coproduct of a certain object

view this post on Zulip Chris Hughes (May 27 2019 at 11:35):

The trouble with using the category theory library, is then I'll need to do things like prove polynomial is a functor, which we already have basically, but not in the language of category theory. Also, direct limit is not in the category theory language.

view this post on Zulip Johan Commelin (May 27 2019 at 11:38):

Turning polynomial into a functor costs you 3 lines: https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/instances/CommRing/adjunctions.lean#L23

view this post on Zulip Johan Commelin (May 27 2019 at 11:39):

This file gives you a whole bunch of stuff about colimits of CommRings: https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/instances/CommRing/colimits.lean

view this post on Zulip Johan Commelin (May 27 2019 at 11:39):

Maybe you need some specialised things, but it shouldn't take more time than it takes to build those specialised things directly.

view this post on Zulip Kenny Lau (May 27 2019 at 11:40):

but now everything becomes noncomputable

view this post on Zulip Johan Commelin (May 27 2019 at 11:41):

The computability framework is a pain. I want to be able to post-hoc prove that a definition is computable.

view this post on Zulip Chris Hughes (May 27 2019 at 11:44):

I think the approach we should take to computability is to not sacrifice ease of use for computability, and if you really want to compute something, write the computable version, and prove it's the same as the version with lemmas about it. But this is a different discussion.

view this post on Zulip Reid Barton (May 27 2019 at 11:45):

Why would things become uncomputable?

view this post on Zulip Kenny Lau (May 27 2019 at 11:45):

because polynomial requires decidable equality

view this post on Zulip Kenny Lau (May 27 2019 at 11:45):

but not every object of CommRing has decidable equality

view this post on Zulip Johan Commelin (May 27 2019 at 11:46):

@Reid Barton See this functor: https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/instances/CommRing/adjunctions.lean#L23

view this post on Zulip Johan Commelin (May 27 2019 at 11:47):

There are not that many computable algebraically closed fields. And for computations with those fields, we might want to have more streamlined constructions anyway...

view this post on Zulip Chris Hughes (May 27 2019 at 11:47):

I also need other things like eval2_map. This is something other than functoriality.

view this post on Zulip Johan Commelin (May 27 2019 at 11:48):

Can't you just use it? You might need a rw/simp-lemma that rewrites the application of the functor to a form where you can use eval₂_map...

view this post on Zulip Chris Hughes (May 27 2019 at 11:49):

I can't use it right now. It's really slow without bundled homs.

view this post on Zulip Mario Carneiro (May 27 2019 at 11:49):

I agree about post hoc computability. More generally, we want to separate the computational implementation from the abstract mathematical definition

view this post on Zulip Mario Carneiro (May 27 2019 at 11:50):

lol

view this post on Zulip Johan Commelin (May 27 2019 at 11:51):

@Mario Carneiro @Simon Hudon @Keeley Hoek @Edward Ayers Please make this happen :thank_you:

view this post on Zulip Mario Carneiro (May 27 2019 at 11:51):

VM override goes a long way to making it happen

view this post on Zulip Mario Carneiro (May 27 2019 at 11:52):

I think that the noncomputable marker (or more specifically the lack of it) is not of that much importance if we can't actually use the generated code

view this post on Zulip Kenny Lau (May 27 2019 at 11:53):

import category_theory.concrete_category

universe u

open category_theory

namespace category_theory.instances

@[reducible] def DecEq := bundled decidable_eq

instance (x : DecEq) : decidable_eq x := x.str

instance DecEq_category : category DecEq :=
{ hom := λ x y, x  y,
  id := λ x, id,
  comp := λ x y z f g, g  f }

end category_theory.instances

view this post on Zulip Kenny Lau (May 27 2019 at 11:53):

in the meantime should we have a category of discrete rings?

view this post on Zulip Kenny Lau (May 27 2019 at 12:03):

namespace DecEq

def Option : DecEq  DecEq :=
{ obj := λ x, option x, option.decidable_eq,
  map := λ x y, option.map,
  map_id' := λ x, option.map_id,
  map_comp' := λ x y z f g, funext $ λ a, by cases a; refl }

end DecEq

view this post on Zulip Kenny Lau (May 27 2019 at 12:03):

this framework is quite promising

view this post on Zulip Kenny Lau (May 27 2019 at 12:08):

speaking of which, do we have those functors for Type?

view this post on Zulip Keeley Hoek (May 27 2019 at 12:09):

What does "functor for Type" mean

view this post on Zulip Kenny Lau (May 27 2019 at 12:09):

Option : Type \func Type

view this post on Zulip Keeley Hoek (May 27 2019 at 12:09):

Ah right

view this post on Zulip Kenny Lau (May 27 2019 at 12:10):

wait it can't be called Type, what is it called

view this post on Zulip Kenny Lau (May 27 2019 at 12:10):

oh it is indeed Sort u

view this post on Zulip Kenny Lau (May 27 2019 at 12:11):

def Option : Type u  Type u :=
{ obj := option,
  map := λ x y, option.map,
  map_id' := λ x, option.map_id,
  map_comp' := λ x y z f g, funext $ λ a, by cases a; refl }

view this post on Zulip Scott Morrison (May 28 2019 at 15:38):

I think rather than defining Option by hand we might want to write as_functor option, which would look for the computer scientists' is_lawful_functor instance.


Last updated: May 09 2021 at 09:11 UTC