Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.Relativity.Tensors.ComponentIdx.Single
public import Physlib.Relativity.Tensors.Contraction.SuccSuccAbove
public import Mathlib.Topology.Algebra.Module.ModuleTopology
public import Mathlib.Analysis.RCLike.Basic
public import Mathlib.Tactic.Cases
public import Mathlib.GroupTheory.Perm.FinReindexing of tensor components
In this file we give results related to the reindexing of tensors.
If a tensor has indices specified by a list of colors c : Fin n → C, then reindexing the
tensor corresponds to a bijection σ : Fin m → Fin n such that c ∘ σ = c1 for some other
list of colors c1 : Fin m → C. A reindexing might take a tensor ψⁱⱼ to a tensor ψʲᵢ
by reordering the indices, or it might take a tensor ψⁱⱼᵏ to a tensor ψⁱᵏ.
We are interested in the interaction of reindexing with the following operations on tensors:
Fin.append corresponds to the product of tensors.
Fin.succAbove corresponds to the evaluation of a tensor at a given index.
Fin.succSuccAbove corresponds to the contraction of a tensor at two given indices.
@[expose] public sectionIndex maps
The finite index maps out of which the reindexings below are built: Fin.append for products and
Fin.succAbove for a deleted slot. The lemmas on Fin.succSuccAbove, for a deleted pair, are in
Physlib.Relativity.Tensors.Contraction.SuccSuccAbove.
Splitting Fin (m + n) into its two blocks and reassembling them is the identity.
lemma append_castAdd_natAdd_eq_id {m n : ℕ} :
Fin.append (Fin.castAdd n) (Fin.natAdd m) = (id : Fin (m + n) → Fin (m + n)) := m:ℕn:ℕ⊢ append (castAdd n) (natAdd m) = id
All goals completed! 🐙
Moving slot i to the end is the cycle [i, last]: the block map that lists the
i.succAbove survivors in order and then i is Fin.cycleIcc i (Fin.last n).
All goals completed! 🐙
Given two lists of indices c : Fin n → C and c1 : Fin m → C a map
σ : Fin m → Fin n satisfies the condition IsReindexing c c1 σ if it is:
A bijection
Forms a commutative triangle with c and c1.
def IsReindexing {n m : ℕ} (c : Fin n → C) (c1 : Fin m → C)
(σ : Fin m → Fin n) : Prop :=
Function.Bijective σ ∧ ∀ i, c (σ i) = c1 iProperties of the underlying function
lemma injective {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C}
{σ : Fin m → Fin n} (h : IsReindexing c c1 σ) : Function.Injective σ := h.1.1lemma surjective {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C}
{σ : Fin m → Fin n} (h : IsReindexing c c1 σ) : Function.Surjective σ := h.1.2lemma auto {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C}
{σ : Fin m → Fin n} (h : IsReindexing c c1 σ := by {simp [IsReindexing]; try decide}) :
IsReindexing c c1 σ := h@[simp]
lemma on_id {n : ℕ} {c c1 : Fin n → C} :
IsReindexing c c1 (id : Fin n → Fin n) ↔ ∀ i, c i = c1 i := C:Typen:ℕc:Fin n → Cc1:Fin n → C⊢ IsReindexing c c1 id ↔ ∀ (i : Fin n), c i = c1 i
All goals completed! 🐙lemma on_id_symm {n : ℕ} {c c1 : Fin n → C} (h : IsReindexing c1 c id) :
IsReindexing c c1 (id : Fin n → Fin n) := C:Typen:ℕc:Fin n → Cc1:Fin n → Ch:IsReindexing c1 c id⊢ IsReindexing c c1 id
C:Typen:ℕc:Fin n → Cc1:Fin n → Ch:∀ (i : Fin n), c1 i = c i⊢ ∀ (i : Fin n), c i = c1 i
All goals completed! 🐙
For a map σ satisfying IsReindexing c c1 σ, the inverse of that map.
def inv {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C}
(σ : Fin m → Fin n) (h : IsReindexing c c1 σ) : Fin n → Fin m :=
Fintype.bijInv h.1
For a map σ : Fin m → Fin n satisfying IsReindexing c c1 σ,
that map lifted to an equivalence between
Fin n and Fin m.
def toEquiv {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C}
{σ : Fin m → Fin n} (h : IsReindexing c c1 σ) :
Fin n ≃ Fin m where
toFun := inv σ h
invFun := σ
left_inv := Fintype.rightInverse_bijInv h.1
right_inv := Fintype.leftInverse_bijInv h.1lemma apply_inv_apply {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C}
(σ : Fin m → Fin n) (h : IsReindexing c c1 σ) (x : Fin m) :
h.inv σ (σ x) = x := C:Typen:ℕm:ℕc:Fin n → Cc1:Fin m → Cσ:Fin m → Fin nh:IsReindexing c c1 σx:Fin m⊢ inv σ h (σ x) = x
C:Typen:ℕm:ℕc:Fin n → Cc1:Fin m → Cσ:Fin m → Fin nh:IsReindexing c c1 σx:Fin m⊢ h.toEquiv (h.toEquiv.symm x) = x
All goals completed! 🐙lemma inv_apply_apply {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C}
(σ : Fin m → Fin n) (h : IsReindexing c c1 σ) (x : Fin n) :
σ (h.inv σ x) = x := C:Typen:ℕm:ℕc:Fin n → Cc1:Fin m → Cσ:Fin m → Fin nh:IsReindexing c c1 σx:Fin n⊢ σ (inv σ h x) = x
C:Typen:ℕm:ℕc:Fin n → Cc1:Fin m → Cσ:Fin m → Fin nh:IsReindexing c c1 σx:Fin n⊢ h.toEquiv.symm (h.toEquiv x) = x
All goals completed! 🐙All goals completed! 🐙C:Typen:ℕm:ℕc:Fin n → Cc1:Fin m → Cσ:Fin m → Fin nh:IsReindexing c c1 σx:Fin m⊢ (c ∘ σ) x = c (h.toEquiv.symm x)
All goals completed! 🐙C:Typen:ℕm:ℕc:Fin n → Cc1:Fin m → Cσ:Fin m → Fin nh:IsReindexing c c1 σx:Fin n⊢ c (h.toEquiv.symm (h.toEquiv x)) = (c ∘ σ) (h.toEquiv x)
All goals completed! 🐙Constructors
lemma swap {n : ℕ} {c : Fin n → C} (i j : Fin n) :
IsReindexing c (c ∘ Equiv.swap i j) (Equiv.swap i j) := C:Typen:ℕc:Fin n → Ci:Fin nj:Fin n⊢ IsReindexing c (c ∘ ⇑(Equiv.swap i j)) ⇑(Equiv.swap i j)
All goals completed! 🐙
The inverse of a map satisfying IsReindexing c c1 σ is a reindexing of c1 by c.
lemma symm {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C}
{σ : Fin m → Fin n} (h : IsReindexing c c1 σ) : IsReindexing c1 c (h.inv σ) :=
⟨h.toEquiv.bijective, h.inv_perserve_color⟩lemma symm_of_id {n : ℕ} {c c1 : Fin n → C} (h : IsReindexing c c1 id) :
IsReindexing c1 c id := C:Typen:ℕc:Fin n → Cc1:Fin n → Ch:IsReindexing c c1 id⊢ IsReindexing c1 c id
C:Typen:ℕc:Fin n → Cc1:Fin n → Ch:∀ (i : Fin n), c i = c1 i⊢ ∀ (i : Fin n), c1 i = c i
All goals completed! 🐙
The composition of two maps satisfying IsReindexing also satisfies the IsReindexing.
lemma comp {n n1 n2 : ℕ} {c : Fin n → C} {c1 : Fin n1 → C}
{c2 : Fin n2 → C} {σ : Fin n1 → Fin n} {σ2 : Fin n2 → Fin n1}
(h : IsReindexing c c1 σ) (h2 : IsReindexing c1 c2 σ2) : IsReindexing c c2 (σ ∘ σ2) :=
⟨h.1.comp h2.1, fun x => (h.2 (σ2 x)).trans (h2.2 x)⟩C:Typen:ℕn':ℕn2:ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nc2:Fin n2 → Ch:IsReindexing c c' σheq:append (castAdd n2 ∘ σ) (natAdd n) =
⇑(finSumFinEquiv.symm.trans (((Equiv.ofBijective σ ⋯).sumCongr (Equiv.refl (Fin n2))).trans finSumFinEquiv))⊢ Function.Bijective
⇑(finSumFinEquiv.symm.trans (((Equiv.ofBijective σ ⋯).sumCongr (Equiv.refl (Fin n2))).trans finSumFinEquiv))
All goals completed! 🐙
C:Typen:ℕn':ℕn2:ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nc2:Fin n2 → Ch:IsReindexing c c' σi:Fin (n' + n2)⊢ append c c2 (append (castAdd n2 ∘ σ) (natAdd n) i) = append c' c2 i C:Typen:ℕn':ℕn2:ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nc2:Fin n2 → Ch:IsReindexing c c' σi:Fin (n' + n2)a:Fin n'⊢ append c c2 (append (castAdd n2 ∘ σ) (natAdd n) (castAdd n2 a)) = append c' c2 (castAdd n2 a)C:Typen:ℕn':ℕn2:ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nc2:Fin n2 → Ch:IsReindexing c c' σi:Fin (n' + n2)a:Fin n2⊢ append c c2 (append (castAdd n2 ∘ σ) (natAdd n) (natAdd n' a)) = append c' c2 (natAdd n' a) C:Typen:ℕn':ℕn2:ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nc2:Fin n2 → Ch:IsReindexing c c' σi:Fin (n' + n2)a:Fin n'⊢ append c c2 (append (castAdd n2 ∘ σ) (natAdd n) (castAdd n2 a)) = append c' c2 (castAdd n2 a)C:Typen:ℕn':ℕn2:ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nc2:Fin n2 → Ch:IsReindexing c c' σi:Fin (n' + n2)a:Fin n2⊢ append c c2 (append (castAdd n2 ∘ σ) (natAdd n) (natAdd n' a)) = append c' c2 (natAdd n' a)
All goals completed! 🐙C:Typen:ℕn':ℕn2:ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nc2:Fin n2 → Ch:IsReindexing c c' σheq:append (castAdd n) (natAdd n2 ∘ σ) =
⇑(finSumFinEquiv.symm.trans (((Equiv.refl (Fin n2)).sumCongr (Equiv.ofBijective σ ⋯)).trans finSumFinEquiv))⊢ Function.Bijective
⇑(finSumFinEquiv.symm.trans (((Equiv.refl (Fin n2)).sumCongr (Equiv.ofBijective σ ⋯)).trans finSumFinEquiv))
All goals completed! 🐙
C:Typen:ℕn':ℕn2:ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nc2:Fin n2 → Ch:IsReindexing c c' σi:Fin (n2 + n')⊢ append c2 c (append (castAdd n) (natAdd n2 ∘ σ) i) = append c2 c' i C:Typen:ℕn':ℕn2:ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nc2:Fin n2 → Ch:IsReindexing c c' σi:Fin (n2 + n')a:Fin n2⊢ append c2 c (append (castAdd n) (natAdd n2 ∘ σ) (castAdd n' a)) = append c2 c' (castAdd n' a)C:Typen:ℕn':ℕn2:ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nc2:Fin n2 → Ch:IsReindexing c c' σi:Fin (n2 + n')a:Fin n'⊢ append c2 c (append (castAdd n) (natAdd n2 ∘ σ) (natAdd n2 a)) = append c2 c' (natAdd n2 a) C:Typen:ℕn':ℕn2:ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nc2:Fin n2 → Ch:IsReindexing c c' σi:Fin (n2 + n')a:Fin n2⊢ append c2 c (append (castAdd n) (natAdd n2 ∘ σ) (castAdd n' a)) = append c2 c' (castAdd n' a)C:Typen:ℕn':ℕn2:ℕc:Fin n → Cc':Fin n' → Cσ:Fin n' → Fin nc2:Fin n2 → Ch:IsReindexing c c' σi:Fin (n2 + n')a:Fin n'⊢ append c2 c (append (castAdd n) (natAdd n2 ∘ σ) (natAdd n2 a)) = append c2 c' (natAdd n2 a)
All goals completed! 🐙C:Typen:ℕc:Fin n → Cc1:Fin 0 → CP:∀ (i : Fin (n + 0)), c i = append c c1 i⊢ ∀ (i : Fin n), c i = append c c1 i
All goals completed! 🐙C:Typen:ℕn2:ℕc:Fin n → Cc2:Fin n2 → Cheq:append (natAdd n) (castAdd n2) = ⇑(finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin n2) (Fin n)).trans finSumFinEquiv))⊢ Function.Bijective ⇑(finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin n2) (Fin n)).trans finSumFinEquiv))
All goals completed! 🐙
C:Typen:ℕn2:ℕc:Fin n → Cc2:Fin n2 → Ci:Fin (n2 + n)⊢ append c c2 (append (natAdd n) (castAdd n2) i) = append c2 c i C:Typen:ℕn2:ℕc:Fin n → Cc2:Fin n2 → Ci:Fin (n2 + n)a:Fin n2⊢ append c c2 (append (natAdd n) (castAdd n2) (castAdd n a)) = append c2 c (castAdd n a)C:Typen:ℕn2:ℕc:Fin n → Cc2:Fin n2 → Ci:Fin (n2 + n)a:Fin n⊢ append c c2 (append (natAdd n) (castAdd n2) (natAdd n2 a)) = append c2 c (natAdd n2 a) C:Typen:ℕn2:ℕc:Fin n → Cc2:Fin n2 → Ci:Fin (n2 + n)a:Fin n2⊢ append c c2 (append (natAdd n) (castAdd n2) (castAdd n a)) = append c2 c (castAdd n a)C:Typen:ℕn2:ℕc:Fin n → Cc2:Fin n2 → Ci:Fin (n2 + n)a:Fin n⊢ append c c2 (append (natAdd n) (castAdd n2) (natAdd n2 a)) = append c2 c (natAdd n2 a)
All goals completed! 🐙lemma append_assoc_right {n1 n2 n3 : ℕ} {c : Fin n1 → C} {c2 : Fin n2 → C} {c3 : Fin n3 → C} :
IsReindexing (Fin.append c (Fin.append c2 c3)) (Fin.append (Fin.append c c2) c3)
(Fin.cast (k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕn3:ℕc:Fin n1 → Cc2:Fin n2 → Cc3:Fin n3 → C⊢ n1 + n2 + n3 = n1 + (n2 + n3) All goals completed! 🐙)) :=
⟨(finCongr (C:Typen1:ℕn2:ℕn3:ℕc:Fin n1 → Cc2:Fin n2 → Cc3:Fin n3 → C⊢ n1 + n2 + n3 = n1 + (n2 + n3) All goals completed! 🐙)).bijective, fun i => (congrFun (Fin.append_assoc c c2 c3) i).symm⟩lemma append_assoc_left {n1 n2 n3 : ℕ} {c : Fin n1 → C} {c2 : Fin n2 → C} {c3 : Fin n3 → C} :
IsReindexing (Fin.append (Fin.append c c2) c3) (Fin.append c (Fin.append c2 c3))
(Fin.cast (k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn1:ℕn2:ℕn3:ℕc:Fin n1 → Cc2:Fin n2 → Cc3:Fin n3 → C⊢ n1 + (n2 + n3) = n1 + n2 + n3 All goals completed! 🐙)) :=
⟨(finCongr (C:Typen1:ℕn2:ℕn3:ℕc:Fin n1 → Cc2:Fin n2 → Cc3:Fin n3 → C⊢ n1 + (n2 + n3) = n1 + n2 + n3 All goals completed! 🐙)).bijective, fun i => congrFun (Fin.append_assoc c c2 c3) _⟩C:Typen:ℕn1:ℕc:Fin n → Cc1:Fin (n1 + 1) → Ci:Fin (n1 + 1)x:Fin (n + n1)a:Fin n1hidx:(natAdd n i).succAbove (natAdd n a) = natAdd n (i.succAbove a)⊢ append c c1 ((natAdd n i).succAbove (natAdd n a)) = append c (c1 ∘ i.succAbove) (natAdd n a)
All goals completed! 🐙C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Ci:Fin (n + 1)y:Fin (n + (n1 + 1))a:Fin (n1 + 1)hidx:(castAdd (n1 + 1) i).succAbove (Fin.cast ⋯ (natAdd n a)) = natAdd (n + 1) a⊢ append c c1 ((castAdd (n1 + 1) i).succAbove (Fin.cast ⋯ (natAdd n a))) = append (c ∘ i.succAbove) c1 (natAdd n a)
All goals completed! 🐙
Removing two entries from the right component of Fin.append c1 c commutes with the
append: removing the i-th and j-th entries of c and then appending c1 matches
removing the corresponding entries of Fin.append c1 c, via the identity permutation.
This is used for the commutation of taking a product of tensors
with contraction of indices.
lemma append_succSuccAbove_natAdd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
{c1 : Fin n1 → C} (i j : Fin (n + 1 + 1)) :
IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
(Fin.append c1 (c ∘ i.succSuccAbove j)) id := C:Typen:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)⊢ IsReindexing (append c1 c ∘ (natAdd n1 i).succSuccAbove (natAdd n1 j)) (append c1 (c ∘ i.succSuccAbove j)) id
C:Typen:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)⊢ ∀ (i_1 : Fin (n1 + n)),
(append c1 c ∘ (natAdd n1 i).succSuccAbove (natAdd n1 j)) (id i_1) = append c1 (c ∘ i.succSuccAbove j) i_1
All goals completed! 🐙
Given a reindexing of c by c1 via σ for which the index i is sent to 0,
removing the i-th entry of c1 and the first entry of c yields a reindexing of
c ∘ Fin.succ by c1 ∘ i.succAbove via the map sending j to the predecessor of
σ (i.succAbove j).
C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σhi:σ i = 0k:Fin n⊢ ∃ a, σ (i.succAbove a) = k.succ
C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σhi:σ i = 0k:Fin nj:Fin (n1 + 1)hj:σ j = k.succ⊢ ∃ a, σ (i.succAbove a) = k.succ
C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σhi:σ i = 0k:Fin nj:Fin (n1 + 1)hj:σ j = k.succ⊢ ¬j = i
All goals completed! 🐙
C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σhi:σ i = 0⊢ ∀ (i_1 : Fin n1), (c ∘ succ) ((fun j => (σ (i.succAbove j)).pred ⋯) i_1) = (c1 ∘ i.succAbove) i_1 C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σhi:σ i = 0x:Fin n1⊢ (c ∘ succ) ((fun j => (σ (i.succAbove j)).pred ⋯) x) = (c1 ∘ i.succAbove) x
All goals completed! 🐙
Given a reindexing of c by c1 via σ for which the index i is not sent to 0,
removing the i-th entry of c1 and the (σ i)-th entry of c yields a reindexing of
c ∘ (σ i).succAbove by c1 ∘ i.succAbove via the map
(σ i).pred.predAbove ∘ σ ∘ i.succAbove.
C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σhi:σ i ≠ 0hpr:σ i = ((σ i).pred hi).succhne:∀ (x : Fin n1), σ (i.succAbove x) ≠ σ ik:Fin n⊢ ∃ a, σ (i.succAbove a) = (σ i).succAbove k
C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σhi:σ i ≠ 0hpr:σ i = ((σ i).pred hi).succhne:∀ (x : Fin n1), σ (i.succAbove x) ≠ σ ik:Fin nj:Fin (n1 + 1)hj:σ j = (σ i).succAbove k⊢ ∃ a, σ (i.succAbove a) = (σ i).succAbove k
C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σhi:σ i ≠ 0hpr:σ i = ((σ i).pred hi).succhne:∀ (x : Fin n1), σ (i.succAbove x) ≠ σ ik:Fin nj:Fin (n1 + 1)hj:σ j = (σ i).succAbove k⊢ ¬j = i
C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)h:IsReindexing c c1 σk:Fin nj:Fin (n1 + 1)hi:σ j ≠ 0hpr:σ j = ((σ j).pred hi).succhne:∀ (x : Fin n1), σ (j.succAbove x) ≠ σ jhj:σ j = (σ j).succAbove k⊢ False
All goals completed! 🐙
C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σhi:σ i ≠ 0hpr:σ i = ((σ i).pred hi).succhne:∀ (x : Fin n1), σ (i.succAbove x) ≠ σ i⊢ ∀ (i_1 : Fin n1), (c ∘ (σ i).succAbove) ((((σ i).pred hi).predAbove ∘ σ ∘ i.succAbove) i_1) = (c1 ∘ i.succAbove) i_1 C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σhi:σ i ≠ 0hpr:σ i = ((σ i).pred hi).succhne:∀ (x : Fin n1), σ (i.succAbove x) ≠ σ ix:Fin n1⊢ (c ∘ (σ i).succAbove) ((((σ i).pred hi).predAbove ∘ σ ∘ i.succAbove) x) = (c1 ∘ i.succAbove) x
C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σhi:σ i ≠ 0hpr:σ i = ((σ i).pred hi).succhne:∀ (x : Fin n1), σ (i.succAbove x) ≠ σ ix:Fin n1⊢ c ((σ i).succAbove (((σ i).pred hi).predAbove (σ (i.succAbove x)))) = c (σ (i.succAbove x))
C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σhi:σ i ≠ 0hpr:σ i = ((σ i).pred hi).succhne:∀ (x : Fin n1), σ (i.succAbove x) ≠ σ ix:Fin n1⊢ (σ i).succAbove (((σ i).pred hi).predAbove (σ (i.succAbove x))) = σ (i.succAbove x)
conv_lhs => C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σhi:σ i ≠ 0hpr:σ i = ((σ i).pred hi).succhne:∀ (x : Fin n1), σ (i.succAbove x) ≠ σ ix:Fin n1| σ i; C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σhi:σ i ≠ 0hpr:σ i = ((σ i).pred hi).succhne:∀ (x : Fin n1), σ (i.succAbove x) ≠ σ ix:Fin n1| ((σ i).pred hi).succ
All goals completed! 🐙
Given a reindexing of c by c1 via σ, removing the i-th entry of c1 and the
(σ i)-th entry of c yields a reindexing of c ∘ (σ i).succAbove by c1 ∘ i.succAbove.
This unifies succAbove_of_eq_zero and succAbove_of_neq_zero via a case split on
whether σ i = 0. This is used for the commutation of permutation
of indices with evaluation of indices.
lemma succAbove {n n1 : ℕ} {c : Fin (n + 1) → C} {c1 : Fin (n1 + 1) → C}
{σ : Fin (n1 + 1) → Fin (n + 1)} (i : Fin (n1 + 1))
(h : IsReindexing c c1 σ) :
IsReindexing (c ∘ (σ i).succAbove) (c1 ∘ i.succAbove)
(if hi : σ i = 0 then fun j => (σ (i.succAbove j)).pred (k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σhi:σ i = 0j:Fin n1⊢ σ (i.succAbove j) ≠ 0 All goals completed! 🐙)
else (Fin.pred (σ i) hi).predAbove ∘ σ ∘ i.succAbove) := C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σ⊢ IsReindexing (c ∘ (σ i).succAbove) (c1 ∘ i.succAbove)
(if hi : σ i = 0 then fun j => (σ (i.succAbove j)).pred ⋯ else ((σ i).pred hi).predAbove ∘ σ ∘ i.succAbove)
C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σhi:σ i = 0⊢ IsReindexing (c ∘ (σ i).succAbove) (c1 ∘ i.succAbove)
(if hi : σ i = 0 then fun j => (σ (i.succAbove j)).pred ⋯ else ((σ i).pred hi).predAbove ∘ σ ∘ i.succAbove)C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σhi:¬σ i = 0⊢ IsReindexing (c ∘ (σ i).succAbove) (c1 ∘ i.succAbove)
(if hi : σ i = 0 then fun j => (σ (i.succAbove j)).pred ⋯ else ((σ i).pred hi).predAbove ∘ σ ∘ i.succAbove)
C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σhi:σ i = 0⊢ IsReindexing (c ∘ (σ i).succAbove) (c1 ∘ i.succAbove)
(if hi : σ i = 0 then fun j => (σ (i.succAbove j)).pred ⋯ else ((σ i).pred hi).predAbove ∘ σ ∘ i.succAbove) All goals completed! 🐙
C:Typen:ℕn1:ℕc:Fin (n + 1) → Cc1:Fin (n1 + 1) → Cσ:Fin (n1 + 1) → Fin (n + 1)i:Fin (n1 + 1)h:IsReindexing c c1 σhi:¬σ i = 0⊢ IsReindexing (c ∘ (σ i).succAbove) (c1 ∘ i.succAbove)
(if hi : σ i = 0 then fun j => (σ (i.succAbove j)).pred ⋯ else ((σ i).pred hi).predAbove ∘ σ ∘ i.succAbove) All goals completed! 🐙
The conclusion of succAbove from an explicit survivor relabelling: if σ' fills the square
(σ i).succAbove ∘ σ' = σ ∘ i.succAbove, carrying the complement of i to the complement of
σ i, then it is a reindexing of the two shortened colour lists. The square forces σ' to be
injective, hence bijective, so no bijectivity hypothesis is needed; this is why the statement is
restricted to equal lengths.
Where succAbove builds the relabelling from σ as a dite composite, the map here is the
caller's, which is what lets it stand in the statement of a lemma the caller instantiates.
All goals completed! 🐙))
C:Typen:ℕc:Fin (n + 1) → Cc1:Fin (n + 1) → Cσ:Fin (n + 1) → Fin (n + 1)σ':Fin n → Fin ni:Fin (n + 1)h:IsReindexing c c1 σhσ':(σ i).succAbove ∘ σ' = σ ∘ i.succAbovekey:∀ (a : Fin n), (σ i).succAbove (σ' a) = σ (i.succAbove a)a:Fin n⊢ (c ∘ (σ i).succAbove) (σ' a) = (c1 ∘ i.succAbove) a All goals completed! 🐙
Given a reindexing of c by c1 via σ and two distinct indices i ≠ j, removing the
i-th and j-th entries of c1 and the (σ i)-th and (σ j)-th entries of c yields a
reindexing of c ∘ (σ i).succSuccAbove (σ j) by c1 ∘ i.succSuccAbove j.
This is used for the commutation of permutation of indices with
contraction of indices.
lemma succSuccAbove {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
{c1 : Fin (n1 + 1 + 1) → C}
(i j : Fin (n1 + 1 + 1)) (hij : i ≠ j)
{σ : Fin (n1 + 1 + 1) → Fin (n + 1 + 1)} (hσ : IsReindexing c c1 σ) :
IsReindexing (c ∘ (σ i).succSuccAbove (σ j))
(c1 ∘ i.succSuccAbove j) (i.funPredPredAbove j hij σ hσ.1) := C:Typen:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σ⊢ IsReindexing (c ∘ (σ i).succSuccAbove (σ j)) (c1 ∘ i.succSuccAbove j) (i.funPredPredAbove j hij σ ⋯)
C:Typen:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σ⊢ Function.Bijective (i.funPredPredAbove j hij σ ⋯)C:Typen:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σ⊢ ∀ (i_1 : Fin n1), (c ∘ (σ i).succSuccAbove (σ j)) (i.funPredPredAbove j hij σ ⋯ i_1) = (c1 ∘ i.succSuccAbove j) i_1
C:Typen:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σ⊢ Function.Bijective (i.funPredPredAbove j hij σ ⋯) All goals completed! 🐙
C:Typen:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σ⊢ ∀ (i_1 : Fin n1), (c ∘ (σ i).succSuccAbove (σ j)) (i.funPredPredAbove j hij σ ⋯ i_1) = (c1 ∘ i.succSuccAbove j) i_1 C:Typen:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σm:Fin n1⊢ (c ∘ (σ i).succSuccAbove (σ j)) (i.funPredPredAbove j hij σ ⋯ m) = (c1 ∘ i.succSuccAbove j) m
All goals completed! 🐙
Removing two pairs of entries from c in either order gives the same colour list:
removing the i1-th and j1-th entries and then the (shifted) i2-th and j2-th entries
matches removing the i2-th and j2-th entries first and then the (shifted) i1-th and
j1-th entries, via the identity permutation.
This is used for the commutation of two contractions.
C:Typen:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1hij2:i2 ≠ j2i:Fin n⊢ i1 ≠ j1C:Typen:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1hij2:i2 ≠ j2i:Fin n⊢ i2 ≠ j2
C:Typen:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1hij2:i2 ≠ j2i:Fin n⊢ i1 ≠ j1 All goals completed! 🐙
C:Typen:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1hij2:i2 ≠ j2i:Fin n⊢ i2 ≠ j2 All goals completed! 🐙lemma succSuccAbove_succAbove_comm {n : ℕ} {c : Fin (n + 1 + 1 + 1) → C}
(k : Fin (n + 1)) (i j : Fin (n + 1 + 1 + 1)) :
-- The corresponding position of k in the full list.
let k' := Fin.succSuccAbove i j k
let k'' := Fin.predAbove 0 k'
-- The position of i after removing k'
let i' := k''.predAbove i
-- The position of j after removing k'
let j' := k''.predAbove j
IsReindexing ((c ∘ k'.succAbove) ∘ i'.succSuccAbove j')
((c ∘ i.succSuccAbove j) ∘ k.succAbove) id := C:Typen:ℕc:Fin (n + 1 + 1 + 1) → Ck:Fin (n + 1)i:Fin (n + 1 + 1 + 1)j:Fin (n + 1 + 1 + 1)⊢ let k' := i.succSuccAbove j k;
let k'' := predAbove 0 k';
let i' := k''.predAbove i;
let j' := k''.predAbove j;
IsReindexing ((c ∘ k'.succAbove) ∘ i'.succSuccAbove j') ((c ∘ i.succSuccAbove j) ∘ k.succAbove) id
C:Typen:ℕc:Fin (n + 1 + 1 + 1) → Ck:Fin (n + 1)i:Fin (n + 1 + 1 + 1)j:Fin (n + 1 + 1 + 1)m:Fin n⊢ ((c ∘ (i.succSuccAbove j k).succAbove) ∘
((predAbove 0 (i.succSuccAbove j k)).predAbove i).succSuccAbove ((predAbove 0 (i.succSuccAbove j k)).predAbove j))
(id m) =
((c ∘ i.succSuccAbove j) ∘ k.succAbove) m
C:Typen:ℕc:Fin (n + 1 + 1 + 1) → Ck:Fin (n + 1)i:Fin (n + 1 + 1 + 1)j:Fin (n + 1 + 1 + 1)m:Fin n⊢ c
((i.succSuccAbove j k).succAbove
(((predAbove 0 (i.succSuccAbove j k)).predAbove i).succSuccAbove ((predAbove 0 (i.succSuccAbove j k)).predAbove j)
m)) =
c (i.succSuccAbove j (k.succAbove m))
C:Typen:ℕc:Fin (n + 1 + 1 + 1) → Ck:Fin (n + 1)i:Fin (n + 1 + 1 + 1)j:Fin (n + 1 + 1 + 1)m:Fin n⊢ (i.succSuccAbove j k).succAbove
(((predAbove 0 (i.succSuccAbove j k)).predAbove i).succSuccAbove ((predAbove 0 (i.succSuccAbove j k)).predAbove j)
m) =
i.succSuccAbove j (k.succAbove m)
C:Typen:ℕc:Fin (n + 1 + 1 + 1) → Ck:Fin (n + 1)i:Fin (n + 1 + 1 + 1)j:Fin (n + 1 + 1 + 1)m:Fin n⊢ ↑((i.succSuccAbove j k).succAbove
(((predAbove 0 (i.succSuccAbove j k)).predAbove i).succSuccAbove ((predAbove 0 (i.succSuccAbove j k)).predAbove j)
m)) =
↑(i.succSuccAbove j (k.succAbove m))
C:Typen:ℕc:Fin (n + 1 + 1 + 1) → Ck:Fin (n + 1)i:Fin (n + 1 + 1 + 1)j:Fin (n + 1 + 1 + 1)m:Fin n⊢ (if
(if
(↑m <
if h :
(if h :
↑0 <
if ↑k < ↑i ∧ ↑k < ↑j then ↑k
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ↑k + 1
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ↑k + 1 else ↑k + 2 then
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).pred
⋯)
else
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).castLT
⋯)) <
↑i then
↑(i.pred ⋯)
else ↑(i.castLT ⋯)) ∧
↑m <
if h :
(if h :
↑0 <
if ↑k < ↑i ∧ ↑k < ↑j then ↑k
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ↑k + 1
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ↑k + 1 else ↑k + 2 then
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).pred
⋯)
else
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).castLT
⋯)) <
↑j then
↑(j.pred ⋯)
else ↑(j.castLT ⋯) then
↑m
else
if
(↑m + 1 <
if h :
(if h :
↑0 <
if ↑k < ↑i ∧ ↑k < ↑j then ↑k
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ↑k + 1
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ↑k + 1 else ↑k + 2 then
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).pred
⋯)
else
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).castLT
⋯)) <
↑i then
↑(i.pred ⋯)
else ↑(i.castLT ⋯)) ∧
(if h :
(if h :
↑0 <
if ↑k < ↑i ∧ ↑k < ↑j then ↑k
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ↑k + 1
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ↑k + 1 else ↑k + 2 then
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).pred
⋯)
else
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).castLT
⋯)) <
↑j then
↑(j.pred ⋯)
else ↑(j.castLT ⋯)) ≤
↑m then
↑m + 1
else
if
(if h :
(if h :
↑0 <
if ↑k < ↑i ∧ ↑k < ↑j then ↑k
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ↑k + 1
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ↑k + 1 else ↑k + 2 then
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).pred
⋯)
else
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).castLT
⋯)) <
↑i then
↑(i.pred ⋯)
else ↑(i.castLT ⋯)) ≤
↑m ∧
↑m + 1 <
if h :
(if h :
↑0 <
if ↑k < ↑i ∧ ↑k < ↑j then ↑k
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ↑k + 1
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ↑k + 1 else ↑k + 2 then
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).pred
⋯)
else
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).castLT
⋯)) <
↑j then
↑(j.pred ⋯)
else ↑(j.castLT ⋯) then
↑m + 1
else ↑m + 2) <
if ↑k < ↑i ∧ ↑k < ↑j then ↑k
else if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ↑k + 1 else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ↑k + 1 else ↑k + 2 then
if
(↑m <
if h :
(if h :
↑0 <
if ↑k < ↑i ∧ ↑k < ↑j then ↑k
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ↑k + 1
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ↑k + 1 else ↑k + 2 then
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).pred
⋯)
else
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).castLT
⋯)) <
↑i then
↑(i.pred ⋯)
else ↑(i.castLT ⋯)) ∧
↑m <
if h :
(if h :
↑0 <
if ↑k < ↑i ∧ ↑k < ↑j then ↑k
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ↑k + 1
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ↑k + 1 else ↑k + 2 then
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).pred
⋯)
else
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).castLT
⋯)) <
↑j then
↑(j.pred ⋯)
else ↑(j.castLT ⋯) then
↑m
else
if
(↑m + 1 <
if h :
(if h :
↑0 <
if ↑k < ↑i ∧ ↑k < ↑j then ↑k
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ↑k + 1
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ↑k + 1 else ↑k + 2 then
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).pred
⋯)
else
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).castLT
⋯)) <
↑i then
↑(i.pred ⋯)
else ↑(i.castLT ⋯)) ∧
(if h :
(if h :
↑0 <
if ↑k < ↑i ∧ ↑k < ↑j then ↑k
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ↑k + 1
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ↑k + 1 else ↑k + 2 then
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).pred
⋯)
else
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).castLT
⋯)) <
↑j then
↑(j.pred ⋯)
else ↑(j.castLT ⋯)) ≤
↑m then
↑m + 1
else
if
(if h :
(if h :
↑0 <
if ↑k < ↑i ∧ ↑k < ↑j then ↑k
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ↑k + 1
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ↑k + 1 else ↑k + 2 then
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).pred
⋯)
else
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).castLT
⋯)) <
↑i then
↑(i.pred ⋯)
else ↑(i.castLT ⋯)) ≤
↑m ∧
↑m + 1 <
if h :
(if h :
↑0 <
if ↑k < ↑i ∧ ↑k < ↑j then ↑k
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ↑k + 1
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ↑k + 1 else ↑k + 2 then
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).pred
⋯)
else
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).castLT
⋯)) <
↑j then
↑(j.pred ⋯)
else ↑(j.castLT ⋯) then
↑m + 1
else ↑m + 2
else
(if
(↑m <
if h :
(if h :
↑0 <
if ↑k < ↑i ∧ ↑k < ↑j then ↑k
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ↑k + 1
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ↑k + 1 else ↑k + 2 then
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).pred
⋯)
else
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).castLT
⋯)) <
↑i then
↑(i.pred ⋯)
else ↑(i.castLT ⋯)) ∧
↑m <
if h :
(if h :
↑0 <
if ↑k < ↑i ∧ ↑k < ↑j then ↑k
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ↑k + 1
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ↑k + 1 else ↑k + 2 then
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).pred
⋯)
else
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).castLT
⋯)) <
↑j then
↑(j.pred ⋯)
else ↑(j.castLT ⋯) then
↑m
else
if
(↑m + 1 <
if h :
(if h :
↑0 <
if ↑k < ↑i ∧ ↑k < ↑j then ↑k
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ↑k + 1
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ↑k + 1 else ↑k + 2 then
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).pred
⋯)
else
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).castLT
⋯)) <
↑i then
↑(i.pred ⋯)
else ↑(i.castLT ⋯)) ∧
(if h :
(if h :
↑0 <
if ↑k < ↑i ∧ ↑k < ↑j then ↑k
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ↑k + 1
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ↑k + 1 else ↑k + 2 then
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).pred
⋯)
else
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).castLT
⋯)) <
↑j then
↑(j.pred ⋯)
else ↑(j.castLT ⋯)) ≤
↑m then
↑m + 1
else
if
(if h :
(if h :
↑0 <
if ↑k < ↑i ∧ ↑k < ↑j then ↑k
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ↑k + 1
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ↑k + 1 else ↑k + 2 then
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).pred
⋯)
else
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).castLT
⋯)) <
↑i then
↑(i.pred ⋯)
else ↑(i.castLT ⋯)) ≤
↑m ∧
↑m + 1 <
if h :
(if h :
↑0 <
if ↑k < ↑i ∧ ↑k < ↑j then ↑k
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ↑k + 1
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ↑k + 1 else ↑k + 2 then
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).pred
⋯)
else
↑((if ↑k < ↑i ∧ ↑k < ↑j then ⟨↑k, ⋯⟩
else
if ↑k + 1 < ↑i ∧ ↑j ≤ ↑k then ⟨↑k + 1, ⋯⟩
else if ↑i ≤ ↑k ∧ ↑k + 1 < ↑j then ⟨↑k + 1, ⋯⟩ else ⟨↑k + 2, ⋯⟩).castLT
⋯)) <
↑j then
↑(j.pred ⋯)
else ↑(j.castLT ⋯) then
↑m + 1
else ↑m + 2) +
1) =
if (if ↑m < ↑k then ↑m else ↑m + 1) < ↑i ∧ (if ↑m < ↑k then ↑m else ↑m + 1) < ↑j then if ↑m < ↑k then ↑m else ↑m + 1
else
if (if ↑m < ↑k then ↑m else ↑m + 1) + 1 < ↑i ∧ ↑j ≤ if ↑m < ↑k then ↑m else ↑m + 1 then
(if ↑m < ↑k then ↑m else ↑m + 1) + 1
else
if (↑i ≤ if ↑m < ↑k then ↑m else ↑m + 1) ∧ (if ↑m < ↑k then ↑m else ↑m + 1) + 1 < ↑j then
(if ↑m < ↑k then ↑m else ↑m + 1) + 1
else (if ↑m < ↑k then ↑m else ↑m + 1) + 2
All goals completed! 🐙
Removing two single entries from c in either order gives the same colour list:
removing the k1-th entry and then the (shifted) k2-th entry matches removing the
k2-th entry first and then the (shifted) k1-th entry, via the identity permutation.
This is used for the commutation of two evaluations of indices.
lemma succAbove_succAbove_comm {n : ℕ} {c : Fin (n + 1 + 1) → C}
(k1 : Fin (n + 1 + 1)) (k2 : Fin (n + 1)) :
let k2' := k1.succAbove k2;
let k1' := k2.predAbove k1;
IsReindexing ((c ∘ k2'.succAbove) ∘ k1'.succAbove)
((c ∘ k1.succAbove) ∘ k2.succAbove) id := C:Typen:ℕc:Fin (n + 1 + 1) → Ck1:Fin (n + 1 + 1)k2:Fin (n + 1)⊢ let k2' := k1.succAbove k2;
let k1' := k2.predAbove k1;
IsReindexing ((c ∘ k2'.succAbove) ∘ k1'.succAbove) ((c ∘ k1.succAbove) ∘ k2.succAbove) id
C:Typen:ℕc:Fin (n + 1 + 1) → Ck1:Fin (n + 1 + 1)k2:Fin (n + 1)k2':Fin (n + 1 + 1) := k1.succAbove k2k1':Fin (n + 1) := k2.predAbove k1⊢ IsReindexing ((c ∘ k2'.succAbove) ∘ k1'.succAbove) ((c ∘ k1.succAbove) ∘ k2.succAbove) id
C:Typen:ℕc:Fin (n + 1 + 1) → Ck1:Fin (n + 1 + 1)k2:Fin (n + 1)k2':Fin (n + 1 + 1) := k1.succAbove k2k1':Fin (n + 1) := k2.predAbove k1m:Fin n⊢ ((c ∘ k2'.succAbove) ∘ k1'.succAbove) (id m) = ((c ∘ k1.succAbove) ∘ k2.succAbove) m
C:Typen:ℕc:Fin (n + 1 + 1) → Ck1:Fin (n + 1 + 1)k2:Fin (n + 1)k2':Fin (n + 1 + 1) := k1.succAbove k2k1':Fin (n + 1) := k2.predAbove k1m:Fin n⊢ c (k2'.succAbove (k1'.succAbove m)) = c (k1.succAbove (k2.succAbove m))
C:Typen:ℕc:Fin (n + 1 + 1) → Ck1:Fin (n + 1 + 1)k2:Fin (n + 1)k2':Fin (n + 1 + 1) := k1.succAbove k2k1':Fin (n + 1) := k2.predAbove k1m:Fin n⊢ k2'.succAbove (k1'.succAbove m) = k1.succAbove (k2.succAbove m)
All goals completed! 🐙
Splitting a list of colours c : Fin (n + 1) → C into its first n entries and its
last entry recovers c: the identity permutation matches
Fin.append (c ∘ (Fin.last n).succAbove) ![c (Fin.last n)] with c.
C:Typen:ℕc:Fin (n + 1) → C⊢ ∀ (i : Fin (n + Nat.succ 0)), append (c ∘ castSucc) ![c (last n)] i = c i
C:Typen:ℕc:Fin (n + 1) → Ci:Fin n⊢ append (c ∘ castSucc) ![c (last n)] (castAdd (Nat.succ 0) i) = c (castAdd (Nat.succ 0) i)C:Typen:ℕc:Fin (n + 1) → Ci:Fin (Nat.succ 0)⊢ append (c ∘ castSucc) ![c (last n)] (natAdd n i) = c (natAdd n i)
C:Typen:ℕc:Fin (n + 1) → Ci:Fin n⊢ append (c ∘ castSucc) ![c (last n)] (castAdd (Nat.succ 0) i) = c (castAdd (Nat.succ 0) i) C:Typen:ℕc:Fin (n + 1) → Ci:Fin n⊢ c i.castSucc = c (castAdd (Nat.succ 0) i); All goals completed! 🐙
C:Typen:ℕc:Fin (n + 1) → Ci:Fin (Nat.succ 0)⊢ append (c ∘ castSucc) ![c (last n)] (natAdd n i) = c (natAdd n i) C:Typen:ℕc:Fin (n + 1) → C⊢ append (c ∘ castSucc) ![c (last n)] (natAdd n ((fun i => i) ⟨0, ⋯⟩)) = c (natAdd n ((fun i => i) ⟨0, ⋯⟩)); C:Typen:ℕc:Fin (n + 1) → C⊢ c (last n) = c (natAdd n ⟨0, ⋯⟩); All goals completed! 🐙
Splitting a list of colours c : Fin (n + 1) → C at an arbitrary slot i, rather than at the
last one as in append_succ_last: the block map that lists the i.succAbove survivors and then
i itself matches c with the survivors of i followed by the surviving entry c1 1 of a
rank-two list c1 whose second entry is slot i's colour.
C:Typen:ℕc:Fin (n + 1) → Cc1:Fin 2 → Ci:Fin (n + 1)hc:c i = c1 1⊢ Function.Bijective ⇑(i.cycleIcc (last n))
All goals completed! 🐙,
fun x => C:Typen:ℕc:Fin (n + 1) → Cc1:Fin 2 → Ci:Fin (n + 1)hc:c i = c1 1x:Fin (n + 1)⊢ c (append i.succAbove (fun x => i) x) = append (c ∘ i.succAbove) (c1 ∘ Fin.succAbove 0) x
C:Typen:ℕc:Fin (n + 1) → Cc1:Fin 2 → Ci:Fin (n + 1)hc:c i = c1 1x:Fin (n + 1)a:Fin n⊢ c (append i.succAbove (fun x => i) (castAdd 1 a)) = append (c ∘ i.succAbove) (c1 ∘ Fin.succAbove 0) (castAdd 1 a)C:Typen:ℕc:Fin (n + 1) → Cc1:Fin 2 → Ci:Fin (n + 1)hc:c i = c1 1x:Fin (n + 1)a:Fin 1⊢ c (append i.succAbove (fun x => i) (natAdd n a)) = append (c ∘ i.succAbove) (c1 ∘ Fin.succAbove 0) (natAdd n a)
C:Typen:ℕc:Fin (n + 1) → Cc1:Fin 2 → Ci:Fin (n + 1)hc:c i = c1 1x:Fin (n + 1)a:Fin n⊢ c (append i.succAbove (fun x => i) (castAdd 1 a)) = append (c ∘ i.succAbove) (c1 ∘ Fin.succAbove 0) (castAdd 1 a) All goals completed! 🐙
C:Typen:ℕc:Fin (n + 1) → Cc1:Fin 2 → Ci:Fin (n + 1)hc:c i = c1 1x:Fin (n + 1)a:Fin 1⊢ c (append i.succAbove (fun x => i) (natAdd n a)) = append (c ∘ i.succAbove) (c1 ∘ Fin.succAbove 0) (natAdd n a) C:Typen:ℕc:Fin (n + 1) → Cc1:Fin 2 → Ci:Fin (n + 1)hc:c i = c1 1x:Fin (n + 1)⊢ c (append i.succAbove (fun x => i) (natAdd n ((fun i => i) ⟨0, ⋯⟩))) =
append (c ∘ i.succAbove) (c1 ∘ Fin.succAbove 0) (natAdd n ((fun i => i) ⟨0, ⋯⟩))
All goals completed! 🐙⟩
Updating slot i of c to d and then back to e = c i returns c, no other slot moving:
the colour cast a round trip of two contractions at slot i generates.
lemma update_update_of_eq {n : ℕ} {c : Fin n → C} {d e : C} (i : Fin n) (he : c i = e) :
IsReindexing c (Function.update (Function.update c i d) i e) (id : Fin n → Fin n) :=
on_id.mpr (fun j => C:Typen:ℕc:Fin n → Cd:Ce:Ci:Fin nhe:c i = ej:Fin n⊢ c j = Function.update (Function.update c i d) i e j C:Typen:ℕc:Fin n → Cd:Ce:Ci:Fin nhe:c i = ej:Fin nh:j = i⊢ c j = Function.update (Function.update c i d) i e jC:Typen:ℕc:Fin n → Cd:Ce:Ci:Fin nhe:c i = ej:Fin nh:¬j = i⊢ c j = Function.update (Function.update c i d) i e j C:Typen:ℕc:Fin n → Cd:Ce:Ci:Fin nhe:c i = ej:Fin nh:j = i⊢ c j = Function.update (Function.update c i d) i e jC:Typen:ℕc:Fin n → Cd:Ce:Ci:Fin nhe:c i = ej:Fin nh:¬j = i⊢ c j = Function.update (Function.update c i d) i e j All goals completed! 🐙)
Splitting a list of colours c : Fin (n + 1) → C into its first entry and its remaining
n entries recovers c: the canonical reindexing Fin (1 + n) ≃ Fin (n + 1) matches
Fin.append ![c 0] (c ∘ Fin.succAbove 0) with c.
lemma append_of_first {n : ℕ} (c : Fin (n + 1) → C) :
IsReindexing (Fin.append ![c 0] (c ∘ Fin.succAbove 0)) c (Fin.cast (k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1) → C⊢ n + 1 = Nat.succ 0 + n All goals completed! 🐙)) := C:Typen:ℕc:Fin (n + 1) → C⊢ IsReindexing (append ![c 0] (c ∘ Fin.succAbove 0)) c (Fin.cast ⋯)
refine ⟨(finCongr (C:Typen:ℕc:Fin (n + 1) → C⊢ n + 1 = Nat.succ 0 + n All goals completed! 🐙)).bijective, fun i => ?_⟩
C:Typen:ℕc:Fin (n + 1) → C⊢ append ![c 0] (c ∘ Fin.succAbove 0) (Fin.cast ⋯ 0) = c 0C:Typen:ℕc:Fin (n + 1) → Ci:Fin n⊢ append ![c 0] (c ∘ Fin.succAbove 0) (Fin.cast ⋯ i.succ) = c i.succ
C:Typen:ℕc:Fin (n + 1) → C⊢ append ![c 0] (c ∘ Fin.succAbove 0) (Fin.cast ⋯ 0) = c 0 All goals completed! 🐙
C:Typen:ℕc:Fin (n + 1) → Ci:Fin n⊢ append ![c 0] (c ∘ Fin.succAbove 0) (Fin.cast ⋯ i.succ) = c i.succ simpa using congrArg (Fin.append ![c 0] (c ∘ Fin.succ)) (a₁ := Fin.cast _ i.succ)
(a₂ := Fin.natAdd 1 i) (C:Typen:ℕc:Fin (n + 1) → Ci:Fin n⊢ Fin.cast ⋯ i.succ = natAdd 1 i C:Typen:ℕc:Fin (n + 1) → Ci:Fin n⊢ ↑(Fin.cast ⋯ i.succ) = ↑(natAdd 1 i); All goals completed! 🐙)
Casting the domain along an equality n1 = n of lengths is a reindexing of c by
c ∘ Fin.cast h.
lemma fin_cast_isReindexing (n n1 : ℕ) {c : Fin n → C} (h : n1 = n) :
IsReindexing c (c ∘ Fin.cast h) (Fin.cast h) := C:Typen:ℕn1:ℕc:Fin n → Ch:n1 = n⊢ IsReindexing c (c ∘ Fin.cast h) (Fin.cast h)
C:Typen:ℕn1:ℕc:Fin n → Ch:n1 = n⊢ Function.Bijective (Fin.cast h)C:Typen:ℕn1:ℕc:Fin n → Ch:n1 = n⊢ ∀ (i : Fin n1), c (Fin.cast h i) = (c ∘ Fin.cast h) i
C:Typen:ℕn1:ℕc:Fin n → Ch:n1 = n⊢ Function.Bijective (Fin.cast h) All goals completed! 🐙
C:Typen:ℕn1:ℕc:Fin n → Ch:n1 = n⊢ ∀ (i : Fin n1), c (Fin.cast h i) = (c ∘ Fin.cast h) i C:Typen:ℕn1:ℕc:Fin n → Ch:n1 = ni:Fin n1⊢ c (Fin.cast h i) = (c ∘ Fin.cast h) i
All goals completed! 🐙