Mathlib.Algebra.Group.Support

Function.mulSupport definition

(f : α → M) : Set α

Full source

/-- `mulSupport` of a function is the set of points `x` such that `f x ≠ 1`. -/
@[to_additive "`support` of a function is the set of points `x` such that `f x ≠ 0`."]
def mulSupport (f : α → M) : Set α := {x | f x ≠ 1}

Multiplicative support of a function

Informal description

For a function $ f : \alpha \to M $, the multiplicative support of $ f $ is the set of all points $ x \in \alpha $ such that $ f(x) \neq 1 $. In other words, it is the complement of the preimage of $ \{1\} $ under $ f $.

Function.mulSupport_eq_preimage theorem

(f : α → M) : mulSupport f = f ⁻¹' { 1 }ᶜ

Full source

@[to_additive]
theorem mulSupport_eq_preimage (f : α → M) : mulSupport f = f ⁻¹' {1}ᶜ :=
  rfl

Multiplicative Support as Preimage Complement: $\operatorname{mulSupport}(f) = f^{-1}(\{1\})^c$

Informal description

For any function $f \colon \alpha \to M$, the multiplicative support of $f$ is equal to the complement of the preimage of $\{1\}$ under $f$, i.e., \[ \operatorname{mulSupport}(f) = f^{-1}(\{1\})^c. \]

Function.nmem_mulSupport theorem

{f : α → M} {x : α} : x ∉ mulSupport f ↔ f x = 1

Full source

@[to_additive]
theorem nmem_mulSupport {f : α → M} {x : α} : x ∉ mulSupport fx ∉ mulSupport f ↔ f x = 1 :=
  not_not

Characterization of Elements Outside Multiplicative Support

Informal description

For a function $f : \alpha \to M$ and an element $x \in \alpha$, the element $x$ is not in the multiplicative support of $f$ if and only if $f(x) = 1$. In other words, $x \notin \mathrm{mulSupport}(f) \leftrightarrow f(x) = 1$.

Function.compl_mulSupport theorem

{f : α → M} : (mulSupport f)ᶜ = {x | f x = 1}

Full source

@[to_additive]
theorem compl_mulSupport {f : α → M} : (mulSupport f)ᶜ = { x | f x = 1 } :=
  ext fun _ => nmem_mulSupport

Complement of Multiplicative Support Equals Preimage of One: $(\operatorname{mulSupport}(f))^c = \{x \mid f(x) = 1\}$

Informal description

For any function $f \colon \alpha \to M$, the complement of the multiplicative support of $f$ is equal to the set of all $x \in \alpha$ such that $f(x) = 1$. That is, \[ (\operatorname{mulSupport}(f))^c = \{x \mid f(x) = 1\}. \]

Function.mem_mulSupport theorem

{f : α → M} {x : α} : x ∈ mulSupport f ↔ f x ≠ 1

Full source

@[to_additive (attr := simp)]
theorem mem_mulSupport {f : α → M} {x : α} : x ∈ mulSupport fx ∈ mulSupport f ↔ f x ≠ 1 :=
  Iff.rfl

Characterization of Multiplicative Support Membership: $x \in \mathrm{mulSupport}(f) \leftrightarrow f(x) \neq 1$

Informal description

For a function $f : \alpha \to M$ and an element $x \in \alpha$, $x$ belongs to the multiplicative support of $f$ if and only if $f(x) \neq 1$. In other words, $x \in \mathrm{mulSupport}(f) \leftrightarrow f(x) \neq 1$.

Function.mulSupport_subset_iff theorem

{f : α → M} {s : Set α} : mulSupport f ⊆ s ↔ ∀ x, f x ≠ 1 → x ∈ s

Full source

@[to_additive (attr := simp)]
theorem mulSupport_subset_iff {f : α → M} {s : Set α} : mulSupportmulSupport f ⊆ smulSupport f ⊆ s ↔ ∀ x, f x ≠ 1 → x ∈ s :=
  Iff.rfl

Characterization of Multiplicative Support Containment: $\mathrm{mulSupport}(f) \subseteq s \leftrightarrow \forall x, f(x) \neq 1 \to x \in s$

Informal description

For a function $f : \alpha \to M$ and a set $s \subseteq \alpha$, the multiplicative support of $f$ is contained in $s$ if and only if for every $x \in \alpha$, if $f(x) \neq 1$ then $x \in s$.

Function.mulSupport_subset_iff' theorem

{f : α → M} {s : Set α} : mulSupport f ⊆ s ↔ ∀ x ∉ s, f x = 1

Full source

@[to_additive]
theorem mulSupport_subset_iff' {f : α → M} {s : Set α} :
    mulSupportmulSupport f ⊆ smulSupport f ⊆ s ↔ ∀ x ∉ s, f x = 1 :=
  forall_congr' fun _ => not_imp_comm

Characterization of Multiplicative Support Containment: $\mathrm{mulSupport}(f) \subseteq s \leftrightarrow \forall x \notin s, f(x) = 1$

Informal description

For a function $f : \alpha \to M$ and a set $s \subseteq \alpha$, the multiplicative support of $f$ is contained in $s$ if and only if for every $x \notin s$, the value $f(x)$ equals $1$.

Function.mulSupport_eq_iff theorem

