Physlib.Relativity.Tensors.ComponentIdx.Contraction

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.Basic
public import Physlib.Relativity.Tensors.Contraction.SuccSuccAbove

Contractions of component indices

i. Overview

This file contains the component-index API induced by dropping a pair of contracted indices from a tensor.

The constructions here describe how component indices restrict along Fin.succSuccAbove, and how the fiber of this restriction is equivalent to the two component choices at the contracted positions.

ii. Key results

TensorSpecies.Tensor.ComponentIdx.dropPair restricts a component index by dropping two positions.

TensorSpecies.Tensor.ComponentIdx.DropPairSection is the finite set of component indices mapping to a fixed restricted component index.

TensorSpecies.Tensor.ComponentIdx.DropPairSection.ofFinEquiv identifies a DropPairSection with the two basis indices at the dropped positions.

iii. Table of contents

A. Dropping a pair

B. Sections of the drop-pair map

iv. References

There are no known references for the material in this module.

@[expose] public section

A. Dropping a pair

The ComponentIdx obtained by dropping two components.

def dropPair {n : ℕ} {c : Fin (n + 1 + 1) → C}
    (i j : Fin (n + 1 + 1)) (b : ComponentIdx (S := S) c) :
    ComponentIdx (S := S) (c ∘ Fin.succSuccAbove i j) :=
  fun m => b (Fin.succSuccAbove i j m)

B. Sections of the drop-pair map

Given a coordinate parameter b : Π k, Fin (S.repDim ((c ∘ i.succAbove ∘ j.succAbove) k))), the coordinate parameter Π k, Fin (S.repDim (c k)) which map down to b.

def DropPairSection {n : ℕ} {c : Fin (n + 1 + 1) → C}
    {i : Fin (n + 1 + 1)} {j : Fin (n + 1 + 1)}
    (b : ComponentIdx (S := S) (c ∘ Fin.succSuccAbove i j)) :
    Finset (ComponentIdx (S := S) c) :=
  {b' : ComponentIdx c | dropPair i j b' = b}



lemma mem_iff_apply_succSuccAbove_eq {n : ℕ} {c : Fin (n + 1 + 1) → C}
    {i j : Fin (n + 1 + 1)}
    (b : ComponentIdx (c ∘ Fin.succSuccAbove i j))
    (b' : ComponentIdx c) :
    b' ∈ DropPairSection (S := S) b ↔
      ∀ m, b' (Fin.succSuccAbove i j m) = b m := byk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)b:ComponentIdx (c ∘ i.succSuccAbove j)b':ComponentIdx c⊢ b' ∈ b.DropPairSection ↔ ∀ (m : Fin n), b' (i.succSuccAbove j m) = b m
  simp only [DropPairSection, Finset.mem_filter, Finset.mem_univ, true_and]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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)b:ComponentIdx (c ∘ i.succSuccAbove j)b':ComponentIdx c⊢ dropPair i j b' = b ↔ ∀ (m : Fin n), b' (i.succSuccAbove j m) = b m
  rw [funext_iffk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)b:ComponentIdx (c ∘ i.succSuccAbove j)b':ComponentIdx c⊢ (∀ (x : Fin n), dropPair i j b' x = b x) ↔ ∀ (m : Fin n), b' (i.succSuccAbove j m) = b mk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)b:ComponentIdx (c ∘ i.succSuccAbove j)b':ComponentIdx c⊢ (∀ (x : Fin n), dropPair i j b' x = b x) ↔ ∀ (m : Fin n), b' (i.succSuccAbove j m) = b m]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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)b:ComponentIdx (c ∘ i.succSuccAbove j)b':ComponentIdx c⊢ (∀ (x : Fin n), dropPair i j b' x = b x) ↔ ∀ (m : Fin n), b' (i.succSuccAbove j m) = b m
  simp [dropPair]All goals completed! 🐙

@[simp]
lemma mem_self_of_dropPair {n : ℕ} {c : Fin (n + 1 + 1) → C}
    {i j : Fin (n + 1 + 1)}
    (b : ComponentIdx (c)) :
    b ∈ DropPairSection (S := S) (b.dropPair i j) := byk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)b:ComponentIdx c⊢ b ∈ (dropPair i j b).DropPairSection
  simp [DropPairSection]All goals completed! 🐙

