Stream: maths

Topic: making an equiv

Ali Sever (Sep 07 2018 at 19:21):

I have f : α → α → α → α → α → α → Prop that says a ≠ b ∧ c ≠ b ∧ d ≠ e ∧ f ≠ e ∧ blah. I have shown fis reflexive, symmetric and transitive (i.e. an equiv on α × α × α), but only when a ≠ b ∧ c ≠ b. Now I want to make the equiv classes, I'm having trouble with deciding what to do.
If I set f to take a random value for a = b, then working with fis going to be annoying. If I make the equiv on α × α × α such that a ≠ b ∧ c ≠ b, then any time I talk about the class a b c I have to give proofs of a ≠ band c ≠ b. Is there different method?

In GeoCoq they cheat, instead of making an equiv, they make a new function (which is what the book does too),

Definition Q_CongA a :=
∃ A B C,
A ≠ B ∧ C ≠ B ∧ ∀ X Y Z, CongA A B C X Y Z ↔ a X Y Z.


Chris Hughes (Sep 07 2018 at 19:33):

You could define the equivalence relation on the subtype. It sounds like you just have to give proofs that a \ne b and stuff. Lean is all about edge cases. Why do you consider the GeoCoq solution cheating? You can define quotients on non-equivalence relations in lean, but it's not recommended.

Ali Sever (Sep 08 2018 at 08:21):

I want to define a function from an equivalence class, but to give the value I first need an element from the class (but every element gives the same result), how would I do this? i.e. I want to make a function which I know is well-defined

Reid Barton (Sep 08 2018 at 08:24):

Assuming you're using quot/quotient, then quot.lift/quotient.lift

Kevin Buzzard (Sep 08 2018 at 10:26):

Ali I don't know if this helps, but when Luca was learning about equivalence classes (because he wanted to define a group structure on pi_1(X,x), which is a quotient) I wrote https://github.com/kbuzzard/xena/blob/master/xenalib/m1f/zmod37.lean to show him some basic tricks. For basic questions like how to define a function on a set of equivalence classes I could recommend the relevant docs https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#quotients from TPIL, however mathlib adds extra functions which one can use with quotients, and these are not documented here. The mathlib file is here https://github.com/leanprover/mathlib/blob/master/data/quot.lean and it defines things such as quotient.eq which are very useful in practice.

Ali Sever (Sep 08 2018 at 14:44):

Thanks, I was reading up on these this morning. I don't think there's a way to use the "cheat" method Coq uses (above), because I can't use exists to eliminate into something that isn't Prop.

Ali Sever (Sep 09 2018 at 12:59):

is there a way to do quot.lift on a set with a function that is constant over the set?

Chris Hughes (Sep 09 2018 at 13:03):

You mean a computable function from set \a that's based on some arbitrary element of a set?

Chris Hughes (Sep 09 2018 at 13:03):

The answer is probably no, because a set contains no computational content about it's elements.

Ali Sever (Sep 09 2018 at 13:05):

Why does it work for quotient sets, but not just normal sets?

Kevin Buzzard (Sep 09 2018 at 13:07):

Why don't you formalise exactly what you're asking in Lean and post it? It's good practice, and also good practice.

Ali Sever (Sep 09 2018 at 13:19):

Something like this,
def F {α β : Type} (A : set α) (f : α → β) : (∀ a b, a ∈ A → b ∈ A → f a = f b) → β := x

Johannes Hölzl (Sep 09 2018 at 13:26):

This is not enough. You need to assume that A is not empty.

Johannes Hölzl (Sep 09 2018 at 13:27):

Then you can use some form of choice. (or you know that β is not empty and chose a default element.

Reid Barton (Sep 09 2018 at 13:28):

Or if you express the nonempty condition as trunc A, which is the quotient of A by the relation which identifies everything, then you can define F (computably) using quotient.lift.

Reid Barton (Sep 09 2018 at 13:29):

If you use choice, then you don't even need the condition (∀ a b, a ∈ A → b ∈ A → f a = f b) to define F, which is mildly alarming, but you do need it to prove that F equals f a for any a ∈ A.

Ali Sever (Sep 09 2018 at 13:34):

If I use trunc, will it be annoying to switch between A and trunc A?

Reid Barton (Sep 09 2018 at 13:47):

Well trunc A is an alternative to nonempty A, which you would need instead.
The main annoyance of trunc A is that it isn't a proposition.

Kevin Buzzard (Sep 09 2018 at 13:50):

Something like this,
def F {α β : Type} (A : set α) (f : α → β) : (∀ a b, a ∈ A → b ∈ A → f a = f b) → β := x

You mean := sorry? As others have pointed out this can't yet be done (alpha and beta could both be empty at this point). So in some sense you still haven't asked the question.

Ali Sever (Sep 09 2018 at 13:58):

I guess I'll have to try a different approach

Kevin Buzzard (Sep 09 2018 at 14:04):

I'm not saying that any approach doesn't work, but I am saying that I've learnt from experience that actually formalising my question precisely as definition : blah := sorry or theorem : blah := sorry really helps me to understand what I am asking before I ask it.

Last updated: May 12 2021 at 07:17 UTC