Injective relabeling as extension by zero

For an injective index map, pushing forward a finitely supported function is ordinary function extension by zero, over any additive commutative monoid.

Pushing forward along a strictly monotone map of linearly ordered indices preserves and reflects the strict and non-strict lexicographic orders, since the relabeled functions vanish off the image and the order relabels the positions where they first differ.

theorem Finsupp.coe_mapDomain_eq_extend {α : Type u_1} {β : Type u_2} {M : Type u_3} [AddCommMonoid M] {e : α → β} (he : Function.Injective e) (x : α →₀ M) : ⇑(mapDomain e x) = Function.extend e (⇑x) 0

Pushing a finitely supported function along an injection extends its values by zero outside the image.

theorem Finsupp.mapDomain_subtypeDomain_subtype {α : Type u_1} {M : Type u_2} [AddCommMonoid M] {s : Set α} {f : α →₀ M} (hf : ↑f.support ⊆ s) : mapDomain Subtype.val (subtypeDomain (fun (x : α) => x ∈ s) f) = f

A finitely supported function supported on a set s is the push-forward along the inclusion of its restriction to s.

theorem Finsupp.toLex_mapDomain_lt_toLex_mapDomain_iff {α : Type u_1} {β : Type u_2} {M : Type u_3} [LinearOrder α] [Preorder β] [AddCommMonoid M] [Preorder M] {f : α → β} (hf : StrictMono f) {x y : α →₀ M} : toLex (mapDomain f x) < toLex (mapDomain f y) ↔ toLex x < toLex y

Pushing forward along a strictly monotone map of indices preserves and reflects the strict lexicographic order: the first position at which two relabeled functions differ is the image of the first position at which the original functions differ.

theorem Finsupp.toLex_mapDomain_le_toLex_mapDomain_iff {α : Type u_1} {β : Type u_2} {M : Type u_3} [LinearOrder α] [LinearOrder β] [AddCommMonoid M] [PartialOrder M] {f : α → β} (hf : StrictMono f) {x y : α →₀ M} : toLex (mapDomain f x) ≤ toLex (mapDomain f y) ↔ toLex x ≤ toLex y

Pushing forward along a strictly monotone map of linearly ordered indices preserves and reflects the lexicographic order.