Given a b in ComponentIdx (c ∘ Fin.succSuccAbove i j)) and an x in Fin (S.repDim (c i)) × Fin (S.repDim (c j)), the corresponding coordinate parameter in ComponentIdx c.

unsolved goals
k:Typeinst✝⁵:CommRing kC G: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)m:Fin (n + 1 + 1)hi:¬m = ihj:¬m = j⊢ c (i.succSuccAbove j (i.predPredAbove j hij m ?m.127)) = c munsolved goals
k:Typeinst✝⁵:CommRing kC G: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)m:Fin (n + 1 + 1)hi:¬m = ihj:¬m = j⊢ c (i.succSuccAbove j (i.predPredAbove j hij m ?m.127)) = c m
def ofFin {n : ℕ} {c : Fin (n + 1 + 1) → C}
    {i j : Fin (n + 1 + 1)} (hij : i ≠ j) (b : ComponentIdx (S := S) (c ∘ Fin.succSuccAbove i j))
    (x : basisIdx (c i) × basisIdx (c j)) :
    ComponentIdx (S := S) c := fun m =>
  if hi : m = i then basisIdxCongr (byk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)m:Fin (n + 1 + 1)hi:m = i⊢ c i = c m subst hik: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Cj:Fin (n + 1 + 1)m:Fin (n + 1 + 1)hij:m ≠ jb:ComponentIdx (c ∘ m.succSuccAbove j)x:basisIdx (c m) × basisIdx (c j)⊢ c m = c m; rflAll goals completed! 🐙) x.1
  else if hj : m = j then basisIdxCongr (byk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)m:Fin (n + 1 + 1)hi:¬m = ihj:m = j⊢ c j = c m subst hjk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)m:Fin (n + 1 + 1)hi:¬m = ihij:i ≠ mb:ComponentIdx (c ∘ i.succSuccAbove m)x:basisIdx (c i) × basisIdx (c m)⊢ c m = c m; rflAll goals completed! 🐙) x.2
  else
    basisIdxCongr (unsolved goals
k:Typeinst✝⁵:CommRing kC G: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)m:Fin (n + 1 + 1)hi:¬m = ihj:¬m = j⊢ c (i.succSuccAbove j (i.predPredAbove j hij m ?m.127)) = c mbyk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)m:Fin (n + 1 + 1)hi:¬m = ihj:¬m = j⊢ (c ∘ i.succSuccAbove j) (i.predPredAbove j hij m ?m.127) = c m simpk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)m:Fin (n + 1 + 1)hi:¬m = ihj:¬m = j⊢ c (i.succSuccAbove j (i.predPredAbove j hij m ?m.127)) = c m)
    (b (Fin.predPredAbove i j hij m (byk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)m:Fin (n + 1 + 1)hi:¬m = ihj:¬m = j⊢ m ≠ i ∧ m ≠ j omegaAll goals completed! 🐙)))

              @[simp]
lemma declaration uses `sorry`ofFin_apply_fst {n : ℕ} {c : Fin (n + 1 + 1) → C}
    {i j : Fin (n + 1 + 1)} (hij : i ≠ j) (b : ComponentIdx (c ∘ Fin.succSuccAbove i j))
    (x : basisIdx (c i) × basisIdx (c j)) :
    ofFin (S := S) hij b x i = x.1 := byk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)⊢ ofFin hij b x i = x.1
  simp [ofFin]All goals completed! 🐙@[simp]
