# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Quotient of a fintype is a fintype

#### Eric Wieser (Dec 06 2020 at 10:55):

This is complaining about a missing instance, but I'm pretty sure the instance is in mathlib somewhere:

```
import group_theory.perm.sign
def mod_sum_congr (α β : Type*) : setoid (equiv.perm (α ⊕ β)) :=
{ r := λ σ₁ σ₂, ∃ sl sr, σ₁ = σ₂ * equiv.sum_congr sl sr,
iseqv := ⟨
λ σ, ⟨1, 1, by simp [equiv.perm.mul_def, equiv.perm.one_def]⟩,
λ σ₁ σ₂ ⟨sl, sr, h⟩, ⟨sl⁻¹, sr⁻¹, by {
rw [h, mul_assoc],
simp [equiv.perm.mul_def, equiv.perm.inv_def]}⟩,
λ σ₁ σ₂ σ₃ ⟨sl₁₂, sr₁₂, h₁₂⟩ ⟨sl₂₃, sr₂₃, h₂₃⟩, ⟨sl₂₃ * sl₁₂, sr₂₃ * sr₁₂, by {
rw [h₁₂, h₂₃, mul_assoc],
simp [equiv.perm.mul_def, equiv.perm.inv_def]}⟩
⟩}
variables (α β : Type*) [fintype α] [fintype β] [decidable_eq α] [decidable_eq β]
#check (infer_instance : fintype (equiv.perm $ α ⊕ β)) -- ok
#check ∑ σ : quotient (mod_sum_congr α β), 1
-- failed to synthesize type class instance for "fintype (quotient (mod_sum_congr α β))"
```

#### Eric Wieser (Dec 06 2020 at 10:57):

Ah, it seems docs#quotient.fintype needs the setoid to be decidable

#### Reid Barton (Dec 06 2020 at 10:57):

This needs some decidability of the equivalence relation ... yes

#### Eric Wieser (Dec 06 2020 at 10:57):

Or `noncomputable theory`

, I suppose...

#### Eric Wieser (Dec 06 2020 at 11:09):

Any tips for how to construct the decidable instance constructively? I know how I'd write an algorithm to decide the statement, but I don't really know how to transfer them to lean; in particular, I don;t know how to state `pa`

and `pb`

in a way that lean already knows is decidable.

```
instance {α β : Type*} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :
decidable_rel (mod_sum_congr α β).r :=
λ σ₁ σ₂, begin
dunfold mod_sum_congr,
dsimp,
let pa := ∀ a₁, ∃ a₂, (σ₂⁻¹ * σ₁) (sum.inl a₁) = sum.inl a₂,
let pb := ∀ b₁, ∃ b₂, (σ₂⁻¹ * σ₁) (sum.inr b₁) = sum.inr b₂,
haveI : decidable pa := sorry,
haveI : decidable pb := sorry,
by_cases ha : pa; dsimp only [pa] at ha;
by_cases hb : pb; dsimp only [pb] at hb,
{ apply decidable.is_true,
sorry },
{ exfalso, sorry },
{ exfalso, sorry },
{ apply decidable.is_false,
sorry }
end
```

#### Eric Wieser (Dec 06 2020 at 11:11):

`pa`

should be trivially decidable via exhaustive iteration over the fintype `α`

, right?

#### Reid Barton (Dec 06 2020 at 11:14):

are there already `decidable_eq`

/`fintype`

instances for `equiv`

s between two `decidable_eq`

+`fintype`

types?

#### Eric Wieser (Dec 06 2020 at 11:15):

Nevermind:

```
instance {α β : Type*} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :
decidable_rel (mod_sum_congr α β).r :=
λ σ₁ σ₂, begin
dunfold mod_sum_congr,
apply_instance,
end
```

I must have been rememvering an older version where I used sigma types instead of sum type

Last updated: May 19 2021 at 00:40 UTC