Zulip Chat Archive

Stream: maths

Topic: eq_to_hom in category theory


view this post on Zulip Calle Sönne (Dec 06 2020 at 11:42):

Hello. I am currently trying to read through the mathlib stuff on Grothendieck topologies, and whilst reading about sieves I stumbled upon this wierd eq_to_hom defined as:

/--
An equality `X = Y` gives us a morphism `X ⟶ Y`.

It is typically better to use this, rather than rewriting by the equality then using `𝟙 _`
which usually leads to dependent type theory hell.
-/
def eq_to_hom {X Y : C} (p : X = Y) : X  Y := by rw p; exact 𝟙 _

As someone who isnt too well-versed in LEAN yet I am quite confused why this definition is necessary. According to the comment it seems like this is used in order to avoid having to rewrite the equality and then using 𝟙 _. But isnt this exactly what the definition is doing? I guess my question is, whats the difference between using eq_to_hom as opposed to the other method (other than being shorter I guess). Here is a simple example of it in action:

def presieve (X : C) := Π Y⦄, set (Y  X)

/-- The singleton presieve.  -/
-- Note we can't make this into `has_singleton` because of the out-param.
def singleton : presieve X :=
λ Z g,  (H : Z = Y), eq_to_hom H  f = g

view this post on Zulip Kenny Lau (Dec 06 2020 at 12:54):

It is better to have a pre-defined function than to rewrite H at that place, because the goals generated will be difficult to work with.

view this post on Zulip Kevin Buzzard (Dec 06 2020 at 12:55):

But if you unfold eq_to_hom you'll still get messy goals, and if you don't unfold it, how do you work with it? Presumably the idea is that there's some API for this function?

view this post on Zulip Reid Barton (Dec 06 2020 at 12:56):

It's an isomorphism with inverse also an eq_to_hom, if you compose an eq_to_hom from X to Y with an eq_to_hom from Y to Z you get an eq_to_hom from X to Z, and if you have an eq_to_hom from X to X it's the identity. This means that if you accumulated a bunch of these from different places but in the end you need to check some equation, it will always contain eq_to_homs that cancel automatically.

view this post on Zulip Calle Sönne (Dec 06 2020 at 12:57):

So when Is it I get difficult goals? Is it if I am using rewrite in a definition/construction? Because If I am proving some theorem it shouldnt matter right?

view this post on Zulip Kevin Buzzard (Dec 06 2020 at 12:58):

Don't unfold it and it sounds like you'll be fine.

view this post on Zulip Reid Barton (Dec 06 2020 at 12:58):

Calle means using rw instead I think. If you use rw in a definition then you'll get difficult goals when you try to prove a theorem about the definition.

view this post on Zulip Reid Barton (Dec 06 2020 at 12:59):

That said I'm not sure it really makes sense to use it in this singleton

view this post on Zulip Calle Sönne (Dec 06 2020 at 13:00):

Oh great then I get it, thanks. So the point is to make some sort of API for this so that when someone needs to use it in a definition then it wont be too bad

view this post on Zulip Calle Sönne (Dec 06 2020 at 13:00):

Reid Barton said:

That said I'm not sure it really makes sense to use it in this singleton

so here it would be OK to rewrite?

view this post on Zulip Reid Barton (Dec 06 2020 at 13:01):

inductive singleton : presieve X
| mk : singleton f

or whatever version of that actually compiles

view this post on Zulip Reid Barton (Dec 06 2020 at 13:04):

It doesn't really matter, but I'd expect anything you'd want to do with a presieve to get slightly easier with that definition

view this post on Zulip Bhavik Mehta (Dec 06 2020 at 14:44):

Yeah, I think this singleton definition isn't ideal, if Reid's suggestion can be made to compile I'm in favour of changing

view this post on Zulip Bhavik Mehta (Dec 06 2020 at 14:46):

I think a good way to understand eq_to_hom is that you're trying to construct data (a morphism) and so using tactics like rw will make it incredibly hard to prove things about the data. But, if you use eq_to_hom then what's left is to fill in a proof, and as Reid says it's usually easy to prove what you need about the eq_to_hom chain that you end up with

view this post on Zulip Bhavik Mehta (Dec 09 2020 at 17:42):

Reid Barton said:

inductive singleton : presieve X
| mk : singleton f

or whatever version of that actually compiles

this worked and improved proofs! https://github.com/leanprover-community/mathlib/pull/5295

view this post on Zulip Eric Wieser (Dec 10 2020 at 09:30):

@Reid Barton, would you mind explaining what's going on there? I'm used to only seeing : Type or : Prop to the right of inductive

view this post on Zulip Reid Barton (Dec 10 2020 at 09:47):

Lean is happy to unfold a term which expands to a Pi type ending in Type or Prop (within reason, I don't know the exact rules)

view this post on Zulip Eric Wieser (Dec 10 2020 at 09:49):

I can't see to construct an example myself that doesn't depend on presieve

view this post on Zulip Eric Wieser (Dec 10 2020 at 09:50):

Oh, right - the key thing is that set A is actually A → Prop

view this post on Zulip Eric Wieser (Dec 10 2020 at 09:51):

A simple example is

inductive singleton : set 
| mk : singleton 1

Last updated: May 09 2021 at 09:11 UTC