lemma declaration uses `sorry`ofFin_apply_snd {n : ℕ} {c : Fin (n + 1 + 1) → C}
    {i j : Fin (n + 1 + 1)} (hij : i ≠ j) (b : ComponentIdx (c ∘ Fin.succSuccAbove i j))
    (x : basisIdx (c i) × basisIdx (c j)) :
    ofFin (S := S) hij b x j = x.2 := byk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)⊢ ofFin hij b x j = x.2
  simp [ofFin]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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)⊢ ∀ (h : j = i), (basisIdxCongr ⋯) x.1 = x.2
  intro hk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)h:j = i⊢ (basisIdxCongr ⋯) x.1 = x.2
  omegaAll goals completed! 🐙lemma declaration uses `sorry`ofFin_mem_succSuccAboveSection {n : ℕ} {c : Fin (n + 1 + 1) → C}
    {i j : Fin (n + 1 + 1)} (hij : i ≠ j) (b : ComponentIdx (c ∘ Fin.succSuccAbove i j))
    (x : basisIdx (c i) × basisIdx (c j)) :
    ofFin (S := S) hij b x ∈ DropPairSection b := byk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)⊢ ofFin hij b x ∈ b.DropPairSection
  simp only [DropPairSection, Finset.mem_filter, Finset.mem_univ, true_and]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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)⊢ dropPair i j (ofFin hij b x) = b
  ext mk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)m:Fin n⊢ dropPair i j (ofFin hij b x) m = b m
  simp only [ofFin, dropPair, Fin.succSuccAbove_ne_fst, ↓reduceDIte, Fin.succSuccAbove_ne_snd,
    Function.comp_apply]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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)m:Fin n⊢ (basisIdxCongr ⋯) (b (i.predPredAbove j hij (i.succSuccAbove j m) ⋯)) = b m
  symmk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)m:Fin n⊢ b m = (basisIdxCongr ⋯) (b (i.predPredAbove j hij (i.succSuccAbove j m) ⋯))
  apply ComponentIdx.congr_rightk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)m:Fin n⊢ m = i.predPredAbove j hij (i.succSuccAbove j m) ⋯
  simpAll goals completed! 🐙

The equivalence between ContrSection b and basisIdx (c i) × basisIdx (c j).

