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). On permutations it is Fin.permAdd σ τ, a permutation of Fin (m + n).

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.

    source
    def Fin.permAdd {m n : ℕ} (σ : Equiv.Perm (Fin m)) (τ : Equiv.Perm (Fin n)) :
    Equiv.Perm (Fin (m + n))

    appendMap of two permutations, as a permutation.

    Equations
    • Fin.permAdd σ τ = finSumFinEquiv.permCongr (σ.sumCongr τ)
    Instances For
      source
      @[simp]
      theorem Fin.coe_permAdd {m n : ℕ} (σ : Equiv.Perm (Fin m)) (τ : Equiv.Perm (Fin n)) :
      ⇑(permAdd σ τ) = appendMap ⇑σ ⇑τ
      source
      theorem Fin.append_comp_permAdd {m n : ℕ} {α : Type u_1} (a : Fin m → α) (b : Fin n → α) (σ : Equiv.Perm (Fin m)) (τ : Equiv.Perm (Fin n)) :
      append a b ∘ ⇑(permAdd σ τ) = append (a ∘ ⇑σ) (b ∘ ⇑τ)