import algebra.module.linear_map

import algebra.big_operators.basic

import data.set.finite

import group_theory.submonoid.membership

import group_theory.group_action.big_operators

import data.finset.preimage

universes u u₁ u₂ v v₁ v₂ v₃ w x y l

open_locale big_operators

variables {ι : Type u} {γ : Type w} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂}

variable (β)

structure dfinsupp [Π i, has_zero (β i)] : Type (max u v) :=

mk' ::

(to_fun : Π i, β i)

(support' : trunc {s : multiset ι // ∀ i, i ∈ s ∨ to_fun i = 0})

variable {β}

notation `Π₀` binders `, ` r:(scoped f, dfinsupp f) := r

infix ` →ₚ `:25 := dfinsupp

namespace dfinsupp

section basic

variables [Π i, has_zero (β i)] [Π i, has_zero (β₁ i)] [Π i, has_zero (β₂ i)]

instance fun_like : fun_like (Π₀ i, β i) ι β :=

⟨λ f, f.to_fun, λ ⟨f₁, s₁⟩ ⟨f₂, s₁⟩ (h : f₁= f₂), by { subst h, congr'} ⟩

instance : has_coe_to_fun (Π₀ i, β i) (λ _, Π i, β i) := fun_like.has_coe_to_fun

@[simp] lemma to_fun_eq_coe (f : Π₀ i, β i) : f.to_fun = f := rfl

@[ext] lemma ext {f g : Π₀ i, β i} (h : ∀ i, f i = g i) : f = g := fun_like.ext _ _ h

lemma ext_iff {f g : Π₀ i, β i} : f = g ↔ ∀ i, f i = g i := fun_like.ext_iff

lemma coe_fn_injective : @function.injective (Π₀ i, β i) (Π i, β i) coe_fn := fun_like.coe_injective

instance : has_zero (Π₀ i, β i) := ⟨⟨0, trunc.mk $ ⟨∅, λ i, or.inr rfl⟩⟩⟩

instance : inhabited (Π₀ i, β i) := ⟨0⟩

lemma coe_mk' (f : Π i, β i) (s) : ⇑(⟨f, s⟩ : Π₀ i, β i) = f := rfl

@[simp] lemma coe_zero : ⇑(0 : Π₀ i, β i) = 0 := rfl

lemma zero_apply (i : ι) : (0 : Π₀ i, β i) i = 0 := rfl

def map_range (f : Π i, β₁ i → β₂ i) (hf : ∀ i, f i 0 = 0) (x : Π₀ i, β₁ i) : Π₀ i, β₂ i :=

⟨λ i, f i (x i), x.support'.map $ λ s, ⟨s, λ i, (s.2 i).imp_right $ λ h : x i = 0, h.symm ▸ hf i⟩⟩

@[simp] lemma map_range_apply

(f : Π i, β₁ i → β₂ i) (hf : ∀ i, f i 0 = 0) (g : Π₀ i, β₁ i) (i : ι) :

map_range f hf g i = f i (g i) :=

rfl

@[simp] lemma map_range_id (h : ∀ i, id (0 : β₁ i) = 0 := λ i, rfl) (g : Π₀ (i : ι), β₁ i) :

map_range (λ i, (id : β₁ i → β₁ i)) h g = g :=

by { ext, refl }

lemma map_range_comp (f : Π i, β₁ i → β₂ i) (f₂ : Π i, β i → β₁ i)

(hf : ∀ i, f i 0 = 0) (hf₂ : ∀ i, f₂ i 0 = 0) (h : ∀ i, (f i ∘ f₂ i) 0 = 0)

(g : Π₀ (i : ι), β i) :

map_range (λ i, f i ∘ f₂ i) h g = map_range f hf (map_range f₂ hf₂ g) :=

by { ext, simp only [map_range_apply] }

@[simp] lemma map_range_zero (f : Π i, β₁ i → β₂ i) (hf : ∀ i, f i 0 = 0) :

map_range f hf (0 : Π₀ i, β₁ i) = 0 :=

by { ext, simp only [map_range_apply, coe_zero, pi.zero_apply, hf] }

def zip_with (f : Π i, β₁ i → β₂ i → β i) (hf : ∀ i, f i 0 0 = 0)

(x : Π₀ i, β₁ i) (y : Π₀ i, β₂ i) : (Π₀ i, β i) :=

⟨λ i, f i (x i) (y i), begin

refine x.support'.bind (λ xs, _),

refine y.support'.map (λ ys, _),

refine ⟨xs + ys, λ i, _⟩,

obtain h1 | (h1 : x i = 0) := xs.prop i,

{ left, rw multiset.mem_add, left, exact h1 },

obtain h2 | (h2 : y i = 0) := ys.prop i,

{ left, rw multiset.mem_add, right, exact h2 },

right, rw [h1, h2, hf]

end⟩

@[simp] lemma zip_with_apply

(f : Π i, β₁ i → β₂ i → β i) (hf : ∀ i, f i 0 0 = 0) (g₁ : Π₀ i, β₁ i) (g₂ : Π₀ i, β₂ i) (i : ι) :

zip_with f hf g₁ g₂ i = f i (g₁ i) (g₂ i) :=

rfl

section piecewise

variables (x y : Π₀ i, β i) (s : set ι) [Π i, decidable (i ∈ s)]

def piecewise : Π₀ i, β i := zip_with (λ i x y, if i ∈ s then x else y) (λ _, if_t_t _ 0) x y

lemma piecewise_apply (i : ι) : x.piecewise y s i = if i ∈ s then x i else y i :=

zip_with_apply _ _ x y i

@[simp, norm_cast] lemma coe_piecewise : ⇑(x.piecewise y s) = s.piecewise x y :=

by { ext, apply piecewise_apply }

end piecewise

end basic

section algebra

instance [Π i, add_zero_class (β i)] : has_add (Π₀ i, β i) :=

⟨zip_with (λ _, (+)) (λ _, add_zero 0)⟩

lemma add_apply [Π i, add_zero_class (β i)] (g₁ g₂ : Π₀ i, β i) (i : ι) :

(g₁ + g₂) i = g₁ i + g₂ i :=

rfl

@[simp] lemma coe_add [Π i, add_zero_class (β i)] (g₁ g₂ : Π₀ i, β i) :

⇑(g₁ + g₂) = g₁ + g₂ :=

rfl

instance [Π i, add_zero_class (β i)] : add_zero_class (Π₀ i, β i) :=

fun_like.coe_injective.add_zero_class _ coe_zero coe_add

instance has_nat_scalar [Π i, add_monoid (β i)] : has_smul ℕ (Π₀ i, β i) :=

⟨λc v, v.map_range (λ _, (•) c) (λ _, nsmul_zero _)⟩

lemma nsmul_apply [Π i, add_monoid (β i)] (b : ℕ) (v : Π₀ i, β i) (i : ι) :

(b • v) i = b • (v i) :=

rfl

@[simp] lemma coe_nsmul [Π i, add_monoid (β i)] (b : ℕ) (v : Π₀ i, β i) : ⇑(b • v) = b • v :=

rfl

instance [Π i, add_monoid (β i)] : add_monoid (Π₀ i, β i) :=

fun_like.coe_injective.add_monoid _ coe_zero coe_add (λ _ _, coe_nsmul _ _)

def coe_fn_add_monoid_hom [Π i, add_zero_class (β i)] : (Π₀ i, β i) →+ (Π i, β i) :=

{ to_fun := coe_fn, map_zero' := coe_zero, map_add' := coe_add }

def eval_add_monoid_hom [Π i, add_zero_class (β i)] (i : ι) : (Π₀ i, β i) →+ β i :=

(pi.eval_add_monoid_hom β i).comp coe_fn_add_monoid_hom

instance [Π i, add_comm_monoid (β i)] : add_comm_monoid (Π₀ i, β i) :=

fun_like.coe_injective.add_comm_monoid _ coe_zero coe_add (λ _ _, coe_nsmul _ _)

@[simp] lemma coe_finset_sum {α} [Π i, add_comm_monoid (β i)] (s : finset α) (g : α → Π₀ i, β i) :

⇑(∑ a in s, g a) = ∑ a in s, g a :=

(coe_fn_add_monoid_hom : _ →+ (Π i, β i)).map_sum g s

@[simp] lemma finset_sum_apply {α} [Π i, add_comm_monoid (β i)] (s : finset α) (g : α → Π₀ i, β i)

(i : ι) :

(∑ a in s, g a) i = ∑ a in s, g a i :=

(eval_add_monoid_hom i : _ →+ β i).map_sum g s

instance [Π i, add_group (β i)] : has_neg (Π₀ i, β i) :=

⟨λ f, f.map_range (λ _, has_neg.neg) (λ _, neg_zero)⟩

lemma neg_apply [Π i, add_group (β i)] (g : Π₀ i, β i) (i : ι) : (- g) i = - g i :=

rfl

@[simp] lemma coe_neg [Π i, add_group (β i)] (g : Π₀ i, β i) : ⇑(- g) = - g :=

rfl

instance [Π i, add_group (β i)] : has_sub (Π₀ i, β i) :=

⟨zip_with (λ _, has_sub.sub) (λ _, sub_zero 0)⟩

lemma sub_apply [Π i, add_group (β i)] (g₁ g₂ : Π₀ i, β i) (i : ι) :

(g₁ - g₂) i = g₁ i - g₂ i :=

rfl

@[simp] lemma coe_sub [Π i, add_group (β i)] (g₁ g₂ : Π₀ i, β i) :

⇑(g₁ - g₂) = g₁ - g₂ :=

rfl

instance has_int_scalar [Π i, add_group (β i)] : has_smul ℤ (Π₀ i, β i) :=

⟨λc v, v.map_range (λ _, (•) c) (λ _, zsmul_zero _)⟩

lemma zsmul_apply [Π i, add_group (β i)] (b : ℤ) (v : Π₀ i, β i) (i : ι) : (b • v) i = b • (v i) :=

rfl

@[simp] lemma coe_zsmul [Π i, add_group (β i)] (b : ℤ) (v : Π₀ i, β i) : ⇑(b • v) = b • v :=

rfl

instance [Π i, add_group (β i)] : add_group (Π₀ i, β i) :=

fun_like.coe_injective.add_group _

coe_zero coe_add coe_neg coe_sub (λ _ _, coe_nsmul _ _) (λ _ _, coe_zsmul _ _)

instance [Π i, add_comm_group (β i)] : add_comm_group (Π₀ i, β i) :=

fun_like.coe_injective.add_comm_group _

coe_zero coe_add coe_neg coe_sub (λ _ _, coe_nsmul _ _) (λ _ _, coe_zsmul _ _)

instance [monoid γ] [Π i, add_monoid (β i)] [Π i, distrib_mul_action γ (β i)] :

has_smul γ (Π₀ i, β i) :=

⟨λc v, v.map_range (λ _, (•) c) (λ _, smul_zero _)⟩

lemma smul_apply [monoid γ] [Π i, add_monoid (β i)]

[Π i, distrib_mul_action γ (β i)] (b : γ) (v : Π₀ i, β i) (i : ι) :

(b • v) i = b • (v i) :=

rfl

@[simp] lemma coe_smul [monoid γ] [Π i, add_monoid (β i)]

[Π i, distrib_mul_action γ (β i)] (b : γ) (v : Π₀ i, β i) :

⇑(b • v) = b • v :=

rfl

instance {δ : Type*} [monoid γ] [monoid δ]

[Π i, add_monoid (β i)] [Π i, distrib_mul_action γ (β i)] [Π i, distrib_mul_action δ (β i)]

[Π i, smul_comm_class γ δ (β i)] :

smul_comm_class γ δ (Π₀ i, β i) :=

{ smul_comm := λ r s m, ext $ λ i, by simp only [smul_apply, smul_comm r s (m i)] }

instance {δ : Type*} [monoid γ] [monoid δ]

[Π i, add_monoid (β i)] [Π i, distrib_mul_action γ (β i)] [Π i, distrib_mul_action δ (β i)]

[has_smul γ δ] [Π i, is_scalar_tower γ δ (β i)] :

is_scalar_tower γ δ (Π₀ i, β i) :=

{ smul_assoc := λ r s m, ext $ λ i, by simp only [smul_apply, smul_assoc r s (m i)] }

instance [monoid γ] [Π i, add_monoid (β i)] [Π i, distrib_mul_action γ (β i)]

[Π i, distrib_mul_action γᵐᵒᵖ (β i)] [∀ i, is_central_scalar γ (β i)] :

is_central_scalar γ (Π₀ i, β i) :=

{ op_smul_eq_smul := λ r m, ext $ λ i, by simp only [smul_apply, op_smul_eq_smul r (m i)] }

instance [monoid γ] [Π i, add_monoid (β i)] [Π i, distrib_mul_action γ (β i)] :

distrib_mul_action γ (Π₀ i, β i) :=

function.injective.distrib_mul_action coe_fn_add_monoid_hom fun_like.coe_injective coe_smul

instance [semiring γ] [Π i, add_comm_monoid (β i)] [Π i, module γ (β i)] :

module γ (Π₀ i, β i) :=

{ zero_smul := λ c, ext $ λ i, by simp only [smul_apply, zero_smul, zero_apply],

add_smul := λ c x y, ext $ λ i, by simp only [add_apply, smul_apply, add_smul],

..dfinsupp.distrib_mul_action }

end algebra

section filter_and_subtype_domain

def filter [Π i, has_zero (β i)] (p : ι → Prop) [decidable_pred p] (x : Π₀ i, β i) : Π₀ i, β i :=

⟨λ i, if p i then x i else 0, x.support'.map

(λ xs, ⟨xs, λ i, (xs.prop i).imp_right $ λ H : x i = 0, by rw [H, if_t_t]⟩)⟩

@[simp] lemma filter_apply [Π i, has_zero (β i)]

(p : ι → Prop) [decidable_pred p] (i : ι) (f : Π₀ i, β i) :

f.filter p i = if p i then f i else 0 :=

rfl

lemma filter_apply_pos [Π i, has_zero (β i)]

{p : ι → Prop} [decidable_pred p] (f : Π₀ i, β i) {i : ι} (h : p i) :

f.filter p i = f i :=

by simp only [filter_apply, if_pos h]

lemma filter_apply_neg [Π i, has_zero (β i)]

{p : ι → Prop} [decidable_pred p] (f : Π₀ i, β i) {i : ι} (h : ¬ p i) :

f.filter p i = 0 :=

by simp only [filter_apply, if_neg h]

lemma filter_pos_add_filter_neg [Π i, add_zero_class (β i)] (f : Π₀ i, β i)

(p : ι → Prop) [decidable_pred p] :

f.filter p + f.filter (λi, ¬ p i) = f :=

ext $ λ i, by simp only [add_apply, filter_apply]; split_ifs; simp only [add_zero, zero_add]

@[simp] lemma filter_zero [Π i, has_zero (β i)] (p : ι → Prop) [decidable_pred p] :

(0 : Π₀ i, β i).filter p = 0 :=

by { ext, simp }

@[simp] lemma filter_add [Π i, add_zero_class (β i)] (p : ι → Prop) [decidable_pred p]

(f g : Π₀ i, β i) :

(f + g).filter p = f.filter p + g.filter p :=

by { ext, simp [ite_add_zero] }

@[simp] lemma filter_smul [monoid γ] [Π i, add_monoid (β i)] [Π i, distrib_mul_action γ (β i)]

(p : ι → Prop) [decidable_pred p] (r : γ) (f : Π₀ i, β i) :

(r • f).filter p = r • f.filter p :=

by { ext, simp [smul_ite] }

variables (γ β)

def filter_add_monoid_hom [Π i, add_zero_class (β i)] (p : ι → Prop) [decidable_pred p] :

(Π₀ i, β i) →+ (Π₀ i, β i) :=

{ to_fun := filter p,

map_zero' := filter_zero p,

map_add' := filter_add p }

def filter_linear_map [semiring γ] [Π i, add_comm_monoid (β i)] [Π i, module γ (β i)]

(p : ι → Prop) [decidable_pred p] :

(Π₀ i, β i) →ₗ[γ] (Π₀ i, β i) :=

{ to_fun := filter p,

map_add' := filter_add p,

map_smul' := filter_smul p }

variables {γ β}

@[simp] lemma filter_neg [Π i, add_group (β i)] (p : ι → Prop) [decidable_pred p]

(f : Π₀ i, β i) :

(-f).filter p = -f.filter p :=

(filter_add_monoid_hom β p).map_neg f

@[simp] lemma filter_sub [Π i, add_group (β i)] (p : ι → Prop) [decidable_pred p]

(f g : Π₀ i, β i) :

(f - g).filter p = f.filter p - g.filter p :=

(filter_add_monoid_hom β p).map_sub f g

def subtype_domain [Π i, has_zero (β i)] (p : ι → Prop) [decidable_pred p] (x : Π₀ i, β i) :

Π₀ i : subtype p, β i :=

⟨λ i, x (i : ι), x.support'.map

(λ xs, ⟨(multiset.filter p xs).attach.map $ λ j, ⟨j, (multiset.mem_filter.1 j.2).2⟩,

λ i, (xs.prop i).imp_left $ λ H, multiset.mem_map.2

⟨⟨i, multiset.mem_filter.2 ⟨H, i.2⟩⟩, multiset.mem_attach _ _, subtype.eta _ _⟩⟩)⟩

@[simp] lemma subtype_domain_zero [Π i, has_zero (β i)] {p : ι → Prop} [decidable_pred p] :

subtype_domain p (0 : Π₀ i, β i) = 0 :=

rfl

@[simp] lemma subtype_domain_apply [Π i, has_zero (β i)] {p : ι → Prop} [decidable_pred p]

{i : subtype p} {v : Π₀ i, β i} :

(subtype_domain p v) i = v i :=

rfl

@[simp] lemma subtype_domain_add [Π i, add_zero_class (β i)] {p : ι → Prop} [decidable_pred p]

(v v' : Π₀ i, β i) :

(v + v').subtype_domain p = v.subtype_domain p + v'.subtype_domain p :=

coe_fn_injective rfl

@[simp] lemma subtype_domain_smul [monoid γ] [Π i, add_monoid (β i)]

[Π i, distrib_mul_action γ (β i)] {p : ι → Prop} [decidable_pred p] (r : γ) (f : Π₀ i, β i) :

(r • f).subtype_domain p = r • f.subtype_domain p :=

coe_fn_injective rfl

variables (γ β)

@[simps] def subtype_domain_add_monoid_hom [Π i, add_zero_class (β i)]

(p : ι → Prop) [decidable_pred p] : (Π₀ i : ι, β i) →+ Π₀ i : subtype p, β i :=

{ to_fun := subtype_domain p,

map_zero' := subtype_domain_zero,

map_add' := subtype_domain_add }

def subtype_domain_linear_map [semiring γ] [Π i, add_comm_monoid (β i)] [Π i, module γ (β i)]

(p : ι → Prop) [decidable_pred p] :

(Π₀ i, β i) →ₗ[γ] (Π₀ i : subtype p, β i) :=

{ to_fun := subtype_domain p,

map_add' := subtype_domain_add,

map_smul' := subtype_domain_smul }

variables {γ β}

lemma subtype_domain_neg [Π i, add_group (β i)] {p : ι → Prop} [decidable_pred p] {v : Π₀ i, β i} :

(- v).subtype_domain p = - v.subtype_domain p :=

coe_fn_injective rfl

@[simp] lemma subtype_domain_sub [Π i, add_group (β i)] {p : ι → Prop} [decidable_pred p]

{v v' : Π₀ i, β i} :

(v - v').subtype_domain p = v.subtype_domain p - v'.subtype_domain p :=

coe_fn_injective rfl

end filter_and_subtype_domain

variable [dec : decidable_eq ι]

include dec

section basic

variable [Π i, has_zero (β i)]

omit dec

lemma finite_support (f : Π₀ i, β i) : set.finite {i | f i ≠ 0} :=

classical,

exact trunc.induction_on f.support' (λ xs, (multiset.to_finset ↑xs).finite_to_set.subset (λ i H,

multiset.mem_to_finset.2 ((xs.prop i).resolve_right H)))

include dec

def mk (s : finset ι) (x : Π i : (↑s : set ι), β (i : ι)) : Π₀ i, β i :=

⟨λ i, if H : i ∈ s then x ⟨i, H⟩ else 0, trunc.mk ⟨s.1,

λ i, if H : i ∈ s then or.inl H else or.inr $ dif_neg H⟩⟩

variables {s : finset ι} {x : Π i : (↑s : set ι), β i} {i : ι}

@[simp] lemma mk_apply : (mk s x : Π i, β i) i = if H : i ∈ s then x ⟨i, H⟩ else 0 := rfl

lemma mk_of_mem (hi : i ∈ s) : (mk s x : Π i, β i) i = x ⟨i, hi⟩ := dif_pos hi

lemma mk_of_not_mem (hi : i ∉ s) : (mk s x : Π i, β i) i = 0 := dif_neg hi

theorem mk_injective (s : finset ι) : function.injective (@mk ι β _ _ s) :=

intros x y H,

ext i,

have h1 : (mk s x : Π i, β i) i = (mk s y : Π i, β i) i, {rw H},

cases i with i hi,

change i ∈ s at hi,

dsimp only [mk_apply, subtype.coe_mk] at h1,

simpa only [dif_pos hi] using h1

omit dec

instance unique [∀ i, subsingleton (β i)] : unique (Π₀ i, β i) := fun_like.coe_injective.unique

instance unique_of_is_empty [is_empty ι] : unique (Π₀ i, β i) := fun_like.coe_injective.unique

@[simps apply] def equiv_fun_on_fintype [fintype ι] : (Π₀ i, β i) ≃ (Π i, β i) :=

{ to_fun := coe_fn,

inv_fun := λ f, ⟨f, trunc.mk ⟨finset.univ.1, λ i, or.inl $ finset.mem_univ_val _⟩⟩,

left_inv := λ x, coe_fn_injective rfl,

right_inv := λ x, rfl }

@[simp] lemma equiv_fun_on_fintype_symm_coe [fintype ι] (f : Π₀ i, β i) :

equiv_fun_on_fintype.symm f = f :=

equiv.symm_apply_apply _ _

include dec

def single (i : ι) (b : β i) : Π₀ i, β i :=

⟨pi.single i b,

trunc.mk ⟨{i}, λ j, (decidable.eq_or_ne j i).imp (by simp) (λ h, pi.single_eq_of_ne h _)⟩⟩

lemma single_eq_pi_single {i b} : ⇑(single i b : Π₀ i, β i) = pi.single i b :=

rfl

@[simp] lemma single_apply {i i' b} :

(single i b : Π₀ i, β i) i' = (if h : i = i' then eq.rec_on h b else 0) :=

rw [single_eq_pi_single, pi.single, function.update],

simp [@eq_comm _ i i'],

@[simp] lemma single_zero (i) : (single i 0 : Π₀ i, β i) = 0 :=

fun_like.coe_injective $ pi.single_zero _

@[simp] lemma single_eq_same {i b} : (single i b : Π₀ i, β i) i = b :=

by simp only [single_apply, dif_pos rfl]

lemma single_eq_of_ne {i i' b} (h : i ≠ i') : (single i b : Π₀ i, β i) i' = 0 :=

by simp only [single_apply, dif_neg h]

lemma single_injective {i} : function.injective (single i : β i → Π₀ i, β i) :=

λ x y H, pi.single_injective β i $ coe_fn_injective.eq_iff.mpr H

lemma single_eq_single_iff (i j : ι) (xi : β i) (xj : β j) :

dfinsupp.single i xi = dfinsupp.single j xj ↔ i = j ∧ xi == xj ∨ xi = 0 ∧ xj = 0 :=

split,

{ intro h,

by_cases hij : i = j,

{ subst hij,

exact or.inl ⟨rfl, heq_of_eq (dfinsupp.single_injective h)⟩, },

{ have h_coe : ⇑(dfinsupp.single i xi) = dfinsupp.single j xj := congr_arg coe_fn h,

have hci := congr_fun h_coe i,

have hcj := congr_fun h_coe j,

rw dfinsupp.single_eq_same at hci hcj,

rw dfinsupp.single_eq_of_ne (ne.symm hij) at hci,

rw dfinsupp.single_eq_of_ne (hij) at hcj,

exact or.inr ⟨hci, hcj.symm⟩, }, },

{ rintros (⟨rfl, hxi⟩ | ⟨hi, hj⟩),

{ rw eq_of_heq hxi, },

{ rw [hi, hj, dfinsupp.single_zero, dfinsupp.single_zero], }, },

lemma single_left_injective {b : Π (i : ι), β i} (h : ∀ i, b i ≠ 0) :

function.injective (λ i, single i (b i) : ι → Π₀ i, β i) :=

λ a a' H, (((single_eq_single_iff _ _ _ _).mp H).resolve_right $ λ hb, h _ hb.1).left

@[simp] lemma single_eq_zero {i : ι} {xi : β i} : single i xi = 0 ↔ xi = 0 :=

rw [←single_zero i, single_eq_single_iff],

simp,

lemma filter_single (p : ι → Prop) [decidable_pred p] (i : ι) (x : β i) :

(single i x).filter p = if p i then single i x else 0 :=

ext j,

have := apply_ite (λ x : Π₀ i, β i, x j) (p i) (single i x) 0,

dsimp at this,

rw [filter_apply, this],

obtain rfl | hij := decidable.eq_or_ne i j,

{ refl, },

{ rw [single_eq_of_ne hij, if_t_t, if_t_t], },

@[simp] lemma filter_single_pos {p : ι → Prop} [decidable_pred p] (i : ι) (x : β i) (h : p i) :

(single i x).filter p = single i x :=

by rw [filter_single, if_pos h]

@[simp] lemma filter_single_neg {p : ι → Prop} [decidable_pred p] (i : ι) (x : β i) (h : ¬p i) :

(single i x).filter p = 0 :=

by rw [filter_single, if_neg h]

lemma single_eq_of_sigma_eq

{i j} {xi : β i} {xj : β j} (h : (⟨i, xi⟩ : sigma β) = ⟨j, xj⟩) :

dfinsupp.single i xi = dfinsupp.single j xj :=

by { cases h, refl }

@[simp] lemma equiv_fun_on_fintype_single [fintype ι] (i : ι) (m : β i) :

(@dfinsupp.equiv_fun_on_fintype ι β _ _) (dfinsupp.single i m) = pi.single i m :=

by { ext, simp [dfinsupp.single_eq_pi_single], }

@[simp] lemma equiv_fun_on_fintype_symm_single [fintype ι] (i : ι) (m : β i) :

(@dfinsupp.equiv_fun_on_fintype ι β _ _).symm (pi.single i m) = dfinsupp.single i m :=

by { ext i', simp only [← single_eq_pi_single, equiv_fun_on_fintype_symm_coe] }

def erase (i : ι) (x : Π₀ i, β i) : Π₀ i, β i :=

⟨λ j, if j = i then 0 else x.1 j, x.support'.map $ λ xs,

⟨xs, λ j, (xs.prop j).imp_right $ λ H, by simp only [H, if_t_t]⟩⟩

@[simp] lemma erase_apply {i j : ι} {f : Π₀ i, β i} :

(f.erase i) j = if j = i then 0 else f j :=

rfl

@[simp] lemma erase_same {i : ι} {f : Π₀ i, β i} : (f.erase i) i = 0 :=

by simp

lemma erase_ne {i i' : ι} {f : Π₀ i, β i} (h : i' ≠ i) : (f.erase i) i' = f i' :=

by simp [h]

lemma piecewise_single_erase (x : Π₀ i, β i) (i : ι) :

(single i (x i)).piecewise (x.erase i) {i} = x :=

ext j, rw piecewise_apply, split_ifs,

{ rw [(id h : j = i), single_eq_same] },

{ exact erase_ne h },

lemma erase_eq_sub_single {β : ι → Type*} [Π i, add_group (β i)] (f : Π₀ i, β i) (i : ι) :

f.erase i = f - single i (f i) :=

ext j,

rcases eq_or_ne i j with rfl|h,

{ simp },

{ simp [erase_ne h.symm, single_eq_of_ne h] }

@[simp] lemma erase_zero (i : ι) : erase i (0 : Π₀ i, β i) = 0 :=

ext $ λ _, if_t_t _ _

@[simp] lemma filter_ne_eq_erase (f : Π₀ i, β i) (i : ι) : f.filter (≠ i) = f.erase i :=

ext1 j,

simp only [dfinsupp.filter_apply, dfinsupp.erase_apply, ite_not],

@[simp] lemma filter_ne_eq_erase' (f : Π₀ i, β i) (i : ι) : f.filter ((≠) i) = f.erase i :=

rw ←filter_ne_eq_erase f i,

congr' with j,

exact ne_comm,

lemma erase_single (j : ι) (i : ι) (x : β i) :

(single i x).erase j = if i = j then 0 else single i x :=

by rw [←filter_ne_eq_erase, filter_single, ite_not]

@[simp] lemma erase_single_same (i : ι) (x : β i) : (single i x).erase i = 0 :=

by rw [erase_single, if_pos rfl]

@[simp] lemma erase_single_ne {i j : ι} (x : β i) (h : i ≠ j) : (single i x).erase j = single i x :=

by rw [erase_single, if_neg h]

section update

variables (f : Π₀ i, β i) (i) (b : β i)

def update : Π₀ i, β i :=

⟨function.update f i b, f.support'.map $ λ s,

⟨i ::ₘ s, λ j, begin

rcases eq_or_ne i j with rfl|hi,

{ simp, },

{ obtain hj | (hj : f j = 0) := s.prop j,

{ exact or.inl (multiset.mem_cons_of_mem hj), },

{ exact or.inr ((function.update_noteq hi.symm b _).trans hj) } }

end⟩⟩

variables (j : ι)

@[simp] lemma coe_update : (f.update i b : Π (i : ι), β i) = function.update f i b := rfl

@[simp] lemma update_self : f.update i (f i) = f :=

by { ext, simp }

@[simp] lemma update_eq_erase : f.update i 0 = f.erase i :=

ext j,

rcases eq_or_ne i j with rfl|hi,

{ simp },

{ simp [hi.symm] }

lemma update_eq_single_add_erase {β : ι → Type*} [Π i, add_zero_class (β i)] (f : Π₀ i, β i) (i : ι)

(b : β i) :

f.update i b = single i b + f.erase i :=

ext j,

rcases eq_or_ne i j with rfl|h,

{ simp },

{ simp [function.update_noteq h.symm, h, erase_ne, h.symm] }

lemma update_eq_erase_add_single {β : ι → Type*} [Π i, add_zero_class (β i)] (f : Π₀ i, β i) (i : ι)

(b : β i) :

f.update i b = f.erase i + single i b :=

ext j,

rcases eq_or_ne i j with rfl|h,

{ simp },

{ simp [function.update_noteq h.symm, h, erase_ne, h.symm] }

lemma update_eq_sub_add_single {β : ι → Type*} [Π i, add_group (β i)] (f : Π₀ i, β i) (i : ι)

(b : β i) :

f.update i b = f - single i (f i) + single i b :=

by rw [update_eq_erase_add_single f i b, erase_eq_sub_single f i]

end update

end basic

section add_monoid

variable [Π i, add_zero_class (β i)]

@[simp] lemma single_add (i : ι) (b₁ b₂ : β i) : single i (b₁ + b₂) = single i b₁ + single i b₂ :=

ext $ assume i',

by_cases h : i = i',

{ subst h, simp only [add_apply, single_eq_same] },

{ simp only [add_apply, single_eq_of_ne h, zero_add] }

@[simp] lemma erase_add (i : ι) (f₁ f₂ : Π₀ i, β i) : erase i (f₁ + f₂) = erase i f₁ + erase i f₂ :=

ext $ λ _, by simp [ite_zero_add]

variables (β)

@[simps] def single_add_hom (i : ι) : β i →+ Π₀ i, β i :=

{ to_fun := single i, map_zero' := single_zero i, map_add' := single_add i }

@[simps] def erase_add_hom (i : ι) : (Π₀ i, β i) →+ Π₀ i, β i :=

{ to_fun := erase i, map_zero' := erase_zero i, map_add' := erase_add i }

variables {β}

@[simp] lemma single_neg {β : ι → Type v} [Π i, add_group (β i)] (i : ι) (x : β i) :

single i (-x) = -single i x :=

(single_add_hom β i).map_neg x

@[simp] lemma single_sub {β : ι → Type v} [Π i, add_group (β i)] (i : ι) (x y : β i) :

single i (x - y) = single i x - single i y :=

(single_add_hom β i).map_sub x y

@[simp] lemma erase_neg {β : ι → Type v} [Π i, add_group (β i)] (i : ι) (f : Π₀ i, β i) :

(-f).erase i = -f.erase i :=

(erase_add_hom β i).map_neg f

@[simp] lemma erase_sub {β : ι → Type v} [Π i, add_group (β i)] (i : ι) (f g : Π₀ i, β i) :

(f - g).erase i = f.erase i - g.erase i :=

(erase_add_hom β i).map_sub f g

lemma single_add_erase (i : ι) (f : Π₀ i, β i) : single i (f i) + f.erase i = f :=

ext $ λ i',

if h : i = i'

then by subst h; simp only [add_apply, single_apply, erase_apply, dif_pos rfl, if_pos, add_zero]

else by simp only [add_apply, single_apply, erase_apply, dif_neg h, if_neg (ne.symm h), zero_add]

lemma erase_add_single (i : ι) (f : Π₀ i, β i) : f.erase i + single i (f i) = f :=

ext $ λ i',

if h : i = i'

then by subst h; simp only [add_apply, single_apply, erase_apply, dif_pos rfl, if_pos, zero_add]

else by simp only [add_apply, single_apply, erase_apply, dif_neg h, if_neg (ne.symm h), add_zero]

protected theorem induction {p : (Π₀ i, β i) → Prop} (f : Π₀ i, β i)

(h0 : p 0) (ha : ∀i b (f : Π₀ i, β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)) :

p f :=

cases f with f s,

induction s using trunc.induction_on,

cases s with s H,

induction s using multiset.induction_on with i s ih generalizing f,

{ have : f = 0 := funext (λ i, (H i).resolve_left id),

subst this,

exact h0 },

have H2 : p (erase i ⟨f, trunc.mk ⟨i ::ₘ s, H⟩⟩),

{ dsimp only [erase, trunc.map, trunc.bind, trunc.lift_on, trunc.lift_mk, function.comp,

subtype.coe_mk],

have H2 : ∀ j, j ∈ s ∨ ite (j = i) 0 (f j) = 0,

{ intro j, cases H j with H2 H2,

{ cases multiset.mem_cons.1 H2 with H3 H3,

{ right, exact if_pos H3 },

{ left, exact H3 } },

right, split_ifs; [refl, exact H2] },

have H3 : (⟨λ (j : ι), ite (j = i) 0 (f j), trunc.mk ⟨i ::ₘ s, _⟩⟩ : Π₀ i, β i)

= ⟨λ (j : ι), ite (j = i) 0 (f j), trunc.mk ⟨s, H2⟩⟩ := ext (λ _, rfl),

rw H3, apply ih },

have H3 : single i _ + _ = (⟨f, trunc.mk ⟨i ::ₘ s, H⟩⟩ : Π₀ i, β i) :=

single_add_erase _ _,

rw ← H3,

change p (single i (f i) + _),

cases classical.em (f i = 0) with h h,

{ rw [h, single_zero, zero_add], exact H2 },

refine ha _ _ _ _ h H2,

rw erase_same

lemma induction₂ {p : (Π₀ i, β i) → Prop} (f : Π₀ i, β i)

(h0 : p 0) (ha : ∀i b (f : Π₀ i, β i), f i = 0 → b ≠ 0 → p f → p (f + single i b)) :

p f :=

dfinsupp.induction f h0 $ λ i b f h1 h2 h3,

have h4 : f + single i b = single i b + f,

{ ext j, by_cases H : i = j,

{ subst H, simp [h1] },

{ simp [H] } },

eq.rec_on h4 $ ha i b f h1 h2 h3

@[simp] lemma add_closure_Union_range_single :

add_submonoid.closure (⋃ i : ι, set.range (single i : β i → (Π₀ i, β i))) = ⊤ :=

top_unique $ λ x hx, (begin

apply dfinsupp.induction x,

exact add_submonoid.zero_mem _,

exact λ a b f ha hb hf, add_submonoid.add_mem _

(add_submonoid.subset_closure $ set.mem_Union.2 ⟨a, set.mem_range_self _⟩) hf

end)

lemma add_hom_ext {γ : Type w} [add_zero_class γ] ⦃f g : (Π₀ i, β i) →+ γ⦄

(H : ∀ (i : ι) (y : β i), f (single i y) = g (single i y)) :

f = g :=

refine add_monoid_hom.eq_of_eq_on_mdense add_closure_Union_range_single (λ f hf, _),

simp only [set.mem_Union, set.mem_range] at hf,

rcases hf with ⟨x, y, rfl⟩,

apply H

@[ext] lemma add_hom_ext' {γ : Type w} [add_zero_class γ] ⦃f g : (Π₀ i, β i) →+ γ⦄

(H : ∀ x, f.comp (single_add_hom β x) = g.comp (single_add_hom β x)) :

f = g :=

add_hom_ext $ λ x, add_monoid_hom.congr_fun (H x)

end add_monoid

@[simp] lemma mk_add [Π i, add_zero_class (β i)] {s : finset ι} {x y : Π i : (↑s : set ι), β i} :

mk s (x + y) = mk s x + mk s y :=

ext $ λ i, by simp only [add_apply, mk_apply]; split_ifs; [refl, rw zero_add]

@[simp] lemma mk_zero [Π i, has_zero (β i)] {s : finset ι} :

mk s (0 : Π i : (↑s : set ι), β i.1) = 0 :=

ext $ λ i, by simp only [mk_apply]; split_ifs; refl

@[simp] lemma mk_neg [Π i, add_group (β i)] {s : finset ι} {x : Π i : (↑s : set ι), β i.1} :

mk s (-x) = -mk s x :=

ext $ λ i, by simp only [neg_apply, mk_apply]; split_ifs; [refl, rw neg_zero]

@[simp] lemma mk_sub [Π i, add_group (β i)] {s : finset ι} {x y : Π i : (↑s : set ι), β i.1} :

mk s (x - y) = mk s x - mk s y :=

ext $ λ i, by simp only [sub_apply, mk_apply]; split_ifs; [refl, rw sub_zero]

def mk_add_group_hom [Π i, add_group (β i)] (s : finset ι) :

(Π (i : (s : set ι)), β ↑i) →+ (Π₀ (i : ι), β i) :=

{ to_fun := mk s,

map_zero' := mk_zero,

map_add' := λ _ _, mk_add }

variables [monoid γ] [Π i, add_monoid (β i)] [Π i, distrib_mul_action γ (β i)]

@[simp] lemma mk_smul {s : finset ι} (c : γ) (x : Π i : (↑s : set ι), β (i : ι)) :

mk s (c • x) = c • mk s x :=

ext $ λ i, by simp only [smul_apply, mk_apply]; split_ifs; [refl, rw smul_zero]

@[simp] lemma single_smul {i : ι} (c : γ) (x : β i) :

single i (c • x) = c • single i x :=

ext $ λ i, by simp only [smul_apply, single_apply]; split_ifs; [cases h, rw smul_zero]; refl

section support_basic

variables [Π i, has_zero (β i)] [Π i (x : β i), decidable (x ≠ 0)]

def support (f : Π₀ i, β i) : finset ι :=

f.support'.lift (λ xs, (multiset.to_finset ↑xs).filter $ λ i, f i ≠ 0) $

rintros ⟨sx, hx⟩ ⟨sy, hy⟩,

dsimp only [subtype.coe_mk, to_fun_eq_coe] at *,

ext i, split,

{ intro H,

rcases finset.mem_filter.1 H with ⟨h1, h2⟩,

exact finset.mem_filter.2 ⟨multiset.mem_to_finset.2 $ (hy i).resolve_right h2, h2⟩ },

{ intro H,

rcases finset.mem_filter.1 H with ⟨h1, h2⟩,

exact finset.mem_filter.2 ⟨multiset.mem_to_finset.2 $ (hx i).resolve_right h2, h2⟩ },

@[simp] theorem support_mk_subset {s : finset ι} {x : Π i : (↑s : set ι), β i.1} :

(mk s x).support ⊆ s :=

λ i H, multiset.mem_to_finset.1 (finset.mem_filter.1 H).1

@[simp] theorem support_mk'_subset {f : Π i, β i} {s : multiset ι} {h} :

(mk' f $ trunc.mk ⟨s, h⟩).support ⊆ s.to_finset :=

λ i H, multiset.mem_to_finset.1 $ by simpa using (finset.mem_filter.1 H).1

@[simp] theorem mem_support_to_fun (f : Π₀ i, β i) (i) : i ∈ f.support ↔ f i ≠ 0 :=

cases f with f s,

induction s using trunc.induction_on,

dsimp only [support, trunc.lift_mk],

rw [finset.mem_filter, multiset.mem_to_finset, coe_mk'],

exact and_iff_right_of_imp (s.prop i).resolve_right

theorem eq_mk_support (f : Π₀ i, β i) : f = mk f.support (λ i, f i) :=

change f = mk f.support (λ i, f i.1),

ext i,

by_cases h : f i ≠ 0; [skip, rw [not_not] at h];

simp [h]

@[simp] lemma support_zero : (0 : Π₀ i, β i).support = ∅ := rfl

lemma mem_support_iff {f : Π₀ i, β i} {i : ι} : i ∈ f.support ↔ f i ≠ 0 := f.mem_support_to_fun _

lemma not_mem_support_iff {f : Π₀ i, β i} {i : ι} : i ∉ f.support ↔ f i = 0 :=

not_iff_comm.1 mem_support_iff.symm

@[simp] lemma support_eq_empty {f : Π₀ i, β i} : f.support = ∅ ↔ f = 0 :=

⟨λ H, ext $ by simpa [finset.ext_iff] using H, by simp {contextual:=tt}⟩

instance decidable_zero : decidable_pred (eq (0 : Π₀ i, β i)) :=

λ f, decidable_of_iff _ $ support_eq_empty.trans eq_comm

lemma support_subset_iff {s : set ι} {f : Π₀ i, β i} :

↑f.support ⊆ s ↔ (∀i∉s, f i = 0) :=

by simp [set.subset_def];

exact forall_congr (assume i, not_imp_comm)

lemma support_single_ne_zero {i : ι} {b : β i} (hb : b ≠ 0) : (single i b).support = {i} :=

ext j, by_cases h : i = j,

{ subst h, simp [hb] },

simp [ne.symm h, h]

lemma support_single_subset {i : ι} {b : β i} : (single i b).support ⊆ {i} :=

support_mk'_subset

section map_range_and_zip_with

variables [Π i, has_zero (β₁ i)] [Π i, has_zero (β₂ i)]

lemma map_range_def [Π i (x : β₁ i), decidable (x ≠ 0)]

{f : Π i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0} {g : Π₀ i, β₁ i} :

map_range f hf g = mk g.support (λ i, f i.1 (g i.1)) :=

ext i,

by_cases h : g i ≠ 0; simp at h; simp [h, hf]

@[simp] lemma map_range_single {f : Π i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0} {i : ι} {b : β₁ i} :

map_range f hf (single i b) = single i (f i b) :=

dfinsupp.ext $ λ i', by by_cases i = i'; [{subst i', simp}, simp [h, hf]]

variables [Π i (x : β₁ i), decidable (x ≠ 0)] [Π i (x : β₂ i), decidable (x ≠ 0)]

lemma support_map_range {f : Π i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0} {g : Π₀ i, β₁ i} :

(map_range f hf g).support ⊆ g.support :=

by simp [map_range_def]

lemma zip_with_def {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂}

[dec : decidable_eq ι] [Π (i : ι), has_zero (β i)] [Π (i : ι), has_zero (β₁ i)]

[Π (i : ι), has_zero (β₂ i)] [Π (i : ι) (x : β₁ i), decidable (x ≠ 0)]

[Π (i : ι) (x : β₂ i), decidable (x ≠ 0)]

{f : Π i, β₁ i → β₂ i → β i} {hf : ∀ i, f i 0 0 = 0}

{g₁ : Π₀ i, β₁ i} {g₂ : Π₀ i, β₂ i} :

zip_with f hf g₁ g₂ = mk (g₁.support ∪ g₂.support) (λ i, f i.1 (g₁ i.1) (g₂ i.1)) :=

ext i,

by_cases h1 : g₁ i ≠ 0; by_cases h2 : g₂ i ≠ 0;

simp only [not_not, ne.def] at h1 h2; simp [h1, h2, hf]

lemma support_zip_with {f : Π i, β₁ i → β₂ i → β i} {hf : ∀ i, f i 0 0 = 0}

{g₁ : Π₀ i, β₁ i} {g₂ : Π₀ i, β₂ i} :

(zip_with f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support :=

by simp [zip_with_def]

end map_range_and_zip_with

lemma erase_def (i : ι) (f : Π₀ i, β i) :

f.erase i = mk (f.support.erase i) (λ j, f j.1) :=

by { ext j, by_cases h1 : j = i; by_cases h2 : f j ≠ 0; simp at h2; simp [h1, h2] }