def declaration uses `sorry`ofFinEquiv {n : ℕ} {c : Fin n.succ.succ → C}
    {i j : Fin (n + 1 + 1)} (hij : i ≠ j)
    (b : ComponentIdx (c ∘ Fin.succSuccAbove i j)) :
    basisIdx (c i) × basisIdx (c j) ≃ DropPairSection (S := S) b where
  invFun b' := ⟨b'.1 i, b'.1 j⟩
  toFun x := ⟨ofFin hij b x, ofFin_mem_succSuccAboveSection hij b x⟩
  right_inv b' := byk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin n.succ.succ → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)b':↥b.DropPairSection⊢ (fun x => ⟨ofFin hij b x, ⋯⟩) ((fun b' => (↑b' i, ↑b' j)) b') = b'
    ext mk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin n.succ.succ → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)b':↥b.DropPairSectionm:Fin (n + 1 + 1)⊢ ↑((fun x => ⟨ofFin hij b x, ⋯⟩) ((fun b' => (↑b' i, ↑b' j)) b')) m = ↑b' m
    simpk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin n.succ.succ → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)b':↥b.DropPairSectionm:Fin (n + 1 + 1)⊢ ofFin hij b (↑b' i, ↑b' j) m = ↑b' m
    rcases Fin.eq_or_exists_succSuccAbove i j hij m with rfl | rfl | ⟨m, rfl⟩inlk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin n.succ.succ → Cj:Fin (n + 1 + 1)m:Fin (n + 1 + 1)hij:m ≠ jb:ComponentIdx (c ∘ m.succSuccAbove j)b':↥b.DropPairSection⊢ ofFin hij b (↑b' m, ↑b' j) m = ↑b' minr.inlk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin n.succ.succ → Ci:Fin (n + 1 + 1)m:Fin (n + 1 + 1)hij:i ≠ mb:ComponentIdx (c ∘ i.succSuccAbove m)b':↥b.DropPairSection⊢ ofFin hij b (↑b' i, ↑b' m) m = ↑b' minr.inrk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin n.succ.succ → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)b':↥b.DropPairSectionm:Fin n⊢ ofFin hij b (↑b' i, ↑b' j) (i.succSuccAbove j m) = ↑b' (i.succSuccAbove j m)
    ·inlk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin n.succ.succ → Cj:Fin (n + 1 + 1)m:Fin (n + 1 + 1)hij:m ≠ jb:ComponentIdx (c ∘ m.succSuccAbove j)b':↥b.DropPairSection⊢ ofFin hij b (↑b' m, ↑b' j) m = ↑b' m simpAll goals completed! 🐙
    ·inr.inlk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin n.succ.succ → Ci:Fin (n + 1 + 1)m:Fin (n + 1 + 1)hij:i ≠ mb:ComponentIdx (c ∘ i.succSuccAbove m)b':↥b.DropPairSection⊢ ofFin hij b (↑b' i, ↑b' m) m = ↑b' m simpAll goals completed! 🐙
    ·inr.inrk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin n.succ.succ → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)b':↥b.DropPairSectionm:Fin n⊢ ofFin hij b (↑b' i, ↑b' j) (i.succSuccAbove j m) = ↑b' (i.succSuccAbove j m) simp [ofFin]inr.inrk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin n.succ.succ → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)b':↥b.DropPairSectionm:Fin n⊢ (basisIdxCongr ⋯) (b (i.predPredAbove j hij (i.succSuccAbove j m) ⋯)) = ↑b' (i.succSuccAbove j m)
      obtain ⟨b', hb'⟩ := b'inr.inrk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin n.succ.succ → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)m:Fin nb':ComponentIdx chb':b' ∈ b.DropPairSection⊢ (basisIdxCongr ⋯) (b (i.predPredAbove j hij (i.succSuccAbove j m) ⋯)) = ↑⟨b', hb'⟩ (i.succSuccAbove j m)
      simp only [mem_iff_apply_succSuccAbove_eq] at hb'inr.inrk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin n.succ.succ → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)m:Fin nb':ComponentIdx chb'✝:b' ∈ b.DropPairSectionhb':∀ (m : Fin n), b' (i.succSuccAbove j m) = b m⊢ (basisIdxCongr ⋯) (b (i.predPredAbove j hij (i.succSuccAbove j m) ⋯)) = ↑⟨b', hb'⟩ (i.succSuccAbove j m)
      simp [hb']inr.inrk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin n.succ.succ → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)m:Fin nb':ComponentIdx chb'✝:b' ∈ b.DropPairSectionhb':∀ (m : Fin n), b' (i.succSuccAbove j m) = b m⊢ (basisIdxCongr ⋯) (b (i.predPredAbove j hij (i.succSuccAbove j m) ⋯)) = b m
      symminr.inrk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin n.succ.succ → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)m:Fin nb':ComponentIdx chb'✝:b' ∈ b.DropPairSectionhb':∀ (m : Fin n), b' (i.succSuccAbove j m) = b m⊢ b m = (basisIdxCongr ⋯) (b (i.predPredAbove j hij (i.succSuccAbove j m) ⋯))
      apply ComponentIdx.congr_rightinr.inrk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin n.succ.succ → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)m:Fin nb':ComponentIdx chb'✝:b' ∈ b.DropPairSectionhb':∀ (m : Fin n), b' (i.succSuccAbove j m) = b m⊢ m = i.predPredAbove j hij (i.succSuccAbove j m) ⋯
      simpAll goals completed! 🐙
  left_inv x := byk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin n.succ.succ → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)⊢ (fun b' => (↑b' i, ↑b' j)) ((fun x => ⟨ofFin hij b x, ⋯⟩) x) = x
    simpAll goals completed! 🐙

@[simp]
lemma ofFinEquiv_apply_fst {n : ℕ} {c : Fin (n + 1 + 1) → C}
    {i j : Fin (n + 1 + 1)} (hij : i ≠ j) (b : ComponentIdx (c ∘ Fin.succSuccAbove i j))
    (x : basisIdx (c i) × basisIdx (c j)) :
    (ofFinEquiv (S := S) hij b x).1 i = x.1 := byk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)⊢ ↑((ofFinEquiv hij b) x) i = x.1
  simp [ofFinEquiv]All goals completed! 🐙

@[simp]
lemma ofFinEquiv_apply_snd {n : ℕ} {c : Fin (n + 1 + 1) → C}
    {i j : Fin (n + 1 + 1)} (hij : i ≠ j) (b : ComponentIdx (c ∘ Fin.succSuccAbove i j))
    (x : basisIdx (c i) × basisIdx (c j)) :
    (ofFinEquiv (S := S) hij b x).1 j = x.2 := byk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx (c ∘ i.succSuccAbove j)x:basisIdx (c i) × basisIdx (c j)⊢ ↑((ofFinEquiv hij b) x) j = x.2
  simp [ofFinEquiv]All goals completed! 🐙