Documentation

Linglib.Core.Data.Fin.Tuple.Basic

Fin.appendMap: Fin.append as a bifunctor on index maps #

[UPSTREAM] candidate for Mathlib/Data/Fin/Tuple/Basic.lean. Mathlib has Fin.append (the action of + on tuples) and its naturality only for Fin.cast maps; it lacks the action of + on arbitrary index maps. Fin.appendMap f g routes a Fin (m + n) index through f on the left block and g on the right, and is functorial (appendMap_id/appendMap_comp) with Fin.append natural in it (append_comp_appendMap).

source
def Fin.appendMap {m m' n n' : ℕ} (f : Fin m → Fin m') (g : Fin n → Fin n') :
Fin (m + n) → Fin (m' + n')

The action of + on index maps: f on the left block, g on the right.

Equations
  • Fin.appendMap f g = ⇑finSumFinEquiv ∘ Sum.map f g ∘ ⇑finSumFinEquiv.symm
Instances For
    source
    @[simp]
    theorem Fin.appendMap_castAdd {m m' n n' : ℕ} (f : Fin m → Fin m') (g : Fin n → Fin n') (i : Fin m) :
    appendMap f g (castAdd n i) = castAdd n' (f i)
    source
    @[simp]
    theorem Fin.appendMap_natAdd {m m' n n' : ℕ} (f : Fin m → Fin m') (g : Fin n → Fin n') (j : Fin n) :
    appendMap f g (natAdd m j) = natAdd m' (g j)
    source
    theorem Fin.appendMap_val {m m' n n' : ℕ} (f : Fin m → Fin m') (g : Fin n → Fin n') (k : Fin (m + n)) :
    ↑(appendMap f g k) = if h : ↑k < m then ↑(f ⟨↑k, h⟩) else ↑(g ⟨↑k - m, ⋯⟩) + m'

    Value characterisation: left-block indices route through f, right-block (shifted) through g.

    source
    theorem Fin.append_val {m n p : ℕ} (u : Fin m → Fin p) (v : Fin n → Fin p) (k : Fin (m + n)) :
    ↑(append u v k) = if h : ↑k < m then ↑(u ⟨↑k, h⟩) else ↑(v ⟨↑k - m, ⋯⟩)

    Value of a common-codomain Fin.append (the copairing Fin (m + n) → Fin p) at a raw index: left-block indices route through u, right-block (shifted) through v. The copairing analogue of appendMap_val.

    source
    @[simp]
    theorem Fin.appendMap_id {m n : ℕ} :
    appendMap id id = id
    source
    theorem Fin.appendMap_comp {m m' m'' n n' n'' : ℕ} (f : Fin m → Fin m') (f' : Fin m' → Fin m'') (g : Fin n → Fin n') (g' : Fin n' → Fin n'') :
    appendMap (f' ∘ f) (g' ∘ g) = appendMap f' g' ∘ appendMap f g
    source
    theorem Fin.append_comp_appendMap {m m' n n' : ℕ} {α : Type u_1} {a : Fin m → α} {a' : Fin m' → α} {b : Fin n → α} {b' : Fin n' → α} {f : Fin m → Fin m'} {g : Fin n → Fin n'} (hf : a' ∘ f = a) (hg : b' ∘ g = b) :
    append a' b' ∘ appendMap f g = append a b

    Fin.append is natural in its index maps: a block-routing map intertwines the two appended tuples. The label-preservation core for concatenation.