eq_to_hom in category theory

Stream: maths

[Calle Sönne]

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

[Kenny Lau]

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.

[Kevin Buzzard]

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?

[Reid Barton]

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.

[Calle Sönne]

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?

[Kevin Buzzard]

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

[Reid Barton]

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.

[Reid Barton]

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

[Calle Sönne]

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

[Calle Sönne]

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?

[Reid Barton]

inductive singleton : presieve X
| mk : singleton f

or whatever version of that actually compiles

[Reid Barton]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Eric Wieser]

@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

[Reid Barton]

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)

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

A simple example is

inductive singleton : set ℕ
| mk : singleton 1