Skip to content

Commit c9524b6

Browse files
casavacacasavaca
committed
feat: Port Data.Dfinsupp.NeLocus (#1937)
1 parent 1246b7b commit c9524b6

File tree

2 files changed

+186
-0
lines changed

2 files changed

+186
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -266,6 +266,7 @@ import Mathlib.Data.Countable.Defs
266266
import Mathlib.Data.Countable.Small
267267
import Mathlib.Data.DList.Basic
268268
import Mathlib.Data.Dfinsupp.Basic
269+
import Mathlib.Data.Dfinsupp.NeLocus
269270
import Mathlib.Data.ENat.Basic
270271
import Mathlib.Data.ENat.Lattice
271272
import Mathlib.Data.Equiv.Functor

‎Mathlib/Data/Dfinsupp/NeLocus.lean‎

Lines changed: 185 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,185 @@
1+
/-
2+
Copyright (c) 2022 Junyan Xu. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Damiano Testa, Junyan Xu
5+
6+
! This file was ported from Lean 3 source module data.dfinsupp.ne_locus
7+
! leanprover-community/mathlib commit f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.Data.Dfinsupp.Basic
12+
13+
/-!
14+
# Locus of unequal values of finitely supported dependent functions
15+
16+
Let `N : α → Type*` be a type family, assume that `N a` has a `0` for all `a : α` and let
17+
`f g : Π₀ a, N a` be finitely supported dependent functions.
18+
19+
## Main definition
20+
21+
* `Dfinsupp.neLocus f g : finset α`, the finite subset of `α` where `f` and `g` differ.
22+
In the case in which `N a` is an additive group for all `a`, `Dfinsupp.neLocus f g` coincides with
23+
`Dfinsupp.support (f - g)`.
24+
-/
25+
26+
27+
variable {α : Type _} {N : α → Type _}
28+
29+
namespace Dfinsupp
30+
31+
variable [DecidableEq α]
32+
33+
section NHasZero
34+
35+
variable [∀ a, DecidableEq (N a)] [∀ a, Zero (N a)] (f g : Π₀ a, N a)
36+
37+
/-- Given two finitely supported functions `f g : α →₀ N`, `Finsupp.neLocus f g` is the `Finset`
38+
where `f` and `g` differ. This generalizes `(f - g).support` to situations without subtraction. -/
39+
def neLocus (f g : Π₀ a, N a) : Finset α :=
40+
(f.support ∪ g.support).filter fun x ↦ f x ≠ g x
41+
#align dfinsupp.ne_locus Dfinsupp.neLocus
42+
43+
@[simp]
44+
theorem mem_neLocus {f g : Π₀ a, N a} {a : α} : a ∈ f.neLocus g ↔ f a ≠ g a := by
45+
simpa only [neLocus, Finset.mem_filter, Finset.mem_union, mem_support_iff,
46+
and_iff_right_iff_imp] using Ne.ne_or_ne _
47+
#align dfinsupp.mem_ne_locus Dfinsupp.mem_neLocus
48+
49+
theorem not_mem_neLocus {f g : Π₀ a, N a} {a : α} : a ∉ f.neLocus g ↔ f a = g a :=
50+
mem_neLocus.not.trans not_ne_iff
51+
#align dfinsupp.not_mem_ne_locus Dfinsupp.not_mem_neLocus
52+
53+
@[simp]
54+
theorem coe_neLocus : ↑(f.neLocus g) = { x | f x ≠ g x } :=
55+
Set.ext fun _x ↦ mem_neLocus
56+
#align dfinsupp.coe_ne_locus Dfinsupp.coe_neLocus
57+
58+
@[simp]
59+
theorem neLocus_eq_empty {f g : Π₀ a, N a} : f.neLocus g = ∅ ↔ f = g :=
60+
⟨fun h ↦
61+
ext fun a ↦ not_not.mp (mem_neLocus.not.mp (Finset.eq_empty_iff_forall_not_mem.mp h a)),
62+
fun h ↦ h ▸ by simp only [neLocus, Ne.def, eq_self_iff_true, not_true, Finset.filter_False]⟩
63+
#align dfinsupp.ne_locus_eq_empty Dfinsupp.neLocus_eq_empty
64+
65+
@[simp]
66+
theorem nonempty_neLocus_iff {f g : Π₀ a, N a} : (f.neLocus g).Nonempty ↔ f ≠ g :=
67+
Finset.nonempty_iff_ne_empty.trans neLocus_eq_empty.not
68+
#align dfinsupp.nonempty_ne_locus_iff Dfinsupp.nonempty_neLocus_iff
69+
70+
theorem neLocus_comm : f.neLocus g = g.neLocus f := by
71+
simp_rw [neLocus, Finset.union_comm, ne_comm]
72+
#align dfinsupp.ne_locus_comm Dfinsupp.neLocus_comm
73+
74+
@[simp]
75+
theorem neLocus_zero_right : f.neLocus 0 = f.support := by
76+
ext
77+
rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]
78+
#align dfinsupp.ne_locus_zero_right Dfinsupp.neLocus_zero_right
79+
80+
@[simp]
81+
theorem neLocus_zero_left : (0 : Π₀ a, N a).neLocus f = f.support :=
82+
(neLocus_comm _ _).trans (neLocus_zero_right _)
83+
#align dfinsupp.ne_locus_zero_left Dfinsupp.neLocus_zero_left
84+
85+
end NHasZero
86+
87+
section NeLocusAndMaps
88+
89+
variable {M P : α → Type _} [∀ a, Zero (N a)] [∀ a, Zero (M a)] [∀ a, Zero (P a)]
90+
91+
theorem subset_mapRange_neLocus [∀ a, DecidableEq (N a)] [∀ a, DecidableEq (M a)] (f g : Π₀ a, N a)
92+
{F : ∀ a, N a → M a} (F0 : ∀ a, F a 0 = 0) :
93+
(f.mapRange F F0).neLocus (g.mapRange F F0) ⊆ f.neLocus g := fun a ↦ by
94+
simpa only [mem_neLocus, mapRange_apply, not_imp_not] using congr_arg (F a)
95+
#align dfinsupp.subset_map_range_ne_locus Dfinsupp.subset_mapRange_neLocus
96+
97+
theorem zipWith_neLocus_eq_left [∀ a, DecidableEq (N a)] [∀ a, DecidableEq (P a)]
98+
{F : ∀ a, M a → N a → P a} (F0 : ∀ a, F a 0 0 = 0) (f : Π₀ a, M a) (g₁ g₂ : Π₀ a, N a)
99+
(hF : ∀ a f, Function.Injective fun g ↦ F a f g) :
100+
(zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) = g₁.neLocus g₂ := by
101+
ext a
102+
simpa only [mem_neLocus] using (hF a _).ne_iff
103+
#align dfinsupp.zip_with_ne_locus_eq_left Dfinsupp.zipWith_neLocus_eq_left
104+
105+
theorem zipWith_neLocus_eq_right [∀ a, DecidableEq (M a)] [∀ a, DecidableEq (P a)]
106+
{F : ∀ a, M a → N a → P a} (F0 : ∀ a, F a 0 0 = 0) (f₁ f₂ : Π₀ a, M a) (g : Π₀ a, N a)
107+
(hF : ∀ a g, Function.Injective fun f ↦ F a f g) :
108+
(zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) = f₁.neLocus f₂ := by
109+
ext a
110+
simpa only [mem_neLocus] using (hF a _).ne_iff
111+
#align dfinsupp.zip_with_ne_locus_eq_right Dfinsupp.zipWith_neLocus_eq_right
112+
113+
theorem mapRange_neLocus_eq [∀ a, DecidableEq (N a)] [∀ a, DecidableEq (M a)] (f g : Π₀ a, N a)
114+
{F : ∀ a, N a → M a} (F0 : ∀ a, F a 0 = 0) (hF : ∀ a, Function.Injective (F a)) :
115+
(f.mapRange F F0).neLocus (g.mapRange F F0) = f.neLocus g := by
116+
ext a
117+
simpa only [mem_neLocus] using (hF a).ne_iff
118+
#align dfinsupp.map_range_ne_locus_eq Dfinsupp.mapRange_neLocus_eq
119+
120+
end NeLocusAndMaps
121+
122+
variable [∀ a, DecidableEq (N a)]
123+
124+
@[simp]
125+
theorem neLocus_add_left [∀ a, AddLeftCancelMonoid (N a)] (f g h : Π₀ a, N a) :
126+
(f + g).neLocus (f + h) = g.neLocus h :=
127+
zipWith_neLocus_eq_left _ _ _ _ fun _a ↦ add_right_injective
128+
#align dfinsupp.ne_locus_add_left Dfinsupp.neLocus_add_left
129+
130+
@[simp]
131+
theorem neLocus_add_right [∀ a, AddRightCancelMonoid (N a)] (f g h : Π₀ a, N a) :
132+
(f + h).neLocus (g + h) = f.neLocus g :=
133+
zipWith_neLocus_eq_right _ _ _ _ fun _a ↦ add_left_injective
134+
#align dfinsupp.ne_locus_add_right Dfinsupp.neLocus_add_right
135+
136+
section AddGroup
137+
138+
variable [∀ a, AddGroup (N a)] (f f₁ f₂ g g₁ g₂ : Π₀ a, N a)
139+
140+
@[simp]
141+
theorem neLocus_neg_neg : neLocus (-f) (-g) = f.neLocus g :=
142+
mapRange_neLocus_eq _ _ (fun _a ↦ neg_zero) fun _a ↦ neg_injective
143+
#align dfinsupp.ne_locus_neg_neg Dfinsupp.neLocus_neg_neg
144+
145+
theorem neLocus_neg : neLocus (-f) g = f.neLocus (-g) := by rw [← neLocus_neg_neg, neg_neg]
146+
#align dfinsupp.ne_locus_neg Dfinsupp.neLocus_neg
147+
148+
theorem neLocus_eq_support_sub : f.neLocus g = (f - g).support := by
149+
rw [← @neLocus_add_right α N _ _ _ _ _ (-g), add_right_neg, neLocus_zero_right, sub_eq_add_neg]
150+
#align dfinsupp.ne_locus_eq_support_sub Dfinsupp.neLocus_eq_support_sub
151+
152+
@[simp]
153+
theorem neLocus_sub_left : neLocus (f - g₁) (f - g₂) = neLocus g₁ g₂ := by
154+
simp only [sub_eq_add_neg, @neLocus_add_left α N _ _ _, neLocus_neg_neg]
155+
#align dfinsupp.ne_locus_sub_left Dfinsupp.neLocus_sub_left
156+
157+
@[simp]
158+
theorem neLocus_sub_right : neLocus (f₁ - g) (f₂ - g) = neLocus f₁ f₂ := by
159+
simpa only [sub_eq_add_neg] using @neLocus_add_right α N _ _ _ _ _ _
160+
#align dfinsupp.ne_locus_sub_right Dfinsupp.neLocus_sub_right
161+
162+
@[simp]
163+
theorem neLocus_self_add_right : neLocus f (f + g) = g.support := by
164+
rw [← neLocus_zero_left, ← @neLocus_add_left α N _ _ _ f 0 g, add_zero]
165+
#align dfinsupp.ne_locus_self_add_right Dfinsupp.neLocus_self_add_right
166+
167+
@[simp]
168+
theorem neLocus_self_add_left : neLocus (f + g) f = g.support := by
169+
rw [neLocus_comm, neLocus_self_add_right]
170+
#align dfinsupp.ne_locus_self_add_left Dfinsupp.neLocus_self_add_left
171+
172+
@[simp]
173+
theorem neLocus_self_sub_right : neLocus f (f - g) = g.support := by
174+
rw [sub_eq_add_neg, neLocus_self_add_right, support_neg]
175+
#align dfinsupp.ne_locus_self_sub_right Dfinsupp.neLocus_self_sub_right
176+
177+
@[simp]
178+
theorem neLocus_self_sub_left : neLocus (f - g) f = g.support := by
179+
rw [neLocus_comm, neLocus_self_sub_right]
180+
#align dfinsupp.ne_locus_self_sub_left Dfinsupp.neLocus_self_sub_left
181+
182+
end AddGroup
183+
184+
end Dfinsupp
185+

0 commit comments

Comments
 (0)