feat: mult on arbitary index

HepLean/SpaceTime/LorentzTensor/Real/Basic.lean

@@ -8,6 +8,7 @@ import Mathlib.Data.Real.Basic
 import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Logic.Equiv.Fin
 import Mathlib.Tactic.FinCases
+import Mathlib.Logic.Equiv.Fintype
 /-!
 
 # Real Lorentz Tensors
@@ -386,9 +387,8 @@ def twoMarkedIndexValue (T : Marked d X 2) (x : ColorsIndex d (T.color (markedPo
   | 1 => y
 
 /-- An equivalence of types used to turn the first marked index into an unmarked index. -/
-def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Fin n.succ) ≃
-    (X ⊕ Fin 1) ⊕ Fin n :=
-  trans (Equiv.sumCongr (Equiv.refl _) $
+def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Fin n.succ) ≃ (X ⊕ Fin 1) ⊕ Fin n :=
+  trans (Equiv.sumCongr (Equiv.refl _)
     (((Fin.castOrderIso (Nat.succ_eq_one_add n)).toEquiv.trans finSumFinEquiv.symm)))
   (Equiv.sumAssoc _ _ _).symm
 
@@ -396,6 +396,151 @@ def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Fin n.succ) ≃
 def unmarkFirst {X : Type} : Marked d X n.succ ≃ Marked d (X ⊕ Fin 1) n :=
   mapIso d (unmarkFirstSet X n)
 
+@[simps!]
+def notInImage {n m : ℕ} (f : Fin m ↪ Fin (n + m)) :
+    Fin n ≃ {x // x ∈ (Finset.image (⇑f) Finset.univ)ᶜ} :=
+  (Finset.orderIsoOfFin (Finset.image f Finset.univ)ᶜ (by rw [Finset.card_compl,
+    Finset.card_image_of_injective _ (Function.Embedding.injective f)]; simp)).toEquiv
+
+@[simps!]
+def splitMarkedIndices {n m : ℕ} (f : Fin m ↪ Fin (n + m)) : Fin (n + m) ≃ Fin n ⊕ Fin m :=
+  (Equiv.Set.sumCompl (Set.range ⇑f)).symm.trans <|
+  (Equiv.sumComm _ _).trans <|
+  Equiv.sumCongr ((Equiv.subtypeEquivRight (by simp)).trans (notInImage f).symm) <|
+  (Function.Embedding.toEquivRange f).symm
+
+@[simps!]
+def oneEmbed {n : ℕ} (i : Fin n.succ) : Fin 1 ↪ Fin n.succ :=
+  ⟨fun _ => i, fun x y => by fin_cases x; fin_cases y; simp⟩
+
+@[simps!]
+def splitMarkedIndicesOne {n : ℕ} (i : Fin n.succ) : Fin n.succ ≃ Fin n ⊕ Fin 1 :=
+  splitMarkedIndices (oneEmbed i)
+
+lemma splitMarkedIndicesOne_self {n : ℕ} (i : Fin n.succ) :
+    splitMarkedIndicesOne i i = Sum.inr 0 := by
+  rw [splitMarkedIndicesOne, splitMarkedIndices]
+  have h1 : (Equiv.Set.sumCompl (Set.range (oneEmbed i))).symm i =
+      Sum.inl ⟨i, by simp⟩ := by
+    rw  [Equiv.Set.sumCompl_symm_apply_of_mem]
+  simp
+  rw [h1]
+  change Sum.inr ((⇑(oneEmbed i).toEquivRange.symm) (⟨(oneEmbed i) 0, _⟩)) = Sum.inr 0
+  congr
+  rw [Function.Embedding.toEquivRange_symm_apply_self]
+
+lemma notInImage_oneEmbed {n : ℕ} (i : Fin n.succ) :
+    (notInImage (oneEmbed i)).toFun = fun x => ⟨i.succAbove x, by simpa using Fin.succAbove_ne i x⟩ := by
+  symm
+  simp [notInImage]
+  funext x
+  apply Subtype.ext
+  rw [Finset.coe_orderIsoOfFin_apply]
+  symm
+  apply congrFun
+  symm
+  apply Finset.orderEmbOfFin_unique
+  intro x
+  simp
+  exact Fin.succAbove_ne i x
+  exact Fin.strictMono_succAbove i
+
+lemma splitMarkedIndicesOne_not_self {n : ℕ} {i j : Fin n.succ.succ} (hij : i ≠ j) :
+    splitMarkedIndicesOne i j = Sum.inl ((Fin.predAbove 0 i).predAbove j) := by
+  rw [splitMarkedIndicesOne, splitMarkedIndices]
+  have h1 : (Equiv.Set.sumCompl (Set.range (oneEmbed i))).symm j =
+      Sum.inr ⟨j, by simp [hij]⟩ := by
+    rw [Equiv.Set.sumCompl_symm_apply_of_not_mem]
+  simp
+  rw [h1]
+  change Sum.inl ((⇑(notInImage (oneEmbed i)).symm ∘ ⇑(Equiv.subtypeEquivRight _))
+    ⟨j, _⟩) = _
+  apply congrArg
+  simp
+  rw [Equiv.symm_apply_eq]
+  change _ = (notInImage (oneEmbed i)).toFun ((Fin.predAbove 0 i).predAbove j)
+  rw [notInImage_oneEmbed]
+  simp
+  apply Subtype.ext
+  simp
+  simp [Fin.succAbove, Fin.predAbove, Fin.lt_def]
+  split <;> split <;> simp <;> split <;> apply Fin.ext_iff.mpr
+    <;> rename_i _ h2 h3 h4 <;> simp at h1 h2 h3 h4  <;> omega
+
+
+@[simps!]
+def markSelectedIndex (i : Fin n.succ) : Marked d X n.succ ≃ Marked d (X ⊕ Fin n) 1 :=
+  mapIso d ((Equiv.sumCongr (Equiv.refl X) (splitMarkedIndicesOne i)).trans
+    (Equiv.sumAssoc _ _ _).symm)
+
+lemma markSelectedIndex_markedColor (T : Marked d X n.succ) (i : Fin n.succ) :
+    (markSelectedIndex i T).markedColor 0 = T.markedColor i := rfl
+
+/-! TODO: Simplify prove and move. -/
+lemma succAbove_predAbove_predAbove (i p : Fin n.succ.succ) (hip : i ≠ p) :
+     i.succAbove ((Fin.predAbove 0 i).predAbove p) = p := by
+  simp [Fin.succAbove, Fin.predAbove, Fin.lt_def]
+  split <;> split <;> simp   <;> rw [Fin.ext_iff] <;> simp
+  intro h
+  all_goals
+    rename_i h1 h2
+    simp at h1 h2
+    omega
+
+@[simps!]
+def equivDropPoint  (e : Fin n.succ ≃ Fin m.succ) {i : Fin n.succ} {j : Fin m.succ} (he : e i = j) :
+    Fin n ≃ Fin m :=
+  (notInImage (oneEmbed i)).trans <|
+  (Equiv.subtypeEquivOfSubtype' e).trans  <|
+  (Equiv.subtypeEquivRight (fun x => by simp [oneEmbed, Equiv.symm_apply_eq, he])).trans <|
+  (notInImage (oneEmbed j)).symm
+
+
+lemma markSelectedIndex_mapIso (f : X ≃ Y) (e : Fin n.succ.succ ≃ Fin m.succ.succ) (i : Fin n.succ.succ)
+    (j : Fin m.succ.succ) (he : e i = j) (T : Marked d X n.succ.succ) :
+    mapIso d (Equiv.sumCongr (Equiv.sumCongr f (equivDropPoint e he)) (Equiv.refl (Fin 1)))
+    (markSelectedIndex i T) = markSelectedIndex j (mapIso d (Equiv.sumCongr f e) T) := by
+  rw [markSelectedIndex, markSelectedIndex]
+  erw [← Equiv.trans_apply, ← Equiv.trans_apply]
+  rw [mapIso_trans, mapIso_trans]
+  apply congrFun
+  apply congrArg
+  apply congrArg
+  apply Equiv.ext
+  intro x
+  match x with
+  | Sum.inl x => rfl
+  | Sum.inr x =>
+    simp only [Nat.succ_eq_add_one, Equiv.trans_apply, Equiv.coe_refl,
+       Fin.isValue]
+    change  ((f.sumCongr (equivDropPoint e he)).sumCongr (Equiv.refl (Fin 1)))
+      ((Equiv.sumAssoc X (Fin n.succ) (Fin 1)).symm (Sum.inr ((splitMarkedIndicesOne i) x)))  =
+      (Equiv.sumAssoc Y (Fin m.succ) (Fin 1)).symm (Sum.inr ((splitMarkedIndicesOne j) (e x)))
+    by_cases h : x = i
+    subst h
+    rw [he]
+    rw [splitMarkedIndicesOne_self, splitMarkedIndicesOne_self]
+    simp
+    subst he
+    rw [splitMarkedIndicesOne_not_self (fun a => h a.symm), splitMarkedIndicesOne_not_self]
+    simp [equivDropPoint]
+    rw [Equiv.symm_apply_eq]
+    change _ =
+      (notInImage (oneEmbed (e i))).toFun ((Fin.predAbove 0 (e i)).predAbove (e x))
+    rw [notInImage_oneEmbed]
+    simp
+    apply Subtype.ext
+    simp
+    change (e.subtypeEquivOfSubtype'
+      ((notInImage (oneEmbed i)).toFun ((Fin.predAbove 0 i).predAbove x))).1 = _
+    rw [notInImage_oneEmbed]
+    rw [Equiv.subtypeEquivOfSubtype', Equiv.subtypeEquivOfSubtype]
+    simp
+    rw [succAbove_predAbove_predAbove, succAbove_predAbove_predAbove]
+    exact e.apply_eq_iff_eq.mp.mt (fun a => h a.symm)
+    exact fun a => h a.symm
+    exact e.apply_eq_iff_eq.mp.mt (fun a => h a.symm)
+
 end Marked
 
 /-!

HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean

@@ -18,6 +18,43 @@ We will derive properties of these constructors.
 -/
 
 namespace RealLorentzTensor
+/-!
+
+# Tensors from and to the reals
+
+An important point that we shall see here is that there is a well defined map
+to the real numbers, i.e. which is invariant under transformations of mapIso.
+
+-/
+
+/-- An equivalence from Real tensors on an empty set to `ℝ`. -/
+@[simps!]
+def toReal (d : ℕ) {X : Type} (h : IsEmpty X) : RealLorentzTensor d X ≃ ℝ where
+  toFun := fun T => T.coord (IsEmpty.elim h)
+  invFun := fun r => {
+    color := fun x => IsEmpty.elim h x,
+    coord := fun _ => r}
+  left_inv T := by
+    refine ext ?_ ?_
+    funext x
+    exact IsEmpty.elim h x
+    funext a
+    change T.coord (IsEmpty.elim h) = _
+    apply congrArg
+    funext x
+    exact IsEmpty.elim h x
+  right_inv x := rfl
+
+/-- The real number obtained from a tensor is invariant under `mapIso`. -/
+lemma toReal_mapIso (d : ℕ) {X Y : Type} (h : IsEmpty X) (f : X ≃ Y) :
+    (mapIso d f).trans (toReal d (Equiv.isEmpty f.symm)) = toReal d h := by
+  apply Equiv.ext
+  intro x
+  simp
+  apply congrArg
+  funext x
+  exact IsEmpty.elim h x
+
 
 /-!
 
@@ -28,11 +65,6 @@ action of the Lorentz group. They are provided for constructive purposes.
 
 -/
 
-/-- A 0-tensor from a real number. -/
-def ofReal (d : ℕ) (r : ℝ) : RealLorentzTensor d Empty where
-  color := fun _ => Colors.up
-  coord := fun _ => r
-
 /-- A marked 1-tensor with a single up index constructed from a vector.
 
   Note: This is not the same as rising indices on `ofVecDown`. -/
@@ -186,14 +218,14 @@ open Marked
 
 /-- Contracting the indices of `ofMatUpDown` returns the trace of the matrix. -/
 lemma contr_ofMatUpDown_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
-    contr (ofMatUpDown M) (by rfl) = ofReal d M.trace := by
+    contr (ofMatUpDown M) (by rfl) = (toReal d instIsEmptyEmpty).symm M.trace := by
   refine ext ?_ rfl
   · funext i
     exact Empty.elim i
 
 /-- Contracting the indices of `ofMatDownUp` returns the trace of the matrix. -/
 lemma contr_ofMatDownUp_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
-    contr (ofMatDownUp M) (by rfl) = ofReal d M.trace := by
+    contr (ofMatDownUp M) (by rfl) = (toReal d instIsEmptyEmpty).symm M.trace := by
   refine ext ?_ rfl
   · funext i
     exact Empty.elim i
@@ -207,20 +239,18 @@ lemma contr_ofMatDownUp_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1
 /-- Multiplying `ofVecUp` with `ofVecDown` gives the dot product. -/
 @[simp]
 lemma mul_ofVecUp_ofVecDown_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
-    mapIso d (@Equiv.equivEmpty (Empty ⊕ Empty) instIsEmptySum)
-    (mul (ofVecUp v₁) (ofVecDown v₂) (by rfl)) = ofReal d (v₁ ⬝ᵥ v₂) := by
+    mul (ofVecUp v₁) (ofVecDown v₂) rfl = (toReal d instIsEmptySum).symm (v₁ ⬝ᵥ v₂) := by
   refine ext ?_ rfl
   · funext i
-    exact Empty.elim i
+    exact IsEmpty.elim instIsEmptySum i
 
 /-- Multiplying `ofVecDown` with `ofVecUp` gives the dot product. -/
 @[simp]
 lemma mul_ofVecDown_ofVecUp_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
-    mapIso d (Equiv.equivEmpty (Empty ⊕ Empty))
-    (mul (ofVecDown v₁) (ofVecUp v₂) rfl) = ofReal d (v₁ ⬝ᵥ v₂) := by
+    mul (ofVecDown v₁) (ofVecUp v₂) rfl = (toReal d instIsEmptySum).symm (v₁ ⬝ᵥ v₂) := by
   refine ext ?_ rfl
   · funext i
-    exact Empty.elim i
+    exact IsEmpty.elim instIsEmptySum i
 
 lemma mul_ofMatUpDown_ofVecUp_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
     (v : Fin 1 ⊕ Fin d → ℝ) :
@@ -255,8 +285,8 @@ open Matrix
 
 /-- The action of the Lorentz group on `ofReal v` is trivial. -/
 @[simp]
-lemma lorentzAction_ofReal (r : ℝ) : Λ • ofReal d r = ofReal d r :=
-  lorentzAction_on_isEmpty Λ (ofReal d r)
+lemma lorentzAction_toReal (h : IsEmpty X) (r : ℝ) : Λ • (toReal d h).symm r = (toReal d h).symm r :=
+  lorentzAction_on_isEmpty Λ  ((toReal d h).symm r)
 
 /-- The action of the Lorentz group on `ofVecUp v` is by vector multiplication. -/
 @[simp]

HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean

@@ -231,4 +231,85 @@ lemma mul_lorentzAction (T : Marked d X 1) (S : Marked d Y 1)
   simp only [← marked_unmarked_action_eq_action]
   rw [mul_markedLorentzAction, mul_unmarkedLorentzAction]
 
+/-!
+
+## Multiplication on selected indices
+
+-/
+
+variable {n m : ℕ}
+
+def mulSSetEquiv : (X ⊕ Fin n) ⊕ Y ⊕ Fin m ≃ (X ⊕ Y) ⊕ (Fin (n + m)) :=
+  (Equiv.sumAssoc _ _ _).trans <|
+  (Equiv.sumCongr (Equiv.refl _ ) (Equiv.sumAssoc _ _ _).symm).trans <|
+  (Equiv.sumCongr (Equiv.refl _ ) (Equiv.sumCongr (Equiv.sumComm _ _) (Equiv.refl _)).symm).trans <|
+  (Equiv.sumAssoc _ _ _).symm.trans <|
+  (Equiv.sumCongr (Equiv.sumAssoc _ _ _) (Equiv.refl _ )).symm.trans <|
+  (Equiv.sumAssoc _ _ _).trans <|
+  Equiv.sumCongr (Equiv.refl _) finSumFinEquiv
+
+@[simps!]
+def mulS (T : Marked d X n.succ) (S : Marked d Y m.succ) (i : Fin n.succ) (j : Fin m.succ)
+    (h : T.markedColor i = τ (S.markedColor j)) : Marked d (X ⊕ Y) (n + m) :=
+  mapIso d mulSSetEquiv (mul (markSelectedIndex i T) (markSelectedIndex j S) h)
+
+
+/-- Given a marked index of `T` and returns a marked index of `mulS T S _ _ _`. -/
+def mulSInl {n m : ℕ} {i j : Fin n.succ.succ} (h : j ≠ i) : Fin (n.succ + m) :=
+  finSumFinEquiv <|
+  Sum.inl <|
+  (notInImage (oneEmbed i)).symm <|
+  ⟨j, by simp [oneEmbed, h]⟩
+
+/-- Given a marked index of `S` and returns a marked index of `mulS S T _ _ _`. -/
+def mulSInr {n m : ℕ} {i j : Fin m.succ.succ} (h : j ≠ i) : Fin (n + m.succ) :=
+  finSumFinEquiv <|
+  Sum.inr <|
+  (notInImage (oneEmbed i)).symm <|
+  ⟨j, by simp [oneEmbed, h]⟩
+
+lemma mulSInl_mulSSetEquiv {n m : ℕ} {i j : Fin n.succ.succ} (h : j ≠ i) :
+    (@mulSSetEquiv X Y n.succ m).symm (Sum.inr (mulSInl h)) =
+    Sum.inl (Sum.inr ((notInImage (oneEmbed i)).symm  ⟨j, by simp [oneEmbed, h]⟩)) := by
+  rw [Equiv.symm_apply_eq]
+  rfl
+
+lemma mulSInr_mulSSetEquiv {n m : ℕ} {i j : Fin m.succ.succ} (h : j ≠ i) :
+    (@mulSSetEquiv X Y n m.succ).symm (Sum.inr (mulSInr h)) =
+    Sum.inr (Sum.inr ((notInImage (oneEmbed i)).symm  ⟨j, by simp [oneEmbed, h]⟩)) := by
+  rw [Equiv.symm_apply_eq]
+  rfl
+/-
+@[simp]
+lemma mulSInl_color {n m : ℕ}
+    (T : Marked d X n.succ.succ) (S : Marked d Y m.succ) (a b : Fin n.succ.succ) (c : Fin m.succ)
+    (h : T.markedColor a = τ (S.markedColor c)) (hab : b ≠ a):
+    (mulS T S a c h).markedColor (mulSInl hab) = T.markedColor b := by
+  rw [markedColor]
+  simp [mulS_color]
+  rw [mulSInl_mulSSetEquiv]
+  simp  [unmarkedColor, markSelectedIndex, Nat.succ_eq_add_one, Fintype.univ_ofSubsingleton,
+    Fin.zero_eta, Fin.isValue, notInImage, OrderIso.toEquiv_symm, RelIso.coe_fn_toEquiv,
+    Sum.elim_inl, Function.comp_apply, mapIso_apply_color, Equiv.symm_trans_apply,
+    Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.symm_symm, Equiv.sumAssoc_apply_inl_inr,
+    Equiv.sumCongr_apply, Equiv.coe_refl, Sum.map_inr, splitMarkedIndicesOne_symm_apply,
+    Sum.map_inl, OrderIso.symm_symm, OrderIso.apply_symm_apply, Equiv.coe_fn_symm_mk, Sum.swap_inl,
+    Equiv.Set.sumCompl_apply_inr, markedColor]
+
+@[simp]
+lemma mulSInr_color {n m : ℕ}
+    (T : Marked d X n.succ) (S : Marked d Y m.succ.succ) (c : Fin n.succ) (a b : Fin m.succ.succ)
+    (h : T.markedColor c = τ (S.markedColor a)) (hab : b ≠ a) :
+    (mulS T S c a h).markedColor (mulSInr hab) = S.markedColor b := by
+  rw [markedColor]
+  simp [mulS_color]
+  rw [mulSInr_mulSSetEquiv]
+  simp only [unmarkedColor, markSelectedIndex, Nat.succ_eq_add_one, Fintype.univ_ofSubsingleton,
+    Fin.zero_eta, Fin.isValue, notInImage, OrderIso.toEquiv_symm, RelIso.coe_fn_toEquiv,
+    Sum.elim_inr, Function.comp_apply, mapIso_apply_color, Equiv.symm_trans_apply,
+    Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.symm_symm, Equiv.sumAssoc_apply_inl_inr,
+    Equiv.sumCongr_apply, Equiv.coe_refl, Sum.map_inr, splitMarkedIndicesOne_symm_apply,
+    Sum.map_inl, OrderIso.symm_symm, OrderIso.apply_symm_apply, Equiv.coe_fn_symm_mk, Sum.swap_inl,
+    Equiv.Set.sumCompl_apply_inr, markedColor]
+-/
 end RealLorentzTensor