my_defs.lean

import algebra.hom.group_action
import algebra.indicator_function

open set function
open_locale big_operators

variables {α β γ ι M M' N P G H R S : Type*}

structure finsupp (α : Type*) (M : Type*) [has_zero M] :=
(to_fun : α → M)
(finite_support' : to_fun.support.finite)

infixr ` →₀ `:25 := finsupp

namespace finsupp

/-! ### Basic declarations about `finsupp` -/

section basic
variable [has_zero M]

def support (f : α →₀ M) : set α := f.to_fun.support

instance fun_like : fun_like (α →₀ M) α (λ _, M) :=
⟨to_fun, by { rintro ⟨f, hf⟩ ⟨g, hg⟩ (rfl : f = g), refl }⟩

instance : has_coe_to_fun (α →₀ M) (λ _, α → M) := fun_like.has_coe_to_fun

@[simp] lemma coe_mk (f : α → M) (hf : f.support.finite) : ⇑(⟨f, hf⟩ : α →₀ M) = f := rfl

instance : has_zero (α →₀ M) := ⟨⟨0, by { convert set.finite_empty, exact support_zero' }⟩⟩

@[simp] lemma coe_zero : ⇑(0 : α →₀ M) = 0 := rfl
lemma zero_apply {a : α} : (0 : α →₀ M) a = 0 := rfl
@[simp] lemma support_zero : (0 : α →₀ M).support = ∅ := support_zero'

instance : inhabited (α →₀ M) := ⟨0⟩

@[simp] lemma mem_support_iff {f : α →₀ M} {a : α} : a ∈ f.support ↔ f a ≠ 0 := iff.rfl

@[simp, norm_cast] lemma fun_support_eq (f : α →₀ M) : function.support f = f.support :=
set.ext $ λ x, mem_support_iff.symm

lemma not_mem_support_iff {f : α →₀ M} {a} : a ∉ f.support ↔ f a = 0 :=
not_iff_comm.1 mem_support_iff.symm

@[simp, norm_cast] lemma coe_eq_zero {f : α →₀ M} : (f : α → M) = 0 ↔ f = 0 :=
by rw [← coe_zero, fun_like.coe_fn_eq]

lemma ext_iff' {f g : α →₀ M} : f = g ↔ f.support = g.support ∧ ∀ x ∈ f.support, f x = g x :=
⟨λ h, h ▸ ⟨rfl, λ _ _, rfl⟩, λ ⟨h₁, h₂⟩, fun_like.ext f g $ λ a,
by {  by_cases h : a ∈ f.support,
      { exact h₂ a h },
      { have hf : f a = 0, from not_mem_support_iff.1 h,
        have hg : g a = 0, by rwa [h₁, not_mem_support_iff] at h,
        by rw [hf, hg] } } ⟩

@[simp] lemma support_eq_empty {f : α →₀ M} : f.support = ∅ ↔ f = 0 :=
by exact_mod_cast @function.support_eq_empty_iff _ _ _ f

lemma support_nonempty_iff {f : α →₀ M} : f.support.nonempty ↔ f ≠ 0 :=
by exact_mod_cast @function.support_nonempty_iff _ _ _ f

lemma nonzero_iff_exists {f : α →₀ M} : f ≠ 0 ↔ ∃ a : α, f a ≠ 0 :=
by simp_rw [← support_nonempty_iff, set.nonempty, mem_support_iff]

/-
lemma card_support_eq_zero {f : α →₀ M} : card f.support = 0 ↔ f = 0 :=
by simp

instance [decidable_eq α] [decidable_eq M] : decidable_eq (α →₀ M) :=
assume f g, decidable_of_iff (f.support = g.support ∧ (∀a∈f.support, f a = g a)) ext_iff'.symm
-/

lemma finite_support (f : α →₀ M) : set.finite (function.support f) := f.finite_support'

lemma support_subset_iff {s : set α} {f : α →₀ M} :
  f.support ⊆ s ↔ (∀a∉s, f a = 0) :=
by simp only [set.subset_def, mem_support_iff];
   exact forall_congr (assume a, not_imp_comm)

@[simps] def equiv_fun_on_fintype [fintype α] : (α →₀ M) ≃ (α → M) :=
{ to_fun := coe_fn,
  inv_fun := λ f, ⟨f, to_finite _⟩,
  left_inv := λ f, fun_like.ext' (coe_mk f _),
  right_inv := λ f, coe_mk f _ }

@[simp] lemma equiv_fun_on_fintype_symm_coe {α} [fintype α] (f : α →₀ M) :
  equiv_fun_on_fintype.symm f = f :=
by { rw fun_like.ext_iff, simp [equiv_fun_on_fintype] }

@[simps] def _root_.equiv.finsupp_unique {ι : Type*} [unique ι] : (ι →₀ M) ≃ M :=
finsupp.equiv_fun_on_fintype.trans (equiv.fun_unique ι M)

end basic

end finsupp