feat(data/support): add function.mul_support (#6791)

This will help us add `finprod` in #6355

src/algebra/group/to_additive.lean

@@ -91,6 +91,7 @@ meta def tr : bool → list string → list string
 | is_comm ("one" :: "lt" :: s) := add_comm_prefix is_comm "pos"    :: tr ff s
 | is_comm ("le" :: "one" :: s) := add_comm_prefix is_comm "nonpos" :: tr ff s
 | is_comm ("lt" :: "one" :: s) := add_comm_prefix is_comm "neg"    :: tr ff s
+| is_comm ("mul" :: "support" :: s) := add_comm_prefix is_comm "support" :: tr ff s
 | is_comm ("mul" :: s)         := add_comm_prefix is_comm "add"    :: tr ff s
 | is_comm ("inv" :: s)         := add_comm_prefix is_comm "neg"    :: tr ff s
 | is_comm ("div" :: s)         := add_comm_prefix is_comm "sub"    :: tr ff s

src/data/support.lean

@@ -13,133 +13,183 @@ import algebra.module.pi
 # Support of a function
 
 In this file we define `function.support f = {x | f x ≠ 0}` and prove its basic properties.
+We also define `function.mul_support f = {x | f x ≠ 1}`.
 -/
 
-universes u v w x y
-
 open set
 open_locale big_operators
 namespace function
 
-variables {α : Type u} {β : Type v} {ι : Sort w} {A : Type x} {B : Type y}
+variables {α β A B M N P R S G M₀ G₀ : Type*} {ι : Sort*}
+
+section has_one
+
+variables [has_one M] [has_one N] [has_one P]
 
-/-- `support` of a function is the set of points `x` such that `f x ≠ 0`. -/
+/-- `support` of a function is the set of points `x` such that `f x ≠ 0` -/
 def support [has_zero A] (f : α → A) : set α := {x | f x ≠ 0}
 
-lemma nmem_support [has_zero A] {f : α → A} {x : α} :
-  x ∉ support f ↔ f x = 0 :=
+/-- `mul_support` of a function is the set of points `x` such that `f x ≠ 1`. -/
+@[to_additive] def mul_support (f : α → M) : set α := {x | f x ≠ 1}
+
+@[to_additive] lemma nmem_mul_support {f : α → M} {x : α} :
+  x ∉ mul_support f ↔ f x = 1 :=
 not_not
 
-lemma compl_support [has_zero A] {f : α → A} : (support f)ᶜ = {x | f x = 0} :=
-ext $ λ x, nmem_support
+@[to_additive] lemma compl_mul_support {f : α → M} :
+  (mul_support f)ᶜ = {x | f x = 1} :=
+ext $ λ x, nmem_mul_support
 
-@[simp]
-lemma mem_support [has_zero A] {f : α → A} {x : α} :
-  x ∈ support f ↔ f x ≠ 0 :=
+@[simp, to_additive] lemma mem_mul_support {f : α → M} {x : α} :
+  x ∈ mul_support f ↔ f x ≠ 1 :=
 iff.rfl
 
-lemma support_subset_iff [has_zero A] {f : α → A} {s : set α} :
-  support f ⊆ s ↔ ∀ x, f x ≠ 0 → x ∈ s :=
+@[simp, to_additive] lemma mul_support_subset_iff {f : α → M} {s : set α} :
+  mul_support f ⊆ s ↔ ∀ x, f x ≠ 1 → x ∈ s :=
 iff.rfl
 
-lemma support_subset_iff' [has_zero A] {f : α → A} {s : set α} :
-  support f ⊆ s ↔ ∀ x ∉ s, f x = 0 :=
-forall_congr $ λ x, by classical; exact not_imp_comm
+@[to_additive] lemma mul_support_subset_iff' {f : α → M} {s : set α} :
+  mul_support f ⊆ s ↔ ∀ x ∉ s, f x = 1 :=
+forall_congr $ λ x, not_imp_comm
 
-@[simp] lemma support_eq_empty_iff [has_zero A] {f : α → A} :
-  support f = ∅ ↔ f = 0 :=
-by { simp_rw [← subset_empty_iff, support_subset_iff', funext_iff], simp }
+@[simp, to_additive] lemma mul_support_eq_empty_iff {f : α → M} :
+  mul_support f = ∅ ↔ f = 1 :=
+by { simp_rw [← subset_empty_iff, mul_support_subset_iff', funext_iff], simp }
 
-@[simp] lemma support_zero' [has_zero A] : support (0 : α → A) = ∅ :=
-support_eq_empty_iff.2 rfl
+@[simp, to_additive] lemma mul_support_one' : mul_support (1 : α → M) = ∅ :=
+mul_support_eq_empty_iff.2 rfl
 
-@[simp] lemma support_zero [has_zero A] : support (λ x : α, (0 : A)) = ∅ :=
-support_zero'
+@[simp, to_additive] lemma mul_support_one : mul_support (λ x : α, (1 : M)) = ∅ :=
+mul_support_one'
 
-lemma support_binop_subset [has_zero A] (op : A → A → A) (op0 : op 0 0 = 0) (f g : α → A) :
-  support (λ x, op (f x) (g x)) ⊆ support f ∪ support g :=
+@[to_additive] lemma mul_support_binop_subset (op : M → N → P) (op1 : op 1 1 = 1)
+  (f : α → M) (g : α → N) :
+  mul_support (λ x, op (f x) (g x)) ⊆ mul_support f ∪ mul_support g :=
 λ x hx, classical.by_cases
-  (λ hf : f x = 0, or.inr $ λ hg, hx $ by simp only [hf, hg, op0])
+  (λ hf : f x = 1, or.inr $ λ hg, hx $ by simp only [hf, hg, op1])
   or.inl
 
-lemma support_add [add_monoid A] (f g : α → A) :
-  support (λ x, f x + g x) ⊆ support f ∪ support g :=
-support_binop_subset (+) (zero_add _) f g
+@[to_additive] lemma mul_support_sup [semilattice_sup M] (f g : α → M) :
+  mul_support (λ x, f x ⊔ g x) ⊆ mul_support f ∪ mul_support g :=
+mul_support_binop_subset (⊔) sup_idem f g
+
+@[to_additive] lemma mul_support_inf [semilattice_inf M] (f g : α → M) :
+  mul_support (λ x, f x ⊓ g x) ⊆ mul_support f ∪ mul_support g :=
+mul_support_binop_subset (⊓) inf_idem f g
+
+@[to_additive] lemma mul_support_max [linear_order M] (f g : α → M) :
+  mul_support (λ x, max (f x) (g x)) ⊆ mul_support f ∪ mul_support g :=
+mul_support_sup f g
+
+@[to_additive] lemma mul_support_min [linear_order M] (f g : α → M) :
+  mul_support (λ x, min (f x) (g x)) ⊆ mul_support f ∪ mul_support g :=
+mul_support_inf f g
+
+@[to_additive] lemma mul_support_supr [conditionally_complete_lattice M] [nonempty ι]
+  (f : ι → α → M) :
+  mul_support (λ x, ⨆ i, f i x) ⊆ ⋃ i, mul_support (f i) :=
+begin
+  rw mul_support_subset_iff',
+  simp only [mem_Union, not_exists, nmem_mul_support],
+  intros x hx,
+  simp only [hx, csupr_const]
+end
+
+@[to_additive] lemma mul_support_infi [conditionally_complete_lattice M] [nonempty ι]
+  (f : ι → α → M) :
+  mul_support (λ x, ⨅ i, f i x) ⊆ ⋃ i, mul_support (f i) :=
+@mul_support_supr _ (order_dual M) ι ⟨(1:M)⟩ _ _ f
+
+@[to_additive] lemma mul_support_comp_subset {g : M → N} (hg : g 1 = 1) (f : α → M) :
+  mul_support (g ∘ f) ⊆ mul_support f :=
+λ x, mt $ λ h, by simp only [(∘), *]
+
+@[to_additive] lemma mul_support_subset_comp {g : M → N} (hg : ∀ {x}, g x = 1 → x = 1)
+  (f : α → M) :
+  mul_support f ⊆ mul_support (g ∘ f) :=
+λ x, mt hg
+
+@[to_additive] lemma mul_support_comp_eq (g : M → N) (hg : ∀ {x}, g x = 1 ↔ x = 1)
+  (f : α → M) :
+  mul_support (g ∘ f) = mul_support f :=
+set.ext $ λ x, not_congr hg
+
+@[to_additive] lemma mul_support_comp_eq_preimage (g : β → M) (f : α → β) :
+  mul_support (g ∘ f) = f ⁻¹' mul_support g :=
+rfl
+
+@[to_additive support_prod_mk] lemma mul_support_prod_mk (f : α → M) (g : α → N) :
+  mul_support (λ x, (f x, g x)) = mul_support f ∪ mul_support g :=
+set.ext $ λ x, by simp only [mul_support, not_and_distrib, mem_union_eq, mem_set_of_eq,
+  prod.mk_eq_one, ne.def]
+
+@[to_additive support_prod_mk'] lemma mul_support_prod_mk' (f : α → M × N) :
+  mul_support f = mul_support (λ x, (f x).1) ∪ mul_support (λ x, (f x).2) :=
+by simp only [← mul_support_prod_mk, prod.mk.eta]
+
+end has_one
 
-@[simp] lemma support_neg [add_group A] (f : α → A) :
-  support (λ x, -f x) = support f :=
-set.ext $ λ x, not_congr neg_eq_zero
+@[to_additive] lemma mul_support_mul [monoid M] (f g : α → M) :
+  mul_support (λ x, f x * g x) ⊆ mul_support f ∪ mul_support g :=
+mul_support_binop_subset (*) (one_mul _) f g
 
-lemma support_sub [add_group A] (f g : α → A) :
-  support (λ x, f x - g x) ⊆ support f ∪ support g :=
-support_binop_subset (has_sub.sub) (sub_self _) f g
+@[simp, to_additive] lemma mul_support_inv [group G] (f : α → G) :
+  mul_support (λ x, (f x)⁻¹) = mul_support f :=
+set.ext $ λ x, not_congr inv_eq_one
 
-@[simp] lemma support_mul [mul_zero_class A] [no_zero_divisors A] (f g : α → A) :
+@[simp, to_additive support_neg'] lemma mul_support_inv'' [group G] (f : α → G) :
+  mul_support (f⁻¹) = mul_support f :=
+mul_support_inv f
+
+@[simp] lemma mul_support_inv' [group_with_zero G₀] (f : α → G₀) :
+  mul_support (λ x, (f x)⁻¹) = mul_support f :=
+set.ext $ λ x, not_congr inv_eq_one'
+
+@[to_additive] lemma mul_support_mul_inv [group G] (f g : α → G) :
+  mul_support (λ x, f x * (g x)⁻¹) ⊆ mul_support f ∪ mul_support g :=
+mul_support_binop_subset (λ a b, a * b⁻¹) (by simp) f g
+
+@[to_additive support_sub] lemma mul_support_group_div [group G] (f g : α → G) :
+  mul_support (λ x, f x / g x) ⊆ mul_support f ∪ mul_support g :=
+mul_support_binop_subset (/) (by simp only [one_div, one_inv]) f g
+
+lemma mul_support_div [group_with_zero G₀] (f g : α → G₀) :
+  mul_support (λ x, f x / g x) ⊆ mul_support f ∪ mul_support g :=
+mul_support_binop_subset (/) (by simp only [div_one]) f g
+
+@[simp] lemma support_mul [mul_zero_class R] [no_zero_divisors R] (f g : α → R) :
   support (λ x, f x * g x) = support f ∩ support g :=
-set.ext $ λ x, by simp only [support, ne.def, mul_eq_zero, mem_set_of_eq,
-  mem_inter_iff, not_or_distrib]
+set.ext $ λ x, by simp only [mem_support, mul_ne_zero_iff, mem_inter_eq, not_or_distrib]
 
 lemma support_smul_subset_right [add_monoid A] [monoid B] [distrib_mul_action B A]
   (b : B) (f : α → A) :
   support (b • f) ⊆ support f :=
 λ x hbf hf, hbf $ by rw [pi.smul_apply, hf, smul_zero]
 
-lemma support_smul_subset_left {R M} [semiring R] [add_comm_monoid M] [semimodule R M]
+lemma support_smul_subset_left [semiring R] [add_comm_monoid M] [semimodule R M]
   (f : α → R) (g : α → M) :
   support (f • g) ⊆ support f :=
 λ x hfg hf, hfg $ by rw [pi.smul_apply', hf, zero_smul]
 
-lemma support_smul {R M} [semiring R] [add_comm_monoid M] [semimodule R M]
+lemma support_smul [semiring R] [add_comm_monoid M] [semimodule R M]
   [no_zero_smul_divisors R M] (f : α → R) (g : α → M) :
   support (f • g) = support f ∩ support g :=
 ext $ λ x, smul_ne_zero
 
-@[simp] lemma support_inv [division_ring A] (f : α → A) :
+@[simp] lemma support_inv [group_with_zero G₀] (f : α → G₀) :
   support (λ x, (f x)⁻¹) = support f :=
 set.ext $ λ x, not_congr inv_eq_zero
 
-@[simp] lemma support_div [division_ring A] (f g : α → A) :
+@[simp] lemma support_div [group_with_zero G₀] (f g : α → G₀) :
   support (λ x, f x / g x) = support f ∩ support g :=
 by simp [div_eq_mul_inv]
 
-lemma support_sup [has_zero A] [semilattice_sup A] (f g : α → A) :
-  support (λ x, (f x) ⊔ (g x)) ⊆ support f ∪ support g :=
-support_binop_subset (⊔) sup_idem f g
-
-lemma support_inf [has_zero A] [semilattice_inf A] (f g : α → A) :
-  support (λ x, (f x) ⊓ (g x)) ⊆ support f ∪ support g :=
-support_binop_subset (⊓) inf_idem f g
-
-lemma support_max [has_zero A] [linear_order A] (f g : α → A) :
-  support (λ x, max (f x) (g x)) ⊆ support f ∪ support g :=
-support_sup f g
-
-lemma support_min [has_zero A] [linear_order A] (f g : α → A) :
-  support (λ x, min (f x) (g x)) ⊆ support f ∪ support g :=
-support_inf f g
-
-lemma support_supr [has_zero A] [conditionally_complete_lattice A] [nonempty ι] (f : ι → α → A) :
-  support (λ x, ⨆ i, f i x) ⊆ ⋃ i, support (f i) :=
-begin
-  intros x hx,
-  classical,
-  contrapose hx,
-  simp only [mem_Union, not_exists, nmem_support] at hx ⊢,
-  simp only [hx, csupr_const]
-end
-
-lemma support_infi [has_zero A] [conditionally_complete_lattice A] [nonempty ι] (f : ι → α → A) :
-  support (λ x, ⨅ i, f i x) ⊆ ⋃ i, support (f i) :=
-@support_supr _ _ (order_dual A) ⟨(0:A)⟩ _ _ f
-
-lemma support_sum [add_comm_monoid A] (s : finset α) (f : α → β → A) :
-  support (λ x, ∑ i in s, f i x) ⊆ ⋃ i ∈ s, support (f i) :=
+@[to_additive] lemma mul_support_prod [comm_monoid M] (s : finset α) (f : α → β → M) :
+  mul_support (λ x, ∏ i in s, f i x) ⊆ ⋃ i ∈ s, mul_support (f i) :=
 begin
-  intros x hx,
-  classical,
-  contrapose hx,
-  simp only [mem_Union, not_exists, nmem_support] at hx ⊢,
-  exact finset.sum_eq_zero hx
+  rw mul_support_subset_iff',
+  simp only [mem_Union, not_exists, nmem_mul_support],
+  exact λ x, finset.prod_eq_one
 end
 
 lemma support_prod_subset [comm_monoid_with_zero A] (s : finset α) (f : α → β → A) :
@@ -152,28 +202,29 @@ lemma support_prod [comm_monoid_with_zero A] [no_zero_divisors A] [nontrivial A]
 set.ext $ λ x, by
   simp only [support, ne.def, finset.prod_eq_zero_iff, mem_set_of_eq, set.mem_Inter, not_exists]
 
-lemma support_comp_subset [has_zero A] [has_zero B] {g : A → B} (hg : g 0 = 0) (f : α → A) :
-  support (g ∘ f) ⊆ support f :=
-λ x, mt $ λ h, by simp [(∘), *]
+lemma mul_support_one_add [has_one R] [add_left_cancel_monoid R] (f : α → R) :
+  mul_support (λ x, 1 + f x) = support f :=
+set.ext $ λ x, not_congr add_right_eq_self
 
-lemma support_subset_comp [has_zero A] [has_zero B] {g : A → B} (hg : ∀ {x}, g x = 0 → x = 0)
-  (f : α → A) :
-  support f ⊆ support (g ∘ f) :=
-λ x, mt hg
+lemma mul_support_one_add' [has_one R] [add_left_cancel_monoid R] (f : α → R) :
+  mul_support (1 + f) = support f :=
+mul_support_one_add f
 
-lemma support_comp_eq [has_zero A] [has_zero B] (g : A → B) (hg : ∀ {x}, g x = 0 ↔ x = 0)
-  (f : α → A) :
-  support (g ∘ f) = support f :=
-set.ext $ λ x, not_congr hg
+lemma mul_support_add_one [has_one R] [add_right_cancel_monoid R] (f : α → R) :
+  mul_support (λ x, f x + 1) = support f :=
+set.ext $ λ x, not_congr add_left_eq_self
 
-lemma support_comp_eq_preimage [has_zero B] (g : A → B) (f : α → A) :
-  support (g ∘ f) = f ⁻¹' support g :=
-rfl
+lemma mul_support_add_one' [has_one R] [add_right_cancel_monoid R] (f : α → R) :
+  mul_support (f + 1) = support f :=
+mul_support_add_one f
+
+lemma mul_support_one_sub' [has_one R] [add_group R] (f : α → R) :
+  mul_support (1 - f) = support f :=
+by rw [sub_eq_add_neg, mul_support_one_add', support_neg']
 
-lemma support_prod_mk [has_zero A] [has_zero B] (f : α → A) (g : α → B) :
-  support (λ x, (f x, g x)) = support f ∪ support g :=
-set.ext $ λ x, by simp only [support, not_and_distrib, mem_union_eq, mem_set_of_eq,
-  prod.mk_eq_zero, ne.def]
+lemma mul_support_one_sub [has_one R] [add_group R] (f : α → R) :
+  mul_support (λ x, 1 - f x) = support f :=
+mul_support_one_sub' f
 
 end function
 
@@ -182,8 +233,7 @@ variables {A : Type*} {B : Type*} [decidable_eq A] [has_zero B] {a : A} {b : B}
 
 lemma support_single_zero : function.support (pi.single a (0 : B)) = ∅ := by simp
 
-@[simp]
-lemma support_single_of_ne (h : b ≠ 0) :
+@[simp] lemma support_single_of_ne (h : b ≠ 0) :
   function.support (pi.single a b) = {a} :=
 begin
   ext,