## 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 equivs 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