Commit 2024-07-14 21:27 81112189

refactor(Mathlib/Data/DFinsupp/Basic): remove Decidable instances from some DFinsupp functions (#13235) This PR removes Decidable instances from these DFinsupp functions:

def DFinsupp.sigmaUncurry
    {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → Zero (δ i j)]
    [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → Decidable (x ≠ 0)]
    (f : Π₀ (i : ι) (j : α i), δ i j) : Π₀ (i : (i : ι) × α i), δ i.fst i.snd
def DFinsupp.sigmaCurryEquiv
    {ι : Type u} [DecidableEq ι] {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → Zero (δ i j)]
    [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → Decidable (x ≠ 0)] :
  Π₀ (i : (i : ι) × α i), δ i.fst i.snd ≃ Π₀ (i : ι) (j : α i), δ i j

to

def DFinsupp.sigmaUncurry
    {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → Zero (δ i j)] [DecidableEq ι]
    (f : Π₀ (i : ι) (j : α i), δ i j) : Π₀ (i : (i : ι) × α i), δ i.fst i.snd
def DFinsupp.sigmaCurryEquiv
    {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → Zero (δ i j)] [DecidableEq ι] :
  Π₀ (i : (i : ι) × α i), δ i.fst i.snd ≃ Π₀ (i : ι) (j : α i), δ i j

We use Trunc.finChoice from #13025 to compute support with the only DecidableEq ι instance. 2.

instance DFinsupp.decidableZero
    {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (f : Π₀ (i : ι), β i) :
  Decidable (0 = f)

to

instance DFinsupp.decidableZero
    {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x = 0)] (f : Π₀ (i : ι), β i) :
  Decidable (f = 0)

We remove the redundant DecidableEq ι instance. Additionally, We replace the (i : ι) → (x : β i) → Decidable (x ≠ 0) instance with (i : ι) → (x : β i) → Decidable (x = 0) because it's more principal, and swaps f and 0. 3.

noncomputable def DFinsupp.comapDomain
    {ι : Type u} {β : ι → Type v} [DecidableEq ι] {κ : Type u_1} [(i : ι) → Zero (β i)] (h : κ → ι) (hh : Function.Injective h) (f : Π₀ (i : ι), β i) :
  Π₀ (k : κ), β (h k)

to

noncomputable def DFinsupp.comapDomain
    {ι : Type u} {β : ι → Type v} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : κ → ι) (hh : Function.Injective h) (f : Π₀ (i : ι), β i) :
  Π₀ (k : κ), β (h k)

DecidableEq ι is required to compute unconstructive support so this is redundant.