Fin lemmas

The purpose of this file is to define some results Fin currently in Mathlib.

At some point these should either be up-streamed to Mathlib or replaced with definitions already in Mathlib.

def PhysLean.Fin.predAboveI {n : ℕ} (i x : Fin n.succ.succ) : Fin n.succ

Given a i and x in Fin n.succ.succ returns an element of Fin n.succ subtracting 1 if i.val ≤ x.val else casting x.

Equations

• PhysLean.Fin.predAboveI i x = if h : ↑x < ↑i then ⟨↑x, ⋯⟩ else ⟨↑x - 1, ⋯⟩

theorem PhysLean.Fin.predAboveI_self {n : ℕ} (i : Fin n.succ.succ) : predAboveI i i = ⟨↑i - 1, ⋯⟩

@[simp]

theorem PhysLean.Fin.predAboveI_succAbove {n : ℕ} (i : Fin n.succ.succ) (x : Fin n.succ) : predAboveI i (i.succAbove x) = x

theorem PhysLean.Fin.succsAbove_predAboveI {n : ℕ} {i x : Fin n.succ.succ} (h : i ≠ x) : i.succAbove (predAboveI i x) = x

theorem PhysLean.Fin.predAboveI_eq_iff {n : ℕ} {i x : Fin n.succ.succ} (h : i ≠ x) (y : Fin n.succ) : y = predAboveI i x ↔ i.succAbove y = x

theorem PhysLean.Fin.predAboveI_lt {n : ℕ} {i x : Fin n.succ.succ} (h : ↑x < ↑i) : predAboveI i x = ⟨↑x, ⋯⟩

theorem PhysLean.Fin.predAboveI_ge {n : ℕ} {i x : Fin n.succ.succ} (h : ↑i < ↑x) : predAboveI i x = ⟨↑x - 1, ⋯⟩

theorem PhysLean.Fin.succAbove_succAbove_predAboveI {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) (x : Fin n) : i.succAbove (j.succAbove x) = (i.succAbove j).succAbove ((predAboveI (i.succAbove j) i).succAbove x)

def PhysLean.Fin.finExtractOne {n : ℕ} (i : Fin n.succ) : Fin n.succ ≃ Fin 1 ⊕ Fin n

The equivalence between Fin n.succ and Fin 1 ⊕ Fin n extracting the ith component.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PhysLean.Fin.finExtractOne_apply_eq {n : ℕ} (i : Fin n.succ) : (finExtractOne i) i = Sum.inl 0

theorem PhysLean.Fin.finExtractOne_symm_inr {n : ℕ} (i : Fin n.succ) : ⇑(finExtractOne i).symm ∘ Sum.inr = i.succAbove

@[simp]

theorem PhysLean.Fin.finExtractOne_symm_inr_apply {n : ℕ} (i : Fin n.succ) (x : Fin n) : (finExtractOne i).symm (Sum.inr x) = i.succAbove x

@[simp]

theorem PhysLean.Fin.finExtractOne_symm_inl_apply {n : ℕ} (i : Fin n.succ) : (finExtractOne i).symm (Sum.inl 0) = i

theorem PhysLean.Fin.finExtractOne_apply_neq {n : ℕ} (i j : Fin n.succ.succ) (hij : i ≠ j) : (finExtractOne i) j = Sum.inr (predAboveI i j)

def PhysLean.Fin.finExtractOnPermHom {n m : ℕ} (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin m.succ.succ) : Fin n.succ → Fin m.succ

Given an equivalence Fin n.succ.succ ≃ Fin n.succ.succ, and an i : Fin n.succ.succ, the map Fin n.succ → Fin n.succ obtained by dropping i and it's image.

Equations

• PhysLean.Fin.finExtractOnPermHom i σ x = PhysLean.Fin.predAboveI (σ i) (σ ((PhysLean.Fin.finExtractOne i).symm (Sum.inr x)))

theorem PhysLean.Fin.finExtractOnPermHom_inv {n m : ℕ} (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin m.succ.succ) : finExtractOnPermHom (σ i) σ.symm ∘ finExtractOnPermHom i σ = id

def PhysLean.Fin.finExtractOnePerm {n m : ℕ} (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin m.succ.succ) : Fin n.succ ≃ Fin m.succ

Given an equivalence Fin n.succ.succ ≃ Fin n.succ.succ, and an i : Fin n.succ.succ, the equivalence Fin n.succ ≃ Fin n.succ obtained by dropping i and it's image.

Equations

• One or more equations did not get rendered due to their size.

theorem PhysLean.Fin.finExtractOnePerm_equiv {n m : ℕ} (e : Fin n.succ.succ ≃ Fin m.succ.succ) (i : Fin n.succ.succ) : ⇑e ∘ i.succAbove = (e i).succAbove ∘ ⇑(finExtractOnePerm i e)

@[simp]

theorem PhysLean.Fin.finExtractOnePerm_apply {n : ℕ} (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ) (x : Fin n.succ) : (finExtractOnePerm i σ) x = predAboveI (σ i) (σ ((finExtractOne i).symm (Sum.inr x)))

@[simp]

theorem PhysLean.Fin.finExtractOnePerm_symm_apply {n : ℕ} (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ) (x : Fin n.succ) : (finExtractOnePerm i σ).symm x = predAboveI (σ.symm (σ i)) (σ.symm ((finExtractOne (σ i)).symm (Sum.inr x)))

def PhysLean.Fin.finExtractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) : Fin n.succ.succ ≃ (Fin 1 ⊕ Fin 1) ⊕ Fin n

The equivalence of types Fin n.succ.succ ≃ (Fin 1 ⊕ Fin 1) ⊕ Fin n extracting the i and (i.succAbove j).

Equations

• PhysLean.Fin.finExtractTwo i j = (PhysLean.Fin.finExtractOne i).trans (((Equiv.refl (Fin 1)).sumCongr (PhysLean.Fin.finExtractOne j)).trans (Equiv.sumAssoc (Fin 1) (Fin 1) (Fin n)).symm)

@[simp]

theorem PhysLean.Fin.finExtractTwo_apply_fst {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) : (finExtractTwo i j) i = Sum.inl (Sum.inl 0)

theorem PhysLean.Fin.finExtractTwo_symm_inr {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) : ⇑(finExtractTwo i j).symm ∘ Sum.inr = i.succAbove ∘ j.succAbove

@[simp]

theorem PhysLean.Fin.finExtractTwo_symm_inr_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) (x : Fin n) : (finExtractTwo i j).symm (Sum.inr x) = i.succAbove (j.succAbove x)

@[simp]

theorem PhysLean.Fin.finExtractTwo_symm_inl_inr_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) : (finExtractTwo i j).symm (Sum.inl (Sum.inr 0)) = i.succAbove j

@[simp]

theorem PhysLean.Fin.finExtractTwo_symm_inl_inl_apply {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) : (finExtractTwo i j).symm (Sum.inl (Sum.inl 0)) = i

@[simp]

theorem PhysLean.Fin.finExtractTwo_apply_snd {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) : (finExtractTwo i j) (i.succAbove j) = Sum.inl (Sum.inr 0)

def PhysLean.Fin.finMapToEquiv {n m : ℕ} (f1 : Fin n → Fin m) (f2 : Fin m → Fin n) (h : ∀ (x : Fin m), f1 (f2 x) = x := by decide) (h' : ∀ (x : Fin n), f2 (f1 x) = x := by decide) : Fin n ≃ Fin m

Takes two maps Fin n → Fin n and returns the equivalence they form.

Equations

• PhysLean.Fin.finMapToEquiv f1 f2 h h' = { toFun := f1, invFun := f2, left_inv := h', right_inv := h }

@[simp]

theorem PhysLean.Fin.finMapToEquiv_apply {n m : ℕ} {f1 : Fin n → Fin m} {f2 : Fin m → Fin n} {h : ∀ (x : Fin m), f1 (f2 x) = x} {h' : ∀ (x : Fin n), f2 (f1 x) = x} (x : Fin n) : (finMapToEquiv f1 f2 h h') x = f1 x

@[simp]

theorem PhysLean.Fin.finMapToEquiv_symm_apply {n m : ℕ} {f1 : Fin n → Fin m} {f2 : Fin m → Fin n} {h : ∀ (x : Fin m), f1 (f2 x) = x} {h' : ∀ (x : Fin n), f2 (f1 x) = x} (x : Fin m) : (finMapToEquiv f1 f2 h h').symm x = f2 x

theorem PhysLean.Fin.finMapToEquiv_symm_eq {n m : ℕ} {f1 : Fin n → Fin m} {f2 : Fin m → Fin n} {h : ∀ (x : Fin m), f1 (f2 x) = x} {h' : ∀ (x : Fin n), f2 (f1 x) = x} : (finMapToEquiv f1 f2 h h').symm = finMapToEquiv f2 f1 h' h

def PhysLean.Fin.equivCons {n m : ℕ} (e : Fin n ≃ Fin m) : Fin n.succ ≃ Fin m.succ

Given an equivalence between Fin n and Fin m, the induced equivalence between Fin n.succ and Fin m.succ derived by Fin.cons.

Equations

• PhysLean.Fin.equivCons e = { toFun := Fin.cons 0 (Fin.succ ∘ e.toFun), invFun := Fin.cons 0 (Fin.succ ∘ e.invFun), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem PhysLean.Fin.equivCons_zero {n m : ℕ} (e : Fin n ≃ Fin m) : (equivCons e) 0 = 0

@[simp]

theorem PhysLean.Fin.equivCons_trans {n m k : ℕ} (e : Fin n ≃ Fin m) (f : Fin m ≃ Fin k) : equivCons (e.trans f) = (equivCons e).trans (equivCons f)

@[simp]

theorem PhysLean.Fin.equivCons_castOrderIso {n m : ℕ} (h : n = m) : equivCons (Fin.castOrderIso h).toEquiv = (Fin.castOrderIso ⋯).toEquiv

@[simp]

theorem PhysLean.Fin.equivCons_symm_succ {n m : ℕ} (e : Fin n ≃ Fin m) (i : ℕ) (hi : i + 1 < m.succ) : (equivCons e).symm ⟨i + 1, hi⟩ = (e.symm ⟨i, ⋯⟩).succ

@[simp]

theorem PhysLean.Fin.equivCons_succ {n m : ℕ} (e : Fin n ≃ Fin m) (i : ℕ) (hi : i + 1 < n.succ) : (equivCons e) ⟨i + 1, hi⟩ = (e ⟨i, ⋯⟩).succ