## Stream: maths

### Topic: eq_to_hom in category theory

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


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

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

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

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

#### Kevin Buzzard (Dec 06 2020 at 12:58):

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

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

#### Reid Barton (Dec 06 2020 at 12:59):

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

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

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

#### Reid Barton (Dec 06 2020 at 13:01):

inductive singleton : presieve X
| mk : singleton f


or whatever version of that actually compiles

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

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

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

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

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

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

#### Eric Wieser (Dec 10 2020 at 09:49):

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

#### Eric Wieser (Dec 10 2020 at 09:50):

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

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