## Stream: maths

### Topic: Bundled homs

#### 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?

#### Kenny Lau (May 26 2019 at 12:51):

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

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

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

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

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

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

#### Mario Carneiro (May 26 2019 at 13:28):

same for group/ring/linear isomorphisms

#### Kevin Buzzard (May 26 2019 at 13:44):

Update the issue. Have this conversation there maybe?

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

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

#### Keeley Hoek (May 26 2019 at 14:01):

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

#### 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?

#### 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:

#### Johan Commelin (May 27 2019 at 11:23):

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

#### Kenny Lau (May 27 2019 at 11:23):

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

#### Kenny Lau (May 27 2019 at 11:23):

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

#### Johan Commelin (May 27 2019 at 11:24):

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

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

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

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

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

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

#### Kenny Lau (May 27 2019 at 11:40):

but now everything becomes noncomputable

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

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

#### Reid Barton (May 27 2019 at 11:45):

Why would things become uncomputable?

#### Kenny Lau (May 27 2019 at 11:45):

because polynomial requires decidable equality

#### Kenny Lau (May 27 2019 at 11:45):

but not every object of CommRing has decidable equality

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

#### Chris Hughes (May 27 2019 at 11:47):

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

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

#### Chris Hughes (May 27 2019 at 11:49):

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

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

lol

#### Johan Commelin (May 27 2019 at 11:51):

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

#### Mario Carneiro (May 27 2019 at 11:51):

VM override goes a long way to making it happen

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

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


#### Kenny Lau (May 27 2019 at 11:53):

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

#### 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,


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