From 32aa6e7aff8f0c708f0f5070a44dc3673a73f7fa Mon Sep 17 00:00:00 2001 From: Andrea Pari Date: Mon, 27 Jul 2026 16:15:58 +0100 Subject: [PATCH 1/9] feat(Tensors/Reindexing): index-map and reindexing lemmas for slot-addressed contraction MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The finite-index groundwork for contracting a named slot of one tensor against a named slot of another. `SuccSuccAbove.lean` gains `Fin.reinsert_castAdd` and `Fin.reinsert_natAdd`: reinserting a surviving slot after removing one slot from each block of `Fin ((nA + 1) + (nB + 1))`. Unlike the neighbouring `succSuccAbove_natAdd_apply_castAdd`, the two removed slots straddle the two blocks, which is why the statements carry the reshaping `Fin.cast`s. `Reindexing.lean` gains a `Fin` section for the `Fin.append` and `Fin.succAbove` maps its reindexings are built from: the block-swap and block-reassembly value lemmas, `append_succAbove_const_eq_cycleIcc` and `cycleIcc_last_symm_apply_succAbove` identifying "move slot `i` to the end" with the cycle `[i, last]`, `exists_succAbove_comm` restricting an injection to the survivors of a slot, and two lemmas pinning a reshaped slot to its literal value. `Fin.append_castAdd_cast` and `Fin.append_natAdd_cast`, reassembling the blocks after casting one of them, are stated as equalities of index maps rather than of `.val`, which is the underlying fact; the `.val` form follows from `Fin.val_cast`. At the `IsReindexing` level it gains `succAbove_of_succAbove_eq`, the survivor reindexing obtained from a caller-supplied `Fin.succAbove` square rather than from `σ` as in `succAbove`, and `moveLast`, which splits a color list at an arbitrary slot and generalises `append_succ_last`. The `_of_` names the hypothesis the lemma takes rather than a case of the trichotomy `succAbove` unifies, and `_eq` rather than `_comm`, which this file reserves for lemmas whose conclusion is that two index-map operations commute. `Tensor.permT_injective` records that a reindexing is injective. Co-authored-by: Claude Opus 4.8 --- Physlib/Relativity/Tensors/Basic.lean | 6 + .../Tensors/Contraction/SuccSuccAbove.lean | 31 +++++ Physlib/Relativity/Tensors/Reindexing.lean | 125 ++++++++++++++++++ 3 files changed, 162 insertions(+) diff --git a/Physlib/Relativity/Tensors/Basic.lean b/Physlib/Relativity/Tensors/Basic.lean index fad9622ff..2b73a5e67 100644 --- a/Physlib/Relativity/Tensors/Basic.lean +++ b/Physlib/Relativity/Tensors/Basic.lean @@ -628,6 +628,12 @@ lemma permT_eq_zero_iff {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C} funext x simp [IsReindexing.inv_apply_apply] +/-- `permT` is injective. -/ +lemma permT_injective {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C} + {σ : Fin m → Fin n} (h : IsReindexing c c1 σ) : + Function.Injective (permT (S := S) σ h) := + (injective_iff_map_eq_zero' _).mpr (permT_eq_zero_iff h) + /-! ## field -/ diff --git a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean index d5e1a0a6d..484170ca2 100644 --- a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean +++ b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean @@ -231,6 +231,37 @@ lemma succSuccAbove_natAdd_apply_castAdd {n n1 : ℕ} simp only [Fin.ext_iff, succSuccAbove_val, natAdd, castAdd] grind (splits := 20) +/-- Reinserting a left-block survivor `a` after removing the `i`-th slot of the left block and the + `j`-th slot of the right block of `Fin ((nA + 1) + (nB + 1))`, the removal read at the contracted + length `(nA + nB) + 1 + 1`. Unlike `succSuccAbove_natAdd_apply_castAdd` the two holes straddle the + two blocks, so the statement carries the reshaping `Fin.cast`s. -/ +lemma reinsert_castAdd {nA nB : ℕ} (i : Fin (nA + 1)) (j : Fin (nB + 1)) + (a : Fin nA) : + Fin.cast (show (nA + nB) + 1 + 1 = (nA + 1) + (nB + 1) by omega) + ((Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 by omega) + (Fin.castAdd (nB + 1) i)).succSuccAbove + (Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 by omega) + (Fin.natAdd (nA + 1) j)) (Fin.castAdd nB a)) + = Fin.castAdd (nB + 1) (i.succAbove a) := by + apply Fin.ext + simp only [Fin.succSuccAbove_val, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd, + Fin.succAbove, Fin.lt_def, Fin.val_castSucc, Fin.val_succ, apply_ite Fin.val] + split_ifs <;> omega + +/-- Reinserting a right-block survivor, the mirror of `Fin.reinsert_castAdd`. -/ +lemma reinsert_natAdd {nA nB : ℕ} (i : Fin (nA + 1)) (j : Fin (nB + 1)) + (a : Fin nB) : + Fin.cast (show (nA + nB) + 1 + 1 = (nA + 1) + (nB + 1) by omega) + ((Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 by omega) + (Fin.castAdd (nB + 1) i)).succSuccAbove + (Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 by omega) + (Fin.natAdd (nA + 1) j)) (Fin.natAdd nA a)) + = Fin.natAdd (nA + 1) (j.succAbove a) := by + apply Fin.ext + simp only [Fin.succSuccAbove_val, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd, Fin.succAbove, + Fin.lt_def, Fin.val_castSucc, Fin.val_succ, apply_ite Fin.val] + split_ifs <;> omega + lemma succSuccAbove_natAdd_image_range_castAdd {n n1 : ℕ} (i j : Fin (n + 1 + 1)) : (succSuccAbove (n := n1 + n) (Fin.natAdd n1 i) (Fin.natAdd n1 j)) '' diff --git a/Physlib/Relativity/Tensors/Reindexing.lean b/Physlib/Relativity/Tensors/Reindexing.lean index 8c81e7ce6..bff88d4a7 100644 --- a/Physlib/Relativity/Tensors/Reindexing.lean +++ b/Physlib/Relativity/Tensors/Reindexing.lean @@ -32,6 +32,96 @@ We are interested in the interaction of reindexing with the following operations open Module +namespace Fin + +/-! + +## Index 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`. + +-/ + +/-- The `.val` of the block-swap map, as a piecewise-linear function. -/ +lemma append_swap_val (n n2 : ℕ) (x : Fin (n2 + n)) : + (Fin.append (Fin.natAdd n) (Fin.castAdd n2) x).val = + if x.val < n2 then n + x.val else x.val - n2 := by + refine Fin.addCases (fun i => ?_) (fun i => ?_) x + · simp [Fin.append_left] + · simp [Fin.append_right] + +/-- 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)) := by + simpa using Fin.append_castAdd_natAdd (f := (id : Fin (m + n) → Fin (m + n))) + +/-- Reassembling the blocks of `Fin (na + n2)` after casting the left one along `na = nb` is the + cast of the total length. -/ +lemma append_castAdd_cast (na nb n2 : ℕ) (heq : na = nb) : + Fin.append (Fin.castAdd n2 ∘ Fin.cast heq) (Fin.natAdd nb) = + Fin.cast (show na + n2 = nb + n2 by omega) := by + subst heq + simpa using append_castAdd_natAdd_eq_id + +/-- Reassembling the blocks of `Fin (n2 + na)` after casting the right one along `na = nb` is the + cast of the total length. The right-block mirror of `Fin.append_castAdd_cast`. -/ +lemma append_natAdd_cast (na nb n2 : ℕ) (heq : na = nb) : + Fin.append (Fin.castAdd nb) (Fin.natAdd n2 ∘ Fin.cast heq) = + Fin.cast (show n2 + na = n2 + nb by omega) := by + subst heq + simpa using append_castAdd_natAdd_eq_id + +/-- 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)`. -/ +lemma append_succAbove_const_eq_cycleIcc {n : ℕ} (i : Fin (n + 1)) : + Fin.append i.succAbove (fun _ : Fin 1 => i) = ⇑(Fin.cycleIcc i (Fin.last n)) := by + funext y + refine Fin.addCases (fun a => ?_) (fun a => ?_) y + · rw [Fin.append_left] + have h := congrFun (Fin.cycleIcc_comp_succAbove i (Fin.last n) (Fin.le_last i)) a + rw [Fin.succAbove_last] at h + exact h.symm + · rw [Fin.append_right] + have : (Fin.natAdd n a : Fin (n + 1)) = Fin.last n := by + apply Fin.ext; simp [Fin.val_natAdd] + rw [this, Fin.cycleIcc_of_le_of_le (Fin.le_last _) (Fin.le_last _), if_pos rfl] + +/-- The inverse of the cycle `[i, last]` carries the reinserted survivor `i.succAbove a` back to + its position `a` in the survivor block. -/ +lemma cycleIcc_last_symm_apply_succAbove {n : ℕ} (i : Fin (n + 1)) (a : Fin n) : + (Fin.cycleIcc i (Fin.last n)).symm (i.succAbove a) = Fin.castAdd 1 a := + (Equiv.symm_apply_eq _).2 (by rw [← append_succAbove_const_eq_cycleIcc i, Fin.append_left]) + +/-- An injection `σ` of `Fin (n + 1)` restricts to the survivors of a slot `i`: there is a map + `σ'` filling the square `(σ i).succAbove ∘ σ' = σ ∘ i.succAbove`, carrying the complement of `i` + to the complement of `σ i`. -/ +lemma exists_succAbove_comm {n : ℕ} {σ : Fin (n + 1) → Fin (n + 1)} (hσ : Function.Injective σ) + (i : Fin (n + 1)) : ∃ σ' : Fin n → Fin n, (σ i).succAbove ∘ σ' = σ ∘ i.succAbove := + ⟨fun a => (Fin.exists_succAbove_eq (hσ.ne (Fin.succAbove_ne i a))).choose, + funext fun a => (Fin.exists_succAbove_eq (hσ.ne (Fin.succAbove_ne i a))).choose_spec⟩ + +/-- A `Fin.cast` of a left-block injection is the literal slot `⟨v, _⟩` at the same value `v`. + + Stated at `Fin` level rather than `.val` level so that a rewrite replaces the composite before + `Fin.succSuccAbove_val` builds its `ite` conditions on it, keeping the generated `Decidable` + instances in sync with the reduced conditions. -/ +lemma cast_castAdd_eq_mk {n m N : ℕ} (h : n + m = N) {i : Fin n} {v : ℕ} (hv : i.val = v) : + Fin.cast h (Fin.castAdd m i) = + ⟨v, by subst h hv; exact Nat.lt_of_lt_of_le i.isLt (Nat.le_add_right n m)⟩ := + Fin.ext (by simp [hv]) + +/-- A `Fin.cast` of a right-block injection is the literal slot `⟨v, _⟩` at the offset value `v`. + See `Fin.cast_castAdd_eq_mk` for why the `Fin`-level statement matters. -/ +lemma cast_natAdd_eq_mk {n m N : ℕ} (h : n + m = N) {i : Fin m} {v : ℕ} + (hv : n + i.val = v) : + Fin.cast h (Fin.natAdd n i) = + ⟨v, by subst h hv; exact Nat.add_lt_add_left i.isLt n⟩ := + Fin.ext (by simp [hv]) + +end Fin + namespace TensorSpecies variable {k : Type} [CommRing k] {C : Type} {G : Type} [Group G] @@ -364,6 +454,23 @@ lemma succAbove {n n1 : ℕ} {c : Fin (n + 1) → C} {c1 : Fin (n1 + 1) → C} · simpa [hi] using IsReindexing.succAbove_of_eq_zero i h hi · simpa [hi] using IsReindexing.succAbove_of_neq_zero i h hi +/-- 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. -/ +lemma succAbove_of_succAbove_eq {n : ℕ} {c c1 : Fin (n + 1) → C} + {σ : Fin (n + 1) → Fin (n + 1)} {σ' : Fin n → Fin n} (i : Fin (n + 1)) + (h : IsReindexing c c1 σ) (hσ' : (σ i).succAbove ∘ σ' = σ ∘ i.succAbove) : + IsReindexing (c ∘ (σ i).succAbove) (c1 ∘ i.succAbove) σ' := by + have key : ∀ a, (σ i).succAbove (σ' a) = σ (i.succAbove a) := congrFun hσ' + refine ⟨Finite.injective_iff_bijective.mp (fun a b hab => ?_), fun a => ?_⟩ + · exact Fin.succAbove_right_injective (h.injective (by rw [← key a, ← key b, hab])) + · simpa only [Function.comp_apply, key a] using h.2 (i.succAbove a) + /-- 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`. @@ -472,6 +579,24 @@ lemma append_succ_last {n : ℕ} (c : Fin (n + 1) → C) : · simp only [Fin.append_left, Function.comp_apply]; rfl · fin_cases i; simp only [Fin.append_right, Matrix.cons_val_fin_one]; rfl +/-- 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. -/ +lemma moveLast {n : ℕ} {c : Fin (n + 1) → C} {c1 : Fin 2 → C} (i : Fin (n + 1)) + (hc : c i = c1 1) : + IsReindexing c + (Fin.append (c ∘ i.succAbove) (c1 ∘ (0 : Fin 2).succAbove)) + (Fin.append i.succAbove (fun _ : Fin 1 => i)) := + ⟨by + rw [Fin.append_succAbove_const_eq_cycleIcc i] + exact (Fin.cycleIcc i (Fin.last n)).bijective, + fun x => by + refine Fin.addCases (fun a => ?_) (fun a => ?_) x + · simp [Fin.append_left] + · fin_cases a + simp [Fin.append_right, hc]⟩ + /-- 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`. -/ From 17ada18497793a2369eea14bf03a31ace469cd95 Mon Sep 17 00:00:00 2001 From: Andrea Pari Date: Mon, 27 Jul 2026 16:16:12 +0100 Subject: [PATCH 2/9] feat(Tensors/Contraction): pure-tensor congruences and prodT_contrT_fst `Pure.contrPCoeff_congr` says the contraction coefficient is insensitive to its proof arguments once the two contracted slots agree, the pure-level mirror of `contrT_congr`. `Pure.permP_dropPair_dropPair_congr` and `Pure.permP_dropPair_permP_congr` compare two towers of `permP` and `dropPair` over a common pure tensor: they agree as soon as the composite slot maps agree pointwise. Stating the comparison this way keeps every slot map an opaque variable, so it closes by syntactic unification rather than by `whnf`-reducing the color and index-map composites, which is what makes the rank-two chain calculations tractable. `prodT_contrT_fst` contracts two slots of the first factor of a product, the mirror of the existing `prodT_contrT_snd`. Co-authored-by: Claude Opus 4.8 --- .../Tensors/Contraction/Products.lean | 17 +++++ .../Relativity/Tensors/Contraction/Pure.lean | 64 +++++++++++++++++++ 2 files changed, 81 insertions(+) diff --git a/Physlib/Relativity/Tensors/Contraction/Products.lean b/Physlib/Relativity/Tensors/Contraction/Products.lean index 0d95a6abb..3ccc999bf 100644 --- a/Physlib/Relativity/Tensors/Contraction/Products.lean +++ b/Physlib/Relativity/Tensors/Contraction/Products.lean @@ -153,6 +153,23 @@ lemma contrT_prodT_snd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} rw [prodT_contrT_snd] simp +/-- A contraction internal to the left factor commutes past the outer product with a right + spectator. The mirror of `prodT_contrT_snd`, obtained from it by `prodT_swap`, so the right-hand + side contracts the swapped product `prodT t1 t` and carries a block swap. -/ +lemma prodT_contrT_fst {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} + {c1 : Fin n1 → C} + (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j) + (t : Tensor S c) (t1 : Tensor S c1) : + prodT (contrT n i j hij t) t1 = + permT _ IsReindexing.append_swap + (permT id (IsReindexing.append_succSuccAbove_natAdd i j) <| + contrT _ + (Fin.natAdd n1 i) + (Fin.natAdd n1 j) + (by simpa using hij) <| + prodT t1 t) := by + rw [prodT_swap, prodT_contrT_snd] + end Tensor end TensorSpecies diff --git a/Physlib/Relativity/Tensors/Contraction/Pure.lean b/Physlib/Relativity/Tensors/Contraction/Pure.lean index 87e256b57..8bd7bae9b 100644 --- a/Physlib/Relativity/Tensors/Contraction/Pure.lean +++ b/Physlib/Relativity/Tensors/Contraction/Pure.lean @@ -133,6 +133,60 @@ lemma dropPair_permP {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} · simp [hσ.2] · simp [hσ.2] +/-- Two `permP`–`dropPair`–`dropPair` towers over a common pure tensor agree once their composite + slot maps agree pointwise. Comparing two orders of dropping two pairs of slots this way keeps + every slot map an opaque variable, so the comparison closes by unification rather than by + `whnf`-reducing the color and index-map composites. -/ +lemma permP_dropPair_dropPair_congr {nP nOut : ℕ} + {c : Fin (nP + 1 + 1 + 1 + 1) → C} {cOut : Fin nOut → C} (p : Pure S c) + (aL bL : Fin (nP + 1 + 1 + 1 + 1)) (habL : aL ≠ bL) + (a2L b2L : Fin (nP + 1 + 1)) (hab2L : a2L ≠ b2L) + (σ1L : Fin nOut → Fin nP) + (h1L : IsReindexing ((c ∘ Fin.succSuccAbove aL bL) ∘ Fin.succSuccAbove a2L b2L) cOut σ1L) + (aR bR : Fin (nP + 1 + 1 + 1 + 1)) (habR : aR ≠ bR) + (a2R b2R : Fin (nP + 1 + 1)) (hab2R : a2R ≠ b2R) + (σ1R : Fin nOut → Fin nP) + (h1R : IsReindexing ((c ∘ Fin.succSuccAbove aR bR) ∘ Fin.succSuccAbove a2R b2R) cOut σ1R) + (hslot : ∀ m : Fin nOut, + Fin.succSuccAbove aL bL (Fin.succSuccAbove a2L b2L (σ1L m)) = + Fin.succSuccAbove aR bR (Fin.succSuccAbove a2R b2R (σ1R m))) : + permP σ1L h1L (dropPair a2L b2L hab2L (dropPair aL bL habL p)) = + permP σ1R h1R (dropPair a2R b2R hab2R (dropPair aR bR habR p)) := by + funext m + simp only [permP, dropPair] + exact congr_mid (cOut m) p _ _ (hslot m) (h1L.preserve_color m).symm + (h1R.preserve_color m).symm + +/-- Two `permP`–`dropPair`–`permP` towers over a common pure tensor agree once their composite + slot maps agree pointwise. The one-contraction, inner-relabelled sibling of + `permP_dropPair_dropPair_congr`. -/ +lemma permP_dropPair_permP_congr {nP nOut mL mR : ℕ} + {c : Fin nP → C} {cL : Fin (mL + 1 + 1) → C} {cR : Fin (mR + 1 + 1) → C} + {cOut : Fin nOut → C} (p : Pure S c) + (σ0L : Fin (mL + 1 + 1) → Fin nP) (h0L : IsReindexing c cL σ0L) + (aL bL : Fin (mL + 1 + 1)) (habL : aL ≠ bL) + (σ1L : Fin nOut → Fin mL) + (h1L : IsReindexing (cL ∘ Fin.succSuccAbove aL bL) cOut σ1L) + (σ0R : Fin (mR + 1 + 1) → Fin nP) (h0R : IsReindexing c cR σ0R) + (aR bR : Fin (mR + 1 + 1)) (habR : aR ≠ bR) + (σ1R : Fin nOut → Fin mR) + (h1R : IsReindexing (cR ∘ Fin.succSuccAbove aR bR) cOut σ1R) + (hslot : ∀ m : Fin nOut, + σ0L (Fin.succSuccAbove aL bL (σ1L m)) = σ0R (Fin.succSuccAbove aR bR (σ1R m))) : + permP σ1L h1L (dropPair aL bL habL (permP σ0L h0L p)) = + permP σ1R h1R (dropPair aR bR habR (permP σ0R h0R p)) := by + funext m + simp only [permP, dropPair] + -- Each side is a two-`cast` tower, one cast from the inner `permP` and one from the outer + -- `permP`-after-`dropPair`. `LinearEquiv.cast` is defeq to `_root_.cast`, so drop to the plain + -- cast, fuse the tower with `cast_cast`, and close with the single-cast lemma `congr_mid`. + change _root_.cast _ (_root_.cast _ (p _)) = + _root_.cast _ (_root_.cast _ (p _)) + simp only [_root_.cast_cast] + exact congr_mid (cOut m) p _ _ (hslot m) + ((h0L.2 _).trans (h1L.2 m)) + ((h0R.2 _).trans (h1R.2 m)) + /-! ## Contraction coefficient @@ -146,6 +200,16 @@ noncomputable def contrPCoeff {n : ℕ} {c : Fin n → C} (i j : Fin n) (hij : i ≠ j ∧ S.τ (c i) = c j) (p : Pure S c) : k := S.contr (c i) (p i ⊗ₜ (LinearEquiv.cast (R := k) (by simp [hij.2]) (p j))) +/-- `contrPCoeff` is insensitive to its proof arguments once the two contracted slots agree. Lets a + coefficient comparison rewrite the slots without a `congr` search through the proof fields. -/ +lemma contrPCoeff_congr {n : ℕ} {c : Fin n → C} (p : Pure S c) + {i i' j j' : Fin n} (hi : i = i') (hj : j = j') + {hij : i ≠ j ∧ S.τ (c i) = c j} {hij' : i' ≠ j' ∧ S.τ (c i') = c j'} : + p.contrPCoeff i j hij = p.contrPCoeff i' j' hij' := by + subst hi + subst hj + rfl + attribute [-simp] LinearEquiv.cast_apply @[simp] From fb9bed1579e3fcd253dd5471b65427139ff143aa Mon Sep 17 00:00:00 2001 From: Andrea Pari Date: Mon, 27 Jul 2026 16:16:12 +0100 Subject: [PATCH 3/9] feat(Tensors/Contraction): crossToEnd, the slot-addressed cross contraction MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `contrT` contracts two slots of a single tensor. Contracting a slot of one tensor against a slot of another, which is what pairing a tensor with one of a theory's special tensors amounts to, means forming the product by hand, tracking where each slot lands, and discharging the distinctness and duality goals at every call site. `crossToEnd i j hc` packages that: `prodT` then `contrT`, with the wrapper locating the two post-product slots, discharging the proofs, and normalising the output color to `Fin.append (cA ∘ i.succAbove) (cB ∘ j.succAbove)` — left survivors, then right, gaps closed — so a chain composes without hand-inserted recasts. The slots are named arguments, so any slot, interior included, is reached directly. Proved on it: the value at concrete rank two (`crossToEnd_two`), equivariance, the two `permT` commutators moving a relabelling of either factor through the contraction, and `crossToEnd_assoc_rankTwo`, which rebrackets the metric chain `A —(iA·0)— B —(last·0)— C` at rank-two `B` and `C` up to `permT id`. That regrouping is what lets a metric and its inverse be collapsed first; it is not associativity in general. Its surviving-slot identity pins the reshaped slots to their literals so that `succSuccAbove_val` fires, then closes the nested reinsertion conditionals with `grind (splits := 20)`, the tactic `SuccSuccAbove.lean` already uses for this shape of goal. Co-authored-by: Claude Opus 4.8 --- Physlib.lean | 1 + .../Tensors/Contraction/CrossToEnd.lean | 345 ++++++++++++++++++ 2 files changed, 346 insertions(+) create mode 100644 Physlib/Relativity/Tensors/Contraction/CrossToEnd.lean diff --git a/Physlib.lean b/Physlib.lean index d8e7ea52a..e8da6533e 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -404,6 +404,7 @@ public import Physlib.Relativity.Tensors.Conjugation.Basic public import Physlib.Relativity.Tensors.Constructors public import Physlib.Relativity.Tensors.Contraction.Basic public import Physlib.Relativity.Tensors.Contraction.Basis +public import Physlib.Relativity.Tensors.Contraction.CrossToEnd public import Physlib.Relativity.Tensors.Contraction.Products public import Physlib.Relativity.Tensors.Contraction.Pure public import Physlib.Relativity.Tensors.Contraction.SuccSuccAbove diff --git a/Physlib/Relativity/Tensors/Contraction/CrossToEnd.lean b/Physlib/Relativity/Tensors/Contraction/CrossToEnd.lean new file mode 100644 index 000000000..dbbe38c60 --- /dev/null +++ b/Physlib/Relativity/Tensors/Contraction/CrossToEnd.lean @@ -0,0 +1,345 @@ +/- +Copyright (c) 2026 Andrea Pari. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Andrea Pari +-/ +module + +public import Physlib.Relativity.Tensors.Contraction.Products +/-! + +# Cross contraction at named slots + +## i. Overview + +`contrT` contracts two slots of a single tensor. Contracting a slot of one tensor against a slot of +another (`T^{μν} u_ν`, `g_{μν} v^ν`) is `prodT` then `contrT`, which leaves every call site to +locate the two post-product slots and discharge the distinctness and `τ`-duality goals. + +`crossToEnd i j hc` packages that move at named slots `i` and `j`, with `hc : S.τ (cA i) = cB j` +recording their `τ`-duality and output color `Fin.append (cA ∘ i.succAbove) (cB ∘ j.succAbove)`, +left survivors then right. Any slot is reachable: `crossToEnd 2 0 _ R u` reads as `R_{μνρσ} u^ρ`. +Survivors at the end make the output an append, so both bracketings of a chain produce the same +survivor list. The complementary convention, keeping the replacement index in place +(`T^{μ}{}_{νρ} ↦ T_{μνρ}`), is `crossToSlot`, built on this substrate in +`Physlib.Relativity.Tensors.Contraction.CrossToSlot`. + +## ii. Key results + +- `TensorSpecies.Tensor.crossToEnd` : the slot-addressed cross contraction. +- `TensorSpecies.Tensor.crossToEnd_two` : at rank two on each factor, a plain `contrT` of the + product on slots `1, 2`. +- `TensorSpecies.Tensor.crossToEnd_equivariant` : the contraction commutes with the `G`-action. +- `TensorSpecies.Tensor.crossToEnd_assoc_rankTwo` : rebracket the chain + `A —(iA·0)— B —(last·0)— C` at rank-two `B` and `C`, up to `permT id`. Not full associativity. +- `TensorSpecies.Tensor.crossToEnd_permT_left` / `crossToEnd_permT_right` : move a relabelling of + the left or right factor through the contraction, the contracted slot moving with it. + +## iii. Table of contents + +- A. Slot-addressed cross contraction +- B. Equivariance +- C. Rebracketing the metric chain +- D. Permutation commutators + +## iv. References + +-/ + +@[expose] public section + +namespace TensorSpecies + +variable {k : Type} [CommRing k] {C : Type} {G : Type} [Group G] + {V : C → Type} [∀ c, AddCommGroup (V c)] [∀ c, Module k (V c)] + {basisIdx : C → Type} [∀ c, Fintype (basisIdx 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} + +namespace Tensor + +open Fin + +/-! + +## A. Slot-addressed cross contraction + +-/ + +/-- Slot-addressed cross contraction: contract slot `i` of `t1` against slot `j` of `t2`. The + survivors are `t1`'s slots except `i` followed by `t2`'s slots except `j`, so the output color is + a clean `Fin (nA + nB) → C` and a chain composes without recasts. -/ +noncomputable def crossToEnd {nA nB : ℕ} {cA : Fin (nA + 1) → C} {cB : Fin (nB + 1) → C} + (i : Fin (nA + 1)) (j : Fin (nB + 1)) (hc : S.τ (cA i) = cB j) : + Tensor S cA →ₗ[k] Tensor S cB →ₗ[k] + Tensor S (Fin.append (cA ∘ i.succAbove) (cB ∘ j.succAbove)) := + LinearMap.compr₂ prodT <| + permT id + (by + refine ⟨Function.bijective_id, fun m => ?_⟩ + simp only [id_eq, Function.comp_apply] + refine Fin.addCases (fun a => ?_) (fun a => ?_) m + · rw [Fin.reinsert_castAdd i j a] + simp only [Fin.append_left, Function.comp_apply] + · rw [Fin.reinsert_natAdd i j a] + simp only [Fin.append_right, Function.comp_apply]) ∘ₗ + contrT (nA + nB) + (Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 by omega) (Fin.castAdd (nB + 1) i)) + (Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 by omega) (Fin.natAdd (nA + 1) j)) + (by + refine ⟨Fin.ne_of_val_ne ?_, ?_⟩ + · simp only [Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd]; omega + · simp only [Function.comp_apply, Fin.cast_cast, Fin.cast_eq_self, + Fin.append_left, Fin.append_right] + exact hc) ∘ₗ + permT (Fin.cast (show (nA + nB) + 1 + 1 = (nA + 1) + (nB + 1) by omega)) + (IsReindexing.fin_cast_isReindexing _ _ (by omega)) + +/-- Cross-contracting the last slot of a rank-2 tensor `A` with the `0`-slot of a rank-2 tensor `B` + is a plain `contrT` of their product on the middle slots `1, 2`, up to a color recast. Discharging + the slot arithmetic once lets a `contrT`-level identity lift to `crossToEnd` by one rewrite. -/ +lemma crossToEnd_two {cA cB : Fin 2 → C} (h : S.τ (cA (Fin.last 1)) = cB 0) + (A : Tensor S cA) (B : Tensor S cB) : + crossToEnd (Fin.last 1) (0 : Fin 2) h A B + = permT (id : Fin 2 → Fin 2) (IsReindexing.on_id.mpr (fun i => by fin_cases i <;> rfl)) + (contrT 2 (1 : Fin 4) (2 : Fin 4) + (by + refine ⟨by decide, ?_⟩ + rw [show (1 : Fin 4) = Fin.castAdd 2 (1 : Fin 2) from rfl, + show (2 : Fin 4) = Fin.natAdd 2 (0 : Fin 2) from rfl, + Fin.append_left, Fin.append_right] + exact h) + (prodT A B)) := by + simp only [crossToEnd, LinearMap.compr₂_apply, LinearMap.comp_apply] + rw [contrT_permT, contrT_congr (n := 2) 1 2 _ (by rfl) (by rfl)] + simp only [permT_permT, CompTriple.comp_eq] + refine permT_congr ?_ rfl + ext i + fin_cases i <;> rfl + +/-! + +## B. Equivariance + +`crossToEnd i j hc` is the curried bilinear map `LinearMap.compr₂ prodT` post-composed with the +linear `permT`/`contrT` factors, so additivity, scalar multiplication, and finite sums in either +argument are already the generic `map_add`/`map_smul`/`map_sum` and need no lemmas of their own. + +-/ + +/-- Cross contraction is `G`-equivariant, each of `prodT`, `contrT` and `permT` being so. -/ +@[simp] +lemma crossToEnd_equivariant {nA nB : ℕ} {cA : Fin (nA + 1) → C} {cB : Fin (nB + 1) → C} + (i : Fin (nA + 1)) (j : Fin (nB + 1)) (hc : S.τ (cA i) = cB j) (g : G) + (t1 : Tensor S cA) (t2 : Tensor S cB) : + crossToEnd i j hc (g • t1) (g • t2) = g • crossToEnd i j hc t1 t2 := by + simp only [crossToEnd, LinearMap.compr₂_apply, LinearMap.comp_apply, prodT_equivariant, + contrT_equivariant, permT_equivariant] + +/-! + +## C. Rebracketing the metric chain + +Both bracketings reduce to one product contracted at its two seams in opposite order, then drop to +the pure-tensor level, so the seam permutation never crosses a contraction under `whnf`; +`Pure.permP_dropPair_dropPair_congr` closes the step. + +-/ + +/-- Rebracket the chain `A —(iA·0)— B —(last·0)— C` for rank-two `B` and `C`: contracting `A·B` + first and then `·C` equals contracting `B·C` first and then `A·`, up to the color recast + `permT id`. + + Not full associativity: only `A`'s attachment slot `iA` is free. `B`'s rank two is what makes the + statement possible, the second contraction being addressed at `Fin.last nA`, the slot `B`'s unique + survivor occupies in `A·B`. Other slots are reached by conjugating with the `permT` commutators. + + With `A := T`, `B := g`, `C := g⁻¹` this reassociates `(T·g)·g⁻¹` to `T·(g·g⁻¹)`, after which + `g·g⁻¹` collapses to the unit tensor: the step behind raising then lowering a named index. -/ +lemma crossToEnd_assoc_rankTwo {nA : ℕ} + {cA : Fin (nA + 1) → C} {cB cC : Fin 2 → C} + (iA : Fin (nA + 1)) + (hc1 : S.τ (cA iA) = cB 0) + (hc2 : S.τ (cB (Fin.last 1)) = cC 0) + (tA : Tensor S cA) (tB : Tensor S cB) (tC : Tensor S cC) : + crossToEnd (Fin.last nA) 0 + (by + rw [show (Fin.last nA : Fin (nA + 1)) = Fin.natAdd nA (Fin.last 0) from + Fin.ext (by simp), Fin.append_right, Function.comp_apply, Fin.succAbove_zero, + Fin.succ_last] + exact hc2) + (crossToEnd iA 0 hc1 tA tB) tC = + permT id + (IsReindexing.on_id.mpr fun i => by + refine Fin.addCases (fun a => ?_) (fun a => ?_) i + · simp only [Fin.append_left, Function.comp_apply, Fin.succAbove_last, + show a.castSucc = Fin.castAdd 1 a from rfl, Fin.append_left] + · simp only [Fin.append_right, Function.comp_apply, Fin.succAbove_zero] + fin_cases a + rfl) + (crossToEnd iA 0 + (by + rw [show (0 : Fin (1 + 1)) = Fin.castAdd 1 (0 : Fin 1) from rfl, Fin.append_left, + Function.comp_apply, Fin.succAbove_last, Fin.castSucc_zero] + exact hc1) + tA + (crossToEnd (Fin.last 1) 0 hc2 tB tC)) := by + simp only [crossToEnd, LinearMap.compr₂_apply, LinearMap.comp_apply, permT_permT] + conv_rhs => rw [prodT_permT_right, prodT_contrT_snd] + conv_lhs => rw [prodT_permT_left, prodT_contrT_fst] + rw [prodT_swap tC, prodT_permT_left] + conv_rhs => rw [prodT_permT_right, prodT_assoc' tA tB tC] + simp only [permT_permT] + generalize (prodT (prodT tA tB) tC) = X + conv_lhs => rw [contrT_permT] + conv_rhs => rw [contrT_permT] + simp only [permT_permT] + conv_lhs => rw [contrT_permT] + conv_rhs => rw [contrT_permT] + simp only [permT_permT] + conv_rhs => rw [contrT_permT] + simp only [permT_permT] + apply induction_on_pure (t := X) + · intro p + simp only [contrT_pure, permT_pure, Pure.contrP, map_smul] + rw [smul_smul, smul_smul] + apply congrArg₂ (fun r t => r • t) + · -- Coefficients. + simp only [Pure.contrPCoeff_dropPair] + rw [mul_comm] + apply congrArg₂ (fun x y : k => x * y) + all_goals apply Pure.contrPCoeff_congr p + all_goals apply Fin.ext + all_goals + simp only [Nat.add_eq, Function.id_comp, Function.comp_id, Function.comp_apply, + Fin.cast_castAdd_left, Fin.cast_natAdd_left, + Fin.funPredPredAbove, Fin.succSuccAbove_predPredAbove, + Fin.append_right, Fin.append_swap_val, + Fin.append_castAdd_natAdd_eq_id, id_eq, Fin.append_castAdd_cast, + Fin.append_natAdd_cast, Fin.succSuccAbove_val, Fin.val_castAdd, + Fin.val_natAdd, Fin.val_last, Fin.val_cast, Fin.val_zero] + split_ifs <;> omega + · -- Slot maps. + apply congrArg Pure.toTensor + apply Pure.permP_dropPair_dropPair_congr p + intro m + -- The `funPredPredAbove` layers are nested, so they must be peeled one at a time; one + -- combined `simp` set thrashes `whnf` instead. + iterate 3 + try simp only [Function.comp_apply, id_eq] + try simp only [Fin.funPredPredAbove] + try simp only [Fin.succSuccAbove_predPredAbove] + apply Fin.ext + -- Pin each slot to a literal `⟨v, _⟩`, innermost first, so that `succSuccAbove_val` fires. + rw [Fin.cast_castAdd_eq_mk (i := Fin.last nA) (v := nA) _ rfl, + Fin.cast_natAdd_eq_mk (n := nA + 1) (i := (0 : Fin (1 + 1))) (v := nA + 1) _ + (by simp only [Fin.val_zero, Nat.add_zero]), + Fin.cast_castAdd_eq_mk (i := iA) (v := (iA : ℕ)) _ rfl, + Fin.natAdd_mk (1 + 1) (iA : ℕ), + Fin.natAdd_mk (1 + 1) (nA + 1), + Fin.cast_castAdd_eq_mk (i := Fin.last 1) (v := 1) _ rfl, + Fin.cast_natAdd_eq_mk (n := 1 + 1) (i := (0 : Fin (1 + 1))) (v := 1 + 1) _ + (by simp only [Fin.val_zero, Nat.add_zero]), + Fin.natAdd_mk (nA + 1) 1, + Fin.natAdd_mk (nA + 1) (1 + 1)] + simp only [Function.comp_id] + rw [Fin.append_castAdd_natAdd_eq_id] + simp only [Nat.add_eq, id_eq, Fin.append_swap_val, Fin.append_castAdd_cast, + Fin.append_natAdd_cast, Fin.succSuccAbove_val, Fin.val_cast] + -- Four nested reinsertion conditionals; the split budget is `SuccSuccAbove`'s. + grind (splits := 20) + · intro r t ht; simp only [map_smul, ht] + · intro t1 t2 h1 h2; simp only [map_add, h1, h2] + +/-! + +## D. Permutation commutators + +Moving a relabelling of one factor through the slot-addressed contraction. The relabelling `σ` need +not fix the contracted slot, so it carries the contraction from slot `i` to slot `σ i` and restricts +to the survivors as a map `σ'` filling the square `(σ i).succAbove ∘ σ' = σ ∘ i.succAbove`. Taking +`σ'` as an argument rather than deriving it lets a caller supply the survivor map it wants (`id`, a +swap-induced map) instead of an opaque composite. + +-/ + +/-- Left commutator: contracting slot `i` of `permT σ t1` equals contracting slot `σ i` of `t1`, + then relabelling the survivors by `σ'`. The square `hσ'` records how `σ'` carries the complement + of `i` to the complement of `σ i`, and implies its bijectivity. -/ +lemma crossToEnd_permT_left {nA nB : ℕ} {cA cA' : Fin (nA + 1) → C} + {cB : Fin (nB + 1) → C} + (i : Fin (nA + 1)) (j : Fin (nB + 1)) + (σ : Fin (nA + 1) → Fin (nA + 1)) (σ' : Fin nA → Fin nA) + (hσ : IsReindexing cA cA' σ) + (hσ' : (σ i).succAbove ∘ σ' = σ ∘ i.succAbove) + (hc : S.τ (cA' i) = cB j) + (t1 : Tensor S cA) (t2 : Tensor S cB) : + crossToEnd i j hc (permT σ hσ t1) t2 = + permT (Fin.append (Fin.castAdd nB ∘ σ') (Fin.natAdd nA)) + (IsReindexing.append_congr_left (cB ∘ j.succAbove) + (IsReindexing.succAbove_of_succAbove_eq i hσ hσ')) + (crossToEnd (σ i) j (by rw [hσ.2 i]; exact hc) t1 t2) := by + simp only [crossToEnd, LinearMap.compr₂_apply, LinearMap.comp_apply] + rw [prodT_permT_left] + simp only [permT_permT] + generalize prodT t1 t2 = X + apply induction_on_pure (t := X) + · intro p + simp only [contrT_pure, permT_pure, Pure.contrP, map_smul] + congr 1 + · simp only [Pure.contrPCoeff_permP] + apply Pure.contrPCoeff_congr <;> (apply Fin.ext; simp) + · apply congrArg Pure.toTensor + apply Pure.permP_dropPair_permP_congr p + intro m + simp only [Function.comp_apply, id_eq] + refine Fin.addCases (fun a => ?_) (fun b => ?_) m + · rw [Fin.reinsert_castAdd i j a, Fin.append_left, Function.comp_apply, + Fin.append_left, Function.comp_apply, Fin.reinsert_castAdd (σ i) j _, + show (σ i).succAbove (σ' a) = σ (i.succAbove a) from congrFun hσ' a] + · rw [Fin.reinsert_natAdd i j b, Fin.append_right, Fin.append_right, + Fin.reinsert_natAdd (σ i) j b] + · intro r t ht; simp only [map_smul, ht] + · intro t1 t2 h1 h2; simp only [map_add, h1, h2] + +/-- Right commutator, the mirror of `crossToEnd_permT_left`: contracting slot `j` of `permT σ t2` + equals contracting slot `σ j` of `t2`, then relabelling the survivors by `σ'`. -/ +lemma crossToEnd_permT_right {nA nB : ℕ} {cA : Fin (nA + 1) → C} + {cB cB' : Fin (nB + 1) → C} + (i : Fin (nA + 1)) (j : Fin (nB + 1)) + (σ : Fin (nB + 1) → Fin (nB + 1)) (σ' : Fin nB → Fin nB) + (hσ : IsReindexing cB cB' σ) + (hσ' : (σ j).succAbove ∘ σ' = σ ∘ j.succAbove) + (hc : S.τ (cA i) = cB' j) + (t1 : Tensor S cA) (t2 : Tensor S cB) : + crossToEnd i j hc t1 (permT σ hσ t2) = + permT (Fin.append (Fin.castAdd nB) (Fin.natAdd nA ∘ σ')) + (IsReindexing.append_congr_right (cA ∘ i.succAbove) + (IsReindexing.succAbove_of_succAbove_eq j hσ hσ')) + (crossToEnd i (σ j) (by rw [hσ.2 j]; exact hc) t1 t2) := by + simp only [crossToEnd, LinearMap.compr₂_apply, LinearMap.comp_apply] + rw [prodT_permT_right] + simp only [permT_permT] + generalize prodT t1 t2 = X + apply induction_on_pure (t := X) + · intro p + simp only [contrT_pure, permT_pure, Pure.contrP, map_smul] + congr 1 + · simp only [Pure.contrPCoeff_permP] + apply Pure.contrPCoeff_congr <;> (apply Fin.ext; simp) + · apply congrArg Pure.toTensor + apply Pure.permP_dropPair_permP_congr p + intro m + simp only [Function.comp_apply, id_eq] + refine Fin.addCases (fun a => ?_) (fun b => ?_) m + · rw [Fin.reinsert_castAdd i j a, Fin.append_left, Fin.append_left, + Fin.reinsert_castAdd i (σ j) a] + · rw [Fin.reinsert_natAdd i j b, Fin.append_right, Function.comp_apply, + Fin.append_right, Function.comp_apply, Fin.reinsert_natAdd i (σ j) _, + show (σ j).succAbove (σ' b) = σ (j.succAbove b) from congrFun hσ' b] + · intro r t ht; simp only [map_smul, ht] + · intro t1 t2 h1 h2; simp only [map_add, h1, h2] + +end Tensor + +end TensorSpecies From 6851c3217f802c3817812a5d122e54f7184483cb Mon Sep 17 00:00:00 2001 From: Andrea Pari Date: Mon, 27 Jul 2026 16:16:12 +0100 Subject: [PATCH 4/9] feat(Tensors/Contraction): crossToSlot, the result-to-slot convention MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `crossToEnd` deposits the surviving index at the end of the survivor list. Raising and lowering a named index wants it to stay in place: contracting slot `i` of `t` against a rank-two tensor `M` should return `t` with only slot `i`'s color changed, `T^{μ}{}_{νρ} ↦ T_{μνρ}`. `crossToSlot i j hc M` is that operation, `crossToEnd` followed by the cycle that walks the survivor from the last slot back to `i`. `crossToSlot_eq_crossToEnd` is the single place the two conventions meet. The contracted color is a propositional argument, so a rank-two tensor whose slot color matches only up to an equality enters with no transporting `permT`. The module stays at the `CommRing` altitude of `crossToEnd`; the `RCLike` round trips built on it live with the unit-tensor theory. Co-authored-by: Claude Opus 4.8 --- Physlib.lean | 1 + .../Tensors/Contraction/CrossToSlot.lean | 137 ++++++++++++++++++ 2 files changed, 138 insertions(+) create mode 100644 Physlib/Relativity/Tensors/Contraction/CrossToSlot.lean diff --git a/Physlib.lean b/Physlib.lean index e8da6533e..5065fd5f1 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -405,6 +405,7 @@ public import Physlib.Relativity.Tensors.Constructors public import Physlib.Relativity.Tensors.Contraction.Basic public import Physlib.Relativity.Tensors.Contraction.Basis public import Physlib.Relativity.Tensors.Contraction.CrossToEnd +public import Physlib.Relativity.Tensors.Contraction.CrossToSlot public import Physlib.Relativity.Tensors.Contraction.Products public import Physlib.Relativity.Tensors.Contraction.Pure public import Physlib.Relativity.Tensors.Contraction.SuccSuccAbove diff --git a/Physlib/Relativity/Tensors/Contraction/CrossToSlot.lean b/Physlib/Relativity/Tensors/Contraction/CrossToSlot.lean new file mode 100644 index 000000000..cd3dcf8fc --- /dev/null +++ b/Physlib/Relativity/Tensors/Contraction/CrossToSlot.lean @@ -0,0 +1,137 @@ +/- +Copyright (c) 2026 Andrea Pari. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Andrea Pari +-/ +module + +public import Physlib.Relativity.Tensors.Contraction.CrossToEnd +/-! + +# Result-to-slot contraction against a rank-2 tensor + +## i. Overview + +`crossToEnd` deposits the surviving index of a slot contraction at the end of the survivor list. +Raising and lowering a named index instead wants the replacement to stay *in place*: contracting +slot `i` of `t` against a rank-2 tensor `M` (a metric, the unit tensor) should return `t` with only +slot `i`'s color changed, `T^{μ}{}_{νρ} ↦ T_{μνρ}`. `crossToSlot i j hc M` is that operation, and +`crossToSlot_eq_crossToEnd` is the one place the two conventions meet. + +This module stays at the `CommRing` altitude of `crossToEnd`; the `RCLike` round trips built on the +operation live with the unit-tensor collapse theory in +`Physlib.Relativity.Tensors.Contraction.UnitTensorContraction`. + +## ii. Key results + +- `TensorSpecies.Tensor.crossToSlot` : contract slot `i` against slot `j` of a rank-2 tensor and + rotate the survivor back into position `i`; raising and lowering a named index. +- `TensorSpecies.Tensor.crossToSlot_eq_crossToEnd` : the bridge to the result-to-end convention. +- `TensorSpecies.Tensor.crossToSlot_permT_right_id` : an identity reindexing of the rank-2 tensor + passes through the contraction. +- `TensorSpecies.Tensor.crossToSlot_equivariant` : the contraction commutes with the `G`-action. + +## iii. Table of contents + +- A. The result-to-slot contraction + +## iv. References + +-/ + +@[expose] public section + +namespace TensorSpecies + +variable {k : Type} [CommRing k] {C : Type} {G : Type} [Group G] + {V : C → Type} [∀ c, AddCommGroup (V c)] [∀ c, Module k (V c)] + {basisIdx : C → Type} [∀ c, Fintype (basisIdx 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} + +namespace Tensor + +/-! + +## A. The result-to-slot contraction + +-/ + +/-- The survivor color of `crossToEnd i j` against a rank-2 tensor of color `cM` is `c` with + slot `i` replaced by the surviving color `cM (j.succAbove 0)`, once the survivors are rotated + back by the inverse of the cycle `[i, last]`. -/ +lemma IsReindexing.crossToSlot_cycle {nA : ℕ} {c : Fin (nA + 1) → C} {cM : Fin 2 → C} + (i : Fin (nA + 1)) (j : Fin 2) : + IsReindexing + (Fin.append (c ∘ i.succAbove) (cM ∘ j.succAbove)) + (Function.update c i (cM (j.succAbove 0))) + ⇑(Fin.cycleIcc i (Fin.last nA)).symm := by + refine ⟨(Fin.cycleIcc i (Fin.last nA)).symm.bijective, fun y => ?_⟩ + obtain ⟨z, rfl⟩ : ∃ z, y = Fin.cycleIcc i (Fin.last nA) z := + ⟨_, (Equiv.apply_symm_apply _ _).symm⟩ + rw [Equiv.symm_apply_apply, ← Fin.append_succAbove_const_eq_cycleIcc i] + refine Fin.addCases (fun a => ?_) (fun a => ?_) z + · rw [Fin.append_left, Fin.append_left, Function.comp_apply, + Function.update_of_ne (Fin.succAbove_ne i a)] + · rw [Fin.append_right, Fin.append_right, Function.comp_apply, Function.update_self] + fin_cases a + rfl + +/-- Contract slot `i` of `t` against slot `j` of the rank-2 tensor `M`, whose `j`-slot color must + equal the dual color `τ (c i)` (propositionally, via `hc`), and rotate `M`'s surviving slot back + into position `i`. The result is `t` with slot `i` relabelled to `M`'s surviving color. + + This is raising and lowering a named index; the metric case is `j = 0`, + `M = metricTensor (τ (c i))`. Because `hc` is propositional, a rank-2 tensor whose slot color + matches only up to an equality enters directly, with no transport. -/ +noncomputable def crossToSlot {nA : ℕ} {c : Fin (nA + 1) → C} {cM : Fin 2 → C} + (i : Fin (nA + 1)) (j : Fin 2) (hc : S.τ (c i) = cM j) (M : S.Tensor cM) : + S.Tensor c →ₗ[k] S.Tensor (Function.update c i (cM (j.succAbove 0))) := + permT ⇑(Fin.cycleIcc i (Fin.last nA)).symm (IsReindexing.crossToSlot_cycle i j) ∘ₗ + (crossToEnd i j hc).flip M + +/-- The bridge between the two conventions: `crossToSlot i j hc M t` is `crossToEnd i j hc t M` + with the survivor rotated from the last slot back to slot `i` by the inverse cycle. -/ +lemma crossToSlot_eq_crossToEnd {nA : ℕ} {c : Fin (nA + 1) → C} {cM : Fin 2 → C} + (i : Fin (nA + 1)) (j : Fin 2) (hc : S.τ (c i) = cM j) (M : S.Tensor cM) (t : S.Tensor c) : + crossToSlot i j hc M t = + permT ⇑(Fin.cycleIcc i (Fin.last nA)).symm (IsReindexing.crossToSlot_cycle i j) + (crossToEnd i j hc t M) := rfl + +/-- An identity reindexing of the rank-2 tensor becomes the corresponding identity reindexing of + the contracted output: the `crossToSlot`-level case of `crossToEnd_permT_right` where the rank-2 + tensor's colors are only propositionally recast. -/ +lemma crossToSlot_permT_right_id {nA : ℕ} {c : Fin (nA + 1) → C} {cM cM' : Fin 2 → C} + (i : Fin (nA + 1)) (j : Fin 2) (hc : S.τ (c i) = cM' j) + (M : Tensor S cM) (hM : IsReindexing cM cM' (id : Fin 2 → Fin 2)) (t : Tensor S c) : + crossToSlot i j hc (permT (id : Fin 2 → Fin 2) hM M) t = + permT (id : Fin (nA + 1) → Fin (nA + 1)) + (IsReindexing.on_id.mpr (fun a => by + by_cases ha : a = i + · subst ha + simpa using hM.2 (j.succAbove 0) + · simp [Function.update_of_ne ha])) + (crossToSlot i j (hc.trans (hM.2 j).symm) M t) := by + rw [crossToSlot_eq_crossToEnd, crossToSlot_eq_crossToEnd] + rw [crossToEnd_permT_right i j + (id : Fin 2 → Fin 2) id hM (by rfl)] + simp only [permT_permT] + apply permT_congr + · funext x + simpa only [Function.comp_apply, Function.comp_id, id_eq] using + congrFun Fin.append_castAdd_natAdd_eq_id ((Fin.cycleIcc i (Fin.last nA)).symm x) + · rfl + +/-- Cross contraction into a slot is `G`-equivariant, both constituents (`crossToEnd`, `permT`) + being so. -/ +@[simp] +lemma crossToSlot_equivariant {nA : ℕ} {c : Fin (nA + 1) → C} {cM : Fin 2 → C} + (i : Fin (nA + 1)) (j : Fin 2) (hc : S.τ (c i) = cM j) (g : G) + (M : Tensor S cM) (t : Tensor S c) : + crossToSlot i j hc (g • M) (g • t) = g • crossToSlot i j hc M t := by + rw [crossToSlot_eq_crossToEnd, crossToSlot_eq_crossToEnd, crossToEnd_equivariant, + permT_equivariant] + +end Tensor + +end TensorSpecies From 950827e1c2044be4e650c267e7cd24b1fef1144d Mon Sep 17 00:00:00 2001 From: Andrea Pari Date: Mon, 27 Jul 2026 16:16:12 +0100 Subject: [PATCH 5/9] feat(Tensors/Contraction): unit-tensor collapse and the raise/lower round trip The unit tensor is the identity for slot contraction: contracting any slot of `t` against `unitTensor` for that slot's color returns `t`, the slot carried to the survivor tail. `crossToEnd_unitTensor` proves this at any named slot, from the boundary case by spectator decomposition along the last slot. From it, `crossToSlot_raise_lower_round_trip`: for a rank-two `M` and an inverse `M'` whose shared index contracts away to the unit tensor, contracting slot `i` with `M` and then with `M'` is the identity up to the `Function.update` color reindex, at any rank and any slot. Every color is threaded propositionally, so a caller whose metric and inverse sit at literal colors supplies them directly and recovers the tensor with slot `i` at the literal, with no transporting `permT` on either factor. The result-to-end form `crossToEnd_round_trip_of_unit_slot` is stated separately, since it is what the chain regrouping consumes. Because `unitTensor` is `RCLike`-valued, this material sits over an `[RCLike k]` variable block, apart from the `CommRing` `crossToEnd`/`crossToSlot` algebra. Co-authored-by: Claude Opus 4.8 --- Physlib.lean | 1 + .../Contraction/UnitTensorContraction.lean | 334 ++++++++++++++++++ 2 files changed, 335 insertions(+) create mode 100644 Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean diff --git a/Physlib.lean b/Physlib.lean index 5065fd5f1..f2e70fd4f 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -409,6 +409,7 @@ public import Physlib.Relativity.Tensors.Contraction.CrossToSlot public import Physlib.Relativity.Tensors.Contraction.Products public import Physlib.Relativity.Tensors.Contraction.Pure public import Physlib.Relativity.Tensors.Contraction.SuccSuccAbove +public import Physlib.Relativity.Tensors.Contraction.UnitTensorContraction public import Physlib.Relativity.Tensors.Dual public import Physlib.Relativity.Tensors.Elab public import Physlib.Relativity.Tensors.Evaluation diff --git a/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean b/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean new file mode 100644 index 000000000..5f624ba64 --- /dev/null +++ b/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean @@ -0,0 +1,334 @@ +/- +Copyright (c) 2026 Andrea Pari. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Andrea Pari +-/ +module + +public import Physlib.Relativity.Tensors.Contraction.CrossToSlot +public import Physlib.Relativity.Tensors.UnitTensor +public import Physlib.Relativity.Tensors.Evaluation +/-! + +# Contraction against the unit tensor + +## i. Overview + +The unit tensor is the identity for slot contraction: contracting any slot of `t` against +`unitTensor` for that slot's color returns `t`, the slot relabelled to the survivor tail. That is +what collapses "raise then lower" to the identity, a metric contracted against its dual becoming +the unit tensor and then contracting away. + +`crossToEnd_unitTensor` is proved by decomposing `t` along its last slot (`eq_sum_evalT`) and +transporting to an arbitrary slot with the transposition `swap i (last)`. On it the round trip +against a matched pair is assembled in both conventions: +`crossToEnd_round_trip_of_unit_slot` in result-to-end form and +`crossToSlot_raise_lower_round_trip` in result-to-slot form, with +`toDualMapAtIndex_toDualMapAtIndex` as the metric specialisation. Since `unitTensor` is +`RCLike`-valued, this material sits over an `[RCLike k]` variable block, apart from the `CommRing` +`crossToEnd`/`crossToSlot` algebra. + +## ii. Key results + +- `TensorSpecies.Tensor.crossToEnd_unitTensor` : the unit tensor is an identity for `crossToEnd` + at any named slot. +- `TensorSpecies.Tensor.crossToEnd_round_trip_of_unit_slot` : two contractions against a pair that + collapses to the unit tensor return the original tensor, in result-to-end form. +- `TensorSpecies.Tensor.crossToSlot_raise_lower_round_trip` : the round trip in result-to-slot + form, the shape `toDualMapAtIndex_toDualMapAtIndex` consumes. + +## iii. Table of contents + +- A. The unit tensor as a slot-contraction identity +- B. Round trips against a matched pair + +## iv. References + +-/ + +@[expose] public section + +namespace TensorSpecies + +variable {k : Type} [RCLike k] {C : Type} {G : Type} [Group G] + {V : C → Type} [∀ c, AddCommGroup (V c)] [∀ c, Module k (V c)] + {basisIdx : C → Type} [∀ c, Fintype (basisIdx 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} +attribute [-simp] LinearEquiv.cast_apply + +namespace Tensor + +/-! + +## A. The unit tensor as a slot-contraction identity + +Contracting a named slot against `unitTensor` returns the tensor unchanged, the slot carried to the +survivor tail by `moveLast`. + +-/ + +/-- Cross-contracting the last slot of the product `E ⊗ B` (with `B` rank one) against the unit + tensor for that slot's color returns `E ⊗ B` unchanged, the contracted slot carried to the end. + The rank-one spectator case that seeds `crossToEnd_unitTensor_slot`. -/ +private lemma crossToEnd_prodT_unitTensor {nV : ℕ} {cE : Fin nV → C} {cB : C} + (E : Tensor S cE) (B : Tensor S ![cB]) : + crossToEnd (Fin.last nV) (0 : Fin 2) + (by rw [show (Fin.last nV : Fin (nV + 1)) = Fin.natAdd nV 0 from Fin.ext (by simp)]; simp : + S.τ ((Fin.append cE ![cB]) (Fin.last nV)) = ![S.τ cB, cB] 0) + (prodT E B) (unitTensor cB) = + permT id (IsReindexing.on_id.mpr (fun i => by + refine Fin.addCases (fun j => ?_) (fun j => ?_) i + · simp only [Fin.append_left, Function.comp_apply, Fin.succAbove_last] + exact (Fin.append_left cE ![cB] j).symm + · simp only [Fin.append_right, Function.comp_apply, Fin.succAbove_zero] + fin_cases j + rfl)) (prodT E B) := by + simp only [crossToEnd, LinearMap.compr₂_apply, LinearMap.comp_apply] + rw [contrT_congr (n := nV + 1) (⟨nV, by omega⟩ : Fin (nV + 1 + 1 + 1)) + (⟨nV + 1, by omega⟩ : Fin (nV + 1 + 1 + 1)) _ (Fin.ext (by simp)) (Fin.ext (by simp))] + rw [prodT_assoc E B (unitTensor cB)] + simp only [permT_permT] + rw [contrT_permT] + simp only [Fin.cast_eq_self, Function.comp_apply] + have hij : (0 : Fin 3) ≠ (1 : Fin 3) ∧ + S.τ (Fin.append ![cB] ![S.τ cB, cB] 0) = Fin.append ![cB] ![S.τ cB, cB] 1 := + ⟨by decide, by rfl⟩ + have key : (contrT (nV + 1) (⟨nV, by omega⟩ : Fin (nV + 1 + 1 + 1)) ⟨nV + 1, by omega⟩ + (by refine ⟨by simp [Fin.ext_iff], ?_⟩ + rw [show (⟨nV, by omega⟩ : Fin (nV + 1 + 1 + 1)) + = Fin.natAdd nV (0 : Fin 3) from Fin.ext (by simp), + show (⟨nV + 1, by omega⟩ : Fin (nV + 1 + 1 + 1)) + = Fin.natAdd nV (1 : Fin 3) from Fin.ext (by simp)] + rw [Fin.append_right, Fin.append_right]; exact hij.2) + (prodT E (prodT B (unitTensor cB)))) = + (permT id (IsReindexing.on_id_symm (IsReindexing.append_succSuccAbove_natAdd (0:Fin 3) 1))) + (prodT E (contrT 1 0 1 hij (prodT B (unitTensor cB)))) := + contrT_prodT_snd (0 : Fin 3) 1 hij (prodT B (unitTensor cB)) E + rw [contrT_single_unitTensor] at key + -- The `contrT_congr` pinning above leaves a goal whose slot proofs are not syntactically equal + -- to `key`'s, so `rw` at reducible transparency cannot key on them; `instances` transparency + -- matches. The final `permT_permT` needs the full `erw`. + rw (transparency := .instances) [key, permT_permT] + rw [prodT_permT_right, permT_permT] + erw [permT_permT] + apply permT_congr + · funext i + simp only [Function.comp_apply, id_eq, Fin.funPredPredAbove] + apply Fin.ext + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, CompTriple.comp_eq, + Fin.cast_eq_self, Fin.predPredAbove_succSuccAbove] + refine Fin.addCases (fun j => ?_) (fun j => ?_) i <;> simp [Fin.append_left, Fin.append_right] + · rfl + +/-- The boundary case of `crossToEnd_unitTensor`, proved by spectator decomposition along the last + slot (`eq_sum_evalT`). The last slot is threaded as a variable `i` with `hilast : i = last nA` so + that `crossToEnd_unitTensor` can apply it at the image of `i` under its transposition without a + dependent rewrite of the slot index. -/ +private lemma crossToEnd_unitTensor_slot {nA : ℕ} {cA : Fin (nA + 1) → C} {c : C} + {i : Fin (nA + 1)} (hilast : i = Fin.last nA) (hc : cA i = c) (t1 : Tensor S cA) : + crossToEnd i (0 : Fin 2) (by simp [hc] : S.τ (cA i) = ![S.τ c, c] 0) t1 (unitTensor c) = + permT (Fin.append i.succAbove (fun _ : Fin 1 => i)) (IsReindexing.moveLast i hc) t1 := by + subst hilast + subst hc + rw [eq_sum_evalT t1, map_sum, LinearMap.sum_apply, map_sum] + refine Finset.sum_congr rfl (fun i _ => ?_) + change crossToEnd (Fin.last nA) 0 _ + (permT (fun x => x) _ + (prodT (evalT (Fin.last nA) i t1) + (basis ![cA (Fin.last nA)] (ComponentIdx.single.symm i)))) + (unitTensor (S := S) (cA (Fin.last nA))) = _ + rw [crossToEnd_permT_left (Fin.last nA) 0 (fun x => x) (fun x => x) + (IsReindexing.append_succ_last cA) (by rfl)] + rw [crossToEnd_prodT_unitTensor] + simp only [permT_permT] + refine permT_congr (funext fun x => ?_) rfl + refine Fin.addCases (fun j => ?_) (fun j => ?_) x + · simp only [Fin.append_left, Function.comp_apply, id_eq, Fin.succAbove_last] + rfl + · simp only [Fin.append_right, Function.comp_apply] + exact Fin.ext (by simp) + +/-- Contracting slot `i` of `t1` against the unit tensor for that slot's color returns `t1`, the + contracted slot relabelled by `moveLast i`. The unit tensor acts as an identity for `crossToEnd` + at any named slot. -/ +lemma crossToEnd_unitTensor {nA : ℕ} {cA : Fin (nA + 1) → C} {c : C} + (i : Fin (nA + 1)) (hc : cA i = c) (t1 : Tensor S cA) : + crossToEnd i (0 : Fin 2) (by simp [hc] : S.τ (cA i) = ![S.τ c, c] 0) t1 (unitTensor c) = + permT (Fin.append i.succAbove (fun _ : Fin 1 => i)) (IsReindexing.moveLast i hc) t1 := by + set τ : Fin (nA + 1) → Fin (nA + 1) := ⇑(Equiv.swap i (Fin.last nA)) with hτdef + have hτbij : Function.Bijective τ := (Equiv.swap i (Fin.last nA)).bijective + have hτi : τ i = Fin.last nA := Equiv.swap_apply_left i (Fin.last nA) + have hself : ∀ x, τ (τ x) = x := fun x => Equiv.swap_apply_self i (Fin.last nA) x + obtain ⟨τ', hτ'⟩ := Fin.exists_succAbove_comm hτbij.1 i + have hre2 : IsReindexing cA (cA ∘ τ) τ := Tensor.IsReindexing.swap i (Fin.last nA) + have hre : IsReindexing (cA ∘ τ) cA τ := + ⟨hτbij, fun x => by simp only [Function.comp_apply, hself]⟩ + have ht1 : permT τ hre (permT τ hre2 t1) = t1 := by + rw [permT_permT]; exact permT_congr_eq_id _ _ _ (funext hself) + conv_lhs => rw [← ht1] + rw [crossToEnd_permT_left i (0 : Fin 2) τ τ' hre hτ' _ + (permT τ hre2 t1) (unitTensor c), + crossToEnd_unitTensor_slot hτi (by simp only [Function.comp_apply, hself]; exact hc) + (permT τ hre2 t1), permT_permT, permT_permT] + refine permT_congr (funext fun x => ?_) rfl + refine Fin.addCases (fun a => ?_) (fun a => ?_) x + · simp only [Function.comp_apply, Fin.append_left] + rw [show (τ i).succAbove (τ' a) = τ (i.succAbove a) from congrFun hτ' a, hself] + · simp only [Function.comp_apply, Fin.append_right, hself] + +/-! + +## B. Round trips against a matched pair + +When two rank-2 tensors collapse to the unit tensor after their shared index is contracted, +contracting a slot first against one and then against the other returns the original tensor. + +-/ + +/-- The color list `crossToEnd` produces from a matched rank-2 pair `M : ![a, d]`, + `M' : ![S.τ d, e]` is the color list `![S.τ e, e]` of `unitTensor e`, via the identity slot map; + the reindexing carried by the collapse hypothesis `M · M' = δ` of the round trips below. The + pair's outer color `a` equals `S.τ e` only propositionally, so a caller whose metric sits at a + literal color supplies `h` directly instead of transporting the tensor. -/ +lemma IsReindexing.unitTensor_pair {a d e : C} (h : S.τ e = a) : + IsReindexing (![S.τ e, e] : Fin 2 → C) + (Fin.append ((![a, d] : Fin 2 → C) ∘ (Fin.last 1).succAbove) + ((![S.τ d, e] : Fin 2 → C) ∘ (0 : Fin 2).succAbove)) + (id : Fin 2 → Fin 2) := + IsReindexing.on_id.mpr (fun j => by fin_cases j <;> first | exact h | rfl) + +/-- Round trip of two contractions against a matched pair, in result-to-end form. Contracting slot + `i` of `t` against `M₁`, then contracting the surviving `M₁`-index (deposited at slot `j`) against + `M₂`, returns `t` up to the cycle that moves the round-tripped slot from the end back to `i`, + whenever `M₁` and `M₂` collapse to the unit tensor. The last slot is threaded as a variable `j` + with `hj : j = last nA` so that a caller can apply it at a propositionally-last slot without a + dependent rewrite of the slot index. -/ +lemma crossToEnd_round_trip_of_unit_slot {nA : ℕ} {c : Fin (nA + 1) → C} {d : C} + (i j : Fin (nA + 1)) (hj : j = Fin.last nA) + (M₁ : Tensor S ![S.τ (c i), d]) (M₂ : Tensor S ![S.τ d, c i]) + (hM : crossToEnd (Fin.last 1) (0 : Fin 2) rfl M₁ M₂ = + permT (id : Fin 2 → Fin 2) (IsReindexing.unitTensor_pair rfl) + (unitTensor (S := S) (c i))) + (t : Tensor S c) : + crossToEnd j (0 : Fin 2) + (by subst hj + rw [show (Fin.last nA : Fin (nA + 1)) = Fin.natAdd nA (0 : Fin 1) from + Fin.ext (by simp), Fin.append_right]; rfl) + (crossToEnd i (0 : Fin 2) rfl t M₁) M₂ = + permT (Fin.append i.succAbove (fun _ : Fin 1 => i)) + (by + subst hj + exact ⟨by + rw [Fin.append_succAbove_const_eq_cycleIcc i] + exact (Fin.cycleIcc i (Fin.last nA)).bijective, + fun x => by + refine Fin.addCases (fun a => ?_) (fun a => ?_) x + · simp only [Function.comp_apply, Fin.append_left, Fin.succAbove_last, + show (Fin.castSucc a : Fin (nA + 1)) = Fin.castAdd 1 a from rfl] + · fin_cases a + simp [Fin.append_right, Fin.succAbove_zero]⟩) + t := by + subst hj + rw [crossToEnd_assoc_rankTwo i rfl rfl t M₁ M₂] + rw [hM] + rw [crossToEnd_permT_right i (0 : Fin 2) + (id : Fin 2 → Fin 2) (fun x : Fin 1 => x) + (IsReindexing.on_id.mpr (fun i => by fin_cases i <;> rfl)) rfl] + -- The `id`-spelled map from `crossToEnd_permT_right` leaves the composite slot proof only + -- type-correct at default transparency, so `rw`/`simp` cannot key on `crossToEnd_unitTensor` + -- or `permT_permT`; `erw` matches up to defeq. + erw [crossToEnd_unitTensor (nA := nA) (cA := c) (c := c i) i rfl] + erw [permT_permT, permT_permT] + apply permT_congr + · funext x + refine Fin.addCases (fun a => ?_) (fun a => ?_) x + · simp [Fin.append_left] + · fin_cases a + simp [Fin.append_right, Function.comp_apply] + · rfl + +/-- Round trip for `crossToSlot` at an arbitrary slot, with the colors in their composite form. + The general-color statement `crossToSlot_raise_lower_round_trip` is obtained from this by + substituting its three color equalities. -/ +private lemma crossToSlot_round_trip_of_unit {nA : ℕ} {c : Fin (nA + 1) → C} {d : C} + (i : Fin (nA + 1)) + (M₁ : Tensor S ![S.τ (c i), d]) (M₂ : Tensor S ![S.τ d, c i]) + (hM : crossToEnd (Fin.last 1) (0 : Fin 2) rfl M₁ M₂ = + permT (id : Fin 2 → Fin 2) (IsReindexing.unitTensor_pair rfl) + (unitTensor (S := S) (c i))) + (t : Tensor S c) : + crossToSlot (S := S) i (0 : Fin 2) + (by rw [Function.update_self] : S.τ (Function.update c i d i) = S.τ d) M₂ + (crossToSlot (S := S) i (0 : Fin 2) rfl M₁ t) = + permT (id : Fin (nA + 1) → Fin (nA + 1)) + (IsReindexing.on_id.mpr (fun j => by + by_cases h : j = i + · subst h + simp [Function.update_self] + · simp [Function.update_of_ne h])) + t := by + have hcycle : (⇑(Fin.cycleIcc i (Fin.last nA)).symm) i = Fin.last nA := + (Equiv.symm_apply_eq _).2 (Fin.cycleIcc_of_last (Fin.le_last i)).symm + rw [crossToSlot_eq_crossToEnd, crossToSlot_eq_crossToEnd] + -- `crossToSlot`'s output color `Function.update c i (cM ((0).succAbove 0))` reduces to the clean + -- color only after the `Fin.cons` reduction (default transparency), so the unfolded goal is not + -- type-correct at `instances` transparency and `rw` cannot key on the composite. Precompute the + -- left commutator (its `rfl`-heavy `hσ'` witness elaborated at normal transparency) and `erw` it, + -- which matches up to defeq. + have hpl := crossToEnd_permT_left i (0 : Fin 2) + ⇑(Fin.cycleIcc i (Fin.last nA)).symm id (IsReindexing.crossToSlot_cycle i (0 : Fin 2)) + (by + funext a + simp only [Function.comp_apply, id_eq] + rw [hcycle, Fin.cycleIcc_last_symm_apply_succAbove, Fin.succAbove_last] + rfl) + (show S.τ (Function.update c i d i) = ![S.τ d, c i] 0 by + rw [Function.update_self, Matrix.cons_val_zero]) + (crossToEnd i (0 : Fin 2) rfl t M₁) M₂ + erw [hpl] + erw [permT_permT] + rw [crossToEnd_round_trip_of_unit_slot i ((⇑(Fin.cycleIcc i (Fin.last nA)).symm) i) + hcycle M₁ M₂ hM t, permT_permT] + apply permT_congr + · funext x + simp only [Function.comp_id] + rw [Fin.append_castAdd_natAdd_eq_id] + simp [Function.comp_apply, Fin.append_succAbove_const_eq_cycleIcc] + · rfl + +/-- Raising then lowering a named index, with every color threaded propositionally. For a rank-2 + metric `M : ![a, d]` and an inverse `M' : ![b, e]` collapsing to the unit tensor (`M · M' = δ`), + at any rank and any slot `i`: contracting slot `i` with `M`, then contracting the result with + `M'`, is the identity up to the `Function.update` color reindex. + + No color is pinned to a composite. `ha : τ (c i) = a` places the metric's contracted slot, + `hb : τ d = b` the inverse's, and `he : c i = e` the surviving one, so a caller whose metric and + inverse sit at literal colors supplies them directly, with no transporting `permT` on either + factor, and recovers the tensor with slot `i` at the literal. -/ +lemma crossToSlot_raise_lower_round_trip {nA : ℕ} {c : Fin (nA + 1) → C} {a b d e : C} + (i : Fin (nA + 1)) (he : c i = e) (ha : S.τ (c i) = a) (hb : S.τ d = b) + (M : Tensor S ![a, d]) (M' : Tensor S ![b, e]) + (hM : crossToEnd (Fin.last 1) (0 : Fin 2) hb M M' = + permT (id : Fin 2 → Fin 2) + (IsReindexing.unitTensor_pair ((congrArg S.τ he.symm).trans ha)) + (unitTensor (S := S) e)) + (t : Tensor S c) : + crossToSlot (S := S) i (0 : Fin 2) + (by rw [Function.update_self]; exact hb : S.τ (Function.update c i d i) = b) M' + (crossToSlot (S := S) i (0 : Fin 2) ha M t) = + permT (id : Fin (nA + 1) → Fin (nA + 1)) + (IsReindexing.on_id.mpr (fun j => by + by_cases h : j = i + · subst h + simp [Function.update_self, he] + · simp [Function.update_of_ne h])) + t := by + subst ha + subst hb + subst he + exact crossToSlot_round_trip_of_unit i M M' hM t + +end Tensor + +end TensorSpecies From aebb0ccf7a8665c0d823ed02c900910d58e232dc Mon Sep 17 00:00:00 2001 From: Andrea Pari Date: Mon, 27 Jul 2026 16:16:24 +0100 Subject: [PATCH 6/9] refactor(Tensors/Dual): dualise a named index through crossToSlot, at every rank MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `toDualMapAtIndex` is now `crossToSlot` against `metricTensor (τ (c i))`, the case where the rank-two tensor's two slots share a color, and `toDualMapAtIndex_toDualMapAtIndex` states the double-dual round trip at every rank and every named slot, as the same-color instance of `crossToSlot_raise_lower_round_trip`. That subsumes the rank-one slot-zero maps `toDualMap`, `fromDualMap`, `toDual` and their four round trips, which are removed. Their round trip had needed a bespoke transport computation under `backward.isDefEq.respectTransparency false`; the general-rank proof needs no transparency override. It also retires `IsReindexing.contr_two_rotate`, whose only purpose was to rotate the old `toDualAtIndex`, so the lemma is dropped here rather than left in `Reindexing` without a consumer. `fromDualMapAtIndex` absorbs the color cast the two `Function.update`s generate, which is what makes the round trips cast-free in both directions, and `toDualAtIndex` bundles the pair as a `LinearEquiv`. Its equivariance is `toDualMapAtIndex_equivariant`, which is `@[simp]`; restating it at the bundled type would add nothing, since the two maps are definitionally equal. `Elab.lean` follows the rename in the `jiggle` operator, so the `τ` index notation elaborates to `toDualMapAtIndex`. Co-authored-by: Claude Opus 4.8 --- Physlib/Relativity/Tensors/Dual.lean | 236 ++++++++++----------- Physlib/Relativity/Tensors/Elab.lean | 10 +- Physlib/Relativity/Tensors/Reindexing.lean | 46 ---- 3 files changed, 111 insertions(+), 181 deletions(-) diff --git a/Physlib/Relativity/Tensors/Dual.lean b/Physlib/Relativity/Tensors/Dual.lean index 4771c2077..15f0a0234 100644 --- a/Physlib/Relativity/Tensors/Dual.lean +++ b/Physlib/Relativity/Tensors/Dual.lean @@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith module public import Physlib.Relativity.Tensors.MetricTensor +public import Physlib.Relativity.Tensors.Contraction.UnitTensorContraction /-! # Dual tensors @@ -21,141 +22,118 @@ variable {k : Type} [RCLike k] {C : Type} {G : Type} [Group G] {basisIdx : C → Type} [∀ c, Fintype (basisIdx 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} -attribute [-simp] LinearEquiv.cast_apply namespace Tensor -/-- The linear map taking a tensor based on the color `S.τ c` to a tensor - based on the color `c`, defined by contraction with the metric tensor. -/ -noncomputable def fromDualMap {c : C} : S.Tensor ![S.τ c] →ₗ[k] S.Tensor ![c] where - toFun t := permT id (by simp; rfl) - (contrT 1 1 2 (by simp; rfl) (prodT (metricTensor c) t)) - map_add' t1 t2 := by - simp - map_smul' r t := by - simp - -lemma fromDualMap_apply {c : C} (t : S.Tensor ![S.τ c]) : - fromDualMap t = permT id (by simp; rfl) - (contrT 1 1 2 (by simp; rfl) (prodT (metricTensor c) t)) := by - rfl - -/-- The linear map taking a tensor based on the color `c` to a tensor - based on the color `S.τ c`, defined by contraction with the metric tensor. -/ -noncomputable def toDualMap {c : C} : S.Tensor ![c] →ₗ[k] S.Tensor ![S.τ c] where - toFun t := permT id (by - simp; rfl) (contrT 1 1 2 (by - change _ ∧ S.τ (S.τ c) = c - simp) (prodT (metricTensor (S.τ c)) t)) - map_add' t1 t2 := by - simp - map_smul' r t := by - simp - -lemma toDualMap_apply {c : C} (t : S.Tensor ![c]) : - toDualMap t = permT id (by - simp; rfl) (contrT 1 1 2 (by - change _ ∧ S.τ (S.τ c) = c - simp) (prodT (metricTensor (S.τ c)) t)) := by - rfl - -set_option backward.isDefEq.respectTransparency false in +/-- The linear map between `S.Tensor c` and `S.Tensor (Function.update c i (S.τ (c i)))` formed by + contracting with the metric tensor at a specific index. It is `crossToSlot` against + `metricTensor (S.τ (c i))`, the case where the rank-2 tensor's two slots share a color. -/ +noncomputable def toDualMapAtIndex : {n : ℕ} → {c : Fin n → C} → (i : Fin n) → + S.Tensor c →ₗ[k] S.Tensor (Function.update c i (S.τ (c i))) + | 0, _, i => i.elim0 + | _ + 1, c, i => crossToSlot i (0 : Fin 2) rfl (metricTensor (S := S) (S.τ (c i))) + +/-- Dualising slot `i` twice returns the original color list: `τ (τ (c i)) = c i`, and no other + slot moves. The color cast carried by the double-dual round trips below. -/ +lemma IsReindexing.update_dual_dual {n : ℕ} (c : Fin n → C) (i : Fin n) : + IsReindexing c (Function.update (Function.update c i (S.τ (c i))) i + (S.τ (Function.update c i (S.τ (c i)) i))) (id : Fin n → Fin n) := + IsReindexing.on_id.mpr (fun j => by + by_cases h : j = i <;> simp [h, Function.update_of_ne, τ_τ_apply]) + +/-- Dualising any named index twice returns the original tensor, up to the color cast generated by +the two `Function.update`s. Stated at every rank, matching the domain of `toDualMapAtIndex`. -/ +lemma toDualMapAtIndex_toDualMapAtIndex {n : ℕ} {c : Fin n → C} + (i : Fin n) (t : S.Tensor c) : + toDualMapAtIndex (S := S) i (toDualMapAtIndex (S := S) i t) = + permT (id : Fin n → Fin n) (IsReindexing.update_dual_dual c i) t := by + cases n with + | zero => exact i.elim0 + | succ nA => + let M₁ := metricTensor (S := S) (S.τ (c i)) + let M₂ : S.Tensor ![S.τ (S.τ (c i)), c i] := + permT (fun x : Fin 2 => x) + (IsReindexing.on_id.mpr (fun j => by fin_cases j <;> simp [τ_τ_apply])) + (metricTensor (S := S) (c i)) + -- The two dual metrics collapse to the unit tensor: `gᵃᵇ · g_cd = δ`. + have hM : crossToEnd (S := S) (Fin.last 1) (0 : Fin 2) rfl M₁ M₂ = + permT (id : Fin 2 → Fin 2) (IsReindexing.unitTensor_pair rfl) + (unitTensor (S := S) (c i)) := by + dsimp only [M₁, M₂] + rw [crossToEnd_permT_right (Fin.last 1) (0 : Fin 2) + (fun x : Fin 2 => x) (fun x : Fin 1 => x) + (IsReindexing.on_id.mpr (fun i => by fin_cases i <;> simp [τ_τ_apply])) rfl] + rw [crossToEnd_two, contrT_dual_metricTensor_metricTensor] + simp only [Fin.isValue, Nat.reduceAdd, permT_permT, CompTriple.comp_eq] + refine permT_congr ?_ rfl + ext j; fin_cases j <;> rfl + have key := crossToSlot_raise_lower_round_trip (S := S) i (M := M₁) (M' := M₂) + (he := rfl) (ha := rfl) (hb := rfl) (hM := hM) (t := t) + -- Reconcile the second metric's symmetric color with the mixed contraction color. + let x := S.τ (Function.update c i (S.τ (c i)) i) + have hmetric : metricTensor (S := S) x = + permT (id : Fin 2 → Fin 2) + (IsReindexing.on_id.mpr (fun j => by + fin_cases j <;> simp [x, Function.update_self, τ_τ_apply])) M₂ := by + dsimp only [M₂] + rw [metricTensor_congr (by simp [x, Function.update_self, τ_τ_apply] : x = c i)] + rw [permT_permT] + refine permT_congr ?_ rfl + ext j; fin_cases j <;> rfl + rw [toDualMapAtIndex, toDualMapAtIndex] + change crossToSlot i (0 : Fin 2) rfl (metricTensor (S := S) x) + (crossToSlot i (0 : Fin 2) rfl M₁ t) = _ + rw [hmetric, crossToSlot_permT_right_id, key] + simp only [permT_permT] + refine permT_congr ?_ rfl + funext j; simp + +/-- The inverse of `toDualMapAtIndex` at the same index: dualise again, then absorb the color cast + the two `Function.update`s generate. Absorbing it here is what makes the round trips in both + directions cast-free. -/ +noncomputable def fromDualMapAtIndex {n : ℕ} {c : Fin n → C} (i : Fin n) : + S.Tensor (Function.update c i (S.τ (c i))) →ₗ[k] S.Tensor c := + permT (id : Fin n → Fin n) (IsReindexing.on_id_symm (IsReindexing.update_dual_dual c i)) ∘ₗ + toDualMapAtIndex (S := S) (c := Function.update c i (S.τ (c i))) i + @[simp] -lemma toDualMap_fromDualMap {c : C} (t : S.Tensor ![S.τ c]) : - toDualMap (fromDualMap t) = t := by - rw [toDualMap_apply, fromDualMap_apply, prodT_permT_right, prodT_contrT_snd, - contrT_permT, contrT_permT, contrT_comm, permT_permT, permT_permT] - conv_lhs => - enter [2, 2] - change contrT 1 1 2 _ _ - enter [2] - change contrT 3 1 2 _ _ - rw [prodT_assoc', prodT_swap, contrT_permT, contrT_permT] - conv_lhs => - enter [2, 2, 2, 2, 2] - rw [contrT_congr (n := 1 + 2) (Fin.natAdd (m := 4) 1 1) (Fin.natAdd (m := 4) 1 2) _ - (by rfl) (by rfl)] - rw (transparency := .instances) [contrT_prodT_snd 1 2 (by change _ ∧ S.τ (S.τ c) = c; simp)] - rw [contrT_dual_metricTensor_metricTensor, prodT_permT_right, prodT_swap] - simp only [CompTriple.comp_eq, permT_permT, Fin.reduceNatAdd, Fin.cast_eq_self] - conv_lhs => - enter [2, 2] - rw [permT_permT] - rw (transparency := .instances) [permT_permT, contrT_permT] - conv_lhs => - enter [2, 2, 2] - rw [contrT_congr 1 2 _ (by rfl) (by rfl)] - enter [2] - rw [contrT_unitTensor_dual_single] - simp only [permT_permT, CompTriple.comp_eq] - rw (transparency := .instances) [permT_permT] - apply permT_congr_eq_id - ext i - fin_cases i - simp - -lemma fromDualMap_eq_permT_toDualMap {c : C} (t : S.Tensor ![S.τ c]) : - fromDualMap t = permT id (by simp) (toDualMap t) := by - rw [fromDualMap_apply, toDualMap_apply] - simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, permT_permT, CompTriple.comp_eq] - rw [metricTensor_congr (by simp : c = S.τ (S.τ c))] - rw [prodT_permT_left, contrT_permT] - simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, permT_permT, CompTriple.comp_eq] - apply permT_congr - · ext i - fin_cases i - rfl - · rfl - -lemma toDualMap_eq_permT_fromDualMap {c : C} (t : S.Tensor ![c]) : - toDualMap t = (fromDualMap (permT id (by simp) t)) := by - rw [fromDualMap_eq_permT_toDualMap] - rw [toDualMap_apply, toDualMap_apply] - conv_rhs => - enter [2, 2] - rw [prodT_permT_right] - rw [metricTensor_congr (by simp : S.τ (S.τ (S.τ c)) = S.τ c)] - rw [prodT_permT_left] - rw [contrT_permT, contrT_permT] - simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, permT_permT, CompTriple.comp_eq, - τ_τ_apply, IsReindexing.on_id, Matrix.cons_val_fin_one, implies_true] - apply permT_congr - · ext i - fin_cases i - rfl - · rfl +lemma fromDualMapAtIndex_toDualMapAtIndex {n : ℕ} {c : Fin n → C} (i : Fin n) (t : S.Tensor c) : + fromDualMapAtIndex (S := S) i (toDualMapAtIndex (S := S) i t) = t := by + simp [fromDualMapAtIndex, toDualMapAtIndex_toDualMapAtIndex] @[simp] -lemma fromDualMap_toDualMap {c : C} (t : S.Tensor ![c]) : - fromDualMap (toDualMap t) = t := by - rw [fromDualMap_eq_permT_toDualMap] - conv_lhs => - enter [2, 2] - rw [toDualMap_eq_permT_fromDualMap] - simp - -/-- The linear equivalence between `S.Tensor ![c]` and - `S.Tensor ![S.τ c]` formed by contracting with metric tensors. -/ -noncomputable def toDual {c : C} : S.Tensor ![c] ≃ₗ[k] S.Tensor ![S.τ c] := - LinearEquiv.mk toDualMap fromDualMap.toFun - (fun x => by simp) (fun x => by simp) - -lemma toDual_equivariant {c : C} (g : G) (t : S.Tensor ![c]) : - toDual (g • t) = g • toDual t := by - simp [toDual, toDualMap] - conv_lhs => rw [← metricTensor_invariant g] - rw [prodT_equivariant, contrT_equivariant, permT_equivariant] - -/-- The linear map between `S.Tensor c` and `S.Tensor (Function.update c i (S.τ (c i)))` - formed by contracting with metric tensors at a specific index. -/ -noncomputable def toDualAtIndex {c : Fin n → C} (i : Fin n) : - S.Tensor c →ₗ[k] S.Tensor (Function.update c i (S.τ (c i))) where - toFun t := permT _ (IsReindexing.contr_two_rotate S i) <| - contrT (n) (Fin.natAdd n (0 : Fin 2)) (Fin.castAdd 2 i) - (by simp [Fin.ext_iff]; grind) <| - prodT t (metricTensor (S := S) (S.τ (c i))) - map_add' := by intros; simp - map_smul' := by intros; simp +lemma toDualMapAtIndex_fromDualMapAtIndex {n : ℕ} {c : Fin n → C} (i : Fin n) + (t : S.Tensor (Function.update c i (S.τ (c i)))) : + toDualMapAtIndex (S := S) i (fromDualMapAtIndex (S := S) i t) = t := by + -- `fromDualMapAtIndex` is injective, being an identity reindexing after a dualisation which + -- `fromDualMapAtIndex_toDualMapAtIndex` already inverts at the updated color assignment. + have hinj : Function.Injective (fromDualMapAtIndex (S := S) (c := c) i) := by + simp only [fromDualMapAtIndex, LinearMap.coe_comp] + exact (permT_injective _).comp + (Function.LeftInverse.injective (fromDualMapAtIndex_toDualMapAtIndex i)) + exact Function.LeftInverse.rightInverse_of_injective + (fromDualMapAtIndex_toDualMapAtIndex i) hinj t + +/-- Dualising a named index is `G`-equivariant. The content is the invariance of the metric tensor: + the action must be introduced on the metric factor before the equivariance of the contraction + applies. -/ +@[simp] +lemma toDualMapAtIndex_equivariant {n : ℕ} {c : Fin n → C} (i : Fin n) (g : G) (t : S.Tensor c) : + toDualMapAtIndex (S := S) i (g • t) = g • toDualMapAtIndex (S := S) i t := by + cases n with + | zero => exact i.elim0 + | succ nA => + rw [toDualMapAtIndex] + conv_lhs => rw [← metricTensor_invariant (S := S) g] + exact crossToSlot_equivariant i (0 : Fin 2) _ g _ t + +/-- The linear equivalence between `S.Tensor c` and `S.Tensor (Function.update c i (S.τ (c i)))` + formed by contracting with the metric tensor at the index `i`. Raising and lowering a named + index are mutually inverse, so the two color assignments carry the same information. -/ +noncomputable def toDualAtIndex {n : ℕ} {c : Fin n → C} (i : Fin n) : + S.Tensor c ≃ₗ[k] S.Tensor (Function.update c i (S.τ (c i))) := + LinearEquiv.mk (toDualMapAtIndex i) (fromDualMapAtIndex i).toFun + (fromDualMapAtIndex_toDualMapAtIndex i) (toDualMapAtIndex_fromDualMapAtIndex i) end Tensor diff --git a/Physlib/Relativity/Tensors/Elab.lean b/Physlib/Relativity/Tensors/Elab.lean index efecd4fd6..724434957 100644 --- a/Physlib/Relativity/Tensors/Elab.lean +++ b/Physlib/Relativity/Tensors/Elab.lean @@ -5,10 +5,8 @@ Authors: Joseph Tooby-Smith -/ module -public import Physlib.Relativity.Tensors.Contraction.Basic -public import Physlib.Relativity.Tensors.Evaluation -public import Physlib.Relativity.Tensors.Tensorial public import Physlib.Relativity.Tensors.Dual +public import Physlib.Relativity.Tensors.Tensorial /-! # Elaboration of tensor expressions @@ -401,7 +399,7 @@ def TensorExpressionOperator.create (stx : Syntax) : indices with `τ`-syntax. -/ def TensorExpressionOperator.jiggle : TensorExpressionOperator := fun (ind, T) => do let pos ← getJigglePos ind - let T' := pos.foldl (fun T' x => Syntax.mkApp (mkIdent ``Tensor.toDualAtIndex) + let T' := pos.foldl (fun T' x => Syntax.mkApp (mkIdent ``Tensor.toDualMapAtIndex) #[Syntax.mkNumLit (toString x), T']) T let ind' := ind.map indexRemoveTau return (ind', T') @@ -667,13 +665,13 @@ variable {k : Type} [RCLike k] {C : Type} [DecidableEq C] {G : Type} [Group G] {w : S.Tensor ![c3]} {td : S.Tensor ![S.τ c1, S.τ c2]} {M : Type} [AddCommMonoid M] [Module k M] [Tensorial S c M] (m : M) -/-- info: (toDualAtIndex 0) u : +/-- info: (toDualMapAtIndex 0) u : S.Tensor (Function.update ![c1, c2] 0 (S.τ (![c1, c2] 0))) -/ #guard_msgs (whitespace := lax) in #check {u | τ(α) β}ᵀ /-- info: (contrT 2 1 3 ⋯) - ((prodT u) ((toDualAtIndex 1) u)) : + ((prodT u) ((toDualMapAtIndex 1) u)) : S.Tensor (Fin.append ![c1, c2] (Function.update ![c1, c2] 1 (S.τ (![c1, c2] 1))) ∘ Fin.succSuccAbove 1 3) -/ #guard_msgs (whitespace := lax) in diff --git a/Physlib/Relativity/Tensors/Reindexing.lean b/Physlib/Relativity/Tensors/Reindexing.lean index bff88d4a7..4cb7df562 100644 --- a/Physlib/Relativity/Tensors/Reindexing.lean +++ b/Physlib/Relativity/Tensors/Reindexing.lean @@ -617,52 +617,6 @@ lemma fin_cast_isReindexing (n n1 : ℕ) {c : Fin n → C} (h : n1 = n) : · intro i rfl -/-- Contracting the `i`-th index of a tensor with the first index of an appended metric tensor - is, up to a cycle permutation, a reindexing to the color list where the `i`-th index is - replaced by its dual. -/ -lemma contr_two_rotate {c : Fin n → C} (i : Fin n) : IsReindexing - ((Fin.append c ![S.τ (c i), S.τ (c i)] ∘ - (Fin.natAdd n (0 : Fin 2)).succSuccAbove (Fin.castAdd 2 i))) - (Function.update c i (S.τ (c i))) - (Fin.cycleIcc i ⟨n - 1, by have := i.prop; omega⟩).symm := by - haveI : NeZero n := ⟨by have := i.prop; omega⟩ - set j : Fin n := ⟨n - 1, by have := i.prop; omega⟩ with hj - have key : ∀ y : Fin n, Fin.append c ![S.τ (c i), S.τ (c i)] - ((Fin.natAdd n (0 : Fin 2)).succSuccAbove (Fin.castAdd 2 i) y) - = Function.update c i (S.τ (c i)) (Fin.cycleIcc i j y) := by - intro y - have hval := Fin.succSuccAbove_val (Fin.natAdd n (0 : Fin 2)) (Fin.castAdd 2 i) y - simp only [Fin.val_natAdd, Fin.val_castAdd, Fin.val_zero, Nat.add_zero] at hval - rcases lt_or_ge y.val i.val with hy | hy - · -- y < i - rw [Fin.cycleIcc_of_lt (Fin.lt_def.mpr hy), - Function.update_of_ne (Fin.ne_of_val_ne (by omega)), - Fin.succSuccAbove_apply_lt_lt _ _ _ (by simp) (by simpa using hy), - show y.castSucc.castSucc = Fin.castAdd 2 y from by ext; simp, Fin.append_left] - · rcases eq_or_lt_of_le (show y.val ≤ n - 1 from by have := y.isLt; omega) with hyj | hyj - · -- y = j (the last index) - have hyj' : y = j := Fin.ext (by rw [hj]; exact hyj) - subst hyj' - have hval' : ((Fin.natAdd n (0 : Fin 2)).succSuccAbove (Fin.castAdd 2 i) j).val - = n + 1 := by rw [hval]; split_ifs <;> omega - rw [Fin.cycleIcc_of_last (Fin.le_def.mpr (by rw [hj]; omega)), Function.update_self, - show (Fin.natAdd n (0 : Fin 2)).succSuccAbove (Fin.castAdd 2 i) j = - Fin.natAdd n (1 : Fin 2) - from Fin.ext (by rw [hval']; simp [Fin.val_natAdd]), Fin.append_right] - simp - · -- i ≤ y < j - have hy1 : (y + 1).val = y.val + 1 := by - rw [Fin.val_add, Fin.val_one', Nat.mod_eq_of_lt (show 1 < n by omega), - Nat.mod_eq_of_lt (show y.val + 1 < n by omega)] - have hval' : ((Fin.natAdd n (0 : Fin 2)).succSuccAbove (Fin.castAdd 2 i) y).val - = y.val + 1 := by rw [hval]; split_ifs <;> omega - rw [Fin.cycleIcc_of_ge_of_lt (Fin.le_def.mpr hy) (Fin.lt_def.mpr hyj), - Function.update_of_ne (Fin.ne_of_val_ne (by omega)), - show (Fin.natAdd n (0 : Fin 2)).succSuccAbove (Fin.castAdd 2 i) y = Fin.castAdd 2 (y + 1) - from Fin.ext (by rw [hval', Fin.val_castAdd, hy1]), Fin.append_left] - refine ⟨(Equiv.symm _).bijective, fun x => ?_⟩ - rw [Function.comp_apply, key, Equiv.apply_symm_apply] - end IsReindexing end Tensor From 795b9c1a254ff9b30eb3855f3a6d8509ce03c7c3 Mon Sep 17 00:00:00 2001 From: Andrea Pari Date: Mon, 27 Jul 2026 16:16:24 +0100 Subject: [PATCH 7/9] feat(Tensors/Contraction): raising and lowering a named index as an equivalence MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `crossToSlot_raise_lower_round_trip` showed that contracting slot `i` against `M` and then against `M'` is the identity when the pair collapses to the unit tensor. Nothing bundled that with the reverse collapse, so the only mutually inverse pair in the library was the metric, which `toDualAtIndex` inverted by hand. `crossToSlotEquiv` is the general statement: a pair collapsing to the unit tensor in both orders makes the two contractions mutually inverse, so `c` and `Function.update c i d` carry the same tensors. The surviving colour `d` is unrelated to `c i`, so a pairing of a colour with something other than its variance dual, such as a Hermitian pairing of a colour with its conjugate, is covered as much as a metric and its inverse at `τ (c i)`. The two collapses are independent hypotheses: for a propositionally matched pair neither order follows from the other, and there is no cardinality relation between the index sets to supply one. `IsReindexing.unitTensor_pair` is generalised accordingly. The colour list it certifies reads only the surviving colours `a` and `e`, so pinning the second factor's contracted slot to `S.τ d` constrained nothing; freeing it to `b` is what lets both metrics enter `toDualAtIndex` at literal colours, with no transporting `permT` on either factor. That in turn removes the transported second metric and its reconciliation from `toDualMapAtIndex_toDualMapAtIndex`. `toDualAtIndex` is now that equivalence instantiated at `metricTensor (τ (c i))`, `metricTensor (c i)`, and `fromDualMapAtIndex` is the matching `crossToSlotInv`, so the two round trips are the general ones rather than a second hand-rolled inverse. `crossToSlotInv` and the round trip's colour cast are placed at the altitude they belong to: the former in `CrossToSlot`, which is the `CommRing` layer, the latter in `Reindexing` next to `moveLast`, where the two round-trip statements now use it instead of restating it inline. With its API settled, `Dual.lean` takes the module header used across the contraction files — overview, key results, table of contents, references — and lettered body sections, and its declaration docstrings move to the declarative register of those files: each states what the object is, without commentary on the proof mechanics or on the hypotheses of the helper lemmas. Co-authored-by: Claude Opus 4.8 --- .../Tensors/Contraction/CrossToSlot.lean | 14 ++ .../Contraction/UnitTensorContraction.lean | 123 +++++++--- Physlib/Relativity/Tensors/Dual.lean | 227 ++++++++++++------ Physlib/Relativity/Tensors/Reindexing.lean | 6 + 4 files changed, 268 insertions(+), 102 deletions(-) diff --git a/Physlib/Relativity/Tensors/Contraction/CrossToSlot.lean b/Physlib/Relativity/Tensors/Contraction/CrossToSlot.lean index cd3dcf8fc..c91c25763 100644 --- a/Physlib/Relativity/Tensors/Contraction/CrossToSlot.lean +++ b/Physlib/Relativity/Tensors/Contraction/CrossToSlot.lean @@ -27,6 +27,8 @@ operation live with the unit-tensor collapse theory in - `TensorSpecies.Tensor.crossToSlot` : contract slot `i` against slot `j` of a rank-2 tensor and rotate the survivor back into position `i`; raising and lowering a named index. - `TensorSpecies.Tensor.crossToSlot_eq_crossToEnd` : the bridge to the result-to-end convention. +- `TensorSpecies.Tensor.crossToSlotInv` : the returning half of a round trip, the contraction + against the second factor with the round trip's color cast absorbed. - `TensorSpecies.Tensor.crossToSlot_permT_right_id` : an identity reindexing of the rank-2 tensor passes through the contraction. - `TensorSpecies.Tensor.crossToSlot_equivariant` : the contraction commutes with the `G`-action. @@ -98,6 +100,18 @@ lemma crossToSlot_eq_crossToEnd {nA : ℕ} {c : Fin (nA + 1) → C} {cM : Fin 2 permT ⇑(Fin.cycleIcc i (Fin.last nA)).symm (IsReindexing.crossToSlot_cycle i j) (crossToEnd i j hc t M) := rfl +/-- Contract slot `i` of a tensor whose color there is `d` against `M'`, then absorb the color cast + the two `Function.update`s generate, landing back on `c`. This is the returning half of a + raise-then-lower round trip; absorbing the cast here is what keeps the round trip cast-free at + both ends. -/ +noncomputable def crossToSlotInv {nA : ℕ} {c : Fin (nA + 1) → C} {b d e : C} (i : Fin (nA + 1)) + (he : c i = e) (hb : S.τ d = b) (M' : S.Tensor ![b, e]) : + S.Tensor (Function.update c i d) →ₗ[k] S.Tensor c := + permT (id : Fin (nA + 1) → Fin (nA + 1)) + (IsReindexing.on_id_symm (IsReindexing.update_update_of_eq (d := d) i he)) ∘ₗ + crossToSlot i (0 : Fin 2) + (by rw [Function.update_self]; exact hb : S.τ (Function.update c i d i) = b) M' + /-- An identity reindexing of the rank-2 tensor becomes the corresponding identity reindexing of the contracted output: the `crossToSlot`-level case of `crossToEnd_permT_right` where the rank-2 tensor's colors are only propositionally recast. -/ diff --git a/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean b/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean index 5f624ba64..c6b8688e4 100644 --- a/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean +++ b/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean @@ -21,12 +21,12 @@ the unit tensor and then contracting away. `crossToEnd_unitTensor` is proved by decomposing `t` along its last slot (`eq_sum_evalT`) and transporting to an arbitrary slot with the transposition `swap i (last)`. On it the round trip -against a matched pair is assembled in both conventions: -`crossToEnd_round_trip_of_unit_slot` in result-to-end form and -`crossToSlot_raise_lower_round_trip` in result-to-slot form, with -`toDualMapAtIndex_toDualMapAtIndex` as the metric specialisation. Since `unitTensor` is -`RCLike`-valued, this material sits over an `[RCLike k]` variable block, apart from the `CommRing` -`crossToEnd`/`crossToSlot` algebra. +against a matched pair is assembled in both conventions, and a pair collapsing in *both* orders +makes the two contractions mutually inverse, which `crossToSlotEquiv` bundles as a linear +equivalence between the two color assignments. + +Since `unitTensor` is `RCLike`-valued, this material sits over an `[RCLike k]` variable block, apart +from the `CommRing` `crossToEnd`/`crossToSlot` algebra. ## ii. Key results @@ -35,12 +35,15 @@ against a matched pair is assembled in both conventions: - `TensorSpecies.Tensor.crossToEnd_round_trip_of_unit_slot` : two contractions against a pair that collapses to the unit tensor return the original tensor, in result-to-end form. - `TensorSpecies.Tensor.crossToSlot_raise_lower_round_trip` : the round trip in result-to-slot - form, the shape `toDualMapAtIndex_toDualMapAtIndex` consumes. + form, every color propositional. +- `TensorSpecies.Tensor.crossToSlotEquiv` : raising and lowering a named index against a pair that + collapses in both orders, as a linear equivalence. ## iii. Table of contents - A. The unit tensor as a slot-contraction identity - B. Round trips against a matched pair +- C. Raising and lowering as an equivalence ## iv. References @@ -186,15 +189,15 @@ contracting a slot first against one and then against the other returns the orig -/ -/-- The color list `crossToEnd` produces from a matched rank-2 pair `M : ![a, d]`, - `M' : ![S.τ d, e]` is the color list `![S.τ e, e]` of `unitTensor e`, via the identity slot map; - the reindexing carried by the collapse hypothesis `M · M' = δ` of the round trips below. The - pair's outer color `a` equals `S.τ e` only propositionally, so a caller whose metric sits at a - literal color supplies `h` directly instead of transporting the tensor. -/ -lemma IsReindexing.unitTensor_pair {a d e : C} (h : S.τ e = a) : +/-- The color list `crossToEnd` produces from a matched rank-2 pair `M : ![a, d]`, `M' : ![b, e]` is + the color list `![S.τ e, e]` of `unitTensor e`, via the identity slot map: the reindexing carried + by the collapse hypothesis `M · M' = δ` of the round trips below. Only the surviving colors `a` + and `e` enter, and `a` equals `S.τ e` only propositionally, so a pair whose colors match + propositionally enters with no transport. -/ +lemma IsReindexing.unitTensor_pair {a b d e : C} (h : S.τ e = a) : IsReindexing (![S.τ e, e] : Fin 2 → C) (Fin.append ((![a, d] : Fin 2 → C) ∘ (Fin.last 1).succAbove) - ((![S.τ d, e] : Fin 2 → C) ∘ (0 : Fin 2).succAbove)) + ((![b, e] : Fin 2 → C) ∘ (0 : Fin 2).succAbove)) (id : Fin 2 → Fin 2) := IsReindexing.on_id.mpr (fun j => by fin_cases j <;> first | exact h | rfl) @@ -261,13 +264,7 @@ private lemma crossToSlot_round_trip_of_unit {nA : ℕ} {c : Fin (nA + 1) → C} crossToSlot (S := S) i (0 : Fin 2) (by rw [Function.update_self] : S.τ (Function.update c i d i) = S.τ d) M₂ (crossToSlot (S := S) i (0 : Fin 2) rfl M₁ t) = - permT (id : Fin (nA + 1) → Fin (nA + 1)) - (IsReindexing.on_id.mpr (fun j => by - by_cases h : j = i - · subst h - simp [Function.update_self] - · simp [Function.update_of_ne h])) - t := by + permT (id : Fin (nA + 1) → Fin (nA + 1)) (IsReindexing.update_update_of_eq i rfl) t := by have hcycle : (⇑(Fin.cycleIcc i (Fin.last nA)).symm) i = Fin.last nA := (Equiv.symm_apply_eq _).2 (Fin.cycleIcc_of_last (Fin.le_last i)).symm rw [crossToSlot_eq_crossToEnd, crossToSlot_eq_crossToEnd] @@ -305,7 +302,8 @@ private lemma crossToSlot_round_trip_of_unit {nA : ℕ} {c : Fin (nA + 1) → C} No color is pinned to a composite. `ha : τ (c i) = a` places the metric's contracted slot, `hb : τ d = b` the inverse's, and `he : c i = e` the surviving one, so a caller whose metric and inverse sit at literal colors supplies them directly, with no transporting `permT` on either - factor, and recovers the tensor with slot `i` at the literal. -/ + factor. Lowering then raising is this same statement with `M` and `M'` exchanged and the reversed + collapse `M' · M = δ`; neither collapse follows from the other here. -/ lemma crossToSlot_raise_lower_round_trip {nA : ℕ} {c : Fin (nA + 1) → C} {a b d e : C} (i : Fin (nA + 1)) (he : c i = e) (ha : S.τ (c i) = a) (hb : S.τ d = b) (M : Tensor S ![a, d]) (M' : Tensor S ![b, e]) @@ -317,18 +315,85 @@ lemma crossToSlot_raise_lower_round_trip {nA : ℕ} {c : Fin (nA + 1) → C} {a crossToSlot (S := S) i (0 : Fin 2) (by rw [Function.update_self]; exact hb : S.τ (Function.update c i d i) = b) M' (crossToSlot (S := S) i (0 : Fin 2) ha M t) = - permT (id : Fin (nA + 1) → Fin (nA + 1)) - (IsReindexing.on_id.mpr (fun j => by - by_cases h : j = i - · subst h - simp [Function.update_self, he] - · simp [Function.update_of_ne h])) - t := by + permT (id : Fin (nA + 1) → Fin (nA + 1)) (IsReindexing.update_update_of_eq i he) t := by subst ha subst hb subst he exact crossToSlot_round_trip_of_unit i M M' hM t +/-! + +## C. Raising and lowering as an equivalence + +A pair collapsing to the unit tensor in both orders makes the two contractions mutually inverse, so +the color lists `c` and `Function.update c i d` carry the same tensors. + +-/ + +section RoundTripEquiv + +variable {nA : ℕ} {c : Fin (nA + 1) → C} {a b d e : C} (i : Fin (nA + 1)) + (he : c i = e) (ha : S.τ (c i) = a) (hb : S.τ d = b) + (M : Tensor S ![a, d]) (M' : Tensor S ![b, e]) + (hMM' : crossToEnd (Fin.last 1) (0 : Fin 2) hb M M' = + permT (id : Fin 2 → Fin 2) + (IsReindexing.unitTensor_pair ((congrArg S.τ he.symm).trans ha)) + (unitTensor (S := S) e)) + (hM'M : crossToEnd (Fin.last 1) (0 : Fin 2) ((congrArg S.τ he.symm).trans ha) M' M = + permT (id : Fin 2 → Fin 2) (IsReindexing.unitTensor_pair hb) (unitTensor (S := S) d)) + +include hMM' in +/-- Lowering undoes raising: `crossToSlot_raise_lower_round_trip` with the color cast absorbed into + `crossToSlotInv`. -/ +lemma crossToSlotInv_crossToSlot (t : Tensor S c) : + crossToSlotInv i he hb M' (crossToSlot i (0 : Fin 2) ha M t) = t := by + simp only [crossToSlotInv, LinearMap.coe_comp, Function.comp_apply] + -- Unfolding `crossToSlotInv` leaves the inner slot proof at the clean color `b` where the + -- `crossToSlot` application wants the composite `![b, e] 0`, so `rw` cannot key on the round + -- trip; `erw` matches up to defeq. + erw [crossToSlot_raise_lower_round_trip i he ha hb M M' hMM' t, permT_permT] + exact permT_congr_eq_id _ _ _ rfl + +include hMM' hM'M in +/-- Raising undoes lowering. The reversed collapse `M' · M = δ` is the round trip at the color + list `Function.update c i d` with the pair exchanged, which gives the lowering half a left + inverse and hence injectivity; that upgrades `crossToSlotInv_crossToSlot` to a two-sided + inverse. -/ +lemma crossToSlot_crossToSlotInv (t : Tensor S (Function.update c i d)) : + crossToSlot i (0 : Fin 2) ha M (crossToSlotInv i he hb M' t) = t := by + have hswap := crossToSlot_raise_lower_round_trip (S := S) (c := Function.update c i d) i + (by simp : Function.update c i d i = d) + (by rw [Function.update_self]; exact hb : S.τ (Function.update c i d i) = b) + ((congrArg S.τ he.symm).trans ha) M' M hM'M + have hgi : Function.Injective (crossToSlot (S := S) i (0 : Fin 2) + (show S.τ (Function.update c i d i) = b by rw [Function.update_self]; exact hb) M') := by + intro x y hxy + exact permT_injective _ (by rw [← hswap x, ← hswap y, hxy]) + have hinj : Function.Injective (crossToSlotInv (S := S) i he hb M') := by + simp only [crossToSlotInv, LinearMap.coe_comp] + exact (permT_injective _).comp hgi + exact Function.LeftInverse.rightInverse_of_injective + (crossToSlotInv_crossToSlot i he ha hb M M' hMM') hinj t + +/-- Raising and lowering a named index against a mutually inverse pair, as a linear equivalence: the + two color assignments `c` and `Function.update c i d` carry the same tensors. `M` and `M'` are + matched only propositionally and `d` is unrelated to `c i`, so this covers a metric pairing two + unrelated colors as well as a metric and its inverse at `S.τ (c i)`. -/ +noncomputable def crossToSlotEquiv : Tensor S c ≃ₗ[k] Tensor S (Function.update c i d) := + LinearEquiv.mk (crossToSlot i (0 : Fin 2) ha M) (crossToSlotInv i he hb M').toFun + (crossToSlotInv_crossToSlot i he ha hb M M' hMM') + (crossToSlot_crossToSlotInv i he ha hb M M' hMM' hM'M) + +@[simp] +lemma crossToSlotEquiv_apply (t : Tensor S c) : + crossToSlotEquiv i he ha hb M M' hMM' hM'M t = crossToSlot i (0 : Fin 2) ha M t := rfl + +@[simp] +lemma crossToSlotEquiv_symm_apply (t : Tensor S (Function.update c i d)) : + (crossToSlotEquiv i he ha hb M M' hMM' hM'M).symm t = crossToSlotInv i he hb M' t := rfl + +end RoundTripEquiv + end Tensor end TensorSpecies diff --git a/Physlib/Relativity/Tensors/Dual.lean b/Physlib/Relativity/Tensors/Dual.lean index 15f0a0234..d505a518d 100644 --- a/Physlib/Relativity/Tensors/Dual.lean +++ b/Physlib/Relativity/Tensors/Dual.lean @@ -11,6 +11,44 @@ public import Physlib.Relativity.Tensors.Contraction.UnitTensorContraction # Dual tensors +## i. Overview + +The metric tensor identifies a tensor with the one obtained by dualising the color of a single +index: contracting slot `i` of `t` against `metricTensor (S.τ (c i))` returns a tensor of color +`Function.update c i (S.τ (c i))`, leaving every other slot alone. This is the raising and lowering +of a named index, `T^{μν} ↦ T_{μ}{}^{ν}`. `toDualMapAtIndex i` is that contraction, `crossToSlot` +against the metric, at every rank and every named slot. + +A metric contracted against the metric at the dual color collapses to the unit tensor, in both +orders. So the contraction back against `metricTensor (c i)`, `fromDualMapAtIndex i`, inverts it, +and the two assemble into the linear equivalence `toDualAtIndex i`: the two color assignments +carry the same information. Dualising the same index twice returns the original tensor, up to the +reindexing of the colors. + +## ii. Key results + +- `TensorSpecies.Tensor.toDualMapAtIndex` : dualise the color of the index `i` by contracting with + the metric tensor. +- `TensorSpecies.Tensor.fromDualMapAtIndex` : the returning contraction, against the metric tensor + at `c i`. +- `TensorSpecies.Tensor.toDualMapAtIndex_toDualMapAtIndex` : dualising the index `i` twice returns + the original tensor. +- `TensorSpecies.Tensor.toDualMapAtIndex_equivariant` : dualising an index commutes with the + `G`-action. +- `TensorSpecies.Tensor.toDualAtIndex` : raising and lowering the index `i` as a linear + equivalence. + +## iii. Table of contents + +- A. Dualising a named index +- B. Contracting a metric against its dual +- C. Dualising twice +- D. The returning contraction +- E. Equivariance +- F. Raising and lowering as an equivalence + +## iv. References + -/ @[expose] public section @@ -25,24 +63,59 @@ variable {k : Type} [RCLike k] {C : Type} {G : Type} [Group G] namespace Tensor -/-- The linear map between `S.Tensor c` and `S.Tensor (Function.update c i (S.τ (c i)))` formed by - contracting with the metric tensor at a specific index. It is `crossToSlot` against - `metricTensor (S.τ (c i))`, the case where the rank-2 tensor's two slots share a color. -/ +/-! + +## A. Dualising a named index + +-/ + +/-- The linear map between `S.Tensor c` and `S.Tensor (Function.update c i (S.τ (c i)))` + formed by contracting the index `i` with the metric tensor. -/ noncomputable def toDualMapAtIndex : {n : ℕ} → {c : Fin n → C} → (i : Fin n) → S.Tensor c →ₗ[k] S.Tensor (Function.update c i (S.τ (c i))) | 0, _, i => i.elim0 | _ + 1, c, i => crossToSlot i (0 : Fin 2) rfl (metricTensor (S := S) (S.τ (c i))) -/-- Dualising slot `i` twice returns the original color list: `τ (τ (c i)) = c i`, and no other - slot moves. The color cast carried by the double-dual round trips below. -/ +/-! + +## B. Contracting a metric against its dual + +-/ + +/-- The metric tensor at `S.τ c` contracted with the metric tensor at `c` is the unit tensor + at `c`. -/ +lemma crossToEnd_dual_metricTensor_metricTensor {c : C} : + crossToEnd (Fin.last 1) (0 : Fin 2) (S.τ_τ_apply c) (metricTensor (S := S) (S.τ c)) + (metricTensor (S := S) c) = + permT (id : Fin 2 → Fin 2) (IsReindexing.unitTensor_pair rfl) (unitTensor (S := S) c) := by + rw [crossToEnd_two, contrT_dual_metricTensor_metricTensor, permT_permT] + exact permT_congr rfl rfl + +/-- The metric tensor at `c` contracted with the metric tensor at `S.τ c` is the unit tensor + at `S.τ c`. -/ +lemma crossToEnd_metricTensor_metricTensor_eq_dual_unit {c : C} : + crossToEnd (Fin.last 1) (0 : Fin 2) rfl (metricTensor (S := S) c) + (metricTensor (S := S) (S.τ c)) = + permT (id : Fin 2 → Fin 2) (IsReindexing.unitTensor_pair (S.τ_τ_apply c)) + (unitTensor (S := S) (S.τ c)) := by + rw [crossToEnd_two, contrT_metricTensor_metricTensor_eq_dual_unit, permT_permT] + exact permT_congr (by decide) rfl + +/-! + +## C. Dualising twice + +-/ + +/-- Dualising the color of the index `i` twice gives back `c`, as a reindexing along the + identity. -/ lemma IsReindexing.update_dual_dual {n : ℕ} (c : Fin n → C) (i : Fin n) : IsReindexing c (Function.update (Function.update c i (S.τ (c i))) i (S.τ (Function.update c i (S.τ (c i)) i))) (id : Fin n → Fin n) := - IsReindexing.on_id.mpr (fun j => by - by_cases h : j = i <;> simp [h, Function.update_of_ne, τ_τ_apply]) + IsReindexing.update_update_of_eq i (by simp [τ_τ_apply]) -/-- Dualising any named index twice returns the original tensor, up to the color cast generated by -the two `Function.update`s. Stated at every rank, matching the domain of `toDualMapAtIndex`. -/ +/-- Dualising the index `i` twice returns the original tensor, up to the reindexing of the + colors. -/ lemma toDualMapAtIndex_toDualMapAtIndex {n : ℕ} {c : Fin n → C} (i : Fin n) (t : S.Tensor c) : toDualMapAtIndex (S := S) i (toDualMapAtIndex (S := S) i t) = @@ -50,73 +123,58 @@ lemma toDualMapAtIndex_toDualMapAtIndex {n : ℕ} {c : Fin n → C} cases n with | zero => exact i.elim0 | succ nA => - let M₁ := metricTensor (S := S) (S.τ (c i)) - let M₂ : S.Tensor ![S.τ (S.τ (c i)), c i] := - permT (fun x : Fin 2 => x) - (IsReindexing.on_id.mpr (fun j => by fin_cases j <;> simp [τ_τ_apply])) - (metricTensor (S := S) (c i)) - -- The two dual metrics collapse to the unit tensor: `gᵃᵇ · g_cd = δ`. - have hM : crossToEnd (S := S) (Fin.last 1) (0 : Fin 2) rfl M₁ M₂ = - permT (id : Fin 2 → Fin 2) (IsReindexing.unitTensor_pair rfl) - (unitTensor (S := S) (c i)) := by - dsimp only [M₁, M₂] - rw [crossToEnd_permT_right (Fin.last 1) (0 : Fin 2) - (fun x : Fin 2 => x) (fun x : Fin 1 => x) - (IsReindexing.on_id.mpr (fun i => by fin_cases i <;> simp [τ_τ_apply])) rfl] - rw [crossToEnd_two, contrT_dual_metricTensor_metricTensor] - simp only [Fin.isValue, Nat.reduceAdd, permT_permT, CompTriple.comp_eq] - refine permT_congr ?_ rfl - ext j; fin_cases j <;> rfl - have key := crossToSlot_raise_lower_round_trip (S := S) i (M := M₁) (M' := M₂) - (he := rfl) (ha := rfl) (hb := rfl) (hM := hM) (t := t) - -- Reconcile the second metric's symmetric color with the mixed contraction color. - let x := S.τ (Function.update c i (S.τ (c i)) i) - have hmetric : metricTensor (S := S) x = - permT (id : Fin 2 → Fin 2) - (IsReindexing.on_id.mpr (fun j => by - fin_cases j <;> simp [x, Function.update_self, τ_τ_apply])) M₂ := by - dsimp only [M₂] - rw [metricTensor_congr (by simp [x, Function.update_self, τ_τ_apply] : x = c i)] - rw [permT_permT] - refine permT_congr ?_ rfl - ext j; fin_cases j <;> rfl - rw [toDualMapAtIndex, toDualMapAtIndex] - change crossToSlot i (0 : Fin 2) rfl (metricTensor (S := S) x) - (crossToSlot i (0 : Fin 2) rfl M₁ t) = _ - rw [hmetric, crossToSlot_permT_right_id, key] - simp only [permT_permT] - refine permT_congr ?_ rfl - funext j; simp - -/-- The inverse of `toDualMapAtIndex` at the same index: dualise again, then absorb the color cast - the two `Function.update`s generate. Absorbing it here is what makes the round trips in both - directions cast-free. -/ -noncomputable def fromDualMapAtIndex {n : ℕ} {c : Fin n → C} (i : Fin n) : - S.Tensor (Function.update c i (S.τ (c i))) →ₗ[k] S.Tensor c := - permT (id : Fin n → Fin n) (IsReindexing.on_id_symm (IsReindexing.update_dual_dual c i)) ∘ₗ - toDualMapAtIndex (S := S) (c := Function.update c i (S.τ (c i))) i + -- Both metrics enter at literal colors, matched by `S.τ_τ_apply`, so neither is transported. + have key := crossToSlot_raise_lower_round_trip (S := S) i (he := rfl) (ha := rfl) + (hb := S.τ_τ_apply (c i)) (M := metricTensor (S := S) (S.τ (c i))) + (M' := metricTensor (S := S) (c i)) + (hM := crossToEnd_dual_metricTensor_metricTensor) (t := t) + -- The second dualisation reads its metric at the composite color the first one left behind. + rw [toDualMapAtIndex, toDualMapAtIndex, + metricTensor_congr (by simp [Function.update_self, τ_τ_apply] : + S.τ (Function.update c i (S.τ (c i)) i) = c i)] + erw [crossToSlot_permT_right_id, key, permT_permT] + exact permT_congr (by funext j; simp) rfl + +/-! + +## D. The returning contraction + +-/ + +/-- The linear map between `S.Tensor (Function.update c i (S.τ (c i)))` and `S.Tensor c` + formed by contracting the index `i` with the metric tensor. It is the inverse of + `toDualMapAtIndex`. -/ +noncomputable def fromDualMapAtIndex : {n : ℕ} → {c : Fin n → C} → (i : Fin n) → + S.Tensor (Function.update c i (S.τ (c i))) →ₗ[k] S.Tensor c + | 0, _, i => i.elim0 + | _ + 1, c, i => crossToSlotInv i rfl (S.τ_τ_apply (c i)) (metricTensor (S := S) (c i)) @[simp] lemma fromDualMapAtIndex_toDualMapAtIndex {n : ℕ} {c : Fin n → C} (i : Fin n) (t : S.Tensor c) : fromDualMapAtIndex (S := S) i (toDualMapAtIndex (S := S) i t) = t := by - simp [fromDualMapAtIndex, toDualMapAtIndex_toDualMapAtIndex] + cases n with + | zero => exact i.elim0 + | succ nA => + exact crossToSlotInv_crossToSlot i rfl rfl (S.τ_τ_apply (c i)) _ _ + crossToEnd_dual_metricTensor_metricTensor t @[simp] lemma toDualMapAtIndex_fromDualMapAtIndex {n : ℕ} {c : Fin n → C} (i : Fin n) (t : S.Tensor (Function.update c i (S.τ (c i)))) : toDualMapAtIndex (S := S) i (fromDualMapAtIndex (S := S) i t) = t := by - -- `fromDualMapAtIndex` is injective, being an identity reindexing after a dualisation which - -- `fromDualMapAtIndex_toDualMapAtIndex` already inverts at the updated color assignment. - have hinj : Function.Injective (fromDualMapAtIndex (S := S) (c := c) i) := by - simp only [fromDualMapAtIndex, LinearMap.coe_comp] - exact (permT_injective _).comp - (Function.LeftInverse.injective (fromDualMapAtIndex_toDualMapAtIndex i)) - exact Function.LeftInverse.rightInverse_of_injective - (fromDualMapAtIndex_toDualMapAtIndex i) hinj t - -/-- Dualising a named index is `G`-equivariant. The content is the invariance of the metric tensor: - the action must be introduced on the metric factor before the equivariance of the contraction - applies. -/ + cases n with + | zero => exact i.elim0 + | succ nA => + exact crossToSlot_crossToSlotInv i rfl rfl (S.τ_τ_apply (c i)) _ _ + crossToEnd_dual_metricTensor_metricTensor crossToEnd_metricTensor_metricTensor_eq_dual_unit t + +/-! + +## E. Equivariance + +-/ + +/-- Dualising the index `i` commutes with the action of `G`. -/ @[simp] lemma toDualMapAtIndex_equivariant {n : ℕ} {c : Fin n → C} (i : Fin n) (g : G) (t : S.Tensor c) : toDualMapAtIndex (S := S) i (g • t) = g • toDualMapAtIndex (S := S) i t := by @@ -127,13 +185,36 @@ lemma toDualMapAtIndex_equivariant {n : ℕ} {c : Fin n → C} (i : Fin n) (g : conv_lhs => rw [← metricTensor_invariant (S := S) g] exact crossToSlot_equivariant i (0 : Fin 2) _ g _ t +/-! + +## F. Raising and lowering as an equivalence + +-/ + /-- The linear equivalence between `S.Tensor c` and `S.Tensor (Function.update c i (S.τ (c i)))` - formed by contracting with the metric tensor at the index `i`. Raising and lowering a named - index are mutually inverse, so the two color assignments carry the same information. -/ -noncomputable def toDualAtIndex {n : ℕ} {c : Fin n → C} (i : Fin n) : - S.Tensor c ≃ₗ[k] S.Tensor (Function.update c i (S.τ (c i))) := - LinearEquiv.mk (toDualMapAtIndex i) (fromDualMapAtIndex i).toFun - (fromDualMapAtIndex_toDualMapAtIndex i) (toDualMapAtIndex_fromDualMapAtIndex i) + formed by contracting the index `i` with the metric tensor. -/ +noncomputable def toDualAtIndex : {n : ℕ} → {c : Fin n → C} → (i : Fin n) → + S.Tensor c ≃ₗ[k] S.Tensor (Function.update c i (S.τ (c i))) + | 0, _, i => i.elim0 + | _ + 1, c, i => + crossToSlotEquiv i rfl rfl (S.τ_τ_apply (c i)) (metricTensor (S := S) (S.τ (c i))) + (metricTensor (S := S) (c i)) crossToEnd_dual_metricTensor_metricTensor + crossToEnd_metricTensor_metricTensor_eq_dual_unit + +@[simp] +lemma toDualAtIndex_apply {n : ℕ} {c : Fin n → C} (i : Fin n) (t : S.Tensor c) : + toDualAtIndex (S := S) i t = toDualMapAtIndex (S := S) i t := by + cases n with + | zero => exact i.elim0 + | succ nA => rfl + +@[simp] +lemma toDualAtIndex_symm_apply {n : ℕ} {c : Fin n → C} (i : Fin n) + (t : S.Tensor (Function.update c i (S.τ (c i)))) : + (toDualAtIndex (S := S) i).symm t = fromDualMapAtIndex (S := S) i t := by + cases n with + | zero => exact i.elim0 + | succ nA => rfl end Tensor diff --git a/Physlib/Relativity/Tensors/Reindexing.lean b/Physlib/Relativity/Tensors/Reindexing.lean index 4cb7df562..1a2e32214 100644 --- a/Physlib/Relativity/Tensors/Reindexing.lean +++ b/Physlib/Relativity/Tensors/Reindexing.lean @@ -597,6 +597,12 @@ lemma moveLast {n : ℕ} {c : Fin (n + 1) → C} {c1 : Fin 2 → C} (i : Fin (n · fin_cases a simp [Fin.append_right, hc]⟩ +/-- 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 => by by_cases h : j = i <;> simp [h, Function.update_of_ne, he]) + /-- 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`. -/ From fae84632ac21c80c5ff8a72fbc98d64f3b03bd43 Mon Sep 17 00:00:00 2001 From: Andrea Pari Date: Mon, 27 Jul 2026 23:14:09 +0100 Subject: [PATCH 8/9] refactor(Tensors): drop the unused equivalence unfolding lemmas and update_dual_dual MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `crossToSlotEquiv_apply` and `crossToSlotEquiv_symm_apply` were the standard unfolding pair for a `LinearEquiv`, but nothing keys on them: `crossToSlotEquiv` takes eight explicit arguments, so it is not applied by hand, and the downstream `toDualAtIndex_apply` and `toDualAtIndex_symm_apply` are `rfl` rather than rewrites through them. The remaining three declarations of the section are load-bearing — the two round trips are the `left_inv` and `right_inv` arguments of the equivalence and are what `fromDualMapAtIndex_toDualMapAtIndex` and `toDualMapAtIndex_fromDualMapAtIndex` state at map level, before the equivalence exists. `IsReindexing.update_dual_dual` named the identity reindexing between `c` and its twice-dualised colour list. With `IsReindexing.update_update_of_eq` stating that for an arbitrary colour equality, the specialisation carried nothing beyond `by simp [τ_τ_apply]` and had a single use, which now supplies it inline. The section C header prose of `UnitTensorContraction` restated the overview's sentence on the two collapse orders; it now says instead where each of them is used. The proof comments there are trimmed to the transparency behaviour that the tactics do not show. Co-authored-by: Claude Opus 4.8 --- .../Contraction/UnitTensorContraction.lean | 34 ++++++------------- Physlib/Relativity/Tensors/Dual.lean | 10 ++---- 2 files changed, 12 insertions(+), 32 deletions(-) diff --git a/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean b/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean index c6b8688e4..23729c408 100644 --- a/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean +++ b/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean @@ -109,9 +109,8 @@ private lemma crossToEnd_prodT_unitTensor {nV : ℕ} {cE : Fin nV → C} {cB : C (prodT E (contrT 1 0 1 hij (prodT B (unitTensor cB)))) := contrT_prodT_snd (0 : Fin 3) 1 hij (prodT B (unitTensor cB)) E rw [contrT_single_unitTensor] at key - -- The `contrT_congr` pinning above leaves a goal whose slot proofs are not syntactically equal - -- to `key`'s, so `rw` at reducible transparency cannot key on them; `instances` transparency - -- matches. The final `permT_permT` needs the full `erw`. + -- The `contrT_congr` pinning leaves slot proofs that match `key`'s only at `instances` + -- transparency; the trailing `permT_permT` needs the full `erw`. rw (transparency := .instances) [key, permT_permT] rw [prodT_permT_right, permT_permT] erw [permT_permT] @@ -238,9 +237,8 @@ lemma crossToEnd_round_trip_of_unit_slot {nA : ℕ} {c : Fin (nA + 1) → C} {d rw [crossToEnd_permT_right i (0 : Fin 2) (id : Fin 2 → Fin 2) (fun x : Fin 1 => x) (IsReindexing.on_id.mpr (fun i => by fin_cases i <;> rfl)) rfl] - -- The `id`-spelled map from `crossToEnd_permT_right` leaves the composite slot proof only - -- type-correct at default transparency, so `rw`/`simp` cannot key on `crossToEnd_unitTensor` - -- or `permT_permT`; `erw` matches up to defeq. + -- The `id`-spelled map leaves the composite slot proof type-correct only at default + -- transparency, so `rw`/`simp` cannot key on it; `erw` matches up to defeq. erw [crossToEnd_unitTensor (nA := nA) (cA := c) (c := c i) i rfl] erw [permT_permT, permT_permT] apply permT_congr @@ -268,11 +266,8 @@ private lemma crossToSlot_round_trip_of_unit {nA : ℕ} {c : Fin (nA + 1) → C} have hcycle : (⇑(Fin.cycleIcc i (Fin.last nA)).symm) i = Fin.last nA := (Equiv.symm_apply_eq _).2 (Fin.cycleIcc_of_last (Fin.le_last i)).symm rw [crossToSlot_eq_crossToEnd, crossToSlot_eq_crossToEnd] - -- `crossToSlot`'s output color `Function.update c i (cM ((0).succAbove 0))` reduces to the clean - -- color only after the `Fin.cons` reduction (default transparency), so the unfolded goal is not - -- type-correct at `instances` transparency and `rw` cannot key on the composite. Precompute the - -- left commutator (its `rfl`-heavy `hσ'` witness elaborated at normal transparency) and `erw` it, - -- which matches up to defeq. + -- `crossToSlot`'s output color reduces to the clean one only at default transparency, so `rw` + -- cannot key on the composite. Precompute the left commutator and `erw` it instead. have hpl := crossToEnd_permT_left i (0 : Fin 2) ⇑(Fin.cycleIcc i (Fin.last nA)).symm id (IsReindexing.crossToSlot_cycle i (0 : Fin 2)) (by @@ -325,8 +320,8 @@ lemma crossToSlot_raise_lower_round_trip {nA : ℕ} {c : Fin (nA + 1) → C} {a ## C. Raising and lowering as an equivalence -A pair collapsing to the unit tensor in both orders makes the two contractions mutually inverse, so -the color lists `c` and `Function.update c i d` carry the same tensors. +Both collapse orders are hypotheses here and each is used once: `M · M' = δ` gives one round trip +by section B, `M' · M = δ` the other through injectivity of the lowering half. -/ @@ -348,9 +343,8 @@ include hMM' in lemma crossToSlotInv_crossToSlot (t : Tensor S c) : crossToSlotInv i he hb M' (crossToSlot i (0 : Fin 2) ha M t) = t := by simp only [crossToSlotInv, LinearMap.coe_comp, Function.comp_apply] - -- Unfolding `crossToSlotInv` leaves the inner slot proof at the clean color `b` where the - -- `crossToSlot` application wants the composite `![b, e] 0`, so `rw` cannot key on the round - -- trip; `erw` matches up to defeq. + -- Unfolding `crossToSlotInv` leaves the inner slot proof at the clean color `b` where the goal + -- wants the composite `![b, e] 0`, so `rw` cannot key on the round trip; `erw` matches. erw [crossToSlot_raise_lower_round_trip i he ha hb M M' hMM' t, permT_permT] exact permT_congr_eq_id _ _ _ rfl @@ -384,14 +378,6 @@ noncomputable def crossToSlotEquiv : Tensor S c ≃ₗ[k] Tensor S (Function.upd (crossToSlotInv_crossToSlot i he ha hb M M' hMM') (crossToSlot_crossToSlotInv i he ha hb M M' hMM' hM'M) -@[simp] -lemma crossToSlotEquiv_apply (t : Tensor S c) : - crossToSlotEquiv i he ha hb M M' hMM' hM'M t = crossToSlot i (0 : Fin 2) ha M t := rfl - -@[simp] -lemma crossToSlotEquiv_symm_apply (t : Tensor S (Function.update c i d)) : - (crossToSlotEquiv i he ha hb M M' hMM' hM'M).symm t = crossToSlotInv i he hb M' t := rfl - end RoundTripEquiv end Tensor diff --git a/Physlib/Relativity/Tensors/Dual.lean b/Physlib/Relativity/Tensors/Dual.lean index d505a518d..fa88ec66c 100644 --- a/Physlib/Relativity/Tensors/Dual.lean +++ b/Physlib/Relativity/Tensors/Dual.lean @@ -107,19 +107,13 @@ lemma crossToEnd_metricTensor_metricTensor_eq_dual_unit {c : C} : -/ -/-- Dualising the color of the index `i` twice gives back `c`, as a reindexing along the - identity. -/ -lemma IsReindexing.update_dual_dual {n : ℕ} (c : Fin n → C) (i : Fin n) : - IsReindexing c (Function.update (Function.update c i (S.τ (c i))) i - (S.τ (Function.update c i (S.τ (c i)) i))) (id : Fin n → Fin n) := - IsReindexing.update_update_of_eq i (by simp [τ_τ_apply]) - /-- Dualising the index `i` twice returns the original tensor, up to the reindexing of the colors. -/ lemma toDualMapAtIndex_toDualMapAtIndex {n : ℕ} {c : Fin n → C} (i : Fin n) (t : S.Tensor c) : toDualMapAtIndex (S := S) i (toDualMapAtIndex (S := S) i t) = - permT (id : Fin n → Fin n) (IsReindexing.update_dual_dual c i) t := by + permT (id : Fin n → Fin n) + (IsReindexing.update_update_of_eq i (by simp [τ_τ_apply])) t := by cases n with | zero => exact i.elim0 | succ nA => From 7d53c3100688e8308bfde13ae8889dbe13e31766 Mon Sep 17 00:00:00 2001 From: Andrea Pari Date: Tue, 28 Jul 2026 10:35:58 +0100 Subject: [PATCH 9/9] refactor(Tensors): inline the single-consumer index-map lemmas and rename per review Seven of the nine `Fin` lemmas added to `Reindexing.lean` had a single consuming lemma: five fed only `crossToEnd_assoc_rankTwo`, and one each fed `crossToEnd_unitTensor` and `crossToSlot_round_trip_of_unit`. Their proofs now sit inside those lemmas as local hypotheses. `append_castAdd_natAdd_eq_id` and `append_succAbove_const_eq_cycleIcc` remain, each used in three files. Mathlib's `Fin.append_castAdd_natAdd` cannot stand in for the former: its pattern carries the function being split, so it does not match the eta-reduced `Fin.append (Fin.castAdd n) (Fin.natAdd m)`. The local hypotheses are scoped to the branch that uses them and cleared before the closing `grind (splits := 20)`, which ingests the local context. Leaving them in place cost the module ~8.7s to rebuild against ~4.1s. `Fin.reinsert_castAdd` / `reinsert_natAdd` become `succSuccAbove_castAdd_natAdd_apply_castAdd` / `..._apply_natAdd`, naming the embedding each `succSuccAbove` argument enters by, as `succSuccAbove_natAdd_apply_castAdd` does above them. `IsReindexing.moveLast` becomes `move_last`. The `CrossToEnd` overview states the result-to-end and result-to-slot conventions as the colour lists they produce, glosses the output color against `cA` and `cB`, and names the survivors where it first uses the term. Co-authored-by: Claude Opus 4.8 --- .../Tensors/Contraction/CrossToEnd.lean | 96 +++++++++++++------ .../Tensors/Contraction/SuccSuccAbove.lean | 7 +- .../Contraction/UnitTensorContraction.lean | 22 +++-- Physlib/Relativity/Tensors/Reindexing.lean | 58 +---------- 4 files changed, 90 insertions(+), 93 deletions(-) diff --git a/Physlib/Relativity/Tensors/Contraction/CrossToEnd.lean b/Physlib/Relativity/Tensors/Contraction/CrossToEnd.lean index dbbe38c60..2878a66b6 100644 --- a/Physlib/Relativity/Tensors/Contraction/CrossToEnd.lean +++ b/Physlib/Relativity/Tensors/Contraction/CrossToEnd.lean @@ -16,12 +16,17 @@ public import Physlib.Relativity.Tensors.Contraction.Products another (`T^{μν} u_ν`, `g_{μν} v^ν`) is `prodT` then `contrT`, which leaves every call site to locate the two post-product slots and discharge the distinctness and `τ`-duality goals. -`crossToEnd i j hc` packages that move at named slots `i` and `j`, with `hc : S.τ (cA i) = cB j` -recording their `τ`-duality and output color `Fin.append (cA ∘ i.succAbove) (cB ∘ j.succAbove)`, -left survivors then right. Any slot is reachable: `crossToEnd 2 0 _ R u` reads as `R_{μνρσ} u^ρ`. -Survivors at the end make the output an append, so both bracketings of a chain produce the same -survivor list. The complementary convention, keeping the replacement index in place -(`T^{μ}{}_{νρ} ↦ T_{μνρ}`), is `crossToSlot`, built on this substrate in +`crossToEnd i j hc` performs that contraction at named slots `i` and `j`, with +`hc : S.τ (cA i) = cB j` recording their `τ`-duality. The output color is +`Fin.append (cA ∘ i.succAbove) (cB ∘ j.succAbove)`: every slot of `cA` except `i`, in order, then +every slot of `cB` except `j`. These are the survivors. Any slot is reachable: +`crossToEnd 2 0 _ R u` reads as `R_{μνρσ} u^ρ`. The survivors are appended rather than interleaved, +and appending is associative, so both bracketings of a chain produce the same survivor list in the +same order. + +The complementary convention keeps the replacement index in place. Contracting slot `1` of +`![c₀, c₁, c₂, c₃]` against a rank-two `![S.τ c₁, d]` gives `![c₀, c₂, c₃, d]` here and +`![c₀, d, c₂, c₃]` there; that operation is `crossToSlot`, built on this substrate in `Physlib.Relativity.Tensors.Contraction.CrossToSlot`. ## ii. Key results @@ -79,9 +84,9 @@ noncomputable def crossToEnd {nA nB : ℕ} {cA : Fin (nA + 1) → C} {cB : Fin ( refine ⟨Function.bijective_id, fun m => ?_⟩ simp only [id_eq, Function.comp_apply] refine Fin.addCases (fun a => ?_) (fun a => ?_) m - · rw [Fin.reinsert_castAdd i j a] + · rw [Fin.succSuccAbove_castAdd_natAdd_apply_castAdd i j a] simp only [Fin.append_left, Function.comp_apply] - · rw [Fin.reinsert_natAdd i j a] + · rw [Fin.succSuccAbove_castAdd_natAdd_apply_natAdd i j a] simp only [Fin.append_right, Function.comp_apply]) ∘ₗ contrT (nA + nB) (Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 by omega) (Fin.castAdd (nB + 1) i)) @@ -203,6 +208,27 @@ lemma crossToEnd_assoc_rankTwo {nA : ℕ} · intro p simp only [contrT_pure, permT_pure, Pure.contrP, map_smul] rw [smul_smul, smul_smul] + -- Index-map facts used only by this proof, kept local rather than exported. They are `clear`ed + -- before the closing `grind`, which would otherwise ingest them as candidate facts. + have happend_swap_val : ∀ (n n2 : ℕ) (x : Fin (n2 + n)), + (Fin.append (Fin.natAdd n) (Fin.castAdd n2) x).val = + if x.val < n2 then n + x.val else x.val - n2 := by + intro n n2 x + refine Fin.addCases (fun i => ?_) (fun i => ?_) x + · simp [Fin.append_left] + · simp [Fin.append_right] + have happend_castAdd_cast : ∀ (na nb n2 : ℕ) (heq : na = nb), + Fin.append (Fin.castAdd n2 ∘ Fin.cast heq) (Fin.natAdd nb) = + Fin.cast (show na + n2 = nb + n2 by omega) := by + intro na nb n2 heq + subst heq + simpa using Fin.append_castAdd_natAdd_eq_id + have happend_natAdd_cast : ∀ (na nb n2 : ℕ) (heq : na = nb), + Fin.append (Fin.castAdd nb) (Fin.natAdd n2 ∘ Fin.cast heq) = + Fin.cast (show n2 + na = n2 + nb by omega) := by + intro na nb n2 heq + subst heq + simpa using Fin.append_castAdd_natAdd_eq_id apply congrArg₂ (fun r t => r • t) · -- Coefficients. simp only [Pure.contrPCoeff_dropPair] @@ -214,9 +240,9 @@ lemma crossToEnd_assoc_rankTwo {nA : ℕ} simp only [Nat.add_eq, Function.id_comp, Function.comp_id, Function.comp_apply, Fin.cast_castAdd_left, Fin.cast_natAdd_left, Fin.funPredPredAbove, Fin.succSuccAbove_predPredAbove, - Fin.append_right, Fin.append_swap_val, - Fin.append_castAdd_natAdd_eq_id, id_eq, Fin.append_castAdd_cast, - Fin.append_natAdd_cast, Fin.succSuccAbove_val, Fin.val_castAdd, + Fin.append_right, happend_swap_val, + Fin.append_castAdd_natAdd_eq_id, id_eq, happend_castAdd_cast, + happend_natAdd_cast, Fin.succSuccAbove_val, Fin.val_castAdd, Fin.val_natAdd, Fin.val_last, Fin.val_cast, Fin.val_zero] split_ifs <;> omega · -- Slot maps. @@ -230,23 +256,37 @@ lemma crossToEnd_assoc_rankTwo {nA : ℕ} try simp only [Fin.funPredPredAbove] try simp only [Fin.succSuccAbove_predPredAbove] apply Fin.ext + -- Pinning a block injection to a literal slot `⟨v, _⟩` is stated at `Fin` level, not at + -- `.val` level, so that a rewrite replaces the composite before `Fin.succSuccAbove_val` + -- builds its `ite` conditions on it, keeping the generated `Decidable` instances in sync. + have hcast_castAdd : ∀ {n m N : ℕ} (h : n + m = N) {i : Fin n} {v : ℕ} (hv : i.val = v), + Fin.cast h (Fin.castAdd m i) = ⟨v, by have := i.isLt; omega⟩ := by + intro n m N h i v hv + exact Fin.ext (by simp [hv]) + have hcast_natAdd : ∀ {n m N : ℕ} (h : n + m = N) {i : Fin m} {v : ℕ} (hv : n + i.val = v), + Fin.cast h (Fin.natAdd n i) = ⟨v, by have := i.isLt; omega⟩ := by + intro n m N h i v hv + exact Fin.ext (by simp [hv]) -- Pin each slot to a literal `⟨v, _⟩`, innermost first, so that `succSuccAbove_val` fires. - rw [Fin.cast_castAdd_eq_mk (i := Fin.last nA) (v := nA) _ rfl, - Fin.cast_natAdd_eq_mk (n := nA + 1) (i := (0 : Fin (1 + 1))) (v := nA + 1) _ + rw [hcast_castAdd (i := Fin.last nA) (v := nA) _ rfl, + hcast_natAdd (n := nA + 1) (i := (0 : Fin (1 + 1))) (v := nA + 1) _ (by simp only [Fin.val_zero, Nat.add_zero]), - Fin.cast_castAdd_eq_mk (i := iA) (v := (iA : ℕ)) _ rfl, + hcast_castAdd (i := iA) (v := (iA : ℕ)) _ rfl, Fin.natAdd_mk (1 + 1) (iA : ℕ), Fin.natAdd_mk (1 + 1) (nA + 1), - Fin.cast_castAdd_eq_mk (i := Fin.last 1) (v := 1) _ rfl, - Fin.cast_natAdd_eq_mk (n := 1 + 1) (i := (0 : Fin (1 + 1))) (v := 1 + 1) _ + hcast_castAdd (i := Fin.last 1) (v := 1) _ rfl, + hcast_natAdd (n := 1 + 1) (i := (0 : Fin (1 + 1))) (v := 1 + 1) _ (by simp only [Fin.val_zero, Nat.add_zero]), Fin.natAdd_mk (nA + 1) 1, Fin.natAdd_mk (nA + 1) (1 + 1)] simp only [Function.comp_id] rw [Fin.append_castAdd_natAdd_eq_id] - simp only [Nat.add_eq, id_eq, Fin.append_swap_val, Fin.append_castAdd_cast, - Fin.append_natAdd_cast, Fin.succSuccAbove_val, Fin.val_cast] - -- Four nested reinsertion conditionals; the split budget is `SuccSuccAbove`'s. + simp only [Nat.add_eq, id_eq, happend_swap_val, happend_castAdd_cast, + happend_natAdd_cast, Fin.succSuccAbove_val, Fin.val_cast] + -- Four nested reinsertion conditionals; the split budget is `SuccSuccAbove`'s. The spent + -- index-map hypotheses are dropped first: `grind` ingests the local context, and leaving + -- them in costs it more than twice the elaboration time. + clear happend_swap_val happend_castAdd_cast happend_natAdd_cast hcast_castAdd hcast_natAdd grind (splits := 20) · intro r t ht; simp only [map_smul, ht] · intro t1 t2 h1 h2; simp only [map_add, h1, h2] @@ -294,11 +334,12 @@ lemma crossToEnd_permT_left {nA nB : ℕ} {cA cA' : Fin (nA + 1) → C} intro m simp only [Function.comp_apply, id_eq] refine Fin.addCases (fun a => ?_) (fun b => ?_) m - · rw [Fin.reinsert_castAdd i j a, Fin.append_left, Function.comp_apply, - Fin.append_left, Function.comp_apply, Fin.reinsert_castAdd (σ i) j _, + · rw [Fin.succSuccAbove_castAdd_natAdd_apply_castAdd i j a, Fin.append_left, + Function.comp_apply, Fin.append_left, Function.comp_apply, + Fin.succSuccAbove_castAdd_natAdd_apply_castAdd (σ i) j _, show (σ i).succAbove (σ' a) = σ (i.succAbove a) from congrFun hσ' a] - · rw [Fin.reinsert_natAdd i j b, Fin.append_right, Fin.append_right, - Fin.reinsert_natAdd (σ i) j b] + · rw [Fin.succSuccAbove_castAdd_natAdd_apply_natAdd i j b, Fin.append_right, + Fin.append_right, Fin.succSuccAbove_castAdd_natAdd_apply_natAdd (σ i) j b] · intro r t ht; simp only [map_smul, ht] · intro t1 t2 h1 h2; simp only [map_add, h1, h2] @@ -332,10 +373,11 @@ lemma crossToEnd_permT_right {nA nB : ℕ} {cA : Fin (nA + 1) → C} intro m simp only [Function.comp_apply, id_eq] refine Fin.addCases (fun a => ?_) (fun b => ?_) m - · rw [Fin.reinsert_castAdd i j a, Fin.append_left, Fin.append_left, - Fin.reinsert_castAdd i (σ j) a] - · rw [Fin.reinsert_natAdd i j b, Fin.append_right, Function.comp_apply, - Fin.append_right, Function.comp_apply, Fin.reinsert_natAdd i (σ j) _, + · rw [Fin.succSuccAbove_castAdd_natAdd_apply_castAdd i j a, Fin.append_left, + Fin.append_left, Fin.succSuccAbove_castAdd_natAdd_apply_castAdd i (σ j) a] + · rw [Fin.succSuccAbove_castAdd_natAdd_apply_natAdd i j b, Fin.append_right, + Function.comp_apply, Fin.append_right, Function.comp_apply, + Fin.succSuccAbove_castAdd_natAdd_apply_natAdd i (σ j) _, show (σ j).succAbove (σ' b) = σ (j.succAbove b) from congrFun hσ' b] · intro r t ht; simp only [map_smul, ht] · intro t1 t2 h1 h2; simp only [map_add, h1, h2] diff --git a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean index 484170ca2..0f8af30f1 100644 --- a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean +++ b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean @@ -235,7 +235,7 @@ lemma succSuccAbove_natAdd_apply_castAdd {n n1 : ℕ} `j`-th slot of the right block of `Fin ((nA + 1) + (nB + 1))`, the removal read at the contracted length `(nA + nB) + 1 + 1`. Unlike `succSuccAbove_natAdd_apply_castAdd` the two holes straddle the two blocks, so the statement carries the reshaping `Fin.cast`s. -/ -lemma reinsert_castAdd {nA nB : ℕ} (i : Fin (nA + 1)) (j : Fin (nB + 1)) +lemma succSuccAbove_castAdd_natAdd_apply_castAdd {nA nB : ℕ} (i : Fin (nA + 1)) (j : Fin (nB + 1)) (a : Fin nA) : Fin.cast (show (nA + nB) + 1 + 1 = (nA + 1) + (nB + 1) by omega) ((Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 by omega) @@ -248,8 +248,9 @@ lemma reinsert_castAdd {nA nB : ℕ} (i : Fin (nA + 1)) (j : Fin (nB + 1)) Fin.succAbove, Fin.lt_def, Fin.val_castSucc, Fin.val_succ, apply_ite Fin.val] split_ifs <;> omega -/-- Reinserting a right-block survivor, the mirror of `Fin.reinsert_castAdd`. -/ -lemma reinsert_natAdd {nA nB : ℕ} (i : Fin (nA + 1)) (j : Fin (nB + 1)) +/-- Reinserting a right-block survivor, the mirror of + `Fin.succSuccAbove_castAdd_natAdd_apply_castAdd`. -/ +lemma succSuccAbove_castAdd_natAdd_apply_natAdd {nA nB : ℕ} (i : Fin (nA + 1)) (j : Fin (nB + 1)) (a : Fin nB) : Fin.cast (show (nA + nB) + 1 + 1 = (nA + 1) + (nB + 1) by omega) ((Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 by omega) diff --git a/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean b/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean index 23729c408..2ea6cfc18 100644 --- a/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean +++ b/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean @@ -67,7 +67,7 @@ namespace Tensor ## A. The unit tensor as a slot-contraction identity Contracting a named slot against `unitTensor` returns the tensor unchanged, the slot carried to the -survivor tail by `moveLast`. +survivor tail by `move_last`. -/ @@ -130,7 +130,7 @@ private lemma crossToEnd_prodT_unitTensor {nV : ℕ} {cE : Fin nV → C} {cB : C private lemma crossToEnd_unitTensor_slot {nA : ℕ} {cA : Fin (nA + 1) → C} {c : C} {i : Fin (nA + 1)} (hilast : i = Fin.last nA) (hc : cA i = c) (t1 : Tensor S cA) : crossToEnd i (0 : Fin 2) (by simp [hc] : S.τ (cA i) = ![S.τ c, c] 0) t1 (unitTensor c) = - permT (Fin.append i.succAbove (fun _ : Fin 1 => i)) (IsReindexing.moveLast i hc) t1 := by + permT (Fin.append i.succAbove (fun _ : Fin 1 => i)) (IsReindexing.move_last i hc) t1 := by subst hilast subst hc rw [eq_sum_evalT t1, map_sum, LinearMap.sum_apply, map_sum] @@ -152,17 +152,21 @@ private lemma crossToEnd_unitTensor_slot {nA : ℕ} {cA : Fin (nA + 1) → C} {c exact Fin.ext (by simp) /-- Contracting slot `i` of `t1` against the unit tensor for that slot's color returns `t1`, the - contracted slot relabelled by `moveLast i`. The unit tensor acts as an identity for `crossToEnd` + contracted slot relabelled by `move_last i`. The unit tensor acts as an identity for `crossToEnd` at any named slot. -/ lemma crossToEnd_unitTensor {nA : ℕ} {cA : Fin (nA + 1) → C} {c : C} (i : Fin (nA + 1)) (hc : cA i = c) (t1 : Tensor S cA) : crossToEnd i (0 : Fin 2) (by simp [hc] : S.τ (cA i) = ![S.τ c, c] 0) t1 (unitTensor c) = - permT (Fin.append i.succAbove (fun _ : Fin 1 => i)) (IsReindexing.moveLast i hc) t1 := by + permT (Fin.append i.succAbove (fun _ : Fin 1 => i)) (IsReindexing.move_last i hc) t1 := by set τ : Fin (nA + 1) → Fin (nA + 1) := ⇑(Equiv.swap i (Fin.last nA)) with hτdef have hτbij : Function.Bijective τ := (Equiv.swap i (Fin.last nA)).bijective have hτi : τ i = Fin.last nA := Equiv.swap_apply_left i (Fin.last nA) have hself : ∀ x, τ (τ x) = x := fun x => Equiv.swap_apply_self i (Fin.last nA) x - obtain ⟨τ', hτ'⟩ := Fin.exists_succAbove_comm hτbij.1 i + -- `τ` is injective, so it restricts to the survivors of `i`: some `τ'` fills the square + -- `(τ i).succAbove ∘ τ' = τ ∘ i.succAbove`. + obtain ⟨τ', hτ'⟩ : ∃ τ' : Fin nA → Fin nA, (τ i).succAbove ∘ τ' = τ ∘ i.succAbove := + ⟨fun a => (Fin.exists_succAbove_eq (hτbij.1.ne (Fin.succAbove_ne i a))).choose, + funext fun a => (Fin.exists_succAbove_eq (hτbij.1.ne (Fin.succAbove_ne i a))).choose_spec⟩ have hre2 : IsReindexing cA (cA ∘ τ) τ := Tensor.IsReindexing.swap i (Fin.last nA) have hre : IsReindexing (cA ∘ τ) cA τ := ⟨hτbij, fun x => by simp only [Function.comp_apply, hself]⟩ @@ -265,6 +269,12 @@ private lemma crossToSlot_round_trip_of_unit {nA : ℕ} {c : Fin (nA + 1) → C} permT (id : Fin (nA + 1) → Fin (nA + 1)) (IsReindexing.update_update_of_eq i rfl) t := by have hcycle : (⇑(Fin.cycleIcc i (Fin.last nA)).symm) i = Fin.last nA := (Equiv.symm_apply_eq _).2 (Fin.cycleIcc_of_last (Fin.le_last i)).symm + -- The inverse cycle carries a reinserted survivor `i.succAbove a` back to its position `a` in + -- the survivor block. + have hcycle_succAbove : ∀ a : Fin nA, + (Fin.cycleIcc i (Fin.last nA)).symm (i.succAbove a) = Fin.castAdd 1 a := fun a => + (Equiv.symm_apply_eq _).2 + (by rw [← Fin.append_succAbove_const_eq_cycleIcc i, Fin.append_left]) rw [crossToSlot_eq_crossToEnd, crossToSlot_eq_crossToEnd] -- `crossToSlot`'s output color reduces to the clean one only at default transparency, so `rw` -- cannot key on the composite. Precompute the left commutator and `erw` it instead. @@ -273,7 +283,7 @@ private lemma crossToSlot_round_trip_of_unit {nA : ℕ} {c : Fin (nA + 1) → C} (by funext a simp only [Function.comp_apply, id_eq] - rw [hcycle, Fin.cycleIcc_last_symm_apply_succAbove, Fin.succAbove_last] + rw [hcycle, hcycle_succAbove, Fin.succAbove_last] rfl) (show S.τ (Function.update c i d i) = ![S.τ d, c i] 0 by rw [Function.update_self, Matrix.cons_val_zero]) diff --git a/Physlib/Relativity/Tensors/Reindexing.lean b/Physlib/Relativity/Tensors/Reindexing.lean index 1a2e32214..6bbb7e51d 100644 --- a/Physlib/Relativity/Tensors/Reindexing.lean +++ b/Physlib/Relativity/Tensors/Reindexing.lean @@ -44,35 +44,11 @@ The finite index maps out of which the reindexings below are built: `Fin.append` -/ -/-- The `.val` of the block-swap map, as a piecewise-linear function. -/ -lemma append_swap_val (n n2 : ℕ) (x : Fin (n2 + n)) : - (Fin.append (Fin.natAdd n) (Fin.castAdd n2) x).val = - if x.val < n2 then n + x.val else x.val - n2 := by - refine Fin.addCases (fun i => ?_) (fun i => ?_) x - · simp [Fin.append_left] - · simp [Fin.append_right] - /-- 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)) := by simpa using Fin.append_castAdd_natAdd (f := (id : Fin (m + n) → Fin (m + n))) -/-- Reassembling the blocks of `Fin (na + n2)` after casting the left one along `na = nb` is the - cast of the total length. -/ -lemma append_castAdd_cast (na nb n2 : ℕ) (heq : na = nb) : - Fin.append (Fin.castAdd n2 ∘ Fin.cast heq) (Fin.natAdd nb) = - Fin.cast (show na + n2 = nb + n2 by omega) := by - subst heq - simpa using append_castAdd_natAdd_eq_id - -/-- Reassembling the blocks of `Fin (n2 + na)` after casting the right one along `na = nb` is the - cast of the total length. The right-block mirror of `Fin.append_castAdd_cast`. -/ -lemma append_natAdd_cast (na nb n2 : ℕ) (heq : na = nb) : - Fin.append (Fin.castAdd nb) (Fin.natAdd n2 ∘ Fin.cast heq) = - Fin.cast (show n2 + na = n2 + nb by omega) := by - subst heq - simpa using append_castAdd_natAdd_eq_id - /-- 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)`. -/ lemma append_succAbove_const_eq_cycleIcc {n : ℕ} (i : Fin (n + 1)) : @@ -88,38 +64,6 @@ lemma append_succAbove_const_eq_cycleIcc {n : ℕ} (i : Fin (n + 1)) : apply Fin.ext; simp [Fin.val_natAdd] rw [this, Fin.cycleIcc_of_le_of_le (Fin.le_last _) (Fin.le_last _), if_pos rfl] -/-- The inverse of the cycle `[i, last]` carries the reinserted survivor `i.succAbove a` back to - its position `a` in the survivor block. -/ -lemma cycleIcc_last_symm_apply_succAbove {n : ℕ} (i : Fin (n + 1)) (a : Fin n) : - (Fin.cycleIcc i (Fin.last n)).symm (i.succAbove a) = Fin.castAdd 1 a := - (Equiv.symm_apply_eq _).2 (by rw [← append_succAbove_const_eq_cycleIcc i, Fin.append_left]) - -/-- An injection `σ` of `Fin (n + 1)` restricts to the survivors of a slot `i`: there is a map - `σ'` filling the square `(σ i).succAbove ∘ σ' = σ ∘ i.succAbove`, carrying the complement of `i` - to the complement of `σ i`. -/ -lemma exists_succAbove_comm {n : ℕ} {σ : Fin (n + 1) → Fin (n + 1)} (hσ : Function.Injective σ) - (i : Fin (n + 1)) : ∃ σ' : Fin n → Fin n, (σ i).succAbove ∘ σ' = σ ∘ i.succAbove := - ⟨fun a => (Fin.exists_succAbove_eq (hσ.ne (Fin.succAbove_ne i a))).choose, - funext fun a => (Fin.exists_succAbove_eq (hσ.ne (Fin.succAbove_ne i a))).choose_spec⟩ - -/-- A `Fin.cast` of a left-block injection is the literal slot `⟨v, _⟩` at the same value `v`. - - Stated at `Fin` level rather than `.val` level so that a rewrite replaces the composite before - `Fin.succSuccAbove_val` builds its `ite` conditions on it, keeping the generated `Decidable` - instances in sync with the reduced conditions. -/ -lemma cast_castAdd_eq_mk {n m N : ℕ} (h : n + m = N) {i : Fin n} {v : ℕ} (hv : i.val = v) : - Fin.cast h (Fin.castAdd m i) = - ⟨v, by subst h hv; exact Nat.lt_of_lt_of_le i.isLt (Nat.le_add_right n m)⟩ := - Fin.ext (by simp [hv]) - -/-- A `Fin.cast` of a right-block injection is the literal slot `⟨v, _⟩` at the offset value `v`. - See `Fin.cast_castAdd_eq_mk` for why the `Fin`-level statement matters. -/ -lemma cast_natAdd_eq_mk {n m N : ℕ} (h : n + m = N) {i : Fin m} {v : ℕ} - (hv : n + i.val = v) : - Fin.cast h (Fin.natAdd n i) = - ⟨v, by subst h hv; exact Nat.add_lt_add_left i.isLt n⟩ := - Fin.ext (by simp [hv]) - end Fin namespace TensorSpecies @@ -583,7 +527,7 @@ lemma append_succ_last {n : ℕ} (c : Fin (n + 1) → C) : 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. -/ -lemma moveLast {n : ℕ} {c : Fin (n + 1) → C} {c1 : Fin 2 → C} (i : Fin (n + 1)) +lemma move_last {n : ℕ} {c : Fin (n + 1) → C} {c1 : Fin 2 → C} (i : Fin (n + 1)) (hc : c i = c1 1) : IsReindexing c (Fin.append (c ∘ i.succAbove) (c1 ∘ (0 : Fin 2).succAbove))