# Zulip Chat Archive

## Stream: new members

### Topic: Showing a function is well-defined (eq.rec)

#### Kyle Miller (Jul 02 2020 at 20:42):

I was trying to show there is a function from `{s : multiset α // s.card = n}`

to the quotient of `vector α n`

by permutations (actually, that there is an equivalence between these types), but I got stuck proving well-definedness due to not knowing how to deal with a `eq.rec`

that appears. Perhaps I'm not defining `to_fun`

correctly -- any suggestions or solutions would be appreciated.

The `sorry`

is in `to_fun`

below:

```
import data.quot
import data.equiv.basic
import data.vector
import data.set.function
import tactic
open function
def sym (α : Type*) (n : ℕ) := {s : multiset α // s.card = n}
def vector.is_setoid (α : Type*) (n : ℕ) : setoid (vector α n) :=
{ r := λ a b, list.perm a.1 b.1,
iseqv := by { rcases list.perm.eqv α with ⟨hr, hs, ht⟩, tidy, } }
def sym' (α : Type*) (n : ℕ) := quotient (vector.is_setoid α n)
variables (α : Type*) (n : ℕ)
def to_fun (s : sym α n) : sym' α n :=
quot.rec (λ l h, quot.mk _ ⟨l, h⟩) (begin
intros a b p,
ext h,
have p' := list.perm.length_eq p,
change b.length = n at h,
sorry,
end) s.1 s.2
def inv_fun (s' : sym' α n) : sym α n :=
quot.rec (λ s, ⟨quot.mk _ s.1, s.2⟩) (begin
intros a b p,
cases a, cases b,
induction s',
{ cases s', induction a_property,
simp only [eq_rec_constant, subtype.mk_eq_mk, multiset.coe_eq_coe, multiset.quot_mk_to_coe''],
exact p, },
refl,
end) s'
lemma left_inv : left_inverse (inv_fun α n) (to_fun α n) :=
by tidy
lemma right_inv : right_inverse (to_fun α n) (inv_fun α n) :=
by tidy
```

#### Mario Carneiro (Jul 02 2020 at 21:10):

don't use `quot.rec`

if you can avoid it

#### Mario Carneiro (Jul 02 2020 at 21:10):

`quot.lift`

is pretty much always better

#### Mario Carneiro (Jul 02 2020 at 21:11):

also, if it's an equivalence then use `quotient`

instead of `quot`

#### Mario Carneiro (Jul 02 2020 at 21:34):

Ah, never mind the `quot.rec`

is necessary

#### Mario Carneiro (Jul 02 2020 at 21:34):

See `multiset.pmap`

for an example of how to do this

#### Yury G. Kudryashov (Jul 02 2020 at 21:41):

Do we have some general statement "quotient and subtype commute up to an equivalence"?

#### Mario Carneiro (Jul 02 2020 at 21:41):

```
def to_fun (s : sym α n) : sym' α n :=
quot.rec (λ l h, quot.mk _ ⟨l, h⟩) (begin
intros a b p,
ext hb,
have ha : a.length = n := (list.perm.length_eq p).trans hb,
have : ∀ {s e h}, @eq.rec (multiset α) ↑a (λ s, s.card = n → sym' α n)
(λ h, quotient.mk' ⟨a, ha⟩) s e h = quotient.mk' ⟨a, ha⟩,
{ intros s₂ e _; subst e },
exact this.trans (quot.sound p),
end) s.1 s.2
```

#### Mario Carneiro (Jul 02 2020 at 21:43):

When defining a partial function on a quotient it is messy because you have to prove the predicate does not depend on the quotient relation. In both of these examples that's because the predicate depends on a `quotient.lift`

. I don't know if that works in general

#### Mario Carneiro (Jul 02 2020 at 22:03):

```
def quot.plift {α r} {p : @quot α r → Prop} {β} (f : ∀ a, p (quot.mk _ a) → β)
(hf : ∀ a b ha hb, r a b → f a ha = f b hb) (a) : p a → β :=
quot.rec f (begin
intros a b h,
ext hb,
have ha : p (quot.mk _ a), {rwa quot.sound h},
have : ∀ {c e h}, @eq.rec (quot r) (quot.mk _ a) (λ s, p s → β)
(λ h, f a ha) c e h = f a ha,
{ intros s₂ e _; subst e },
refine this.trans (hf _ _ _ _ h),
end) a
def to_fun (s : sym α n) : sym' α n :=
@quot.plift _ _ (λ s : multiset α, s.card = n) _
(λ l h, (quot.mk _ ⟨l, h⟩ : sym' α n))
(λ a b ha hb p, quot.sound p) s.1 s.2
```

#### Kyle Miller (Jul 02 2020 at 22:08):

Thanks, and I appreciate that you answered the follow-up question I was just about to ask, which was whether you thought there could be a version of `quot.lift`

that would let you easily use a property that respected the relation.

#### Yury G. Kudryashov (Jul 02 2020 at 22:25):

See also src#equiv.subtype_quotient_equiv_quotient_subtype

#### Yury G. Kudryashov (Jul 02 2020 at 22:26):

Probably we need a version with `{}`

-implicit setoids.

#### Kyle Miller (Jul 02 2020 at 22:39):

@Yury G. Kudryashov Thanks, that's exactly what I needed.

Style-wise, is this sort of definition OK?

```
def sym_equiv_sym' (α : Type*) (n : ℕ) : equiv (sym α n) (sym' α n) :=
begin
apply equiv.subtype_quotient_equiv_quotient_subtype,
tidy,
end
```

#### Mario Carneiro (Jul 02 2020 at 22:39):

lol

#### Mario Carneiro (Jul 02 2020 at 22:40):

it should be fine if those are just proofs, although you should tidy up `tidy`

usage

#### Kyle Miller (Jul 02 2020 at 22:40):

Even though I knew it was about subtypes and quotients commuting, I didn't think to look for it :-/ (It's even well-named! thanks mathlib contributors!)

#### Kyle Miller (Jul 02 2020 at 22:41):

Yeah, they're just proofs. I can `tidy?`

it, though.

#### Kyle Miller (Jul 02 2020 at 22:44):

It was worth it. Here's the one-liner:

```
def sym_equiv_sym' (α : Type*) (n : ℕ) : equiv (sym α n) (sym' α n) :=
equiv.subtype_quotient_equiv_quotient_subtype _ _ (by {intro, refl}) (by { intros _ _, refl })
```

#### Mario Carneiro (Jul 02 2020 at 22:47):

You can do better: `\lam _, rfl`

#### Kyle Miller (Jul 02 2020 at 22:49):

Oh, except that `refl`

is pulling in the `refl`

of a particular relation, so there's at least `(λ _, by refl)`

.

Last updated: May 13 2021 at 20:13 UTC