{f : α → M} {s : Set α} : mulSupport f = s ↔ (∀ x, x ∈ s → f x ≠ 1) ∧ ∀ x, x ∉ s → f x = 1

Full source

@[to_additive]
theorem mulSupport_eq_iff {f : α → M} {s : Set α} :
    mulSupportmulSupport f = s ↔ (∀ x, x ∈ s → f x ≠ 1) ∧ ∀ x, x ∉ s → f x = 1 := by
  simp +contextual only [Set.ext_iff, mem_mulSupport, ne_eq, iff_def,
    not_imp_comm, and_comm, forall_and]

Characterization of Multiplicative Support Equality: $\text{mulSupport}(f) = s \leftrightarrow (\forall x \in s, f(x) \neq 1) \land (\forall x \notin s, f(x) = 1)$

Informal description

For a function $f : \alpha \to M$ and a set $s \subseteq \alpha$, the multiplicative support of $f$ equals $s$ if and only if: 1. For every $x \in s$, $f(x) \neq 1$, and 2. For every $x \notin s$, $f(x) = 1$.

Function.ext_iff_mulSupport theorem

{f g : α → M} : f = g ↔ f.mulSupport = g.mulSupport ∧ ∀ x ∈ f.mulSupport, f x = g x

Full source

@[to_additive]
theorem ext_iff_mulSupport {f g : α → M} :
    f = g ↔ f.mulSupport = g.mulSupport ∧ ∀ x ∈ f.mulSupport, f x = g x :=
  ⟨fun h ↦ h ▸ ⟨rfl, fun _ _ ↦ rfl⟩, fun ⟨h₁, h₂⟩ ↦ funext fun x ↦ by
    if hx : x ∈ f.mulSupport then exact h₂ x hx
    else rw [nmem_mulSupport.1 hx, nmem_mulSupport.1 (mt (Set.ext_iff.1 h₁ x).2 hx)]⟩

Function Equality via Multiplicative Support and Pointwise Agreement

Informal description

Two functions $f, g : \alpha \to M$ are equal if and only if their multiplicative supports are equal and they agree on all points in their multiplicative support, i.e., \[ f = g \leftrightarrow \mathrm{mulSupport}(f) = \mathrm{mulSupport}(g) \land (\forall x \in \mathrm{mulSupport}(f), f(x) = g(x)). \]

Function.mulSupport_update_of_ne_one theorem

[DecidableEq α] (f : α → M) (x : α) {y : M} (hy : y ≠ 1) : mulSupport (update f x y) = insert x (mulSupport f)

Full source

@[to_additive]
theorem mulSupport_update_of_ne_one [DecidableEq α] (f : α → M) (x : α) {y : M} (hy : y ≠ 1) :
    mulSupport (update f x y) = insert x (mulSupport f) := by
  ext a; rcases eq_or_ne a x with rfl | hne <;> simp [*]

Multiplicative Support of Function Update with Non-Unit Value: $\text{mulSupport}(\text{update } f \, x \, y) = \{x\} \cup \text{mulSupport}(f)$ when $y \neq 1$

Informal description

Let $\alpha$ be a type with decidable equality, $M$ be a type, $f : \alpha \to M$ be a function, $x \in \alpha$ be a point, and $y \in M$ be an element such that $y \neq 1$. Then the multiplicative support of the updated function $\text{update } f \, x \, y$ is equal to the set obtained by inserting $x$ into the multiplicative support of $f$, i.e., \[ \text{mulSupport}(\text{update } f \, x \, y) = \{x\} \cup \text{mulSupport}(f). \]

Function.mulSupport_update_one theorem

[DecidableEq α] (f : α → M) (x : α) : mulSupport (update f x 1) = mulSupport f \ { x }

Full source

@[to_additive]
theorem mulSupport_update_one [DecidableEq α] (f : α → M) (x : α) :
    mulSupport (update f x 1) = mulSupportmulSupport f \ {x} := by
  ext a; rcases eq_or_ne a x with rfl | hne <;> simp [*]

Multiplicative Support of Function Update with Unit Value: $\text{mulSupport}(\text{update } f \, x \, 1) = \text{mulSupport}(f) \setminus \{x\}$

Informal description

Let $\alpha$ be a type with decidable equality, $M$ be a type with a multiplicative identity $1$, and $f : \alpha \to M$ be a function. For any $x \in \alpha$, the multiplicative support of the updated function $\text{update } f \, x \, 1$ is equal to the multiplicative support of $f$ with the element $x$ removed, i.e., \[ \text{mulSupport}(\text{update } f \, x \, 1) = \text{mulSupport}(f) \setminus \{x\}. \]

Function.mulSupport_update_eq_ite theorem

 [DecidableEq α] [DecidableEq M] (f : α → M) (x : α) (y : M) :
  mulSupport (update f x y) = if y = 1 then mulSupport f \ { x } else insert x (mulSupport f)

Full source

@[to_additive]
theorem mulSupport_update_eq_ite [DecidableEq α] [DecidableEq M] (f : α → M) (x : α) (y : M) :
    mulSupport (update f x y) = if y = 1 then mulSupport f \ {x} else insert x (mulSupport f) := by
  rcases eq_or_ne y 1 with rfl | hy <;> simp [mulSupport_update_one, mulSupport_update_of_ne_one, *]

