feat: Associativity of multiplication
This commit is contained in:
jstoobysmith
parent
bc2db84389
commit
99ccbb5d04
3 changed files with 451 additions and 197 deletions
|
|
@ -166,7 +166,7 @@ lemma indexValueIso_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) :
|
|||
rw [← Equiv.symm_apply_eq]
|
||||
funext y
|
||||
rw [indexValueIso_symm_apply', indexValueIso_symm_apply']
|
||||
simp [colorsIndexCast]
|
||||
simp only [Function.comp_apply, colorsIndexCast, Equiv.cast_symm, Equiv.cast_apply, cast_cast]
|
||||
apply cast_eq_iff_heq.mpr
|
||||
rw [Equiv.apply_symm_apply]
|
||||
|
||||
|
|
@ -396,150 +396,226 @@ def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Fin n.succ) ≃ (X ⊕ Fin 1)
|
|||
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 :=
|
||||
## Marking elements.
|
||||
|
||||
-/
|
||||
section markingElements
|
||||
|
||||
variable [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
|
||||
|
||||
/-- Splits a type based on an embedding from `Fin n` into elements not in the image of the
|
||||
embedding, and elements in the image. -/
|
||||
def markEmbeddingSet {n : ℕ} (f : Fin n ↪ X) :
|
||||
X ≃ {x // x ∈ (Finset.image f Finset.univ)ᶜ} ⊕ Fin n :=
|
||||
(Equiv.Set.sumCompl (Set.range ⇑f)).symm.trans <|
|
||||
(Equiv.sumComm _ _).trans <|
|
||||
Equiv.sumCongr ((Equiv.subtypeEquivRight (by simp)).trans (notInImage f).symm) <|
|
||||
Equiv.sumCongr ((Equiv.subtypeEquivRight (by simp))) <|
|
||||
(Function.Embedding.toEquivRange f).symm
|
||||
|
||||
lemma markEmbeddingSet_on_mem {n : ℕ} (f : Fin n ↪ X) (x : X)
|
||||
(hx : x ∈ Finset.image f Finset.univ) : markEmbeddingSet f x =
|
||||
Sum.inr (f.toEquivRange.symm ⟨x, by simpa using hx⟩) := by
|
||||
rw [markEmbeddingSet]
|
||||
simp only [Equiv.trans_apply, Equiv.sumComm_apply, Equiv.sumCongr_apply]
|
||||
rw [Equiv.Set.sumCompl_symm_apply_of_mem]
|
||||
rfl
|
||||
|
||||
lemma markEmbeddingSet_on_not_mem {n : ℕ} (f : Fin n ↪ X) (x : X)
|
||||
(hx : ¬ x ∈ (Finset.image f Finset.univ)) : markEmbeddingSet f x =
|
||||
Sum.inl ⟨x, by simpa using hx⟩ := by
|
||||
rw [markEmbeddingSet]
|
||||
simp only [Equiv.trans_apply, Equiv.sumComm_apply, Equiv.sumCongr_apply]
|
||||
rw [Equiv.Set.sumCompl_symm_apply_of_not_mem]
|
||||
rfl
|
||||
simpa using hx
|
||||
|
||||
/-- Marks the indicies of tensor in the image of an embedding. -/
|
||||
@[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⟩
|
||||
def markEmbedding {n : ℕ} (f : Fin n ↪ X) :
|
||||
RealLorentzTensor d X ≃ Marked d {x // x ∈ (Finset.image f Finset.univ)ᶜ} n :=
|
||||
mapIso d (markEmbeddingSet f)
|
||||
|
||||
@[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
|
||||
lemma markEmbeddingSet_on_mem_indexValue_apply {n : ℕ} (f : Fin n ↪ X) (T : RealLorentzTensor d X)
|
||||
(i : IndexValue d (markEmbedding f T).color) (x : X) (hx : x ∈ (Finset.image f Finset.univ)) :
|
||||
i (markEmbeddingSet f x) = colorsIndexCast (congrArg ((markEmbedding f) T).color
|
||||
(markEmbeddingSet_on_mem f x hx).symm)
|
||||
(i (Sum.inr (f.toEquivRange.symm ⟨x, by simpa using hx⟩))) := by
|
||||
simp [colorsIndexCast]
|
||||
symm
|
||||
simp [notInImage]
|
||||
funext x
|
||||
apply Subtype.ext
|
||||
rw [Finset.coe_orderIsoOfFin_apply]
|
||||
apply cast_eq_iff_heq.mpr
|
||||
rw [markEmbeddingSet_on_mem f x hx]
|
||||
|
||||
lemma markEmbeddingSet_on_not_mem_indexValue_apply {n : ℕ}
|
||||
(f : Fin n ↪ X) (T : RealLorentzTensor d X) (i : IndexValue d (markEmbedding f T).color)
|
||||
(x : X) (hx : ¬ x ∈ (Finset.image f Finset.univ)) :
|
||||
i (markEmbeddingSet f x) = colorsIndexCast (congrArg ((markEmbedding f) T).color
|
||||
(markEmbeddingSet_on_not_mem f x hx).symm) (i (Sum.inl ⟨x, by simpa using hx⟩)) := by
|
||||
simp [colorsIndexCast]
|
||||
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
|
||||
|
||||
apply cast_eq_iff_heq.mpr
|
||||
rw [markEmbeddingSet_on_not_mem f x hx]
|
||||
|
||||
/-- An equivalence between the IndexValues for a tensor `T` and the corresponding
|
||||
tensor with indicies maked by an embedding. -/
|
||||
@[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)
|
||||
def markEmbeddingIndexValue {n : ℕ} (f : Fin n ↪ X) (T : RealLorentzTensor d X) :
|
||||
IndexValue d T.color ≃ IndexValue d (markEmbedding f T).color :=
|
||||
indexValueIso d (markEmbeddingSet f) (
|
||||
(Equiv.comp_symm_eq (markEmbeddingSet f) ((markEmbedding f) T).color T.color).mp rfl)
|
||||
|
||||
lemma markSelectedIndex_markedColor (T : Marked d X n.succ) (i : Fin n.succ) :
|
||||
(markSelectedIndex i T).markedColor 0 = T.markedColor i := rfl
|
||||
lemma markEmbeddingIndexValue_apply_symm_on_mem {n : ℕ}
|
||||
(f : Fin n.succ ↪ X) (T : RealLorentzTensor d X) (i : IndexValue d (markEmbedding f T).color)
|
||||
(x : X) (hx : x ∈ (Finset.image f Finset.univ)) :
|
||||
(markEmbeddingIndexValue f T).symm i x = (colorsIndexCast ((congrFun ((Equiv.comp_symm_eq
|
||||
(markEmbeddingSet f) ((markEmbedding f) T).color T.color).mp rfl) x).trans
|
||||
(congrArg ((markEmbedding f) T).color (markEmbeddingSet_on_mem f x hx)))).symm
|
||||
(i (Sum.inr (f.toEquivRange.symm ⟨x, by simpa using hx⟩))) := by
|
||||
rw [markEmbeddingIndexValue, indexValueIso_symm_apply']
|
||||
rw [markEmbeddingSet_on_mem_indexValue_apply f T i x hx]
|
||||
simp [colorsIndexCast]
|
||||
|
||||
/-! 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
|
||||
lemma markEmbeddingIndexValue_apply_symm_on_not_mem {n : ℕ} (f : Fin n.succ ↪ X)
|
||||
(T : RealLorentzTensor d X) (i : IndexValue d (markEmbedding f T).color) (x : X)
|
||||
(hx : ¬ x ∈ (Finset.image f Finset.univ)) : (markEmbeddingIndexValue f T).symm i x =
|
||||
(colorsIndexCast ((congrFun ((Equiv.comp_symm_eq
|
||||
(markEmbeddingSet f) ((markEmbedding f) T).color T.color).mp rfl) x).trans
|
||||
((congrArg ((markEmbedding f) T).color (markEmbeddingSet_on_not_mem f x hx))))).symm
|
||||
(i (Sum.inl ⟨x, by simpa using hx⟩)) := by
|
||||
rw [markEmbeddingIndexValue, indexValueIso_symm_apply']
|
||||
rw [markEmbeddingSet_on_not_mem_indexValue_apply f T i x hx]
|
||||
simp only [Nat.succ_eq_add_one, Function.comp_apply, markEmbedding_apply_color, colorsIndexCast,
|
||||
Equiv.cast_symm, id_eq, eq_mp_eq_cast, eq_mpr_eq_cast, Equiv.cast_apply, cast_cast, cast_eq,
|
||||
Equiv.cast_refl, Equiv.refl_symm]
|
||||
rfl
|
||||
|
||||
/-- Given an equivalence of types, an embedding `f` to an embedding `g`, the equivalence
|
||||
taking the complement of the image of `f` to the complement of the image of `g`. -/
|
||||
@[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
|
||||
def equivEmbedCompl (e : X ≃ Y) {f : Fin n ↪ X} {g : Fin n ↪ Y} (he : f.trans e = g) :
|
||||
{x // x ∈ (Finset.image f Finset.univ)ᶜ} ≃ {y // y ∈ (Finset.image g Finset.univ)ᶜ} :=
|
||||
(Equiv.subtypeEquivOfSubtype' e).trans <|
|
||||
(Equiv.subtypeEquivRight (fun x => by simp [← he, Equiv.eq_symm_apply]))
|
||||
|
||||
|
||||
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]
|
||||
lemma markEmbedding_mapIso_right (e : X ≃ Y) (f : Fin n ↪ X) (g : Fin n ↪ Y) (he : f.trans e = g)
|
||||
(T : RealLorentzTensor d X) : markEmbedding g (mapIso d e T) =
|
||||
mapIso d (Equiv.sumCongr (equivEmbedCompl e he) (Equiv.refl (Fin n))) (markEmbedding f T) := by
|
||||
rw [markEmbedding, markEmbedding]
|
||||
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
|
||||
repeat apply congrArg
|
||||
refine Equiv.ext (fun x => ?_)
|
||||
simp only [Equiv.trans_apply, Equiv.sumCongr_apply, Equiv.coe_refl]
|
||||
by_cases hx : x ∈ Finset.image f Finset.univ
|
||||
· rw [markEmbeddingSet_on_mem f x hx, markEmbeddingSet_on_mem g (e x) (by simpa [← he] using hx)]
|
||||
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)
|
||||
simp only [Sum.map_inr, id_eq, Sum.inr.injEq, Equiv.symm_apply_eq,
|
||||
Function.Embedding.toEquivRange_apply, Function.Embedding.trans_apply, Equiv.coe_toEmbedding,
|
||||
Subtype.mk.injEq, EmbeddingLike.apply_eq_iff_eq]
|
||||
change x = f.toEquivRange _
|
||||
rw [Equiv.apply_symm_apply]
|
||||
· rw [markEmbeddingSet_on_not_mem f x hx,
|
||||
markEmbeddingSet_on_not_mem g (e x) (by simpa [← he] using hx)]
|
||||
subst he
|
||||
rfl
|
||||
|
||||
lemma markEmbedding_mapIso_left {n m : ℕ} (e : Fin n ≃ Fin m) (f : Fin n ↪ X) (g : Fin m ↪ X)
|
||||
(he : e.symm.toEmbedding.trans f = g) (T : RealLorentzTensor d X) :
|
||||
markEmbedding g T = mapIso d (Equiv.sumCongr (Equiv.subtypeEquivRight (fun x => by
|
||||
simpa [← he] using Equiv.forall_congr_left e)) e) (markEmbedding f T) := by
|
||||
rw [markEmbedding, markEmbedding]
|
||||
erw [← Equiv.trans_apply]
|
||||
rw [mapIso_trans]
|
||||
apply congrFun
|
||||
repeat apply congrArg
|
||||
refine Equiv.ext (fun x => ?_)
|
||||
simp only [Equiv.trans_apply, Equiv.sumCongr_apply]
|
||||
by_cases hx : x ∈ Finset.image f Finset.univ
|
||||
· rw [markEmbeddingSet_on_mem f x hx, markEmbeddingSet_on_mem g x (by
|
||||
simp [← he, hx]
|
||||
obtain ⟨y, _, hy2⟩ := Finset.mem_image.mp hx
|
||||
use e y
|
||||
simpa using hy2)]
|
||||
subst he
|
||||
simp [Equiv.symm_apply_eq]
|
||||
change x = f.toEquivRange _
|
||||
rw [Equiv.apply_symm_apply]
|
||||
· rw [markEmbeddingSet_on_not_mem f x hx, markEmbeddingSet_on_not_mem g x (by
|
||||
simpa [← he, hx] using fun x => not_exists.mp (Finset.mem_image.mpr.mt hx) (e.symm x))]
|
||||
subst he
|
||||
rfl
|
||||
|
||||
/-!
|
||||
|
||||
## Marking a single element
|
||||
|
||||
-/
|
||||
|
||||
/-- An embedding from `Fin 1` into `X` given an element `x ∈ X`. -/
|
||||
@[simps!]
|
||||
def embedSingleton (x : X) : Fin 1 ↪ X :=
|
||||
⟨![x], fun x y => by fin_cases x; fin_cases y; simp⟩
|
||||
|
||||
lemma embedSingleton_toEquivRange_symm (x : X) :
|
||||
(embedSingleton x).toEquivRange.symm ⟨x, by simp⟩ = 0 := by
|
||||
exact Fin.fin_one_eq_zero _
|
||||
|
||||
/-- Equivalence, taking a tensor to a tensor with a single marked index. -/
|
||||
@[simps!]
|
||||
def markSingle (x : X) : RealLorentzTensor d X ≃ Marked d {x' // x' ≠ x} 1 :=
|
||||
(markEmbedding (embedSingleton x)).trans
|
||||
(mapIso d (Equiv.sumCongr (Equiv.subtypeEquivRight (fun x => by simp)) (Equiv.refl _)))
|
||||
|
||||
/-- Equivalence between index values of a tensor and the corrsponding tensor with a single
|
||||
marked index. -/
|
||||
@[simps!]
|
||||
def markSingleIndexValue (T : RealLorentzTensor d X) (x : X) :
|
||||
IndexValue d T.color ≃ IndexValue d (markSingle x T).color :=
|
||||
(markEmbeddingIndexValue (embedSingleton x) T).trans <|
|
||||
indexValueIso d (Equiv.sumCongr (Equiv.subtypeEquivRight (fun x => by simp)) (Equiv.refl _))
|
||||
(by funext x_1; simp)
|
||||
|
||||
/-- Given an equivalence of types, taking `x` to `y` the corresponding equivalence of
|
||||
subtypes of elements not equal to `x` and not equal to `y` respectively. -/
|
||||
@[simps!]
|
||||
def equivSingleCompl (e : X ≃ Y) {x : X} {y : Y} (he : e x = y) :
|
||||
{x' // x' ≠ x} ≃ {y' // y' ≠ y} :=
|
||||
(Equiv.subtypeEquivOfSubtype' e).trans <|
|
||||
Equiv.subtypeEquivRight (fun a => by simp [Equiv.symm_apply_eq, he])
|
||||
|
||||
lemma markSingle_mapIso (e : X ≃ Y) (x : X) (y : Y) (he : e x = y)
|
||||
(T : RealLorentzTensor d X) : markSingle y (mapIso d e T) =
|
||||
mapIso d (Equiv.sumCongr (equivSingleCompl e he) (Equiv.refl _)) (markSingle x T) := by
|
||||
rw [markSingle, Equiv.trans_apply]
|
||||
rw [markEmbedding_mapIso_right e (embedSingleton x) (embedSingleton y)
|
||||
(Function.Embedding.ext_iff.mp (fun a => by simpa using he)), markSingle, markEmbedding]
|
||||
erw [← Equiv.trans_apply, ← Equiv.trans_apply, ← Equiv.trans_apply]
|
||||
rw [mapIso_trans, mapIso_trans, mapIso_trans, mapIso_trans]
|
||||
apply congrFun
|
||||
repeat apply congrArg
|
||||
refine Equiv.ext fun x => ?_
|
||||
simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.sumCongr_trans,
|
||||
Equiv.trans_refl, Equiv.trans_apply, Equiv.sumCongr_apply, Equiv.coe_trans, Equiv.coe_refl,
|
||||
Sum.map_map, CompTriple.comp_eq]
|
||||
subst he
|
||||
rfl
|
||||
|
||||
/-!
|
||||
|
||||
## Marking two elements
|
||||
|
||||
-/
|
||||
|
||||
/-- An embedding from `Fin 2` given two inequivalent elements. -/
|
||||
@[simps!]
|
||||
def embedDoubleton (x y : X) (h : x ≠ y) : Fin 2 ↪ X :=
|
||||
⟨![x, y], fun a b => by
|
||||
fin_cases a <;> fin_cases b <;> simp [h]
|
||||
exact h.symm⟩
|
||||
|
||||
end markingElements
|
||||
|
||||
end Marked
|
||||
|
||||
|
|
|
|||
|
|
@ -50,12 +50,11 @@ 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
|
||||
simp only [Equiv.trans_apply, toReal_apply, mapIso_apply_color, mapIso_apply_coord]
|
||||
apply congrArg
|
||||
funext x
|
||||
exact IsEmpty.elim h x
|
||||
|
||||
|
||||
/-!
|
||||
|
||||
# Tensors from reals, vectors and matrices
|
||||
|
|
@ -285,8 +284,9 @@ open Matrix
|
|||
|
||||
/-- The action of the Lorentz group on `ofReal v` is trivial. -/
|
||||
@[simp]
|
||||
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)
|
||||
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]
|
||||
|
|
|
|||
|
|
@ -15,7 +15,6 @@ marked index. This is equivalent to contracting two Lorentz tensors.
|
|||
We prove various results about this multiplication.
|
||||
|
||||
-/
|
||||
/-! TODO: Generalize to contracting any marked index of a marked tensor. -/
|
||||
/-! TODO: Set up a good notation for the multiplication. -/
|
||||
|
||||
namespace RealLorentzTensor
|
||||
|
|
@ -38,6 +37,31 @@ def mul {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
|
|||
S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2,
|
||||
oneMarkedIndexValue $ colorsIndexDualCast h x))
|
||||
|
||||
/-- The index value appearing in the multiplication of Marked tensors on the left. -/
|
||||
def mulFstArg {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
|
||||
(i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor))
|
||||
(x : ColorsIndex d (T.color (markedPoint X 0))) : IndexValue d T.color :=
|
||||
splitIndexValue.symm ((indexValueSumEquiv i).1, oneMarkedIndexValue x)
|
||||
|
||||
lemma mulFstArg_inr {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
|
||||
(i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor))
|
||||
(x : ColorsIndex d (T.color (markedPoint X 0))) :
|
||||
mulFstArg i x (Sum.inr 0) = x := by
|
||||
rfl
|
||||
|
||||
lemma mulFstArg_inl {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
|
||||
(i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor))
|
||||
(x : ColorsIndex d (T.color (markedPoint X 0))) (c : X):
|
||||
mulFstArg i x (Sum.inl c) = i (Sum.inl c) := by
|
||||
rfl
|
||||
|
||||
/-- The index value appearing in the multiplication of Marked tensors on the right. -/
|
||||
def mulSndArg {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
|
||||
(i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor))
|
||||
(x : ColorsIndex d (T.color (markedPoint X 0))) (h : T.markedColor 0 = τ (S.markedColor 0)) :
|
||||
IndexValue d S.color :=
|
||||
splitIndexValue.symm ((indexValueSumEquiv i).2, oneMarkedIndexValue $ colorsIndexDualCast h x)
|
||||
|
||||
/-!
|
||||
|
||||
## Expressions for multiplication
|
||||
|
|
@ -237,79 +261,233 @@ lemma mul_lorentzAction (T : Marked d X 1) (S : Marked d Y 1)
|
|||
|
||||
-/
|
||||
|
||||
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
|
||||
variable {n m : ℕ} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
|
||||
{X' Y' Z : Type} [Fintype X'] [DecidableEq X'] [Fintype Y'] [DecidableEq Y']
|
||||
[Fintype Z] [DecidableEq Z]
|
||||
|
||||
/-- The multiplication of two real Lorentz Tensors along provided indices. -/
|
||||
@[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)
|
||||
def mulS (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (x : X) (y : Y)
|
||||
(h : T.color x = τ (S.color y)) : RealLorentzTensor d ({x' // x' ≠ x} ⊕ {y' // y' ≠ y}) :=
|
||||
mul (markSingle x T) (markSingle y S) h
|
||||
|
||||
/-- The first index value appearing in the multiplication of two Lorentz tensors. -/
|
||||
def mulSFstArg {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
|
||||
(i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
|
||||
(a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))) :
|
||||
IndexValue d T.color := (markSingleIndexValue T x).symm (mulFstArg i a)
|
||||
|
||||
/-- 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]
|
||||
lemma mulSFstArg_ext {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
|
||||
{i j : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)}
|
||||
{a b : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))}
|
||||
(hij : i = j) (hab : a = b) : mulSFstArg i a = mulSFstArg j b := by
|
||||
subst hij; subst hab
|
||||
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]
|
||||
lemma mulSFstArg_on_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
|
||||
(i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
|
||||
(a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))) :
|
||||
mulSFstArg i a x = a := by
|
||||
rw [mulSFstArg, markSingleIndexValue]
|
||||
simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply,
|
||||
Sum.map_inr, id_eq]
|
||||
erw [markEmbeddingIndexValue_apply_symm_on_mem]
|
||||
swap
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Finset.univ_unique, Fin.default_eq_zero,
|
||||
Fin.isValue, Finset.image_singleton, embedSingleton_apply, Finset.mem_singleton]
|
||||
rw [indexValueIso_symm_apply']
|
||||
erw [Equiv.symm_apply_eq, Equiv.symm_apply_eq]
|
||||
simp only [Function.comp_apply, colorsIndexCast, Equiv.cast_symm, Equiv.cast_apply, cast_cast]
|
||||
symm
|
||||
apply cast_eq_iff_heq.mpr
|
||||
rw [embedSingleton_toEquivRange_symm]
|
||||
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]
|
||||
-/
|
||||
lemma mulSFstArg_on_not_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
|
||||
(i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
|
||||
(a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0)))
|
||||
(c : X) (hc : c ≠ x) : mulSFstArg i a c = i (Sum.inl ⟨c, hc⟩) := by
|
||||
rw [mulSFstArg, markSingleIndexValue]
|
||||
simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply,
|
||||
Sum.map_inr, id_eq]
|
||||
erw [markEmbeddingIndexValue_apply_symm_on_not_mem]
|
||||
swap
|
||||
simpa using hc
|
||||
rfl
|
||||
|
||||
/-- The second index value appearing in the multiplication of two Lorentz tensors. -/
|
||||
def mulSSndArg {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
|
||||
(i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
|
||||
(a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0)))
|
||||
(h : T.color x = τ (S.color y)) : IndexValue d S.color :=
|
||||
(markSingleIndexValue S y).symm (mulSndArg i a h)
|
||||
|
||||
lemma mulSSndArg_on_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
|
||||
(i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
|
||||
(a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0)))
|
||||
(h : T.color x = τ (S.color y)) : mulSSndArg i a h y = colorsIndexDualCast h a := by
|
||||
rw [mulSSndArg, markSingleIndexValue]
|
||||
simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply,
|
||||
Sum.map_inr, id_eq]
|
||||
erw [markEmbeddingIndexValue_apply_symm_on_mem]
|
||||
swap
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Finset.univ_unique, Fin.default_eq_zero,
|
||||
Fin.isValue, Finset.image_singleton, embedSingleton_apply, Finset.mem_singleton]
|
||||
rw [indexValueIso_symm_apply']
|
||||
erw [Equiv.symm_apply_eq, Equiv.symm_apply_eq]
|
||||
simp only [Function.comp_apply, colorsIndexCast, Equiv.cast_symm, Equiv.cast_apply, cast_cast]
|
||||
symm
|
||||
apply cast_eq_iff_heq.mpr
|
||||
rw [embedSingleton_toEquivRange_symm]
|
||||
rfl
|
||||
|
||||
lemma mulSSndArg_on_not_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
|
||||
(i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
|
||||
(a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0)))
|
||||
(h : T.color x = τ (S.color y)) (c : Y) (hc : c ≠ y) :
|
||||
mulSSndArg i a h c = i (Sum.inr ⟨c, hc⟩) := by
|
||||
rw [mulSSndArg, markSingleIndexValue]
|
||||
simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply,
|
||||
Sum.map_inr, id_eq]
|
||||
erw [markEmbeddingIndexValue_apply_symm_on_not_mem]
|
||||
swap
|
||||
simpa using hc
|
||||
rfl
|
||||
|
||||
lemma mulSSndArg_ext {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
|
||||
{i j : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)}
|
||||
{a b : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))}
|
||||
(h : T.color x = τ (S.color y)) (hij : i = j) (hab : a = b) :
|
||||
mulSSndArg i a h = mulSSndArg j b h := by
|
||||
subst hij
|
||||
subst hab
|
||||
rfl
|
||||
|
||||
lemma mulS_coord_arg (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (x : X) (y : Y)
|
||||
(h : T.color x = τ (S.color y))
|
||||
(i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)) :
|
||||
(mulS T S x y h).coord i = ∑ a, T.coord (mulSFstArg i a) * S.coord (mulSSndArg i a h) := by
|
||||
rfl
|
||||
|
||||
lemma mulS_mapIso (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y)
|
||||
(eX : X ≃ X') (eY : Y ≃ Y') (x : X) (y : Y) (x' : X') (y' : Y') (hx : eX x = x')
|
||||
(hy : eY y = y') (h : T.color x = τ (S.color y)) :
|
||||
mulS (mapIso d eX T) (mapIso d eY S) x' y' (by subst hx hy; simpa using h) =
|
||||
mapIso d (Equiv.sumCongr (equivSingleCompl eX hx) (equivSingleCompl eY hy))
|
||||
(mulS T S x y h) := by
|
||||
rw [mulS, mulS, mul_mapIso]
|
||||
congr 1 <;> rw [markSingle_mapIso]
|
||||
|
||||
lemma mulS_lorentzAction (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y)
|
||||
(x : X) (y : Y) (h : T.color x = τ (S.color y)) (Λ : LorentzGroup d) :
|
||||
mulS (Λ • T) (Λ • S) x y h = Λ • mulS T S x y h := by
|
||||
rw [mulS, mulS, ← mul_lorentzAction]
|
||||
congr 1
|
||||
all_goals
|
||||
rw [markSingle, markEmbedding, Equiv.trans_apply]
|
||||
erw [lorentzAction_mapIso, lorentzAction_mapIso]
|
||||
rfl
|
||||
|
||||
lemma mulS_symm (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y)
|
||||
(x : X) (y : Y) (h : T.color x = τ (S.color y)) :
|
||||
mapIso d (Equiv.sumComm _ _) (mulS T S x y h) = mulS S T y x (color_eq_dual_symm h) := by
|
||||
rw [mulS, mulS, mul_symm]
|
||||
|
||||
/-- An equivalence of types assocaited with multipying two consecutive indices,
|
||||
with the second index appearing on the left. -/
|
||||
def mulSSplitLeft {y y' : Y} (hy : y ≠ y') (z : Z) :
|
||||
{yz // yz ≠ (Sum.inl ⟨y, hy⟩ : {y'' // y'' ≠ y'} ⊕ {z' // z' ≠ z})} ≃
|
||||
{y'' // y'' ≠ y' ∧ y'' ≠ y} ⊕ {z' // z' ≠ z} :=
|
||||
Equiv.subtypeSum.trans <|
|
||||
Equiv.sumCongr (
|
||||
(Equiv.subtypeEquivRight (fun a => by
|
||||
obtain ⟨a, p⟩ := a; simp only [ne_eq, Sum.inl.injEq, Subtype.mk.injEq])).trans
|
||||
(Equiv.subtypeSubtypeEquivSubtypeInter _ _)) <|
|
||||
Equiv.subtypeUnivEquiv (fun a => by simp)
|
||||
|
||||
/-- An equivalence of types assocaited with multipying two consecutive indices with the
|
||||
second index appearing on the right. -/
|
||||
def mulSSplitRight {y y' : Y} (hy : y ≠ y') (z : Z) :
|
||||
{yz // yz ≠ (Sum.inr ⟨y', hy.symm⟩ : {z' // z' ≠ z} ⊕ {y'' // y'' ≠ y})} ≃
|
||||
{z' // z' ≠ z} ⊕ {y'' // y'' ≠ y' ∧ y'' ≠ y} :=
|
||||
Equiv.subtypeSum.trans <|
|
||||
Equiv.sumCongr (Equiv.subtypeUnivEquiv (fun a => by simp)) <|
|
||||
(Equiv.subtypeEquivRight (fun a => by
|
||||
obtain ⟨a, p⟩ := a; simp only [ne_eq, Sum.inr.injEq, Subtype.mk.injEq])).trans <|
|
||||
((Equiv.subtypeSubtypeEquivSubtypeInter _ _).trans
|
||||
(Equiv.subtypeEquivRight (fun y'' => And.comm)))
|
||||
|
||||
/-- An equivalence of types associated with the associativity property of multiplication. -/
|
||||
def mulSAssocIso (x : X) {y y' : Y} (hy : y ≠ y') (z : Z) :
|
||||
{x' // x' ≠ x} ⊕ {yz // yz ≠ (Sum.inl ⟨y, hy⟩ : {y'' // y'' ≠ y'} ⊕ {z' // z' ≠ z})}
|
||||
≃ {xy // xy ≠ (Sum.inr ⟨y', hy.symm⟩ : {x' // x' ≠ x} ⊕ {y'' // y'' ≠ y})} ⊕ {z' // z' ≠ z} :=
|
||||
(Equiv.sumCongr (Equiv.refl _) (mulSSplitLeft hy z)).trans <|
|
||||
(Equiv.sumAssoc _ _ _).symm.trans <|
|
||||
(Equiv.sumCongr (mulSSplitRight hy x).symm (Equiv.refl _))
|
||||
|
||||
lemma mulS_assoc_color {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y}
|
||||
{U : RealLorentzTensor d Z} {x : X} {y y' : Y} (hy : y ≠ y') {z : Z}
|
||||
(h : T.color x = τ (S.color y))
|
||||
(h' : S.color y' = τ (U.color z)) : (mulS (mulS T S x y h) U (Sum.inr ⟨y', hy.symm⟩) z h').color
|
||||
= (mapIso d (mulSAssocIso x hy z) (mulS T (mulS S U y' z h') x (Sum.inl ⟨y, hy⟩) h)).color := by
|
||||
funext a
|
||||
match a with
|
||||
| .inl ⟨.inl _, _⟩ => rfl
|
||||
| .inl ⟨.inr _, _⟩ => rfl
|
||||
| .inr _ => rfl
|
||||
|
||||
/-- An equivalence of index values associated with the associativity property of multiplication. -/
|
||||
def mulSAssocIndexValue {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y}
|
||||
{U : RealLorentzTensor d Z} {x : X} {y y' : Y} (hy : y ≠ y') {z : Z}
|
||||
(h : T.color x = τ (S.color y)) (h' : S.color y' = τ (U.color z)) :
|
||||
IndexValue d ((T.mulS S x y h).mulS U (Sum.inr ⟨y', hy.symm⟩) z h').color ≃
|
||||
IndexValue d (T.mulS (S.mulS U y' z h') x (Sum.inl ⟨y, hy⟩) h).color :=
|
||||
indexValueIso d (mulSAssocIso x hy z).symm (mulS_assoc_color hy h h')
|
||||
|
||||
/-- Multiplication of indices is associative, up to a `mapIso` equivalence. -/
|
||||
lemma mulS_assoc (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (U : RealLorentzTensor d Z)
|
||||
(x : X) (y y' : Y) (hy : y ≠ y') (z : Z) (h : T.color x = τ (S.color y))
|
||||
(h' : S.color y' = τ (U.color z)) : mulS (mulS T S x y h) U (Sum.inr ⟨y', hy.symm⟩) z h' =
|
||||
mapIso d (mulSAssocIso x hy z) (mulS T (mulS S U y' z h') x (Sum.inl ⟨y, hy⟩) h) := by
|
||||
apply ext ?_ ?_
|
||||
· funext a
|
||||
match a with
|
||||
| .inl ⟨.inl _, _⟩ => rfl
|
||||
| .inl ⟨.inr _, _⟩ => rfl
|
||||
| .inr _ => rfl
|
||||
funext i
|
||||
trans ∑ a, (∑ b, T.coord (mulSFstArg (mulSFstArg i a) b) *
|
||||
S.coord (mulSSndArg (mulSFstArg i a) b h)) * U.coord (mulSSndArg i a h')
|
||||
rfl
|
||||
trans ∑ a, T.coord (mulSFstArg (mulSAssocIndexValue hy h h' i) a) *
|
||||
(∑ b, S.coord (mulSFstArg (mulSSndArg (mulSAssocIndexValue hy h h' i) a h) b) *
|
||||
U.coord (mulSSndArg (mulSSndArg (mulSAssocIndexValue hy h h' i) a h) b h'))
|
||||
swap
|
||||
rw [mapIso_apply_coord, mulS_coord_arg, indexValueIso_symm]
|
||||
rfl
|
||||
rw [Finset.sum_congr rfl (fun x _ => Finset.sum_mul _ _ _)]
|
||||
rw [Finset.sum_congr rfl (fun x _ => Finset.mul_sum _ _ _)]
|
||||
rw [Finset.sum_comm]
|
||||
refine Finset.sum_congr rfl (fun a _ => ?_)
|
||||
refine Finset.sum_congr rfl (fun b _ => ?_)
|
||||
rw [mul_assoc]
|
||||
refine Mathlib.Tactic.Ring.mul_congr rfl (Mathlib.Tactic.Ring.mul_congr ?_ rfl rfl) rfl
|
||||
apply congrArg
|
||||
funext c
|
||||
by_cases hcy : c = y
|
||||
· subst hcy
|
||||
rw [mulSSndArg_on_mem, mulSFstArg_on_not_mem, mulSSndArg_on_mem]
|
||||
rfl
|
||||
· by_cases hcy' : c = y'
|
||||
· subst hcy'
|
||||
rw [mulSFstArg_on_mem, mulSSndArg_on_not_mem, mulSFstArg_on_mem]
|
||||
· rw [mulSFstArg_on_not_mem, mulSSndArg_on_not_mem, mulSSndArg_on_not_mem,
|
||||
mulSFstArg_on_not_mem]
|
||||
rw [mulSAssocIndexValue, indexValueIso_eq_symm, indexValueIso_symm_apply']
|
||||
simp [colorsIndexCast, Equiv.refl_apply]
|
||||
erw [Equiv.refl_apply]
|
||||
rfl
|
||||
exact hcy'
|
||||
simpa using hcy
|
||||
|
||||
end RealLorentzTensor
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue