Bundled homs

Stream: maths

[Chris Hughes]

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]

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

[Chris Hughes]

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

[Keeley Hoek]

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]

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]

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]

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]

same for group/ring/linear isomorphisms

[Kevin Buzzard]

Update the issue. Have this conversation there maybe?

[Kevin Buzzard]

Or link to this.

[Keeley Hoek]

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

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Johan Commelin]

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

[Kenny Lau]

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

[Chris Hughes]

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]

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]

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]

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

[Kenny Lau]

but now everything becomes noncomputable

[Johan Commelin]

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

[Chris Hughes]

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]

Why would things become uncomputable?

[Kenny Lau]

because polynomial requires decidable equality

[Kenny Lau]

but not every object of CommRing has decidable equality

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

lol

[Johan Commelin]

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

[Mario Carneiro]

VM override goes a long way to making it happen

[Mario Carneiro]

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]

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]

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

[Kenny Lau]

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

[Kenny Lau]

this framework is quite promising

[Kenny Lau]

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

[Keeley Hoek]

What does "functor for Type" mean

[Kenny Lau]

Option : Type \func Type

[Keeley Hoek]

Ah right

[Kenny Lau]

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

[Kenny Lau]

oh it is indeed Sort u

[Kenny Lau]

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 }

[Scott Morrison]

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.