Multiplicative Support of Function Update via Case Analysis: $\text{mulSupport}(\text{update } f \, x \, y) = \text{if } y = 1 \text{ then } \text{mulSupport}(f) \setminus \{x\} \text{ else } \{x\} \cup \text{mulSupport}(f)$

Informal description

Let $\alpha$ be a type with decidable equality, $M$ be a type with decidable equality, $f : \alpha \to M$ be a function, $x \in \alpha$ be a point, and $y \in M$ be an element. The multiplicative support of the updated function $\text{update } f \, x \, y$ is given by: \[ \text{mulSupport}(\text{update } f \, x \, y) = \begin{cases} \text{mulSupport}(f) \setminus \{x\} & \text{if } y = 1, \\ \{x\} \cup \text{mulSupport}(f) & \text{otherwise.} \end{cases} \]

Function.mulSupport_extend_one_subset theorem

{f : α → M'} {g : α → N} : mulSupport (f.extend g 1) ⊆ f '' mulSupport g

Full source

@[to_additive]
theorem mulSupport_extend_one_subset {f : α → M'} {g : α → N} :
    mulSupportmulSupport (f.extend g 1) ⊆ f '' mulSupport g :=
  mulSupport_subset_iff'.mpr fun x hfg ↦ by
    by_cases hf : ∃ a, f a = x
    · rw [extend, dif_pos hf, ← nmem_mulSupport]
      rw [← Classical.choose_spec hf] at hfg
      exact fun hg ↦ hfg ⟨_, hg, rfl⟩
    · rw [extend_apply' _ _ _ hf]; rfl

Inclusion of Multiplicative Support in Image of Extended Function

Informal description

For any functions $f : \alpha \to M'$ and $g : \alpha \to N$, the multiplicative support of the extended function $f.\text{extend}\,g\,1$ is contained in the image of the multiplicative support of $g$ under $f$, i.e., \[ \text{mulSupport}(f.\text{extend}\,g\,1) \subseteq f(\text{mulSupport}(g)). \]

Function.mulSupport_extend_one theorem

{f : α → M'} {g : α → N} (hf : f.Injective) : mulSupport (f.extend g 1) = f '' mulSupport g

Full source

@[to_additive]
theorem mulSupport_extend_one {f : α → M'} {g : α → N} (hf : f.Injective) :
    mulSupport (f.extend g 1) = f '' mulSupport g :=
  mulSupport_extend_one_subset.antisymm <| by
    rintro _ ⟨x, hx, rfl⟩; rwa [mem_mulSupport, hf.extend_apply]

Multiplicative Support of Extended Function Equals Image of Support under Injective Map

Informal description

For any injective function $f : \alpha \to M'$ and any function $g : \alpha \to N$, the multiplicative support of the extended function $f.\text{extend}\,g\,1$ is equal to the image under $f$ of the multiplicative support of $g$, i.e., \[ \text{mulSupport}(f.\text{extend}\,g\,1) = f(\text{mulSupport}(g)). \]

Function.mulSupport_disjoint_iff theorem

{f : α → M} {s : Set α} : Disjoint (mulSupport f) s ↔ EqOn f 1 s

Full source

@[to_additive]
theorem mulSupport_disjoint_iff {f : α → M} {s : Set α} :
    DisjointDisjoint (mulSupport f) s ↔ EqOn f 1 s := by
  simp_rw [← subset_compl_iff_disjoint_right, mulSupport_subset_iff', not_mem_compl_iff, EqOn,
    Pi.one_apply]

Disjointness of Multiplicative Support and Set is Equivalent to Function Being One on Set

Informal description

For a function $f : \alpha \to M$ and a set $s \subseteq \alpha$, the multiplicative support of $f$ is disjoint from $s$ if and only if $f$ is identically equal to $1$ on $s$. In other words, \[ \mathrm{mulSupport}(f) \cap s = \emptyset \leftrightarrow \forall x \in s, f(x) = 1. \]

Function.disjoint_mulSupport_iff theorem

{f : α → M} {s : Set α} : Disjoint s (mulSupport f) ↔ EqOn f 1 s

Full source

@[to_additive]
theorem disjoint_mulSupport_iff {f : α → M} {s : Set α} :
    DisjointDisjoint s (mulSupport f) ↔ EqOn f 1 s := by
  rw [disjoint_comm, mulSupport_disjoint_iff]

Disjointness of Set and Multiplicative Support is Equivalent to Function Being One on Set

Informal description

For a function $f : \alpha \to M$ and a set $s \subseteq \alpha$, the set $s$ is disjoint from the multiplicative support of $f$ if and only if $f$ is identically equal to $1$ on $s$. In other words, \[ s \cap \mathrm{mulSupport}(f) = \emptyset \leftrightarrow \forall x \in s, f(x) = 1. \]

Function.mulSupport_eq_empty_iff theorem

{f : α → M} : mulSupport f = ∅ ↔ f = 1

Full source

@[to_additive (attr := simp)]
theorem mulSupport_eq_empty_iff {f : α → M} : mulSupportmulSupport f = ∅ ↔ f = 1 := by
  rw [← subset_empty_iff, mulSupport_subset_iff', funext_iff]
  simp

Characterization of Empty Multiplicative Support: $\mathrm{mulSupport}(f) = \emptyset \leftrightarrow f = 1$

Informal description

For a function $f : \alpha \to M$, the multiplicative support of $f$ is empty if and only if $f$ is identically equal to $1$. In other words, $\mathrm{mulSupport}(f) = \emptyset \leftrightarrow f = 1$.

Function.mulSupport_nonempty_iff theorem

{f : α → M} : (mulSupport f).Nonempty ↔ f ≠ 1

Full source

@[to_additive (attr := simp)]
theorem mulSupport_nonempty_iff {f : α → M} : (mulSupport f).Nonempty ↔ f ≠ 1 := by
  rw [nonempty_iff_ne_empty, Ne, mulSupport_eq_empty_iff]

Nonempty Multiplicative Support Characterization: $\mathrm{mulSupport}(f) \neq \emptyset \leftrightarrow f \neq 1$

Informal description

For a function $f : \alpha \to M$, the multiplicative support of $f$ is nonempty if and only if $f$ is not identically equal to $1$. In other words, $\mathrm{mulSupport}(f) \neq \emptyset \leftrightarrow f \neq 1$.

Function.range_subset_insert_image_mulSupport theorem

(f : α → M) : range f ⊆ insert 1 (f '' mulSupport f)

Full source

@[to_additive]
theorem range_subset_insert_image_mulSupport (f : α → M) :
    rangerange f ⊆ insert 1 (f '' mulSupport f) := by
  simpa only [range_subset_iff, mem_insert_iff, or_iff_not_imp_left] using
    fun x (hx : x ∈ mulSupport f) => mem_image_of_mem f hx

Range of Function is Subset of One Union Image of Multiplicative Support

Informal description

For any function $f : \alpha \to M$, the range of $f$ is contained in the union of $\{1\}$ and the image of the multiplicative support of $f$ under $f$. In other words, $\text{range}(f) \subseteq \{1\} \cup f(\text{mulSupport}(f))$.

Function.range_eq_image_or_of_mulSupport_subset theorem

{f : α → M} {k : Set α} (h : mulSupport f ⊆ k) : range f = f '' k ∨ range f = insert 1 (f '' k)

Full source

@[to_additive]
lemma range_eq_image_or_of_mulSupport_subset {f : α → M} {k : Set α} (h : mulSupportmulSupport f ⊆ k) :
    rangerange f = f '' k ∨ range f = insert 1 (f '' k) := by
  have : rangerange f ⊆ insert 1 (f '' k) :=
    (range_subset_insert_image_mulSupport f).trans (insert_subset_insert (image_subset f h))
  by_cases h1 : 1 ∈ range f
  · exact Or.inr (subset_antisymm this (insert_subset h1 (image_subset_range _ _)))
  refine Or.inl (subset_antisymm ?_ (image_subset_range _ _))
  rwa [← diff_singleton_eq_self h1, diff_singleton_subset_iff]

Range Characterization via Multiplicative Support Subset

Informal description

For any function $f: \alpha \to M$ and any subset $k \subseteq \alpha$ such that the multiplicative support of $f$ is contained in $k$, the range of $f$ is either equal to the image of $k$ under $f$ or equal to the union of $\{1\}$ and the image of $k$ under $f$. That is, either $\text{range}(f) = f(k)$ or $\text{range}(f) = \{1\} \cup f(k)$.

Function.mulSupport_one' theorem

: mulSupport (1 : α → M) = ∅

Full source

@[to_additive (attr := simp)]
theorem mulSupport_one' : mulSupport (1 : α → M) = ∅ :=
  mulSupport_eq_empty_iff.2 rfl

Multiplicative Support of Constant One Function is Empty

Informal description

For the constant function $f : \alpha \to M$ with value $1$, the multiplicative support of $f$ is the empty set, i.e., $\mathrm{mulSupport}(f) = \emptyset$.

Function.mulSupport_one theorem

: (mulSupport fun _ : α => (1 : M)) = ∅

Full source

@[to_additive (attr := simp)]
theorem mulSupport_one : (mulSupport fun _ : α => (1 : M)) = ∅ :=
  mulSupport_one'

Multiplicative Support of Constant One Function is Empty

Informal description

For the constant function $f : \alpha \to M$ defined by $f(x) = 1$ for all $x \in \alpha$, the multiplicative support of $f$ is the empty set, i.e., $\mathrm{mulSupport}(f) = \emptyset$.

Function.mulSupport_const theorem

{c : M} (hc : c ≠ 1) : (mulSupport fun _ : α => c) = Set.univ

Full source

@[to_additive]
theorem mulSupport_const {c : M} (hc : c ≠ 1) : (mulSupport fun _ : α => c) = Set.univ := by
  ext x
  simp [hc]

Multiplicative Support of a Non-One Constant Function is the Entire Domain

Informal description

For any constant function $ f : \alpha \to M $ with value $ c \neq 1 $, the multiplicative support of $ f $ is the entire set $ \alpha $, i.e., $\operatorname{mulSupport} f = \alpha$.

Function.mulSupport_binop_subset theorem

 (op : M → N → P) (op1 : op 1 1 = 1) (f : α → M) (g : α → N) :
  (mulSupport fun x => op (f x) (g x)) ⊆ mulSupport f ∪ mulSupport g

Full source

@[to_additive]
theorem mulSupport_binop_subset (op : M → N → P) (op1 : op 1 1 = 1) (f : α → M) (g : α → N) :
    (mulSupport fun x => op (f x) (g x)) ⊆ mulSupport f ∪ mulSupport g := fun x hx =>
  not_or_of_imp fun hf hg => hx <| by simp only [hf, hg, op1]

Multiplicative support of a binary operation is contained in the union of supports

Informal description

Let $M$, $N$, and $P$ be types with multiplicative identities, and let $\mathrm{op} : M \to N \to P$ be a binary operation such that $\mathrm{op}(1,1) = 1$. For any functions $f : \alpha \to M$ and $g : \alpha \to N$, the multiplicative support of the function $x \mapsto \mathrm{op}(f(x), g(x))$ is a subset of the union of the multiplicative supports of $f$ and $g$.

Function.mulSupport_comp_subset theorem

{g : M → N} (hg : g 1 = 1) (f : α → M) : mulSupport (g ∘ f) ⊆ mulSupport f

Full source

@[to_additive]
theorem mulSupport_comp_subset {g : M → N} (hg : g 1 = 1) (f : α → M) :
    mulSupportmulSupport (g ∘ f) ⊆ mulSupport f := fun x => mt fun h => by simp only [(· ∘ ·), *]

Multiplicative Support of Composition is Subset of Original Support

Informal description

Let $g : M \to N$ be a function satisfying $g(1) = 1$, and let $f : \alpha \to M$ be any function. Then the multiplicative support of the composition $g \circ f$ is a subset of the multiplicative support of $f$, i.e., \[ \{x \in \alpha \mid g(f(x)) \neq 1\} \subseteq \{x \in \alpha \mid f(x) \neq 1\}. \]

Function.mulSupport_subset_comp theorem

{g : M → N} (hg : ∀ {x}, g x = 1 → x = 1) (f : α → M) : mulSupport f ⊆ mulSupport (g ∘ f)

Full source

@[to_additive]
theorem mulSupport_subset_comp {g : M → N} (hg : ∀ {x}, g x = 1 → x = 1) (f : α → M) :
    mulSupportmulSupport f ⊆ mulSupport (g ∘ f) := fun _ => mt hg

Inclusion of Multiplicative Support under Composition with Injective-like Condition

Informal description

For any function $g : M \to N$ satisfying the condition that $g(x) = 1$ implies $x = 1$ for all $x \in M$, and any function $f : \alpha \to M$, the multiplicative support of $f$ is contained in the multiplicative support of the composition $g \circ f$. In other words, $\{x \in \alpha \mid f(x) \neq 1\} \subseteq \{x \in \alpha \mid g(f(x)) \neq 1\}$.

Function.mulSupport_comp_eq theorem

(g : M → N) (hg : ∀ {x}, g x = 1 ↔ x = 1) (f : α → M) : mulSupport (g ∘ f) = mulSupport f

Full source

@[to_additive]
theorem mulSupport_comp_eq (g : M → N) (hg : ∀ {x}, g x = 1 ↔ x = 1) (f : α → M) :
    mulSupport (g ∘ f) = mulSupport f :=
  Set.ext fun _ => not_congr hg

Multiplicative Support of Composition Equals Multiplicative Support of Function When $g$ Preserves Non-One Elements

Informal description

For functions $g : M \to N$ and $f : \alpha \to M$, if $g$ satisfies the property that $g(x) = 1$ if and only if $x = 1$ for all $x \in M$, then the multiplicative support of the composition $g \circ f$ is equal to the multiplicative support of $f$, i.e., \[ \{x \in \alpha \mid g(f(x)) \neq 1\} = \{x \in \alpha \mid f(x) \neq 1\}. \]

Function.mulSupport_comp_eq_of_range_subset theorem

 {g : M → N} {f : α → M} (hg : ∀ {x}, x ∈ range f → (g x = 1 ↔ x = 1)) : mulSupport (g ∘ f) = mulSupport f

Full source

@[to_additive]
theorem mulSupport_comp_eq_of_range_subset {g : M → N} {f : α → M}
    (hg : ∀ {x}, x ∈ range f → (g x = 1 ↔ x = 1)) :
    mulSupport (g ∘ f) = mulSupport f :=
  Set.ext fun x ↦ not_congr <| by rw [Function.comp, hg (mem_range_self x)]

Multiplicative Support of Composition under Range Condition: $\text{mulSupport}(g \circ f) = \text{mulSupport}(f)$

Informal description

Let $g : M \to N$ and $f : \alpha \to M$ be functions. If for every $x$ in the range of $f$, we have $g(x) = 1$ if and only if $x = 1$, then the multiplicative support of the composition $g \circ f$ is equal to the multiplicative support of $f$. In other words, $\{x \in \alpha \mid g(f(x)) \neq 1\} = \{x \in \alpha \mid f(x) \neq 1\}$.

Function.mulSupport_comp_eq_preimage theorem

(g : β → M) (f : α → β) : mulSupport (g ∘ f) = f ⁻¹' mulSupport g

Full source

@[to_additive]
theorem mulSupport_comp_eq_preimage (g : β → M) (f : α → β) :
    mulSupport (g ∘ f) = f ⁻¹' mulSupport g :=
  rfl

Multiplicative Support of Composition Equals Preimage of Support

Informal description

For functions $g : \beta \to M$ and $f : \alpha \to \beta$, the multiplicative support of the composition $g \circ f$ is equal to the preimage under $f$ of the multiplicative support of $g$. That is, $$\{x \in \alpha \mid g(f(x)) \neq 1\} = f^{-1}(\{y \in \beta \mid g(y) \neq 1\}).$$

Function.mulSupport_prod_mk theorem

(f : α → M) (g : α → N) : (mulSupport fun x => (f x, g x)) = mulSupport f ∪ mulSupport g

Full source

@[to_additive support_prod_mk]
theorem mulSupport_prod_mk (f : α → M) (g : α → N) :
    (mulSupport fun x => (f x, g x)) = mulSupportmulSupport f ∪ mulSupport g :=
  Set.ext fun x => by
    simp only [mulSupport, not_and_or, mem_union, mem_setOf_eq, Prod.mk_eq_one, Ne]

Multiplicative Support of Product Function Equals Union of Supports

Informal description

For functions $f: \alpha \to M$ and $g: \alpha \to N$, the multiplicative support of the function $x \mapsto (f(x), g(x))$ is equal to the union of the multiplicative supports of $f$ and $g$. That is, $$\mathrm{mulSupport}(\lambda x. (f(x), g(x))) = \mathrm{mulSupport}(f) \cup \mathrm{mulSupport}(g).$$

Function.mulSupport_prod_mk' theorem

(f : α → M × N) : mulSupport f = (mulSupport fun x => (f x).1) ∪ mulSupport fun x => (f x).2

Full source

@[to_additive support_prod_mk']
theorem mulSupport_prod_mk' (f : α → M × N) :
    mulSupport f = (mulSupport fun x => (f x).1) ∪ mulSupport fun x => (f x).2 := by
  simp only [← mulSupport_prod_mk]

Multiplicative Support of Product Function Equals Union of Component Supports

Informal description

For any function $f : \alpha \to M \times N$, the multiplicative support of $f$ is equal to the union of the multiplicative supports of the component functions $x \mapsto (f(x)).1$ and $x \mapsto (f(x)).2$. In other words, \[ \{x \mid f(x) \neq (1,1)\} = \{x \mid (f(x)).1 \neq 1\} \cup \{x \mid (f(x)).2 \neq 1\}. \]

Function.mulSupport_along_fiber_subset theorem

(f : α × β → M) (a : α) : (mulSupport fun b => f (a, b)) ⊆ (mulSupport f).image Prod.snd

Full source

@[to_additive]
theorem mulSupport_along_fiber_subset (f : α × β → M) (a : α) :
    (mulSupport fun b => f (a, b)) ⊆ (mulSupport f).image Prod.snd :=
  fun x hx => ⟨(a, x), by simpa using hx⟩

Subset Property of Multiplicative Support Along a Fiber

Informal description

For any function $f : \alpha \times \beta \to M$ and any fixed $a \in \alpha$, the multiplicative support of the function $b \mapsto f(a, b)$ is a subset of the image under the second projection $\mathrm{snd}$ of the multiplicative support of $f$. In other words, $$ \{b \in \beta \mid f(a, b) \neq 1\} \subseteq \mathrm{snd}(\{(x, y) \in \alpha \times \beta \mid f(x, y) \neq 1\}). $$

Function.mulSupport_curry theorem

(f : α × β → M) : (mulSupport f.curry) = (mulSupport f).image Prod.fst

Full source

@[to_additive]
theorem mulSupport_curry (f : α × β → M) :
    (mulSupport f.curry) = (mulSupport f).image Prod.fst := by
  simp [mulSupport, funext_iff, image]

Multiplicative Support of Curried Function Equals Projection of Original Support

Informal description

For any function $f : \alpha \times \beta \to M$, the multiplicative support of the curried function $f.\text{curry}$ is equal to the image under the first projection of the multiplicative support of $f$. In other words, \[ \{x \mid \exists y, f(x,y) \neq 1\} = \pi_1(\{(x,y) \mid f(x,y) \neq 1\}), \] where $\pi_1$ denotes the projection onto the first coordinate.

Function.mulSupport_curry' theorem

(f : α × β → M) : (mulSupport fun a b ↦ f (a, b)) = (mulSupport f).image Prod.fst

Full source

@[to_additive]
theorem mulSupport_curry' (f : α × β → M) :
    (mulSupport fun a b ↦ f (a, b)) = (mulSupport f).image Prod.fst :=
  mulSupport_curry f

Multiplicative Support of Uncurried Function Equals Projection of Original Support

Informal description

For any function $f : \alpha \times \beta \to M$, the multiplicative support of the function $(a, b) \mapsto f(a, b)$ is equal to the image under the first projection of the multiplicative support of $f$. That is, \[ \{a \mid \exists b, f(a, b) \neq 1\} = \pi_1(\{(a, b) \mid f(a, b) \neq 1\}), \] where $\pi_1$ denotes the projection onto the first coordinate.

Function.mulSupport_mul theorem

[MulOneClass M] (f g : α → M) : (mulSupport fun x => f x * g x) ⊆ mulSupport f ∪ mulSupport g

Full source

@[to_additive]
theorem mulSupport_mul [MulOneClass M] (f g : α → M) :
    (mulSupport fun x => f x * g x) ⊆ mulSupport f ∪ mulSupport g :=
  mulSupport_binop_subset (· * ·) (one_mul _) f g

Multiplicative Support of Product is Subset of Union of Supports

Informal description

Let $M$ be a type with a multiplicative monoid structure, and let $f, g : \alpha \to M$ be functions. Then the multiplicative support of the pointwise product $x \mapsto f(x) \cdot g(x)$ is contained in the union of the multiplicative supports of $f$ and $g$, i.e., \[ \{x \mid f(x) \cdot g(x) \neq 1\} \subseteq \{x \mid f(x) \neq 1\} \cup \{x \mid g(x) \neq 1\}. \]

Function.mulSupport_pow theorem

[Monoid M] (f : α → M) (n : ℕ) : (mulSupport fun x => f x ^ n) ⊆ mulSupport f

Full source

@[to_additive]
theorem mulSupport_pow [Monoid M] (f : α → M) (n : ℕ) :
    (mulSupport fun x => f x ^ n) ⊆ mulSupport f := by
  induction n with
  | zero => simp [pow_zero, mulSupport_one]
  | succ n hfn =>
    simpa only [pow_succ'] using (mulSupport_mul f _).trans (union_subset Subset.rfl hfn)

Multiplicative Support of Power Function is Contained in Original Support

Informal description

For any function $f : \alpha \to M$ where $M$ is a monoid, and for any natural number $n$, the multiplicative support of the function $x \mapsto f(x)^n$ is contained in the multiplicative support of $f$. That is, \[ \{x \mid f(x)^n \neq 1\} \subseteq \{x \mid f(x) \neq 1\}. \]

Function.mulSupport_inv theorem

: (mulSupport fun x => (f x)⁻¹) = mulSupport f

Full source

@[to_additive (attr := simp)]
theorem mulSupport_inv : (mulSupport fun x => (f x)⁻¹) = mulSupport f :=
  ext fun _ => inv_ne_one

Multiplicative Support of Inverse Equals Support of Original Function

Informal description

For any function $f : \alpha \to M$ where $M$ is a division monoid, the multiplicative support of the function $x \mapsto (f x)^{-1}$ is equal to the multiplicative support of $f$. That is, \[ \{x \mid (f x)^{-1} \neq 1\} = \{x \mid f x \neq 1\}. \]

Function.mulSupport_inv' theorem

: mulSupport f⁻¹ = mulSupport f

Full source

@[to_additive (attr := simp)]
theorem mulSupport_inv' : mulSupport f⁻¹ = mulSupport f :=
  mulSupport_inv f

Multiplicative Support Invariance under Pointwise Inversion: $\mathrm{mulSupport}(f^{-1}) = \mathrm{mulSupport}(f)$

Informal description

For any function $f : \alpha \to M$ where $M$ is a division monoid, the multiplicative support of the pointwise inverse function $f^{-1}$ is equal to the multiplicative support of $f$. That is, \[ \{x \in \alpha \mid f(x)^{-1} \neq 1\} = \{x \in \alpha \mid f(x) \neq 1\}. \]

Function.mulSupport_mul_inv theorem

: (mulSupport fun x => f x * (g x)⁻¹) ⊆ mulSupport f ∪ mulSupport g

Full source

@[to_additive]
theorem mulSupport_mul_inv : (mulSupport fun x => f x * (g x)⁻¹) ⊆ mulSupport f ∪ mulSupport g :=
  mulSupport_binop_subset (fun a b => a * b⁻¹) (by simp) f g

Multiplicative support of product with inverse is contained in union of supports

Informal description

For functions $f, g : \alpha \to M$ where $M$ is a division monoid, the multiplicative support of the function $x \mapsto f(x) * g(x)^{-1}$ is contained in the union of the multiplicative supports of $f$ and $g$. That is, $$\mathrm{mulSupport} (\lambda x, f(x) * g(x)^{-1}) \subseteq \mathrm{mulSupport}(f) \cup \mathrm{mulSupport}(g).$$

Function.mulSupport_div theorem

: (mulSupport fun x => f x / g x) ⊆ mulSupport f ∪ mulSupport g

Full source

@[to_additive]
theorem mulSupport_div : (mulSupport fun x => f x / g x) ⊆ mulSupport f ∪ mulSupport g :=
  mulSupport_binop_subset (· / ·) one_div_one f g

Multiplicative support of quotient is contained in union of supports

Informal description

For functions $f, g : \alpha \to M$ where $M$ is a division monoid, the multiplicative support of the function $x \mapsto f(x) / g(x)$ is contained in the union of the multiplicative supports of $f$ and $g$. That is, $$\{x \in \alpha \mid f(x)/g(x) \neq 1\} \subseteq \{x \in \alpha \mid f(x) \neq 1\} \cup \{x \in \alpha \mid g(x) \neq 1\}.$$

Set.image_inter_mulSupport_eq theorem

{s : Set β} {g : β → α} : g '' s ∩ mulSupport f = g '' (s ∩ mulSupport (f ∘ g))

Full source

@[to_additive]
theorem image_inter_mulSupport_eq {s : Set β} {g : β → α} :
    g '' sg '' s ∩ mulSupport f = g '' (s ∩ mulSupport (f ∘ g)) := by
  rw [mulSupport_comp_eq_preimage f g, image_inter_preimage]

Image Intersection with Multiplicative Support Equals Image of Intersection with Composed Support

Informal description

For any set $s \subseteq \beta$ and function $g : \beta \to \alpha$, the intersection of the image $g(s)$ with the multiplicative support of $f : \alpha \to M$ equals the image under $g$ of the intersection of $s$ with the multiplicative support of $f \circ g$. That is, $$ g(s) \cap \{x \in \alpha \mid f(x) \neq 1\} = g\big(s \cap \{y \in \beta \mid f(g(y)) \neq 1\}\big). $$

Pi.mulSupport_mulSingle_subset theorem

: mulSupport (mulSingle a b) ⊆ { a }

Full source

@[to_additive]
theorem mulSupport_mulSingle_subset : mulSupportmulSupport (mulSingle a b) ⊆ {a} := fun _ hx =>
  by_contra fun hx' => hx <| mulSingle_eq_of_ne hx' _

Multiplicative Support of Point Function is Contained in Singleton

Informal description

For any element $a$ in the domain and $b$ in the codomain, the multiplicative support of the function `mulSingle a b` (which takes the value $b$ at $a$ and $1$ elsewhere) is a subset of the singleton set $\{a\}$. In other words, $\{x \mid \text{mulSingle } a b (x) \neq 1\} \subseteq \{a\}$.

Pi.mulSupport_mulSingle_one theorem

: mulSupport (mulSingle a (1 : B)) = ∅

Full source

@[to_additive]
theorem mulSupport_mulSingle_one : mulSupport (mulSingle a (1 : B)) = ∅ := by simp

Multiplicative Support of Constant One Point Function is Empty

Informal description

For any element $a$ in the domain and the multiplicative identity $1$ in the codomain $B$, the multiplicative support of the function $\text{mulSingle } a 1$ (which takes the value $1$ at $a$ and $1$ elsewhere) is the empty set, i.e., $\{x \mid \text{mulSingle } a 1 (x) \neq 1\} = \emptyset$.

Pi.mulSupport_mulSingle_of_ne theorem

(h : b ≠ 1) : mulSupport (mulSingle a b) = { a }

Full source

@[to_additive (attr := simp)]
theorem mulSupport_mulSingle_of_ne (h : b ≠ 1) : mulSupport (mulSingle a b) = {a} :=
  mulSupport_mulSingle_subset.antisymm fun x (hx : x = a) => by
    rwa [mem_mulSupport, hx, mulSingle_eq_same]

Multiplicative Support of Non-Unit Point Function is Singleton

Informal description

For any element $a$ in the domain and $b$ in the codomain, if $b \neq 1$, then the multiplicative support of the function $\text{mulSingle } a b$ (which takes the value $b$ at $a$ and $1$ elsewhere) is exactly the singleton set $\{a\}$. In other words, $\{x \mid \text{mulSingle } a b (x) \neq 1\} = \{a\}$ when $b \neq 1$.

Pi.mulSupport_mulSingle theorem

[DecidableEq B] : mulSupport (mulSingle a b) = if b = 1 then ∅ else { a }

Full source

@[to_additive]
theorem mulSupport_mulSingle [DecidableEq B] :
    mulSupport (mulSingle a b) = if b = 1 then ∅ else {a} := by split_ifs with h <;> simp [h]

Multiplicative Support of Point Function: $\mathrm{mulSupport}(\text{mulSingle } a b) = \emptyset$ if $b=1$ else $\{a\}$

Informal description

For any elements $a \in A$ and $b \in B$, the multiplicative support of the function $\text{mulSingle } a b$ (which takes the value $b$ at $a$ and $1$ elsewhere) is given by: \[ \mathrm{mulSupport}(\text{mulSingle } a b) = \begin{cases} \emptyset & \text{if } b = 1, \\ \{a\} & \text{otherwise.} \end{cases} \]

Pi.mulSupport_mulSingle_disjoint theorem

 {b' : B} (hb : b ≠ 1) (hb' : b' ≠ 1) {i j : A} :
  Disjoint (mulSupport (mulSingle i b)) (mulSupport (mulSingle j b')) ↔ i ≠ j

Full source

@[to_additive]
theorem mulSupport_mulSingle_disjoint {b' : B} (hb : b ≠ 1) (hb' : b' ≠ 1) {i j : A} :
    DisjointDisjoint (mulSupport (mulSingle i b)) (mulSupport (mulSingle j b')) ↔ i ≠ j := by
  rw [mulSupport_mulSingle_of_ne hb, mulSupport_mulSingle_of_ne hb', disjoint_singleton]

Disjointness of Multiplicative Supports of Point Functions: $\mathrm{mulSupport}(\text{mulSingle } i b) \cap \mathrm{mulSupport}(\text{mulSingle } j b') = \emptyset \leftrightarrow i \neq j$

Informal description

For any elements $b, b' \in B$ with $b \neq 1$ and $b' \neq 1$, and for any $i, j \in A$, the multiplicative supports of the functions $\text{mulSingle } i b$ and $\text{mulSingle } j b'$ are disjoint if and only if $i \neq j$. In other words: \[ \mathrm{mulSupport}(\text{mulSingle } i b) \cap \mathrm{mulSupport}(\text{mulSingle } j b') = \emptyset \leftrightarrow i \neq j. \]