# Zulip Chat Archive

## Stream: new members

### Topic: equivalence classes and quotients

#### Thomas Laraia (Jul 22 2021 at 09:44):

Is there a good way to reconcile the difference of `set (ℕ × ℕ)`

and `↥ourInt`

when defining `pre_add`

? Dealing with the equivalence class of an element being in the powerset of all the elements.

```
import tactic
def is_refl_type {X:Type}(S: X→ X→ Prop):=
∀ a:X, S a a
def is_symm_type {X:Type}(S: X→ X→ Prop):=
∀ a b:X, S a b→ S b a
def is_trans_type {X:Type}(S:X→ X→ Prop):=
∀ a b c:X, S a b→ S b c→ S a c
def is_equiv_type {X:Type}(S:X→ X→ Prop):=
is_refl_type S ∧ is_symm_type S
∧ is_trans_type S
def equiv_class_type {X:Type}(S:X→ X→ Prop)(a:X):set X
:= {x:X | S x a}
def quotient_type {X:Type}(S:X→ X→ Prop):=
{e:set X | ∃ a:X, e=equiv_class_type S a}
def diff : ℕ × ℕ → ℕ × ℕ → Prop :=
λ a, λ b, a.fst + b.snd = a.snd + b.fst
lemma diff_is_refl : is_refl_type diff :=
begin
unfold is_refl_type, /-just for our sanity-/
intro a,
unfold diff,
rw add_comm,
end
lemma diff_is_symm : is_symm_type diff :=
begin
unfold is_symm_type, /-sanity-/
intros a b,
intro h,
unfold diff at *,
symmetry,
rw add_comm,
rw add_comm b.fst,
exact h,
end
lemma diff_is_trans : is_trans_type diff :=
begin
unfold is_trans_type,
intros a b c,
intro h1,
intro h2,
unfold diff at *,
/-have h1h2 : (a.fst + b.snd) + (b.fst + c.snd) = (a.snd + b.fst) + (b.snd + c.fst) := by add_two_eq (a.1 + b.2) (a.2 + b.1) (b.1 + c.2) (b.2 + c.1) h1 h2,-/
have h3 : a.1 + b.2 + c.2 = a.2 + b.1 + c.2,
rw h1,
rw add_assoc a.2 at h3,
rw h2 at h3,
rw add_comm at h3,
rw add_comm b.2 c.1 at h3,
rw ← add_assoc at h3,
rw ← add_assoc at h3,
have g := add_right_cancel h3,
rw add_comm,
exact g,
end
lemma diff_is_equiv : is_equiv_type diff :=
begin
unfold is_equiv_type,
split,
exact diff_is_refl,
split,
exact diff_is_symm,
exact diff_is_trans,
end
lemma equiv_class_type_in_quotient_type {X : Type} (S: X → X → Prop) (a : X) :
equiv_class_type S a ∈ quotient_type S :=
begin
use a,
end
def ourInt := quotient_type diff
def pre_add : ℕ × ℕ → ℕ × ℕ → ourInt :=
λ a, λ b, equiv_class_type diff (a.1 + b.1, a.2 + b.2)
```

#### Anne Baanen (Jul 22 2021 at 14:58):

The error almost says the solution: you have a `set (ℕ × ℕ)`

and you need to provide an `↥ourInt`

. If you unfold the definition of `↥`

in this case, you'll see that it's `subtype (∈ quotient_type S)`

, i.e. the type of all elements `s : set X`

together with a proof that `s ∈ quotient_type S`

. Constructing an element of `subtype p`

is done with `⟨x, hx⟩`

, where `hx`

is a proof of `p x`

.

So the first step is to replace the definition of `pre_add`

with:

```
def pre_add : ℕ × ℕ → ℕ × ℕ → ourInt :=
λ a, λ b, ⟨equiv_class_type diff (a.1 + b.1, a.2 + b.2), sorry⟩
```

#### Thomas Laraia (Jul 22 2021 at 15:53):

How did you go about unfolding the definition of `↥`

here?

#### Kevin Buzzard (Jul 22 2021 at 16:14):

you can use the infoview to figure out what these arrows mean. But in this case it's not hard -- `quotient_type S`

is a set and this is a pretty standard coercion from `set X`

to `Type`

, sending the set to the corresponding subtype.

#### Thomas Laraia (Jul 22 2021 at 16:17):

Ah I'll keep messing with the infoview, with the error that came up I was unable to press on the up arrow or expand anything so I thought I'd ask.

Cheers for the help.

#### Kevin Buzzard (Jul 22 2021 at 16:21):

yeah, you need to catch it before the error :-)

#### Thomas Laraia (Jul 22 2021 at 16:24):

I guess all I have left to ask is how to get from `has_coe_to_sort.S (set (set (ℕ × ℕ)))`

to `subtype (∈ quotient_type S)`

.

#### Yakov Pechersky (Jul 22 2021 at 17:36):

Well, do you have a proof that some `s : (set (ℕ × ℕ))`

satisfies `quotient_type S`

?

#### Yakov Pechersky (Jul 22 2021 at 17:51):

```
def pre_add : ℕ × ℕ → ℕ × ℕ → ourInt :=
λ a b, -- we can introduce both tuples at the same time
-- we construct our term ourInt, which is a combination of data (the value)
-- and the proof that is has the property we require
⟨equiv_class_type diff (a.1 + b.1, a.2 + b.2), -- this is our data
-- now we give a proof that it satisfies our condition of
-- `equiv_class_type diff (a.fst + b.fst, a.snd + b.snd) ∈ ourInt`
-- but all that requires is constructing a tuple that is `diff` to the one we gave in the data
-- and a proof that they are `diff`
-- so again we provide a combination of data and proof
⟨(a.1 + b.1, a.2 + b.2), -- our compared tuple, which we can make the same for simplicity
rfl⟩⟩ -- and the proof, which is that they are the same _by definition_, which is written `rfl
```

#### Thomas Laraia (Jul 23 2021 at 09:07):

Ah yeah sorted that part just didn't know how to apply it.

```
lemma equiv_class_type_in_quotient_type {X : Type} (S: X → X → Prop) (a : X) :
equiv_class_type S a ∈ quotient_type S :=
begin
use a,
end
```

I mean I didn't see the wording `subtype (∈ quotient_type S)`

in the infoview.

I've got pre_add to work now, just asking for the future where to find that type of wording or if it is concluded from something else.

Last updated: Dec 20 2023 at 11:08 UTC