Proving a trivial lemma about homomorphisms.

Stream: new members

[Jan Matula]

Hello, I was wondering how a I might prove this lemma:

lemma equate_hom {X Y : Magma} :
∀ f g : Hom X Y, f.func = g.func  →  f = g

where Hom is defined like this:

class hom {X Y : Magma} (f : X → Y) :=
  (resp_op : ∀ x y : X,
    f (X.op x y) = Y.op (f x) (f y) )

structure Hom (X Y : Magma) :=
  (func : X → Y) (hom_func : hom func)

Somehow I can't seem to do this, though it should probably be quite simple.

[Jan Matula]

the full example online

[Eric Wieser]

Note it's usually best to paste the full code directly here rather than link to the web editor; Zulip adds an "open in web editor" link automatically.

[Jan Matula]

No problem, this is the full code:

universe u

/-
magmas:
-/

structure Magma :=
  (carrier : Type u)
  (op : carrier → carrier → carrier)

instance Magma_to_sort :
has_coe_to_sort Magma (Type u) :=
  ⟨ Magma.carrier ⟩

/-
homomorphisms:
-/

class hom {X Y : Magma} (f : X → Y) :=
  (resp_op : ∀ x y : X,
    f (X.op x y) = Y.op (f x) (f y) )

structure Hom (X Y : Magma) :=
  (func : X → Y) (hom_func : hom func)

instance Hom.to_fun {X Y : Magma} :
has_coe_to_fun (Hom X Y) (λ _, X → Y) :=
  ⟨ Hom.func ⟩

-- how do I prove this?
lemma equate_hom {X Y : Magma} :
∀ f g : Hom X Y, f.func = g.func  →  f = g :=
  sorry

[Eric Wieser]

You will have a better time if you change

class hom {X Y : Magma} (f : X → Y) :=

to

class hom {X Y : Magma} (f : X → Y) : Prop :=

[Patrick Massot]

The most important answer is: you shouldn't be using Lean 3 which is fully deprecated.

[Patrick Massot]

And then indeed the second answer is what Eric wrote.

[Eric Rodriguez]

Eric Wieser said:

You will have a better time if you change

class hom {X Y : Magma} (f : X → Y) :=

to

class hom {X Y : Magma} (f : X → Y) : Prop :=

and then the @[ext] attribute can help you make these lemmas automatically

[Eric Wieser]

Which to be clear, goes on structure Hom not class hom

[Patrick Massot]

To be clear: the fact that this : Prop is required is clearly a bug, but it will never be fixed in Lean 3 which is completely frozen forever.

[Eric Wieser]

I don't know if we opened a Lean4 issue about it yet...

[Patrick Massot]

And the @[ext] attribute will require some import (probably from mathlib).

[Mario Carneiro]

it's in std

[Eric Rodriguez]

Is this goal proable without : Prop? It should still be a subsingleton, right? Just not definitionalyl

[Eric Wieser]

Yeah, but you get an annoying HEq for the hom field

[Patrick Massot]

Mario, I was answering the Lean 3 question, but indeed in Lean 4 it is in std.

[Jan Matula]

Patrick Massot said:

The most important answer is: you shouldn't be using Lean 3 which is fully deprecated.

Somehow I was under the impression that Lean 3 was the stable one, while Lean 4 is work in progress.

[Ruben Van de Velde]

You're a few weeks out of date :)

[Kevin Buzzard]

Mathlib 3 is no longer accepting PRs and mathlib 4 is fully up and running! And yeah this is a recent event.