chore: Bump to 4.11.0
This commit is contained in:
jstoobysmith
parent
b6162217b7
commit
17f09022db
48 changed files with 404 additions and 137 deletions
|
|
@ -74,6 +74,12 @@ lemma doublePoint_B₃_B₃ (R : MSSMACC.LinSols) : cubeTriLin B₃.val B₃.val
|
|||
have h0 := hLin 0
|
||||
have h2 := hLin 2
|
||||
simp [Fin.sum_univ_three] at h0 h2
|
||||
linear_combination 9 * h0 - 24 * h2
|
||||
have h1 {a b : ℚ} (ha : a = 0) (hb : b = 0) : 9 * a - 24 * b = 0 := by
|
||||
rw [ha, hb]
|
||||
simp
|
||||
have h1' := h1 h0 h2
|
||||
ring_nf at h1'
|
||||
ring_nf
|
||||
exact h1'
|
||||
|
||||
end MSSMACC
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith
|
|||
import HepLean.AnomalyCancellation.MSSMNu.Basic
|
||||
import HepLean.AnomalyCancellation.MSSMNu.Y3
|
||||
import HepLean.AnomalyCancellation.MSSMNu.B3
|
||||
import Mathlib.Tactic.Polyrith
|
||||
import Mathlib.Tactic.LinearCombination'
|
||||
/-!
|
||||
# The line through B₃ and Y₃
|
||||
|
||||
|
|
@ -65,21 +65,22 @@ lemma doublePoint_Y₃_B₃ (R : MSSMACC.LinSols) :
|
|||
cubeTriLin Y₃.val B₃.val R.val = 0 := by
|
||||
simp only [cubeTriLin, TriLinearSymm.mk₃_toFun_apply_apply, cubeTriLinToFun,
|
||||
MSSMSpecies_numberCharges, Fin.isValue, Fin.reduceFinMk]
|
||||
rw [Fin.sum_univ_three]
|
||||
rw [B₃_val, Y₃_val]
|
||||
rw [B₃AsCharge, Y₃AsCharge]
|
||||
rw [Fin.sum_univ_three, B₃_val, Y₃_val, B₃AsCharge, Y₃AsCharge]
|
||||
repeat rw [toSMSpecies_toSpecies_inv]
|
||||
rw [Hd_toSpecies_inv, Hu_toSpecies_inv]
|
||||
rw [Hd_toSpecies_inv, Hu_toSpecies_inv]
|
||||
rw [Hd_toSpecies_inv, Hu_toSpecies_inv, Hd_toSpecies_inv, Hu_toSpecies_inv]
|
||||
simp only [mul_one, Fin.isValue, toSMSpecies_apply, one_mul, mul_neg, neg_neg, neg_mul, zero_mul,
|
||||
add_zero, neg_zero, Hd_apply, Fin.reduceFinMk, Hu_apply]
|
||||
have hLin := R.linearSol
|
||||
simp at hLin
|
||||
simp only [MSSMACC_numberLinear, MSSMACC_linearACCs, Nat.reduceMul, Fin.isValue,
|
||||
Fin.reduceFinMk] at hLin
|
||||
have h1 := hLin 1
|
||||
have h2 := hLin 2
|
||||
have h3 := hLin 3
|
||||
simp [Fin.sum_univ_three] at h1 h2 h3
|
||||
linear_combination -(12 * h2) + 9 * h1 + 3 * h3
|
||||
simp only [Fin.isValue, Fin.sum_univ_three, Prod.mk_zero_zero, LinearMap.coe_mk, AddHom.coe_mk,
|
||||
Prod.mk_one_one] at h1 h2 h3
|
||||
linear_combination (norm := ring_nf) -(12 * h2) + 9 * h1 + 3 * h3
|
||||
simp only [Fin.isValue, Prod.mk_zero_zero, Prod.mk_one_one, add_add_sub_cancel, add_neg_cancel]
|
||||
|
||||
|
||||
lemma lineY₃B₃_doublePoint (R : MSSMACC.LinSols) (a b : ℚ) :
|
||||
cubeTriLin (lineY₃B₃ a b).val (lineY₃B₃ a b).val R.val = 0 := by
|
||||
|
|
|
|||
|
|
@ -101,7 +101,7 @@ lemma inQuadSolProp_iff_quadCoeff_zero (T : MSSMACC.Sols) : InQuadSolProp T ↔
|
|||
· rw [quadCoeff, show dot Y₃.val B₃.val = 108 by rfl] at h
|
||||
simp only [Fin.isValue, Fin.reduceFinMk, mul_eq_zero, OfNat.ofNat_ne_zero, ne_eq,
|
||||
not_false_eq_true, pow_eq_zero_iff, or_self, false_or] at h
|
||||
apply (add_eq_zero_iff' (sq_nonneg _) (sq_nonneg _)).mp at h
|
||||
apply (add_eq_zero_iff_of_nonneg (sq_nonneg _) (sq_nonneg _)).mp at h
|
||||
simp only [Fin.isValue, Fin.reduceFinMk, ne_eq, OfNat.ofNat_ne_zero,
|
||||
not_false_eq_true, pow_eq_zero_iff] at h
|
||||
exact h
|
||||
|
|
@ -148,7 +148,7 @@ lemma inCubeSolProp_iff_cubicCoeff_zero (T : MSSMACC.Sols) :
|
|||
· rw [cubicCoeff, show dot Y₃.val B₃.val = 108 by rfl] at h
|
||||
simp only [Fin.isValue, Fin.reduceFinMk, mul_eq_zero, OfNat.ofNat_ne_zero, ne_eq,
|
||||
not_false_eq_true, pow_eq_zero_iff, or_self, false_or] at h
|
||||
apply (add_eq_zero_iff' (sq_nonneg _) (sq_nonneg _)).mp at h
|
||||
apply (add_eq_zero_iff_of_nonneg (sq_nonneg _) (sq_nonneg _)).mp at h
|
||||
simp only [Fin.isValue, Fin.reduceFinMk, ne_eq, OfNat.ofNat_ne_zero,
|
||||
not_false_eq_true, pow_eq_zero_iff] at h
|
||||
exact h.symm
|
||||
|
|
@ -240,7 +240,7 @@ lemma toSolNS_proj (T : NotInLineEqSol) : toSolNS (toSolNSProj T.val) = T.val :=
|
|||
ring
|
||||
rw [h1]
|
||||
have h1 := (lineEqPropSol_iff_lineEqCoeff_zero T.val).mpr.mt T.prop
|
||||
rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h1]
|
||||
rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel₀ h1]
|
||||
exact MulAction.one_smul T.1.val
|
||||
|
||||
/-- A solution to the ACCs, given an element of `inLineEq × ℚ × ℚ × ℚ`. -/
|
||||
|
|
@ -283,7 +283,7 @@ lemma inLineEqToSol_proj (T : InLineEqSol) : inLineEqToSol (inLineEqProj T) = T.
|
|||
ring
|
||||
rw [h1]
|
||||
have h2 := (inQuadSolProp_iff_quadCoeff_zero T.val).mpr.mt T.prop.2
|
||||
rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h2]
|
||||
rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel₀ h2]
|
||||
exact MulAction.one_smul T.1.val
|
||||
|
||||
/-- Given an element of `inQuad × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
|
||||
|
|
@ -328,7 +328,7 @@ lemma inQuadToSol_proj (T : InQuadSol) : inQuadToSol (inQuadProj T) = T.val := b
|
|||
ring
|
||||
rw [h1]
|
||||
have h2 := (inCubeSolProp_iff_cubicCoeff_zero T.val).mpr.mt T.prop.2.2
|
||||
rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h2]
|
||||
rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel₀ h2]
|
||||
exact MulAction.one_smul T.1.val
|
||||
|
||||
/-- Given a element of `inQuadCube × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
|
||||
|
|
@ -368,7 +368,7 @@ lemma inQuadCubeToSol_proj (T : InQuadCubeSol) :
|
|||
rw [Y₃_plus_B₃_plus_proj]
|
||||
ring_nf
|
||||
simp only [Fin.isValue, Fin.reduceFinMk, zero_smul, add_zero, zero_add]
|
||||
rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel]
|
||||
rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel₀]
|
||||
· exact MulAction.one_smul (T.1).val
|
||||
· rw [show dot Y₃.val B₃.val = 108 by rfl]
|
||||
exact Ne.symm (OfNat.zero_ne_ofNat 108)
|
||||
|
|
|
|||
|
|
@ -74,6 +74,9 @@ lemma doublePoint_Y₃_Y₃ (R : MSSMACC.LinSols) :
|
|||
simp at hLin
|
||||
have h3 := hLin 3
|
||||
simp [Fin.sum_univ_three] at h3
|
||||
linear_combination 6 * h3
|
||||
have h5 := congrArg (HMul.hMul 6) h3
|
||||
ring_nf at h5
|
||||
ring_nf
|
||||
exact h5
|
||||
|
||||
end MSSMACC
|
||||
|
|
|
|||
|
|
@ -50,6 +50,7 @@ section charges
|
|||
variable {S : (PureU1 n.succ).Charges} {A : (PureU1 n.succ).LinSols}
|
||||
variable (hS : ConstAbsSorted S) (hA : ConstAbsSorted A.val)
|
||||
|
||||
include hS in
|
||||
lemma lt_eq {k i : Fin n.succ} (hk : S k ≤ 0) (hik : i ≤ k) : S i = S k := by
|
||||
have hSS := hS.2 i k hik
|
||||
have ht := hS.1 i k
|
||||
|
|
@ -58,11 +59,13 @@ lemma lt_eq {k i : Fin n.succ} (hk : S k ≤ 0) (hik : i ≤ k) : S i = S k := b
|
|||
· exact h
|
||||
· linarith
|
||||
|
||||
include hS in
|
||||
lemma val_le_zero {i : Fin n.succ} (hi : S i ≤ 0) : S i = S (0 : Fin n.succ) := by
|
||||
symm
|
||||
apply lt_eq hS hi
|
||||
exact Fin.zero_le i
|
||||
|
||||
include hS in
|
||||
lemma gt_eq {k i: Fin n.succ} (hk : 0 ≤ S k) (hik : k ≤ i) : S i = S k := by
|
||||
have hSS := hS.2 k i hik
|
||||
have ht := hS.1 i k
|
||||
|
|
@ -71,10 +74,12 @@ lemma gt_eq {k i: Fin n.succ} (hk : 0 ≤ S k) (hik : k ≤ i) : S i = S k := by
|
|||
· exact h
|
||||
· linarith
|
||||
|
||||
include hS in
|
||||
lemma zero_gt (h0 : 0 ≤ S (0 : Fin n.succ)) (i : Fin n.succ) : S (0 : Fin n.succ) = S i := by
|
||||
symm
|
||||
refine gt_eq hS h0 (Fin.zero_le i)
|
||||
|
||||
include hS in
|
||||
lemma opposite_signs_eq_neg {i j : Fin n.succ} (hi : S i ≤ 0) (hj : 0 ≤ S j) : S i = - S j := by
|
||||
have hSS := hS.1 i j
|
||||
rw [sq_eq_sq_iff_eq_or_eq_neg] at hSS
|
||||
|
|
@ -83,6 +88,7 @@ lemma opposite_signs_eq_neg {i j : Fin n.succ} (hi : S i ≤ 0) (hj : 0 ≤ S j)
|
|||
linarith
|
||||
· exact h
|
||||
|
||||
include hS in
|
||||
lemma is_zero (h0 : S (0 : Fin n.succ) = 0) : S = 0 := by
|
||||
funext i
|
||||
have ht := hS.1 i (0 : Fin n.succ)
|
||||
|
|
@ -96,9 +102,11 @@ is defined as a element of `k ∈ Fin n` such that `S k.castSucc` and `S k.succ`
|
|||
@[simp]
|
||||
def Boundary (S : (PureU1 n.succ).Charges) (k : Fin n) : Prop := S k.castSucc < 0 ∧ 0 < S k.succ
|
||||
|
||||
include hS in
|
||||
lemma boundary_castSucc {k : Fin n} (hk : Boundary S k) : S k.castSucc = S (0 : Fin n.succ) :=
|
||||
(lt_eq hS (le_of_lt hk.left) (Fin.zero_le k.castSucc : 0 ≤ k.castSucc)).symm
|
||||
|
||||
include hS in
|
||||
lemma boundary_succ {k : Fin n} (hk : Boundary S k) : S k.succ = - S (0 : Fin n.succ) := by
|
||||
have hn := boundary_castSucc hS hk
|
||||
rw [opposite_signs_eq_neg hS (le_of_lt hk.left) (le_of_lt hk.right)] at hn
|
||||
|
|
@ -115,6 +123,7 @@ lemma boundary_accGrav' (k : Fin n) : accGrav n.succ S =
|
|||
simp only [Fin.val_succ, mem_univ, RelIso.coe_fn_toEquiv]
|
||||
· exact fun _ _ => rfl
|
||||
|
||||
include hS in
|
||||
lemma boundary_accGrav'' (k : Fin n) (hk : Boundary S k) :
|
||||
accGrav n.succ S = (2 * ↑↑k + 1 - ↑n) * S (0 : Fin n.succ) := by
|
||||
rw [boundary_accGrav' k]
|
||||
|
|
@ -136,6 +145,7 @@ lemma boundary_accGrav'' (k : Fin n) (hk : Boundary S k) :
|
|||
def HasBoundary (S : (PureU1 n.succ).Charges) : Prop :=
|
||||
∃ (k : Fin n), Boundary S k
|
||||
|
||||
include hS in
|
||||
lemma not_hasBoundary_zero_le (hnot : ¬ (HasBoundary S)) (h0 : S (0 : Fin n.succ) < 0) :
|
||||
∀ i, S (0 : Fin n.succ) = S i := by
|
||||
intro ⟨i, hi⟩
|
||||
|
|
@ -148,6 +158,7 @@ lemma not_hasBoundary_zero_le (hnot : ¬ (HasBoundary S)) (h0 : S (0 : Fin n.suc
|
|||
erw [← hii] at hnott
|
||||
exact (val_le_zero hS (hnott h0)).symm
|
||||
|
||||
include hS in
|
||||
lemma not_hasBoundry_zero (hnot : ¬ (HasBoundary S)) (i : Fin n.succ) :
|
||||
S (0 : Fin n.succ) = S i := by
|
||||
by_cases hi : S (0 : Fin n.succ) < 0
|
||||
|
|
@ -155,10 +166,12 @@ lemma not_hasBoundry_zero (hnot : ¬ (HasBoundary S)) (i : Fin n.succ) :
|
|||
· simp at hi
|
||||
exact zero_gt hS hi i
|
||||
|
||||
include hS in
|
||||
lemma not_hasBoundary_grav (hnot : ¬ (HasBoundary S)) :
|
||||
accGrav n.succ S = n.succ * S (0 : Fin n.succ) := by
|
||||
simp [accGrav, ← not_hasBoundry_zero hS hnot]
|
||||
|
||||
include hA in
|
||||
lemma AFL_hasBoundary (h : A.val (0 : Fin n.succ) ≠ 0) : HasBoundary A.val := by
|
||||
by_contra hn
|
||||
have h0 := not_hasBoundary_grav hA hn
|
||||
|
|
|
|||
|
|
@ -125,7 +125,7 @@ theorem generic_case {S : (PureU1 (2 * n.succ)).Sols} (h : GenericCase S) :
|
|||
rw [parameterizationAsLinear_val]
|
||||
change S.val = _ • (_ • P g + _• P! f)
|
||||
rw [anomalyFree_param _ _ hS]
|
||||
rw [neg_neg, ← smul_add, smul_smul, inv_mul_cancel, one_smul]
|
||||
rw [neg_neg, ← smul_add, smul_smul, inv_mul_cancel₀, one_smul]
|
||||
· exact hS
|
||||
· have h := h g f hS
|
||||
rw [anomalyFree_param _ _ hS] at h
|
||||
|
|
|
|||
|
|
@ -126,7 +126,7 @@ theorem generic_case {S : (PureU1 (2 * n.succ + 1)).Sols} (h : GenericCase S) :
|
|||
rw [parameterizationAsLinear_val]
|
||||
change S.val = _ • (_ • P g + _• P! f)
|
||||
rw [anomalyFree_param _ _ hS]
|
||||
rw [neg_neg, ← smul_add, smul_smul, inv_mul_cancel, one_smul]
|
||||
rw [neg_neg, ← smul_add, smul_smul, inv_mul_cancel₀, one_smul]
|
||||
· exact hS
|
||||
· have h := h g f hS
|
||||
rw [anomalyFree_param _ _ hS] at h
|
||||
|
|
|
|||
|
|
@ -107,7 +107,7 @@ lemma cubic_zero_E'_zero (S : linearParameters) (hc : accCube (S.asCharges) = 0)
|
|||
rw [h1] at hc
|
||||
simp at hc
|
||||
cases' hc with hc hc
|
||||
· have h2 := (add_eq_zero_iff' (by nlinarith) (sq_nonneg S.Y)).mp hc
|
||||
· have h2 := (add_eq_zero_iff_of_nonneg (by nlinarith) (sq_nonneg S.Y)).mp hc
|
||||
simp at h2
|
||||
exact h2.1
|
||||
· exact hc
|
||||
|
|
|
|||
|
|
@ -72,7 +72,7 @@ lemma genericToQuad_on_quad (S : (PlusU1 n).QuadSols) :
|
|||
|
||||
lemma genericToQuad_neq_zero (S : (PlusU1 n).QuadSols) (h : α₁ C S.1 ≠ 0) :
|
||||
(α₁ C S.1)⁻¹ • genericToQuad C S.1 = S := by
|
||||
rw [genericToQuad_on_quad, smul_smul, inv_mul_cancel h, one_smul]
|
||||
rw [genericToQuad_on_quad, smul_smul, Rat.inv_mul_cancel _ h, one_smul]
|
||||
|
||||
/-- The construction of a `QuadSol` from a `LinSols` in the special case when `α₁ C S = 0` and
|
||||
`α₂ S = 0`. -/
|
||||
|
|
|
|||
|
|
@ -64,7 +64,7 @@ lemma generic_on_AF (S : (PlusU1 n).Sols) : generic S.1 = (α₁ S.1) • S := b
|
|||
|
||||
lemma generic_on_AF_α₁_ne_zero (S : (PlusU1 n).Sols) (h : α₁ S.1 ≠ 0) :
|
||||
(α₁ S.1)⁻¹ • generic S.1 = S := by
|
||||
rw [generic_on_AF, smul_smul, inv_mul_cancel h, one_smul]
|
||||
rw [generic_on_AF, smul_smul, inv_mul_cancel₀ h, one_smul]
|
||||
|
||||
/-- The construction of a `Sol` from a `QuadSol` in the case when `α₁ S = 0` and `α₂ S = 0`. -/
|
||||
def special (S : (PlusU1 n).QuadSols) (a b : ℚ) (h1 : α₁ S = 0) (h2 : α₂ S = 0) :
|
||||
|
|
|
|||
|
|
@ -67,7 +67,7 @@ def phaseShift (a b c : ℝ) : unitaryGroup (Fin 3) ℂ :=
|
|||
rw [mem_unitaryGroup_iff]
|
||||
change _ * (phaseShiftMatrix a b c)ᴴ = 1
|
||||
rw [phaseShiftMatrix_star, phaseShiftMatrix_mul, ← phaseShiftMatrix_one]
|
||||
simp only [phaseShiftMatrix, add_right_neg, ofReal_zero, mul_zero, exp_zero]⟩
|
||||
simp only [phaseShiftMatrix, add_neg_cancel, ofReal_zero, mul_zero, exp_zero]⟩
|
||||
|
||||
lemma phaseShift_coe_matrix (a b c : ℝ) : ↑(phaseShift a b c) = phaseShiftMatrix a b c := rfl
|
||||
|
||||
|
|
@ -93,7 +93,7 @@ lemma phaseShiftRelation_symm {U V : unitaryGroup (Fin 3) ℂ} :
|
|||
simp only [Submonoid.coe_mul, phaseShift_coe_matrix, ofReal_neg, mul_neg]
|
||||
rw [phaseShiftMatrix_mul]
|
||||
repeat rw [← mul_assoc]
|
||||
simp only [phaseShiftMatrix_mul, add_left_neg, phaseShiftMatrix_one, one_mul, add_right_neg,
|
||||
simp only [phaseShiftMatrix_mul, neg_add_cancel, phaseShiftMatrix_one, one_mul, add_neg_cancel,
|
||||
mul_one]
|
||||
|
||||
lemma phaseShiftRelation_trans {U V W : unitaryGroup (Fin 3) ℂ} :
|
||||
|
|
|
|||
|
|
@ -73,12 +73,12 @@ lemma ud_us_neq_zero_iff_ub_neq_one (V : CKMMatrix) :
|
|||
refine Iff.intro (fun h h1 => ?_) (fun h => ?_)
|
||||
· rw [h1] at h2
|
||||
simp at h2
|
||||
rw [add_eq_zero_iff' (sq_nonneg _) (sq_nonneg _)] at h2
|
||||
rw [add_eq_zero_iff_of_nonneg (sq_nonneg _) (sq_nonneg _)] at h2
|
||||
simp_all
|
||||
· by_contra hn
|
||||
rw [not_or] at hn
|
||||
simp_all only [ne_eq, Decidable.not_not, map_zero, OfNat.ofNat_ne_zero, not_false_eq_true,
|
||||
zero_pow, add_zero, zero_add, sq_eq_one_iff, false_or, neg_eq_self_iff, one_ne_zero]
|
||||
zero_pow, add_zero, zero_add, sq_eq_one_iff, false_or]
|
||||
have h1 := Complex.abs.nonneg [V]ub
|
||||
rw [h2] at h1
|
||||
refine (?_ : ¬ 0 ≤ (-1 : ℝ)) h1
|
||||
|
|
@ -290,7 +290,7 @@ lemma cb_eq_zero_of_ud_us_zero {V : CKMMatrix} (h : [V]ud = 0 ∧ [V]us = 0) :
|
|||
simp [h] at h1
|
||||
rw [add_assoc] at h1
|
||||
simp at h1
|
||||
rw [add_eq_zero_iff' (sq_nonneg _) (sq_nonneg _)] at h1
|
||||
rw [add_eq_zero_iff_of_nonneg (sq_nonneg _) (sq_nonneg _)] at h1
|
||||
simp at h1
|
||||
exact h1.1
|
||||
|
||||
|
|
@ -298,12 +298,12 @@ lemma cs_of_ud_us_zero {V : CKMMatrix} (ha : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) :
|
|||
VcsAbs ⟦V⟧ = √(1 - VcdAbs ⟦V⟧ ^ 2) := by
|
||||
have h1 := snd_row_normalized_abs V
|
||||
symm
|
||||
rw [Real.sqrt_eq_iff_sq_eq]
|
||||
rw [Real.sqrt_eq_iff_eq_sq]
|
||||
· simp [not_or] at ha
|
||||
rw [cb_eq_zero_of_ud_us_zero ha] at h1
|
||||
simp at h1
|
||||
simp [VAbs]
|
||||
linear_combination h1
|
||||
simp only [VcdAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk, VcsAbs]
|
||||
linear_combination ← h1
|
||||
· simp only [VcdAbs, Fin.isValue, sub_nonneg, sq_le_one_iff_abs_le_one]
|
||||
rw [@abs_le]
|
||||
have h1 := VAbs_leq_one 1 0 ⟦V⟧
|
||||
|
|
@ -325,13 +325,13 @@ lemma cb_tb_neq_zero_iff_ub_neq_one (V : CKMMatrix) :
|
|||
simp at h2
|
||||
have h2 : Complex.abs (V.1 1 2) ^ 2 + Complex.abs (V.1 2 2) ^ 2 = 0 := by
|
||||
linear_combination h2
|
||||
rw [add_eq_zero_iff' (sq_nonneg _) (sq_nonneg _)] at h2
|
||||
rw [add_eq_zero_iff_of_nonneg (sq_nonneg _) (sq_nonneg _)] at h2
|
||||
simp_all
|
||||
· by_contra hn
|
||||
rw [not_or] at hn
|
||||
simp at hn
|
||||
simp_all only [map_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero,
|
||||
sq_eq_one_iff, false_or, neg_eq_self_iff, one_ne_zero]
|
||||
sq_eq_one_iff, false_or, one_ne_zero]
|
||||
have h1 := Complex.abs.nonneg [V]ub
|
||||
rw [h2] at h1
|
||||
have h2 : ¬ 0 ≤ (-1 : ℝ) := by simp
|
||||
|
|
|
|||
|
|
@ -218,7 +218,7 @@ lemma cRow_cross_tRow_eq_uRow (V : CKMMatrix) :
|
|||
simp at h2
|
||||
cases' h2 with h2 h2
|
||||
· have hx : [V]u = (g 0)⁻¹ • (conj ([V]c) ×₃ conj ([V]t)) := by
|
||||
rw [← hg, smul_smul, inv_mul_cancel, one_smul]
|
||||
rw [← hg, smul_smul, inv_mul_cancel₀, one_smul]
|
||||
by_contra hn
|
||||
simp [hn] at h2
|
||||
have hg2 : Complex.abs (g 0)⁻¹ = 1 := by
|
||||
|
|
@ -270,7 +270,7 @@ lemma uRow_cross_cRow_eq_tRow (V : CKMMatrix) :
|
|||
have h4 : (0 : ℝ) < 1 := by norm_num
|
||||
exact False.elim (lt_iff_not_le.mp h4 h3)
|
||||
· have hx : [V]t = (g 2)⁻¹ • (conj ([V]u) ×₃ conj ([V]c)) := by
|
||||
rw [← hg, @smul_smul, inv_mul_cancel, one_smul]
|
||||
rw [← hg, @smul_smul, inv_mul_cancel₀, one_smul]
|
||||
by_contra hn
|
||||
simp [hn] at h2
|
||||
have hg2 : Complex.abs (g 2)⁻¹ = 1 := by
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ open Matrix
|
|||
/-- The group of `3×3` real matrices with determinant 1 and `A * Aᵀ = 1`. -/
|
||||
def SO3 : Type := {A : Matrix (Fin 3) (Fin 3) ℝ // A.det = 1 ∧ A * Aᵀ = 1}
|
||||
|
||||
@[simps mul_coe one_coe inv div]
|
||||
@[simps! mul_coe one_coe inv div]
|
||||
instance SO3Group : Group SO3 where
|
||||
mul A B := ⟨A.1 * B.1,
|
||||
by
|
||||
|
|
@ -31,7 +31,7 @@ instance SO3Group : Group SO3 where
|
|||
one_mul A := Subtype.eq (Matrix.one_mul A.1)
|
||||
mul_one A := Subtype.eq (Matrix.mul_one A.1)
|
||||
inv A := ⟨A.1ᵀ, by simp [A.2], by simp [mul_eq_one_comm.mpr A.2.2]⟩
|
||||
mul_left_inv A := Subtype.eq (mul_eq_one_comm.mpr A.2.2)
|
||||
inv_mul_cancel A := Subtype.eq (mul_eq_one_comm.mpr A.2.2)
|
||||
|
||||
/-- Notation for the group `SO3`. -/
|
||||
scoped[GroupTheory] notation (name := SO3_notation) "SO(3)" => SO3
|
||||
|
|
@ -123,7 +123,7 @@ lemma det_minus_id (A : SO(3)) : det (A.1 - 1) = 0 := by
|
|||
_ = det (- (A.1 - 1)) := by simp
|
||||
_ = (- 1) ^ 3 * det (A.1 - 1) := by simp only [det_neg, Fintype.card_fin, neg_mul, one_mul]
|
||||
_ = - det (A.1 - 1) := by simp [pow_three]
|
||||
simpa using h1
|
||||
exact CharZero.eq_neg_self_iff.mp h1
|
||||
|
||||
@[simp]
|
||||
lemma det_id_minus (A : SO(3)) : det (1 - A.1) = 0 := by
|
||||
|
|
|
|||
|
|
@ -47,7 +47,9 @@ instance : ChartedSpace SpaceTime SpaceTime := chartedSpaceSelf SpaceTime
|
|||
def stdBasis : Basis (Fin 4) ℝ SpaceTime := Pi.basisFun ℝ (Fin 4)
|
||||
|
||||
lemma stdBasis_apply (μ ν : Fin 4) : stdBasis μ ν = if μ = ν then 1 else 0 := by
|
||||
erw [stdBasis, Pi.basisFun_apply, LinearMap.stdBasis_apply']
|
||||
erw [stdBasis, Pi.basisFun_apply, Pi.single_apply]
|
||||
refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
|
||||
exact Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a)
|
||||
|
||||
lemma stdBasis_not_eq {μ ν : Fin 4} (h : μ ≠ ν) : stdBasis μ ν = 0 := by
|
||||
rw [stdBasis_apply]
|
||||
|
|
|
|||
|
|
@ -63,8 +63,11 @@ lemma diag_comp (Λ : lorentzAlgebra) (μ : Fin 1 ⊕ Fin 3) : Λ.1 μ μ = 0 :=
|
|||
have h := congrArg (fun M ↦ M μ μ) $ mem_iff.mp Λ.2
|
||||
simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mul_diagonal,
|
||||
transpose_apply, diagonal_neg, diagonal_mul, neg_mul] at h
|
||||
rcases μ with μ | μ <;>
|
||||
simpa using h
|
||||
rcases μ with μ | μ
|
||||
· simp only [Sum.elim_inl, mul_one, one_mul] at h
|
||||
exact eq_zero_of_neg_eq (id (Eq.symm h))
|
||||
· simp only [Sum.elim_inr, mul_neg, mul_one, neg_mul, one_mul, neg_neg] at h
|
||||
exact eq_zero_of_neg_eq h
|
||||
|
||||
lemma time_comps (Λ : lorentzAlgebra) (i : Fin 3) :
|
||||
Λ.1 (Sum.inr i) (Sum.inl 0) = Λ.1 (Sum.inl 0) (Sum.inr i) := by
|
||||
|
|
|
|||
|
|
@ -116,7 +116,7 @@ end LorentzGroup
|
|||
|
||||
-/
|
||||
|
||||
@[simps mul_coe one_coe inv div]
|
||||
@[simps! mul_coe one_coe inv div]
|
||||
instance lorentzGroupIsGroup : Group (LorentzGroup d) where
|
||||
mul A B := ⟨A.1 * B.1, LorentzGroup.mem_mul A.2 B.2⟩
|
||||
mul_assoc A B C := Subtype.eq (Matrix.mul_assoc A.1 B.1 C.1)
|
||||
|
|
@ -124,7 +124,7 @@ instance lorentzGroupIsGroup : Group (LorentzGroup d) where
|
|||
one_mul A := Subtype.eq (Matrix.one_mul A.1)
|
||||
mul_one A := Subtype.eq (Matrix.mul_one A.1)
|
||||
inv A := ⟨minkowskiMetric.dual A.1, LorentzGroup.dual_mem A.2⟩
|
||||
mul_left_inv A := Subtype.eq (LorentzGroup.mem_iff_dual_mul_self.mp A.2)
|
||||
inv_mul_cancel A := Subtype.eq (LorentzGroup.mem_iff_dual_mul_self.mp A.2)
|
||||
|
||||
/-- `LorentzGroup` has the subtype topology. -/
|
||||
instance : TopologicalSpace (LorentzGroup d) := instTopologicalSpaceSubtype
|
||||
|
|
@ -142,7 +142,7 @@ lemma subtype_inv_mul : (Subtype.val Λ)⁻¹ * (Subtype.val Λ) = 1 := by
|
|||
trans Subtype.val (Λ⁻¹ * Λ)
|
||||
· rw [← coe_inv]
|
||||
rfl
|
||||
· rw [inv_mul_self Λ]
|
||||
· rw [inv_mul_cancel Λ]
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
|
|
@ -150,7 +150,7 @@ lemma subtype_mul_inv : (Subtype.val Λ) * (Subtype.val Λ)⁻¹ = 1 := by
|
|||
trans Subtype.val (Λ * Λ⁻¹)
|
||||
· rw [← coe_inv]
|
||||
rfl
|
||||
· rw [mul_inv_self Λ]
|
||||
· rw [mul_inv_cancel Λ]
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
|
|
@ -275,7 +275,8 @@ def timeComp (Λ : LorentzGroup d) : ℝ := Λ.1 (Sum.inl 0) (Sum.inl 0)
|
|||
|
||||
lemma timeComp_eq_toNormOneLorentzVector : timeComp Λ = (toNormOneLorentzVector Λ).1.time := by
|
||||
simp only [time, toNormOneLorentzVector, timeVec, Fin.isValue, timeComp]
|
||||
erw [Pi.basisFun_apply, mulVec_stdBasis]
|
||||
erw [Pi.basisFun_apply, Matrix.mulVec_single_one]
|
||||
rfl
|
||||
|
||||
lemma timeComp_mul (Λ Λ' : LorentzGroup d) : timeComp (Λ * Λ') =
|
||||
⟪toNormOneLorentzVector (transpose Λ), (toNormOneLorentzVector Λ').1.spaceReflection⟫ₘ := by
|
||||
|
|
@ -283,7 +284,7 @@ lemma timeComp_mul (Λ Λ' : LorentzGroup d) : timeComp (Λ * Λ') =
|
|||
Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton, toNormOneLorentzVector,
|
||||
transpose, timeVec, right_spaceReflection, time, space, PiLp.inner_apply, Function.comp_apply,
|
||||
RCLike.inner_apply, conj_trivial]
|
||||
erw [Pi.basisFun_apply, mulVec_stdBasis]
|
||||
erw [Pi.basisFun_apply, Matrix.mulVec_single_one]
|
||||
simp
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -43,7 +43,7 @@ lemma IsOrthochronous_iff_ge_one :
|
|||
rw [IsOrthochronous_iff_futurePointing, NormOneLorentzVector.FuturePointing.mem_iff,
|
||||
NormOneLorentzVector.time_pos_iff]
|
||||
simp only [time, toNormOneLorentzVector, timeVec, Fin.isValue]
|
||||
erw [Pi.basisFun_apply, mulVec_stdBasis]
|
||||
erw [Pi.basisFun_apply, Matrix.mulVec_single_one]
|
||||
rfl
|
||||
|
||||
lemma not_orthochronous_iff_le_neg_one :
|
||||
|
|
@ -51,7 +51,8 @@ lemma not_orthochronous_iff_le_neg_one :
|
|||
rw [timeComp, IsOrthochronous_iff_futurePointing, NormOneLorentzVector.FuturePointing.not_mem_iff,
|
||||
NormOneLorentzVector.time_nonpos_iff]
|
||||
simp only [time, toNormOneLorentzVector, timeVec, Fin.isValue]
|
||||
erw [Pi.basisFun_apply, mulVec_stdBasis]
|
||||
erw [Pi.basisFun_apply, Matrix.mulVec_single_one]
|
||||
rfl
|
||||
|
||||
lemma not_orthochronous_iff_le_zero :
|
||||
¬ IsOrthochronous Λ ↔ timeComp Λ ≤ 0 := by
|
||||
|
|
@ -119,8 +120,11 @@ lemma orthchroMap_IsOrthochronous {Λ : LorentzGroup d} (h : IsOrthochronous Λ)
|
|||
|
||||
lemma orthchroMap_not_IsOrthochronous {Λ : LorentzGroup d} (h : ¬ IsOrthochronous Λ) :
|
||||
orthchroMap Λ = Additive.toMul (1 : ZMod 2) := by
|
||||
simp [orthchroMap, orthchroMapReal_on_not_IsOrthochronous h]
|
||||
rfl
|
||||
simp only [orthchroMap, ContinuousMap.comp_apply, ContinuousMap.coe_mk,
|
||||
orthchroMapReal_on_not_IsOrthochronous h, coeForℤ₂_apply, Subtype.mk.injEq, Nat.reduceAdd]
|
||||
rw [if_neg]
|
||||
· rfl
|
||||
· linarith
|
||||
|
||||
lemma mul_othchron_of_othchron_othchron {Λ Λ' : LorentzGroup d} (h : IsOrthochronous Λ)
|
||||
(h' : IsOrthochronous Λ') : IsOrthochronous (Λ * Λ') := by
|
||||
|
|
|
|||
|
|
@ -32,6 +32,7 @@ lemma det_eq_one_or_neg_one (Λ : 𝓛 d) : Λ.1.det = 1 ∨ Λ.1.det = -1 := by
|
|||
|
||||
local notation "ℤ₂" => Multiplicative (ZMod 2)
|
||||
|
||||
|
||||
instance : TopologicalSpace ℤ₂ := instTopologicalSpaceFin
|
||||
|
||||
instance : DiscreteTopology ℤ₂ := by
|
||||
|
|
@ -56,34 +57,87 @@ def detContinuous : C(𝓛 d, ℤ₂) :=
|
|||
Continuous.comp' (continuous_iff_le_induced.mpr fun U a => a) continuous_id'
|
||||
}
|
||||
|
||||
lemma detContinuous_eq_one (Λ : LorentzGroup d) :
|
||||
detContinuous Λ = Additive.toMul 0 ↔ Λ.1.det = 1 := by
|
||||
simp only [detContinuous, ContinuousMap.comp_apply, ContinuousMap.coe_mk, coeForℤ₂_apply,
|
||||
Subtype.mk.injEq, ite_eq_left_iff, toMul_eq_one]
|
||||
simp only [toMul_zero, ite_eq_left_iff, toMul_eq_one]
|
||||
refine Iff.intro (fun h => ?_) (fun h => ?_)
|
||||
· by_contra hn
|
||||
have h' := h hn
|
||||
change (1 : Fin 2) = (0 : Fin 2) at h'
|
||||
simp only [Fin.isValue, one_ne_zero] at h'
|
||||
· intro h'
|
||||
exact False.elim (h' h)
|
||||
|
||||
lemma detContinuous_eq_zero (Λ : LorentzGroup d) :
|
||||
detContinuous Λ = Additive.toMul (1 : ZMod 2) ↔ Λ.1.det = - 1 := by
|
||||
simp only [detContinuous, ContinuousMap.comp_apply, ContinuousMap.coe_mk, coeForℤ₂_apply,
|
||||
Subtype.mk.injEq, Nat.reduceAdd]
|
||||
refine Iff.intro (fun h => ?_) (fun h => ?_)
|
||||
· by_contra hn
|
||||
rw [if_pos] at h
|
||||
· change (0 : Fin 2) = (1 : Fin 2) at h
|
||||
simp only [Fin.isValue, zero_ne_one] at h
|
||||
· cases' det_eq_one_or_neg_one Λ with h2 h2
|
||||
· simp_all only [ite_true]
|
||||
· simp_all only [not_true_eq_false]
|
||||
· rw [if_neg]
|
||||
· rfl
|
||||
· cases' det_eq_one_or_neg_one Λ with h2 h2
|
||||
· rw [h]
|
||||
linarith
|
||||
· linarith
|
||||
|
||||
lemma detContinuous_eq_iff_det_eq (Λ Λ' : LorentzGroup d) :
|
||||
detContinuous Λ = detContinuous Λ' ↔ Λ.1.det = Λ'.1.det := by
|
||||
refine Iff.intro (fun h => ?_) (fun h => ?_)
|
||||
· simp only [detContinuous, ContinuousMap.comp_apply, ContinuousMap.coe_mk, coeForℤ₂_apply,
|
||||
Subtype.mk.injEq] at h
|
||||
cases' det_eq_one_or_neg_one Λ with h1 h1
|
||||
<;> cases' det_eq_one_or_neg_one Λ' with h2 h2
|
||||
<;> simp_all [h1, h2, h]
|
||||
· rw [← toMul_zero, @Equiv.apply_eq_iff_eq] at h
|
||||
· change (0 : Fin 2) = (1 : Fin 2) at h
|
||||
simp only [Fin.isValue, zero_ne_one] at h
|
||||
· change (1 : Fin 2) = (0 : Fin 2) at h
|
||||
simp only [Fin.isValue, one_ne_zero] at h
|
||||
· simp [detContinuous, h]
|
||||
cases' det_eq_one_or_neg_one Λ with h1 h1
|
||||
· rw [h1, (detContinuous_eq_one Λ).mpr h1]
|
||||
cases' det_eq_one_or_neg_one Λ' with h2 h2
|
||||
· rw [h2, (detContinuous_eq_one Λ').mpr h2]
|
||||
simp only [toMul_zero]
|
||||
· rw [h2, (detContinuous_eq_zero Λ').mpr h2]
|
||||
erw [Additive.toMul.apply_eq_iff_eq]
|
||||
change (0 : Fin 2) = (1 : Fin 2) ↔ _
|
||||
simp only [Fin.isValue, zero_ne_one, false_iff]
|
||||
linarith
|
||||
· rw [h1, (detContinuous_eq_zero Λ).mpr h1]
|
||||
cases' det_eq_one_or_neg_one Λ' with h2 h2
|
||||
· rw [h2, (detContinuous_eq_one Λ').mpr h2]
|
||||
erw [Additive.toMul.apply_eq_iff_eq]
|
||||
change (1 : Fin 2) = (0 : Fin 2) ↔ _
|
||||
simp only [Fin.isValue, one_ne_zero, false_iff]
|
||||
linarith
|
||||
· rw [h2, (detContinuous_eq_zero Λ').mpr h2]
|
||||
simp only [Nat.reduceAdd]
|
||||
|
||||
/-- The representation taking a Lorentz matrix to its determinant. -/
|
||||
@[simps!]
|
||||
def detRep : 𝓛 d →* ℤ₂ where
|
||||
toFun Λ := detContinuous Λ
|
||||
map_one' := by
|
||||
simp [detContinuous, lorentzGroupIsGroup]
|
||||
simp only [detContinuous, ContinuousMap.comp_apply, ContinuousMap.coe_mk,
|
||||
lorentzGroupIsGroup_one_coe, det_one, coeForℤ₂_apply, ↓reduceIte]
|
||||
map_mul' Λ1 Λ2 := by
|
||||
simp only [Submonoid.coe_mul, Subgroup.coe_toSubmonoid, Units.val_mul, det_mul, toMul_zero,
|
||||
mul_ite, mul_one, ite_mul, one_mul]
|
||||
cases' det_eq_one_or_neg_one Λ1 with h1 h1
|
||||
<;> cases' det_eq_one_or_neg_one Λ2 with h2 h2
|
||||
<;> simp [h1, h2, detContinuous]
|
||||
rfl
|
||||
· rw [(detContinuous_eq_one Λ1).mpr h1]
|
||||
cases' det_eq_one_or_neg_one Λ2 with h2 h2
|
||||
· rw [(detContinuous_eq_one Λ2).mpr h2]
|
||||
apply (detContinuous_eq_one _).mpr
|
||||
simp only [lorentzGroupIsGroup_mul_coe, det_mul, h1, h2, mul_one]
|
||||
· rw [(detContinuous_eq_zero Λ2).mpr h2]
|
||||
apply (detContinuous_eq_zero _).mpr
|
||||
simp only [lorentzGroupIsGroup_mul_coe, det_mul, h1, h2, mul_neg, mul_one]
|
||||
· rw [(detContinuous_eq_zero Λ1).mpr h1]
|
||||
cases' det_eq_one_or_neg_one Λ2 with h2 h2
|
||||
· rw [(detContinuous_eq_one Λ2).mpr h2]
|
||||
apply (detContinuous_eq_zero _).mpr
|
||||
simp only [lorentzGroupIsGroup_mul_coe, det_mul, h1, h2, mul_one]
|
||||
· rw [(detContinuous_eq_zero Λ2).mpr h2]
|
||||
apply (detContinuous_eq_one _).mpr
|
||||
simp only [lorentzGroupIsGroup_mul_coe, det_mul, h1, h2, mul_neg, mul_one, neg_neg]
|
||||
|
||||
lemma detRep_continuous : Continuous (@detRep d) := detContinuous.2
|
||||
|
||||
|
|
|
|||
|
|
@ -54,7 +54,7 @@ def colorRel (μ ν : 𝓒.Color) : Prop := μ = ν ∨ μ = 𝓒.τ ν
|
|||
|
||||
instance : Decidable (colorRel 𝓒 μ ν) :=
|
||||
Or.decidable
|
||||
|
||||
omit [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
|
||||
/-- An equivalence relation on colors which is true if the two colors are equal or are duals. -/
|
||||
lemma colorRel_equivalence : Equivalence 𝓒.colorRel where
|
||||
refl := by
|
||||
|
|
@ -122,6 +122,8 @@ namespace MapIso
|
|||
variable {e : X ≃ Y} {e' : Y ≃ Z} {cX : ColorMap 𝓒 X} {cY : ColorMap 𝓒 Y} {cZ : ColorMap 𝓒 Z}
|
||||
variable {cX' : ColorMap 𝓒 X'} {cY' : ColorMap 𝓒 Y'}
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y][Fintype Z]
|
||||
[DecidableEq Z] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
|
||||
lemma symm (h : cX.MapIso e cY) : cY.MapIso e.symm cX := by
|
||||
rw [MapIso] at h
|
||||
exact (Equiv.eq_comp_symm e cY cX).mpr h.symm
|
||||
|
|
@ -129,12 +131,16 @@ lemma symm (h : cX.MapIso e cY) : cY.MapIso e.symm cX := by
|
|||
lemma symm' : cX.MapIso e cY ↔ cY.MapIso e.symm cX := by
|
||||
refine ⟨symm, symm⟩
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z]
|
||||
[Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
|
||||
lemma trans (h : cX.MapIso e cY) (h' : cY.MapIso e' cZ) :
|
||||
cX.MapIso (e.trans e') cZ:= by
|
||||
funext a
|
||||
subst h h'
|
||||
rfl
|
||||
|
||||
omit [Fintype Y'] [DecidableEq Y']
|
||||
|
||||
lemma sum {eX : X ≃ X'} {eY : Y ≃ Y'} (hX : cX.MapIso eX cX') (hY : cY.MapIso eY cY') :
|
||||
(cX.sum cY).MapIso (eX.sumCongr eY) (cX'.sum cY') := by
|
||||
funext x
|
||||
|
|
@ -274,6 +280,7 @@ def colorModuleCast (h : μ = ν) : 𝓣.ColorModule μ ≃ₗ[R] 𝓣.ColorModu
|
|||
left_inv x := Equiv.symm_apply_apply (Equiv.cast (congrArg 𝓣.ColorModule h)) x
|
||||
right_inv x := Equiv.apply_symm_apply (Equiv.cast (congrArg 𝓣.ColorModule h)) x
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] in
|
||||
lemma tensorProd_piTensorProd_ext {M : Type} [AddCommMonoid M] [Module R M]
|
||||
{f g : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY →ₗ[R] M}
|
||||
(h : ∀ p q, f (PiTensorProduct.tprod R p ⊗ₜ[R] PiTensorProduct.tprod R q)
|
||||
|
|
@ -307,10 +314,13 @@ def mapIso {c : 𝓣.ColorMap X} {d : 𝓣.ColorMap Y} (e : X ≃ Y) (h : c.MapI
|
|||
(PiTensorProduct.reindex R _ e) ≪≫ₗ
|
||||
(PiTensorProduct.congr (fun y => 𝓣.colorModuleCast (by rw [h]; simp)))
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] in
|
||||
lemma mapIso_ext {c : 𝓣.ColorMap X} {d : 𝓣.ColorMap Y} (e e' : X ≃ Y) (h : c.MapIso e d)
|
||||
(h' : c.MapIso e' d) (he : e = e') : 𝓣.mapIso e h = 𝓣.mapIso e' h' := by
|
||||
simp [he]
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype Z]
|
||||
[DecidableEq Z] in
|
||||
@[simp]
|
||||
lemma mapIso_trans (e : X ≃ Y) (e' : Y ≃ Z) (h : cX.MapIso e cY) (h' : cY.MapIso e' cZ) :
|
||||
(𝓣.mapIso e h ≪≫ₗ 𝓣.mapIso e' h') = 𝓣.mapIso (e.trans e') (h.trans h') := by
|
||||
|
|
@ -329,12 +339,16 @@ lemma mapIso_trans (e : X ≃ Y) (e' : Y ≃ Z) (h : cX.MapIso e cY) (h' : cY.Ma
|
|||
PiTensorProduct.congr_tprod, PiTensorProduct.reindex_tprod, PiTensorProduct.congr]
|
||||
simp [colorModuleCast]
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype Z]
|
||||
[DecidableEq Z] in
|
||||
@[simp]
|
||||
lemma mapIso_mapIso (e : X ≃ Y) (e' : Y ≃ Z) (h : cX.MapIso e cY) (h' : cY.MapIso e' cZ)
|
||||
(T : 𝓣.Tensor cX) :
|
||||
(𝓣.mapIso e' h') (𝓣.mapIso e h T) = 𝓣.mapIso (e.trans e') (h.trans h') T := by
|
||||
rw [← LinearEquiv.trans_apply, mapIso_trans]
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype Z]
|
||||
[DecidableEq Z] in
|
||||
@[simp]
|
||||
lemma mapIso_symm (e : X ≃ Y) (h : cX.MapIso e cY) :
|
||||
(𝓣.mapIso e h).symm = 𝓣.mapIso e.symm (h.symm) := by
|
||||
|
|
@ -360,6 +374,8 @@ lemma mapIso_symm (e : X ≃ Y) (h : cX.MapIso e cY) :
|
|||
apply cast_eq_iff_heq.mpr
|
||||
rw [Equiv.apply_symm_apply]
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype Z]
|
||||
[DecidableEq Z] in
|
||||
@[simp]
|
||||
lemma mapIso_refl : 𝓣.mapIso (Equiv.refl X) (rfl : cX = cX) = LinearEquiv.refl R _ := by
|
||||
refine LinearEquiv.toLinearMap_inj.mp ?_
|
||||
|
|
@ -374,6 +390,7 @@ lemma mapIso_refl : 𝓣.mapIso (Equiv.refl X) (rfl : cX = cX) = LinearEquiv.ref
|
|||
rw [PiTensorProduct.congr_tprod]
|
||||
rfl
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] in
|
||||
@[simp]
|
||||
lemma mapIso_tprod {c : 𝓣.ColorMap X} {d : 𝓣.ColorMap Y} (e : X ≃ Y) (h : c.MapIso e d)
|
||||
(f : (i : X) → 𝓣.ColorModule (c i)) : (𝓣.mapIso e h) (PiTensorProduct.tprod R f) =
|
||||
|
|
@ -404,6 +421,7 @@ def elimPureTensor (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor cY) : 𝓣.Pure
|
|||
| Sum.inl x => p x
|
||||
| Sum.inr x => q x
|
||||
|
||||
omit [Fintype X] [Fintype Y] in
|
||||
@[simp]
|
||||
lemma elimPureTensor_update_right (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor cY)
|
||||
(y : Y) (r : 𝓣.ColorModule (cY y)) : 𝓣.elimPureTensor p (Function.update q y r) =
|
||||
|
|
@ -420,6 +438,7 @@ lemma elimPureTensor_update_right (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor
|
|||
simp_all only
|
||||
· rfl
|
||||
|
||||
omit [Fintype X] [Fintype Y] in
|
||||
@[simp]
|
||||
lemma elimPureTensor_update_left (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor cY)
|
||||
(x : X) (r : 𝓣.ColorModule (cX x)) : 𝓣.elimPureTensor (Function.update p x r) q =
|
||||
|
|
@ -444,6 +463,7 @@ def inlPureTensor (p : 𝓣.PureTensor (Sum.elim cX cY)) : 𝓣.PureTensor cX :=
|
|||
`𝓣.PureTensor cY`. -/
|
||||
def inrPureTensor (p : 𝓣.PureTensor (Sum.elim cX cY)) : 𝓣.PureTensor cY := fun y => p (Sum.inr y)
|
||||
|
||||
omit [Fintype X] [Fintype Y] [DecidableEq Y] in
|
||||
@[simp]
|
||||
lemma inlPureTensor_update_left [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (Sum.elim cX cY)) (x : X)
|
||||
(v1 : 𝓣.ColorModule (Sum.elim cX cY (Sum.inl x))) :
|
||||
|
|
@ -457,6 +477,7 @@ lemma inlPureTensor_update_left [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (Su
|
|||
rfl
|
||||
· rfl
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] in
|
||||
@[simp]
|
||||
lemma inrPureTensor_update_left [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (Sum.elim cX cY)) (x : X)
|
||||
(v1 : 𝓣.ColorModule (Sum.elim cX cY (Sum.inl x))) :
|
||||
|
|
@ -464,6 +485,7 @@ lemma inrPureTensor_update_left [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (Su
|
|||
funext x
|
||||
simp [inrPureTensor, Function.update]
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype Y] in
|
||||
@[simp]
|
||||
lemma inrPureTensor_update_right [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (Sum.elim cX cY)) (y : Y)
|
||||
(v1 : 𝓣.ColorModule (Sum.elim cX cY (Sum.inr y))) :
|
||||
|
|
@ -477,6 +499,7 @@ lemma inrPureTensor_update_right [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (S
|
|||
rfl
|
||||
· rfl
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] in
|
||||
@[simp]
|
||||
lemma inlPureTensor_update_right [DecidableEq (X ⊕ Y)] (f : 𝓣.PureTensor (Sum.elim cX cY)) (y : Y)
|
||||
(v1 : 𝓣.ColorModule (Sum.elim cX cY (Sum.inr y))) :
|
||||
|
|
@ -569,6 +592,7 @@ def tensoratorEquiv (c : X → 𝓣.Color) (d : Y → 𝓣.Color) :
|
|||
simp [elimPureTensorMulLin]
|
||||
rfl)
|
||||
|
||||
omit [Fintype X] [Fintype Y] in
|
||||
@[simp]
|
||||
lemma tensoratorEquiv_tmul_tprod (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor cY) :
|
||||
(𝓣.tensoratorEquiv cX cY) ((PiTensorProduct.tprod R) p ⊗ₜ[R] (PiTensorProduct.tprod R) q) =
|
||||
|
|
@ -577,6 +601,7 @@ lemma tensoratorEquiv_tmul_tprod (p : 𝓣.PureTensor cX) (q : 𝓣.PureTensor c
|
|||
lift.tmul, LinearMap.coe_mk, AddHom.coe_mk, PiTensorProduct.lift.tprod]
|
||||
exact PiTensorProduct.lift.tprod q
|
||||
|
||||
omit [Fintype X] [Fintype Y] in
|
||||
@[simp]
|
||||
lemma tensoratorEquiv_symm_tprod (f : 𝓣.PureTensor (Sum.elim cX cY)) :
|
||||
(𝓣.tensoratorEquiv cX cY).symm ((PiTensorProduct.tprod R) f) =
|
||||
|
|
@ -586,6 +611,7 @@ lemma tensoratorEquiv_symm_tprod (f : 𝓣.PureTensor (Sum.elim cX cY)) :
|
|||
change (PiTensorProduct.lift 𝓣.domCoprod) ((PiTensorProduct.tprod R) f) = _
|
||||
simp [domCoprod]
|
||||
|
||||
omit [Fintype X] [Fintype Y] [Fintype W] [Fintype Z] in
|
||||
@[simp]
|
||||
lemma tensoratorEquiv_mapIso (e' : Z ≃ Y) (e'' : W ≃ X)
|
||||
(h' : cZ.MapIso e' cY) (h'' : cW.MapIso e'' cX) :
|
||||
|
|
@ -604,6 +630,7 @@ lemma tensoratorEquiv_mapIso (e' : Z ≃ Y) (e'' : W ≃ X)
|
|||
| Sum.inl x => rfl
|
||||
| Sum.inr x => rfl
|
||||
|
||||
omit [Fintype X] [Fintype Y] [Fintype W] [Fintype Z] in
|
||||
@[simp]
|
||||
lemma tensoratorEquiv_mapIso_apply (e' : Z ≃ Y) (e'' : W ≃ X)
|
||||
(h' : cZ.MapIso e' cY) (h'' : cW.MapIso e'' cX)
|
||||
|
|
@ -617,6 +644,7 @@ lemma tensoratorEquiv_mapIso_apply (e' : Z ≃ Y) (e'' : W ≃ X)
|
|||
· rw [tensoratorEquiv_mapIso]
|
||||
rfl
|
||||
|
||||
omit [Fintype X] [Fintype Y] [Fintype W] [Fintype Z] in
|
||||
lemma tensoratorEquiv_mapIso_tmul (e' : Z ≃ Y) (e'' : W ≃ X)
|
||||
(h' : cZ.MapIso e' cY) (h'' : cW.MapIso e'' cX)
|
||||
(x : 𝓣.Tensor cW) (y : 𝓣.Tensor cZ) :
|
||||
|
|
@ -685,6 +713,7 @@ lemma contrDual_symm_contrRightAux_apply_tmul (h : ν = η)
|
|||
def isEmptyEquiv [IsEmpty X] : 𝓣.Tensor cX ≃ₗ[R] R :=
|
||||
PiTensorProduct.isEmptyEquiv X
|
||||
|
||||
omit [Fintype X] [DecidableEq X] in
|
||||
@[simp]
|
||||
lemma isEmptyEquiv_tprod [IsEmpty X] (f : 𝓣.PureTensor cX) :
|
||||
𝓣.isEmptyEquiv (PiTensorProduct.tprod R f) = 1 := by
|
||||
|
|
@ -716,6 +745,7 @@ def decompEmbedColorLeft (c : X → 𝓣.Color) (f : Y ↪ X) :
|
|||
def decompEmbedColorRight (c : X → 𝓣.Color) (f : Y ↪ X) : Y → 𝓣.Color :=
|
||||
(c ∘ (decompEmbedSet f).symm) ∘ Sum.inr
|
||||
|
||||
omit [DecidableEq Y] in
|
||||
lemma decompEmbed_cond (c : X → 𝓣.Color) (f : Y ↪ X) : c =
|
||||
(Sum.elim (𝓣.decompEmbedColorLeft c f) (𝓣.decompEmbedColorRight c f)) ∘ decompEmbedSet f := by
|
||||
simpa [decompEmbedColorLeft, decompEmbedColorRight] using (Equiv.comp_symm_eq _ _ _).mp rfl
|
||||
|
|
|
|||
|
|
@ -62,22 +62,32 @@ namespace ContrAll
|
|||
variable {e : X ≃ Y} {e' : Y ≃ Z} {cX : ColorMap 𝓒 X} {cY : ColorMap 𝓒 Y} {cZ : ColorMap 𝓒 Z}
|
||||
variable {cX' : ColorMap 𝓒 X'} {cY' : ColorMap 𝓒 Y'}
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
|
||||
[Fintype 𝓒.Color] [DecidableEq 𝓒.Color] in
|
||||
lemma toMapIso (h : cX.ContrAll e cY) : cX.MapIso e cY.dual := by
|
||||
subst h
|
||||
rfl
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
|
||||
[Fintype 𝓒.Color] [DecidableEq 𝓒.Color] in
|
||||
lemma symm (h : cX.ContrAll e cY) : cY.ContrAll e.symm cX := by
|
||||
subst h
|
||||
funext x
|
||||
simp only [Function.comp_apply, Equiv.apply_symm_apply]
|
||||
exact (𝓒.τ_involutive (cY x)).symm
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
|
||||
[Fintype 𝓒.Color] [DecidableEq 𝓒.Color] [Fintype Z]
|
||||
[DecidableEq Z] in
|
||||
lemma trans_mapIso {e : X ≃ Y} {e' : Z ≃ Y}
|
||||
(h : cX.ContrAll e cY) (h' : cZ.MapIso e' cY) : cX.ContrAll (e.trans e'.symm) cZ := by
|
||||
subst h h'
|
||||
funext x
|
||||
simp only [Function.comp_apply, Equiv.coe_trans, Equiv.apply_symm_apply]
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
|
||||
[Fintype 𝓒.Color] [DecidableEq 𝓒.Color] [Fintype Z]
|
||||
[DecidableEq Z] in
|
||||
lemma mapIso_trans {e : X ≃ Y} {e' : Z ≃ X}
|
||||
(h : cX.ContrAll e cY) (h' : cZ.MapIso e' cX) : cZ.ContrAll (e'.trans e) cY := by
|
||||
subst h h'
|
||||
|
|
@ -111,6 +121,9 @@ variable {e : (C ⊕ C) ⊕ P ≃ X} {e' : Y ≃ Z} {cX : ColorMap 𝓒 X} {cY :
|
|||
|
||||
variable {cX' : ColorMap 𝓒 X'} {cY' : ColorMap 𝓒 Y'}
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype C]
|
||||
[DecidableEq C] [Fintype P] [DecidableEq P]
|
||||
[Fintype 𝓒.Color] [DecidableEq 𝓒.Color] in
|
||||
lemma to_contrAll (h : cX.ContrCond e) :
|
||||
(cX.contrLeft e).ContrAll (Equiv.refl _) (cX.contrRight e) := h
|
||||
|
||||
|
|
@ -159,6 +172,7 @@ def pairProd : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cX2 →ₗ[R]
|
|||
PiTensorProduct.map₂ (fun x =>
|
||||
TensorProduct.mk R (𝓣.ColorModule (cX x)) (𝓣.ColorModule (cX2 x))))
|
||||
|
||||
omit [Fintype X] [DecidableEq X] in
|
||||
lemma pairProd_tmul_tprod_tprod (fx : (i : X) → 𝓣.ColorModule (cX i))
|
||||
(fx2 : (i : X) → 𝓣.ColorModule (cX2 i)) :
|
||||
𝓣.pairProd (PiTensorProduct.tprod R fx ⊗ₜ[R] PiTensorProduct.tprod R fx2) =
|
||||
|
|
@ -167,6 +181,7 @@ lemma pairProd_tmul_tprod_tprod (fx : (i : X) → 𝓣.ColorModule (cX i))
|
|||
erw [PiTensorProduct.map₂_tprod_tprod]
|
||||
rfl
|
||||
|
||||
omit [DecidableEq X] [DecidableEq Y]
|
||||
lemma mkPiAlgebra_equiv (e : X ≃ Y) :
|
||||
(PiTensorProduct.lift (MultilinearMap.mkPiAlgebra R X R)) =
|
||||
(PiTensorProduct.lift (MultilinearMap.mkPiAlgebra R Y R)) ∘ₗ
|
||||
|
|
@ -229,13 +244,16 @@ lemma contrAll'_mapIso (e : X ≃ Y) (h : cX.MapIso e cY) :
|
|||
refine fun x ↦
|
||||
PiTensorProduct.induction_on' x ?_ (by
|
||||
intro a b hx hy y
|
||||
simp [map_add, add_tmul, hx, hy])
|
||||
simp only [add_tmul, map_add, hx, LinearMap.coe_comp, Function.comp_apply, hy])
|
||||
intro rx fx
|
||||
refine fun y ↦
|
||||
PiTensorProduct.induction_on' y ?_ (by
|
||||
intro a b hx hy
|
||||
simp at hx hy
|
||||
simp [map_add, tmul_add, hx, hy])
|
||||
simp only [PiTensorProduct.tprodCoeff_eq_smul_tprod, LinearMap.coe_comp, LinearEquiv.coe_coe,
|
||||
Function.comp_apply, congr_tmul, map_smul, mapIso_tprod, LinearEquiv.refl_apply] at hx hy
|
||||
simp only [PiTensorProduct.tprodCoeff_eq_smul_tprod, Function.comp_apply, tmul_add, map_add,
|
||||
LinearMap.coe_comp, LinearEquiv.coe_coe, congr_tmul, map_smul, mapIso_tprod,
|
||||
LinearEquiv.refl_apply, hx, hy])
|
||||
intro ry fy
|
||||
simp only [PiTensorProduct.tprodCoeff_eq_smul_tprod, Function.comp_apply, tmul_smul,
|
||||
LinearMapClass.map_smul, LinearMap.coe_comp, LinearEquiv.coe_coe, congr_tmul, mapIso_tprod,
|
||||
|
|
@ -278,11 +296,14 @@ def contrAll (e : X ≃ Y) (h : cX.ContrAll e cY) : 𝓣.Tensor cX ⊗[R] 𝓣.T
|
|||
𝓣.contrAll' ∘ₗ (TensorProduct.congr (LinearEquiv.refl _ _)
|
||||
(𝓣.mapIso e.symm h.symm.toMapIso)).toLinearMap
|
||||
|
||||
omit [Fintype Y]
|
||||
|
||||
lemma contrAll_tmul (e : X ≃ Y) (h : cX.ContrAll e cY) (x : 𝓣.Tensor cX) (y : 𝓣.Tensor cY) :
|
||||
𝓣.contrAll e h (x ⊗ₜ[R] y) = 𝓣.contrAll' (x ⊗ₜ[R] ((𝓣.mapIso e.symm h.symm.toMapIso) y)) := by
|
||||
rw [contrAll]
|
||||
rfl
|
||||
|
||||
omit [Fintype Z] [DecidableEq Z] in
|
||||
@[simp]
|
||||
lemma contrAll_mapIso_right_tmul (e : X ≃ Y) (e' : Z ≃ Y)
|
||||
(h : c.ContrAll e cY) (h' : cZ.MapIso e' cY) (x : 𝓣.Tensor c) (z : 𝓣.Tensor cZ) :
|
||||
|
|
@ -291,6 +312,7 @@ lemma contrAll_mapIso_right_tmul (e : X ≃ Y) (e' : Z ≃ Y)
|
|||
simp only [contrAll_tmul, mapIso_mapIso]
|
||||
rfl
|
||||
|
||||
omit [Fintype Z] [DecidableEq Z] in
|
||||
@[simp]
|
||||
lemma contrAll_comp_mapIso_right (e : X ≃ Y) (e' : Z ≃ Y)
|
||||
(h : c.ContrAll e cY) (h' : cZ.MapIso e' cY) : 𝓣.contrAll e h ∘ₗ
|
||||
|
|
@ -300,6 +322,7 @@ lemma contrAll_comp_mapIso_right (e : X ≃ Y) (e' : Z ≃ Y)
|
|||
intro x y
|
||||
exact 𝓣.contrAll_mapIso_right_tmul e e' h h' x y
|
||||
|
||||
omit [DecidableEq Z] in
|
||||
@[simp]
|
||||
lemma contrAll_mapIso_left_tmul {e : X ≃ Y} {e' : Z ≃ X}
|
||||
(h : cX.ContrAll e cY) (h' : cZ.MapIso e' cX) (x : 𝓣.Tensor cZ) (y : 𝓣.Tensor cY) :
|
||||
|
|
@ -308,6 +331,7 @@ lemma contrAll_mapIso_left_tmul {e : X ≃ Y} {e' : Z ≃ X}
|
|||
simp only [contrAll_tmul, contrAll'_mapIso_tmul, mapIso_mapIso]
|
||||
rfl
|
||||
|
||||
omit [DecidableEq Z] in
|
||||
@[simp]
|
||||
lemma contrAll_mapIso_left {e : X ≃ Y} {e' : Z ≃ X}
|
||||
(h : cX.ContrAll e cY) (h' : cZ.MapIso e' cX) :
|
||||
|
|
@ -399,6 +423,7 @@ lemma contrAll_rep_tmul {c : X → 𝓣.Color} {d : Y → 𝓣.Color} (e : X ≃
|
|||
|
||||
-/
|
||||
|
||||
omit [Fintype X] [Fintype C] [DecidableEq C] [Fintype P] [DecidableEq P] in
|
||||
lemma contr_cond (e : (C ⊕ C) ⊕ P ≃ X) :
|
||||
cX.MapIso e.symm (Sum.elim (Sum.elim (cX.contrLeft e) (cX.contrRight e)) (cX.contr e)) := by
|
||||
rw [TensorColor.ColorMap.MapIso, Equiv.eq_comp_symm]
|
||||
|
|
@ -419,6 +444,8 @@ def contr (e : (C ⊕ C) ⊕ P ≃ X) (h : cX.ContrCond e) :
|
|||
(𝓣.mapIso e.symm (𝓣.contr_cond e)).toLinearMap
|
||||
|
||||
open PiTensorProduct in
|
||||
|
||||
omit [Fintype X] [Fintype P] in
|
||||
lemma contr_tprod (e : (C ⊕ C) ⊕ P ≃ X) (h : cX.ContrCond e) (f : (i : X) → 𝓣.ColorModule (cX i)) :
|
||||
𝓣.contr e h (tprod R f) = (𝓣.contrAll (Equiv.refl C) h.to_contrAll
|
||||
(tprod R (fun i => f (e (Sum.inl (Sum.inl i)))) ⊗ₜ[R]
|
||||
|
|
@ -431,6 +458,7 @@ lemma contr_tprod (e : (C ⊕ C) ⊕ P ≃ X) (h : cX.ContrCond e) (f : (i : X)
|
|||
rfl
|
||||
|
||||
open PiTensorProduct in
|
||||
omit [Fintype X] [Fintype P] in
|
||||
@[simp]
|
||||
lemma contr_tprod_isEmpty [IsEmpty C] (e : (C ⊕ C) ⊕ P ≃ X) (h : cX.ContrCond e)
|
||||
(f : (i : X) → 𝓣.ColorModule (cX i)) :
|
||||
|
|
@ -441,6 +469,7 @@ lemma contr_tprod_isEmpty [IsEmpty C] (e : (C ⊕ C) ⊕ P ≃ X) (h : cX.ContrC
|
|||
erw [isEmptyEquiv_tprod]
|
||||
exact MulAction.one_smul ((tprod R) fun p => f (e (Sum.inr p)))
|
||||
|
||||
omit [Fintype X] [Fintype P] in
|
||||
/-- The contraction of indices via `contr` is equivariant. -/
|
||||
@[simp]
|
||||
lemma contr_equivariant (e : (C ⊕ C) ⊕ P ≃ X) (h : cX.ContrCond e)
|
||||
|
|
|
|||
|
|
@ -37,9 +37,9 @@ noncomputable def einsteinTensor (R : Type) [CommSemiring R] (n : ℕ) : TensorS
|
|||
ColorModule _ := Fin n → R
|
||||
colorModule_addCommMonoid _ := Pi.addCommMonoid
|
||||
colorModule_module _ := Pi.Function.module (Fin n) R R
|
||||
contrDual _ := TensorProduct.lift (Fintype.total R R)
|
||||
contrDual _ := TensorProduct.lift (Fintype.linearCombination R R)
|
||||
contrDual_symm a x y := by
|
||||
simp only [lift.tmul, Fintype.total_apply, smul_eq_mul, mul_comm, Equiv.cast_refl,
|
||||
simp only [lift.tmul, Fintype.linearCombination_apply, smul_eq_mul, mul_comm, Equiv.cast_refl,
|
||||
Equiv.refl_apply]
|
||||
unit a := ∑ i, Pi.basisFun R (Fin n) i ⊗ₜ[R] Pi.basisFun R (Fin n) i
|
||||
unit_rid a x:= by
|
||||
|
|
@ -49,12 +49,12 @@ noncomputable def einsteinTensor (R : Type) [CommSemiring R] (n : ℕ) : TensorS
|
|||
· refine Finset.sum_congr rfl (fun i _ => ?_)
|
||||
simp only [TensorStructure.contrLeftAux, LinearEquiv.refl_toLinearMap, LinearMap.coe_comp,
|
||||
LinearEquiv.coe_coe, Function.comp_apply, assoc_symm_tmul, map_tmul, lift.tmul,
|
||||
Fintype.total_apply, LinearMap.stdBasis_apply', smul_eq_mul, ite_mul, one_mul, zero_mul,
|
||||
Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, LinearMap.id_coe, id_eq, lid_tmul,
|
||||
Fintype.linearCombination_apply, Pi.single_apply, smul_eq_mul, ite_mul, one_mul, zero_mul,
|
||||
Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte, LinearMap.id_coe, id_eq, lid_tmul,
|
||||
Pi.basisFun_apply]
|
||||
· funext a
|
||||
simp only [Pi.basisFun_apply, Finset.sum_apply, Pi.smul_apply, LinearMap.stdBasis_apply',
|
||||
smul_eq_mul, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte]
|
||||
simp only [Pi.basisFun_apply, Finset.sum_apply, Pi.smul_apply, Pi.single_apply, smul_eq_mul,
|
||||
mul_ite, mul_one, mul_zero, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte]
|
||||
metric a := ∑ i, Pi.basisFun R (Fin n) i ⊗ₜ[R] Pi.basisFun R (Fin n) i
|
||||
metric_dual a := by
|
||||
simp only [Pi.basisFun_apply, map_sum, comm_tmul]
|
||||
|
|
@ -62,18 +62,18 @@ noncomputable def einsteinTensor (R : Type) [CommSemiring R] (n : ℕ) : TensorS
|
|||
refine Finset.sum_congr rfl (fun i _ => ?_)
|
||||
rw [sum_tmul, map_sum, Fintype.sum_eq_single i]
|
||||
· simp only [TensorStructure.contrMidAux, LinearEquiv.refl_toLinearMap,
|
||||
TensorStructure.contrLeftAux, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
|
||||
assoc_tmul, map_tmul, LinearMap.id_coe, id_eq, assoc_symm_tmul, lift.tmul,
|
||||
Fintype.total_apply, LinearMap.stdBasis_apply', smul_eq_mul, mul_ite, mul_one, mul_zero,
|
||||
Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, lid_tmul, one_smul]
|
||||
TensorStructure.contrLeftAux, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
|
||||
assoc_tmul, map_tmul, LinearMap.id_coe, id_eq, assoc_symm_tmul, lift.tmul,
|
||||
Fintype.linearCombination_apply, Pi.single_apply, smul_eq_mul, mul_ite, mul_one, mul_zero,
|
||||
Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte, lid_tmul, one_smul]
|
||||
· intro x hi
|
||||
simp only [TensorStructure.contrMidAux, LinearEquiv.refl_toLinearMap,
|
||||
simp [TensorStructure.contrMidAux, LinearEquiv.refl_toLinearMap,
|
||||
TensorStructure.contrLeftAux, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
|
||||
assoc_tmul, map_tmul, LinearMap.id_coe, id_eq, assoc_symm_tmul, lift.tmul,
|
||||
Fintype.total_apply, LinearMap.stdBasis_apply', smul_eq_mul, mul_ite, mul_one, mul_zero,
|
||||
Fintype.linearCombination_apply, Pi.single_apply, smul_eq_mul, mul_ite, mul_one, mul_zero,
|
||||
Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte, lid_tmul, ite_smul, one_smul, zero_smul]
|
||||
rw [if_neg (id (Ne.symm hi))]
|
||||
exact tmul_zero (Fin n → R) ((LinearMap.stdBasis R (fun _ => R) x) 1)
|
||||
rw [if_neg hi]
|
||||
exact tmul_zero (Fin n → R) (Pi.single x 1)
|
||||
|
||||
namespace einsteinTensor
|
||||
|
||||
|
|
@ -104,7 +104,7 @@ def toMatrix : (einsteinTensor R n).Tensor ![Unit.unit, Unit.unit] ≃ₗ[R] Mat
|
|||
(Finsupp.linearEquivFunOnFinite R R (Fin n)).symm).trans <|
|
||||
(finsuppTensorFinsupp' R (Fin n) (Fin n)).trans <|
|
||||
(Finsupp.linearEquivFunOnFinite R R (Fin n × Fin n)).trans <|
|
||||
(LinearEquiv.curry R (Fin n) (Fin n))
|
||||
(LinearEquiv.curry R R (Fin n) (Fin n))
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -81,6 +81,7 @@ def listCharIndex (l : List Char) : Prop :=
|
|||
else
|
||||
listCharIndexTail sfst l.tail
|
||||
|
||||
omit [Fintype X] [DecidableEq X] in
|
||||
/-- An auxillary rewrite lemma to prove that `listCharIndex` is decidable. -/
|
||||
lemma listCharIndex_iff (l : List Char) : listCharIndex X l
|
||||
↔ (if h : l = [] then True else
|
||||
|
|
@ -117,6 +118,7 @@ def toColor (I : Index X) : X := I.1
|
|||
/-- The natural number representating the id of an index. -/
|
||||
def id (I : Index X) : ℕ := I.2
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma eq_iff_color_eq_and_id_eq (I J : Index X) : I = J ↔ I.toColor = J.toColor ∧ I.id = J.id := by
|
||||
refine Iff.intro (fun h => Prod.mk.inj_iff.mp h) (fun h => ?_)
|
||||
· cases I
|
||||
|
|
|
|||
|
|
@ -20,7 +20,7 @@ It is conditional on `AppendCond` being true, which we define.
|
|||
namespace IndexNotation
|
||||
namespace ColorIndexList
|
||||
|
||||
variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
|
||||
variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [DecidableEq 𝓒.Color]
|
||||
(l l2 : ColorIndexList 𝓒)
|
||||
|
||||
open IndexList TensorColor
|
||||
|
|
@ -50,6 +50,7 @@ def append (h : AppendCond l l2) : ColorIndexList 𝓒 where
|
|||
can be appended to form a `ColorIndexList`. -/
|
||||
scoped[IndexNotation.ColorIndexList] notation l " ++["h"] " l2 => append l l2 h
|
||||
|
||||
omit [DecidableEq 𝓒.Color] in
|
||||
@[simp]
|
||||
lemma append_toIndexList (h : AppendCond l l2) :
|
||||
(l ++[h] l2).toIndexList = l.toIndexList ++ l2.toIndexList := rfl
|
||||
|
|
@ -113,6 +114,7 @@ def bool (l l2 : IndexList 𝓒.Color) : Bool :=
|
|||
else
|
||||
ColorCond.bool (l ++ l2)
|
||||
|
||||
omit [IndexNotation 𝓒.Color] in
|
||||
lemma bool_iff (l l2 : IndexList 𝓒.Color) :
|
||||
bool l l2 ↔ (l ++ l2).withUniqueDual = (l ++ l2).withDual ∧ ColorCond.bool (l ++ l2) := by
|
||||
simp [bool]
|
||||
|
|
|
|||
|
|
@ -38,7 +38,7 @@ structure ColorIndexList (𝓒 : TensorColor) [IndexNotation 𝓒.Color] extends
|
|||
|
||||
namespace ColorIndexList
|
||||
|
||||
variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
|
||||
variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color]
|
||||
|
||||
variable (l l2 : ColorIndexList 𝓒)
|
||||
open IndexList TensorColor
|
||||
|
|
@ -95,7 +95,8 @@ def empty : ColorIndexList 𝓒 where
|
|||
|
||||
-/
|
||||
|
||||
lemma countId_le_two (l : ColorIndexList 𝓒) (I : Index 𝓒.Color) : l.countId I ≤ 2 :=
|
||||
lemma countId_le_two [DecidableEq 𝓒.Color] (l : ColorIndexList 𝓒) (I : Index 𝓒.Color) :
|
||||
l.countId I ≤ 2 :=
|
||||
(OnlyUniqueDuals.iff_countId_leq_two').mp l.unique_duals I
|
||||
|
||||
end ColorIndexList
|
||||
|
|
|
|||
|
|
@ -20,7 +20,7 @@ namespace IndexNotation
|
|||
|
||||
namespace ColorIndexList
|
||||
|
||||
variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
|
||||
variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [DecidableEq 𝓒.Color]
|
||||
|
||||
variable (l l' : ColorIndexList 𝓒)
|
||||
open IndexList TensorColor
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ We define the contraction of ColorIndexLists.
|
|||
namespace IndexNotation
|
||||
namespace ColorIndexList
|
||||
|
||||
variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
|
||||
variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color]
|
||||
(l l2 : ColorIndexList 𝓒)
|
||||
|
||||
open IndexList TensorColor
|
||||
|
|
@ -116,7 +116,7 @@ lemma countId_contr_le_one (I : Index 𝓒.Color) :
|
|||
l.contr.countId I ≤ 1 := by
|
||||
exact l.countId_contrIndexList_le_one I
|
||||
|
||||
lemma countId_contr_eq_zero_iff (I : Index 𝓒.Color) :
|
||||
lemma countId_contr_eq_zero_iff [DecidableEq 𝓒.Color] (I : Index 𝓒.Color) :
|
||||
l.contr.countId I = 0 ↔ l.countId I = 0 ∨ l.countId I = 2 := by
|
||||
by_cases hI : l.contr.countId I = 1
|
||||
· have hI' := hI
|
||||
|
|
|
|||
|
|
@ -34,6 +34,7 @@ variable (l : IndexList X)
|
|||
/-- The number of indices in an index list. -/
|
||||
def length : ℕ := l.val.length
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma ext (h : l.val = l2.val) : l = l2 := by
|
||||
cases l
|
||||
cases l2
|
||||
|
|
@ -42,10 +43,12 @@ lemma ext (h : l.val = l2.val) : l = l2 := by
|
|||
/-- The index list constructed by prepending an index to the list. -/
|
||||
def cons (i : Index X) : IndexList X := {val := i :: l.val}
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
@[simp]
|
||||
lemma cons_val (i : Index X) : (l.cons i).val = i :: l.val := by
|
||||
rfl
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
@[simp]
|
||||
lemma cons_length (i : Index X) : (l.cons i).length = l.length + 1 := by
|
||||
rfl
|
||||
|
|
@ -53,6 +56,7 @@ lemma cons_length (i : Index X) : (l.cons i).length = l.length + 1 := by
|
|||
/-- The tail of an index list. That is, the index list with the first index dropped. -/
|
||||
def tail : IndexList X := {val := l.val.tail}
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
@[simp]
|
||||
lemma tail_val : l.tail.val = l.val.tail := by
|
||||
rfl
|
||||
|
|
@ -60,11 +64,13 @@ lemma tail_val : l.tail.val = l.val.tail := by
|
|||
/-- The first index in a non-empty index list. -/
|
||||
def head (h : l ≠ {val := ∅}) : Index X := l.val.head (by cases' l; simpa using h)
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma head_cons_tail (h : l ≠ {val := ∅}) : l = (l.tail.cons (l.head h)) := by
|
||||
apply ext
|
||||
simp only [cons_val, tail_val]
|
||||
simp only [head, List.head_cons_tail]
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma induction {P : IndexList X → Prop } (h_nil : P {val := ∅})
|
||||
(h_cons : ∀ (x : Index X) (xs : IndexList X), P xs → P (xs.cons x)) (l : IndexList X) : P l := by
|
||||
cases' l with val
|
||||
|
|
@ -77,6 +83,7 @@ lemma induction {P : IndexList X → Prop } (h_nil : P {val := ∅})
|
|||
def colorMap : Fin l.length → X :=
|
||||
fun i => (l.val.get i).toColor
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma colorMap_cast {l1 l2 : IndexList X} (h : l1 = l2) :
|
||||
l1.colorMap = l2.colorMap ∘ Fin.cast (congrArg length h) := by
|
||||
subst h
|
||||
|
|
@ -86,6 +93,8 @@ lemma colorMap_cast {l1 l2 : IndexList X} (h : l1 = l2) :
|
|||
def idMap : Fin l.length → Nat :=
|
||||
fun i => (l.val.get i).id
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X]
|
||||
|
||||
lemma idMap_cast {l1 l2 : IndexList X} (h : l1 = l2) (i : Fin l1.length) :
|
||||
l1.idMap i = l2.idMap (Fin.cast (by rw [h]) i) := by
|
||||
subst h
|
||||
|
|
@ -132,6 +141,7 @@ def toPosSetEquiv (l : IndexList X) : l.toPosSet ≃ Fin l.length where
|
|||
intro x
|
||||
rfl
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma toPosSet_is_finite (l : IndexList X) : l.toPosSet.Finite :=
|
||||
Finite.intro l.toPosSetEquiv
|
||||
|
||||
|
|
@ -151,6 +161,7 @@ def toPosFinset (l : IndexList X) : Finset (Fin l.length × Index X) :=
|
|||
def fromFinMap {n : ℕ} (f : Fin n → Index X) : IndexList X where
|
||||
val := (Fin.list n).map f
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
@[simp]
|
||||
lemma fromFinMap_numIndices {n : ℕ} (f : Fin n → Index X) :
|
||||
(fromFinMap f).length = n := by
|
||||
|
|
@ -170,10 +181,11 @@ variable (l l2 l3 : IndexList X)
|
|||
instance : HAppend (IndexList X) (IndexList X) (IndexList X) where
|
||||
hAppend := fun l l2 => {val := l.val ++ l2.val}
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
@[simp]
|
||||
lemma cons_append (i : Index X) : (l.cons i) ++ l2 = (l ++ l2).cons i := by
|
||||
rfl
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X]
|
||||
@[simp]
|
||||
lemma append_length : (l ++ l2).length = l.length + l2.length := by
|
||||
simp [IndexList.length]
|
||||
|
|
@ -317,6 +329,7 @@ lemma filter_sort_comm {n : ℕ} (s : Finset (Fin n)) (p : Fin n → Prop) [Deci
|
|||
exact List.sorted_mergeSort (fun i j => i ≤ j) (List.filter (fun b => decide (p b)) m)
|
||||
exact this s.val
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma filter_id_eq_sort (i : Fin l.length) : l.val.filter (fun J => (l.val.get i).id = J.id) =
|
||||
List.map l.val.get (Finset.sort (fun i j => i ≤ j)
|
||||
(Finset.filter (fun j => l.idMap i = l.idMap j) Finset.univ)) := by
|
||||
|
|
|
|||
|
|
@ -21,7 +21,6 @@ namespace IndexNotation
|
|||
namespace Index
|
||||
|
||||
variable {𝓒 : TensorColor}
|
||||
variable [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
|
||||
variable (I : Index 𝓒.Color)
|
||||
|
||||
/-- The dual of an index is the index with the same id, but opposite color. -/
|
||||
|
|
@ -44,7 +43,7 @@ end Index
|
|||
namespace IndexList
|
||||
|
||||
variable {𝓒 : TensorColor}
|
||||
variable [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
|
||||
variable [DecidableEq 𝓒.Color]
|
||||
variable (l l2 l3 : IndexList 𝓒.Color)
|
||||
|
||||
/-- The number of times `I` or its dual appears in an `IndexList`. -/
|
||||
|
|
@ -352,6 +351,7 @@ namespace ColorCond
|
|||
|
||||
variable {l l2 l3 : IndexList 𝓒.Color}
|
||||
|
||||
omit [DecidableEq 𝓒.Color] in
|
||||
lemma iff_withDual :
|
||||
l.ColorCond ↔ ∀ (i : l.withDual), 𝓒.τ
|
||||
(l.colorMap ((l.getDual? i).get (l.withDual_isSome i))) = l.colorMap i := by
|
||||
|
|
@ -382,6 +382,7 @@ lemma iff_withDual :
|
|||
· simp [Option.guard, hi]
|
||||
exact Option.not_isSome_iff_eq_none.mp hi
|
||||
|
||||
omit [DecidableEq 𝓒.Color] in
|
||||
lemma iff_on_isSome : l.ColorCond ↔ ∀ (i : Fin l.length) (h : (l.getDual? i).isSome), 𝓒.τ
|
||||
(l.colorMap ((l.getDual? i).get h)) = l.colorMap i := by
|
||||
rw [iff_withDual]
|
||||
|
|
@ -476,6 +477,7 @@ lemma iff_countColorCond (hl : l.OnlyUniqueDuals) :
|
|||
rw [countSelf_neq_zero]
|
||||
exact hmem
|
||||
|
||||
omit [DecidableEq 𝓒.Color] in
|
||||
lemma assoc (h : ColorCond (l ++ l2 ++ l3)) : ColorCond (l ++ (l2 ++ l3)) := by
|
||||
rw [← append_assoc]
|
||||
exact h
|
||||
|
|
@ -525,6 +527,7 @@ lemma swap (hl : (l ++ l2 ++ l3).OnlyUniqueDuals) (h : ColorCond (l ++ l2 ++ l3)
|
|||
|
||||
-/
|
||||
|
||||
omit [DecidableEq 𝓒.Color] in
|
||||
lemma contrIndexList : ColorCond l.contrIndexList := by
|
||||
funext i
|
||||
simp [Option.guard]
|
||||
|
|
|
|||
|
|
@ -35,7 +35,7 @@ namespace IndexNotation
|
|||
|
||||
namespace IndexList
|
||||
|
||||
variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
|
||||
variable {X : Type}
|
||||
variable (l l2 l3 : IndexList X)
|
||||
|
||||
/-- The index list formed from `l` by selecting only those indices in `l` which
|
||||
|
|
|
|||
|
|
@ -32,25 +32,30 @@ def countId (I : Index X) : ℕ :=
|
|||
## Basic properties
|
||||
|
||||
-/
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
@[simp]
|
||||
lemma countId_append (I : Index X) : (l ++ l2).countId I = l.countId I + l2.countId I := by
|
||||
simp [countId]
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma countId_eq_length_filter (I : Index X) :
|
||||
l.countId I = (l.val.filter (fun J => I.id = J.id)).length := by
|
||||
simp [countId]
|
||||
rw [List.countP_eq_length_filter]
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma countId_index_neq_zero (i : Fin l.length) : l.countId (l.val.get i) ≠ 0 := by
|
||||
by_contra hn
|
||||
rw [countId_eq_length_filter, List.length_eq_zero] at hn
|
||||
refine (List.mem_nil_iff (l.val.get i)).mp ?_
|
||||
simpa [← hn] using List.getElem_mem l.val i.1 i.isLt
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma countId_append_symm (I : Index X) : (l ++ l2).countId I = (l2 ++ l).countId I := by
|
||||
simp only [countId_append]
|
||||
exact Nat.add_comm (l.countId I) (l2.countId I)
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma countId_eq_one_append_mem_right_self_eq_one {I : Index X} (hI : I ∈ l2.val)
|
||||
(h : (l ++ l2).countId I = 1) : l2.countId I = 1 := by
|
||||
simp at h
|
||||
|
|
@ -64,6 +69,7 @@ lemma countId_eq_one_append_mem_right_self_eq_one {I : Index X} (hI : I ∈ l2.v
|
|||
exact (List.mem_nil_iff I).mp hmem
|
||||
omega
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma countId_eq_one_append_mem_right_other_eq_zero {I : Index X} (hI : I ∈ l2.val)
|
||||
(h : (l ++ l2).countId I = 1) : l.countId I = 0 := by
|
||||
simp at h
|
||||
|
|
@ -77,14 +83,17 @@ lemma countId_eq_one_append_mem_right_other_eq_zero {I : Index X} (hI : I ∈ l2
|
|||
exact (List.mem_nil_iff I).mp hmem
|
||||
omega
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
@[simp]
|
||||
lemma countId_cons_eq_two {I : Index X} :
|
||||
(l.cons I).countId I = 2 ↔ l.countId I = 1 := by
|
||||
simp [countId]
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma countId_congr {I J : Index X} (h : I.id = J.id) : l.countId I = l.countId J := by
|
||||
simp [countId, h]
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma countId_neq_zero_mem (I : Index X) (h : l.countId I ≠ 0) :
|
||||
∃ I', I' ∈ l.val ∧ I.id = I'.id := by
|
||||
rw [countId_eq_length_filter] at h
|
||||
|
|
@ -96,6 +105,7 @@ lemma countId_neq_zero_mem (I : Index X) (h : l.countId I ≠ 0) :
|
|||
simp only [List.mem_filter, decide_eq_true_eq] at hI'
|
||||
exact ⟨I', hI'⟩
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma countId_mem (I : Index X) (hI : I ∈ l.val) : l.countId I ≠ 0 := by
|
||||
rw [countId_eq_length_filter]
|
||||
by_contra hn
|
||||
|
|
@ -105,6 +115,7 @@ lemma countId_mem (I : Index X) (hI : I ∈ l.val) : l.countId I ≠ 0 := by
|
|||
rw [hn] at hIme
|
||||
exact (List.mem_nil_iff I).mp hIme
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma countId_get_other (i : Fin l.length) : l2.countId (l.val.get i) =
|
||||
(List.finRange l2.length).countP (fun j => l.AreDualInOther l2 i j) := by
|
||||
rw [countId_eq_length_filter]
|
||||
|
|
@ -116,6 +127,7 @@ lemma countId_get_other (i : Fin l.length) : l2.countId (l.val.get i) =
|
|||
rfl
|
||||
|
||||
/-! TODO: Replace with mathlib lemma. -/
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma filter_finRange (i : Fin l.length) :
|
||||
List.filter (fun j => i = j) (List.finRange l.length) = [i] := by
|
||||
have h3 : (List.filter (fun j => i = j) (List.finRange l.length)).length = 1 := by
|
||||
|
|
@ -135,6 +147,7 @@ lemma filter_finRange (i : Fin l.length) :
|
|||
subst h4
|
||||
exact ha
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma countId_get (i : Fin l.length) : l.countId (l.val.get i) =
|
||||
(List.finRange l.length).countP (fun j => l.AreDualInSelf i j) + 1 := by
|
||||
rw [countId_get_other l l]
|
||||
|
|
@ -167,7 +180,7 @@ lemma countId_get (i : Fin l.length) : l.countId (l.val.get i) =
|
|||
## Duals and countId
|
||||
|
||||
-/
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma countId_gt_zero_of_mem_withDual (i : Fin l.length) (h : i ∈ l.withDual) :
|
||||
1 < l.countId (l.val.get i) := by
|
||||
rw [countId_get]
|
||||
|
|
@ -181,6 +194,7 @@ lemma countId_gt_zero_of_mem_withDual (i : Fin l.length) (h : i ∈ l.withDual)
|
|||
rw [hn] at hjmem
|
||||
exact (List.mem_nil_iff j).mp hjmem
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma countId_of_not_mem_withDual (i : Fin l.length)(h : i ∉ l.withDual) :
|
||||
l.countId (l.val.get i) = 1 := by
|
||||
rw [countId_get]
|
||||
|
|
@ -192,6 +206,7 @@ lemma countId_of_not_mem_withDual (i : Fin l.length)(h : i ∉ l.withDual) :
|
|||
rw [mem_withDual_iff_exists] at h
|
||||
simpa using h
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma mem_withDual_iff_countId_gt_one (i : Fin l.length) :
|
||||
i ∈ l.withDual ↔ 1 < l.countId (l.val.get i) := by
|
||||
refine Iff.intro (fun h => countId_gt_zero_of_mem_withDual l i h) (fun h => ?_)
|
||||
|
|
@ -199,6 +214,7 @@ lemma mem_withDual_iff_countId_gt_one (i : Fin l.length) :
|
|||
have hn' := countId_of_not_mem_withDual l i hn
|
||||
omega
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma countId_neq_zero_of_mem_withDualInOther (i : Fin l.length) (h : i ∈ l.withDualInOther l2) :
|
||||
l2.countId (l.val.get i) ≠ 0 := by
|
||||
rw [mem_withInDualOther_iff_exists] at h
|
||||
|
|
@ -214,6 +230,7 @@ lemma countId_neq_zero_of_mem_withDualInOther (i : Fin l.length) (h : i ∈ l.wi
|
|||
rw [hn] at hjmem
|
||||
exact (List.mem_nil_iff (l2.val.get j)).mp hjmem
|
||||
|
||||
omit [IndexNotation X] [Fintype X] in
|
||||
lemma countId_of_not_mem_withDualInOther (i : Fin l.length) (h : i ∉ l.withDualInOther l2) :
|
||||
l2.countId (l.val.get i) = 0 := by
|
||||
by_contra hn
|
||||
|
|
@ -231,6 +248,7 @@ lemma countId_of_not_mem_withDualInOther (i : Fin l.length) (h : i ∉ l.withDua
|
|||
simp at hj
|
||||
simp_all only [List.get_eq_getElem, List.isEmpty_eq_true, List.getElem_indexOf, not_true_eq_false]
|
||||
|
||||
omit [IndexNotation X] [Fintype X] in
|
||||
lemma mem_withDualInOther_iff_countId_neq_zero (i : Fin l.length) :
|
||||
i ∈ l.withDualInOther l2 ↔ l2.countId (l.val.get i) ≠ 0 := by
|
||||
refine Iff.intro (fun h => countId_neq_zero_of_mem_withDualInOther l l2 i h)
|
||||
|
|
@ -239,6 +257,7 @@ lemma mem_withDualInOther_iff_countId_neq_zero (i : Fin l.length) :
|
|||
have hn' := countId_of_not_mem_withDualInOther l l2 i hn
|
||||
exact h hn'
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma mem_withoutDual_iff_countId_eq_one (i : Fin l.length) :
|
||||
i ∈ l.withoutDual ↔ l.countId (l.val.get i) = 1 := by
|
||||
refine Iff.intro (fun h => ?_) (fun h => ?_)
|
||||
|
|
@ -250,6 +269,7 @@ lemma mem_withoutDual_iff_countId_eq_one (i : Fin l.length) :
|
|||
rw [mem_withDual_iff_countId_gt_one] at h
|
||||
omega
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma countId_eq_two_of_mem_withUniqueDual (i : Fin l.length) (h : i ∈ l.withUniqueDual) :
|
||||
l.countId (l.val.get i) = 2 := by
|
||||
rw [countId_get]
|
||||
|
|
@ -280,6 +300,7 @@ lemma countId_eq_two_of_mem_withUniqueDual (i : Fin l.length) (h : i ∈ l.withU
|
|||
rw [List.countP_eq_length_filter, ← h1]
|
||||
rfl
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma mem_withUniqueDual_of_countId_eq_two (i : Fin l.length)
|
||||
(h : l.countId (l.val.get i) = 2) : i ∈ l.withUniqueDual := by
|
||||
have hw : i ∈ l.withDual := by
|
||||
|
|
@ -305,11 +326,13 @@ lemma mem_withUniqueDual_of_countId_eq_two (i : Fin l.length)
|
|||
subst ht
|
||||
simp
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma mem_withUniqueDual_iff_countId_eq_two (i : Fin l.length) :
|
||||
i ∈ l.withUniqueDual ↔ l.countId (l.val.get i) = 2 :=
|
||||
Iff.intro (fun h => l.countId_eq_two_of_mem_withUniqueDual i h)
|
||||
(fun h => l.mem_withUniqueDual_of_countId_eq_two i h)
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma countId_eq_one_of_mem_withUniqueDualInOther (i : Fin l.length)
|
||||
(h : i ∈ l.withUniqueDualInOther l2) :
|
||||
l.countId (l.val.get i) = 1 ∧ l2.countId (l.val.get i) = 1 := by
|
||||
|
|
@ -345,6 +368,7 @@ lemma countId_eq_one_of_mem_withUniqueDualInOther (i : Fin l.length)
|
|||
· rw [countId_get_other, List.countP_eq_length_filter, ← h1]
|
||||
rfl
|
||||
|
||||
omit [IndexNotation X] [Fintype X] in
|
||||
lemma mem_withUniqueDualInOther_of_countId_eq_one (i : Fin l.length)
|
||||
(h : l.countId (l.val.get i) = 1 ∧ l2.countId (l.val.get i) = 1) :
|
||||
i ∈ l.withUniqueDualInOther l2 := by
|
||||
|
|
@ -376,6 +400,7 @@ lemma mem_withUniqueDualInOther_of_countId_eq_one (i : Fin l.length)
|
|||
subst ht
|
||||
exact Option.some_get ((mem_withInDualOther_iff_isSome l l2 i).mp hw)
|
||||
|
||||
omit [IndexNotation X] [Fintype X] in
|
||||
lemma mem_withUniqueDualInOther_iff_countId_eq_one (i : Fin l.length) :
|
||||
i ∈ l.withUniqueDualInOther l2 ↔ l.countId (l.val.get i) = 1 ∧ l2.countId (l.val.get i) = 1 :=
|
||||
Iff.intro (fun h => l.countId_eq_one_of_mem_withUniqueDualInOther l2 i h)
|
||||
|
|
@ -387,6 +412,8 @@ lemma mem_withUniqueDualInOther_iff_countId_eq_one (i : Fin l.length) :
|
|||
|
||||
-/
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X]
|
||||
|
||||
@[simp]
|
||||
lemma getDual?_countId (i : Fin l.length) (h : (l.getDual? i).isSome) :
|
||||
l.countId (l.val[Fin.val ((l.getDual? i).get h)]) = l.countId (l.val.get i) := by
|
||||
|
|
|
|||
|
|
@ -101,6 +101,7 @@ def withUniqueDualInOther : Finset (Fin l.length) :=
|
|||
## Basic properties
|
||||
|
||||
-/
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X]
|
||||
|
||||
@[simp, nolint simpNF]
|
||||
lemma mem_withDual_of_mem_withUniqueDual (i : Fin l.length) (h : i ∈ l.withUniqueDual) :
|
||||
|
|
|
|||
|
|
@ -29,6 +29,7 @@ variable (l l2 l3 : IndexList X)
|
|||
def withoutDualEquiv : Fin l.withoutDual.card ≃ l.withoutDual :=
|
||||
(Finset.orderIsoOfFin l.withoutDual (by rfl)).toEquiv
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
lemma list_ofFn_withoutDualEquiv_eq_sort :
|
||||
List.ofFn (Subtype.val ∘ l.withoutDualEquiv) = l.withoutDual.sort (fun i j => i ≤ j) := by
|
||||
rw [@List.ext_get_iff]
|
||||
|
|
@ -87,6 +88,7 @@ def getDualEquiv : l.withUniqueDual ≃ l.withUniqueDual where
|
|||
rw [← List.mem_singleton, ← ha]
|
||||
simp [d]
|
||||
|
||||
omit [IndexNotation X] [Fintype X] [DecidableEq X] in
|
||||
@[simp]
|
||||
lemma getDual?_getDualEquiv (i : l.withUniqueDual) : l.getDual? (l.getDualEquiv i) = i := by
|
||||
have h1 := (Equiv.apply_symm_apply l.getDualEquiv i).symm
|
||||
|
|
@ -133,6 +135,7 @@ def getDualInOtherEquiv : l.withUniqueDualInOther l2 ≃ l2.withUniqueDualInOthe
|
|||
rw [← List.mem_singleton, ← ha]
|
||||
simp [d]
|
||||
|
||||
omit [IndexNotation X] [Fintype X] in
|
||||
@[simp]
|
||||
lemma getDualInOtherEquiv_self_refl : l.getDualInOtherEquiv l = Equiv.refl _ := by
|
||||
apply Equiv.ext
|
||||
|
|
@ -148,6 +151,7 @@ lemma getDualInOtherEquiv_self_refl : l.getDualInOtherEquiv l = Equiv.refl _ :=
|
|||
rw [hx2.2 x.1 (by rfl)]
|
||||
exact Option.some_get (getDualInOtherEquiv.proof_1 l l x)
|
||||
|
||||
omit [IndexNotation X] [Fintype X] in
|
||||
@[simp]
|
||||
lemma getDualInOtherEquiv_symm : (l.getDualInOtherEquiv l2).symm = l2.getDualInOtherEquiv l := by
|
||||
rfl
|
||||
|
|
@ -175,7 +179,7 @@ def withUniqueDualCast {l1 l2 l1' l2' : IndexList X} (h : l1 = l1') (h2 : l2 = l
|
|||
invFun x := ⟨Fin.cast (by rw [h]) x.1, by subst h h2; exact x.prop⟩
|
||||
left_inv x := SetCoe.ext rfl
|
||||
right_inv x := SetCoe.ext rfl
|
||||
|
||||
omit [IndexNotation X] [Fintype X]
|
||||
lemma getDualInOtherEquiv_cast_left (h : l = l3) :
|
||||
l.getDualInOtherEquiv l2 = ((withUniqueDualCastLeft l l2 l3 h).trans
|
||||
(l3.getDualInOtherEquiv l2)).trans (withUniqueDualCastRight l2 l l3 h).symm := by
|
||||
|
|
@ -200,6 +204,7 @@ lemma getDualInOtherEquiv_cast {l1 l2 l1' l2' : IndexList X} (h : l1 = l1') (h2
|
|||
|
||||
-/
|
||||
|
||||
omit [DecidableEq X]
|
||||
/-! TODO: Replace with a mathlib lemma. -/
|
||||
lemma option_not_lt (i j : Option (Fin l.length)) : i < j → i ≠ j → ¬ j < i := by
|
||||
match i, j with
|
||||
|
|
|
|||
|
|
@ -207,6 +207,9 @@ lemma findIdx?_on_finRange_eq_findIdx {n : ℕ} (p : Fin n → Prop) [DecidableP
|
|||
def idListFin : List (Fin l.length) := ((List.finRange l.length).filter
|
||||
(fun i => (List.finRange l.length).findIdx? (fun j => l.idMap i = l.idMap j) = i))
|
||||
|
||||
omit [IndexNotation X] [Fintype X]
|
||||
|
||||
omit [DecidableEq X] in
|
||||
lemma idListFin_getDualInOther? : l.idListFin =
|
||||
(List.finRange l.length).filter (fun i => l.getDualInOther? l i = i) := by
|
||||
rw [idListFin]
|
||||
|
|
@ -220,6 +223,7 @@ lemma idListFin_getDualInOther? : l.idListFin =
|
|||
/-- The list of ids keeping only the first appearance of each id. -/
|
||||
def idList : List ℕ := List.map l.idMap l.idListFin
|
||||
|
||||
omit [DecidableEq X] in
|
||||
lemma idList_getDualInOther? : l.idList =
|
||||
List.map l.idMap ((List.finRange l.length).filter (fun i => l.getDualInOther? l i = i)) := by
|
||||
rw [idList, idListFin_getDualInOther?]
|
||||
|
|
@ -248,6 +252,7 @@ lemma idList_indexOf_mem {I J : Index X} (hI : I ∈ l.val) (hJ : J ∈ l.val) :
|
|||
rw [← lawful_beq_subsingleton instBEqOfDecidableEq instBEqNat]
|
||||
exact List.indexOf_inj (l.mem_idList_of_mem hI) (l.mem_idList_of_mem hJ)
|
||||
|
||||
omit [DecidableEq X] in
|
||||
lemma idList_indexOf_get (i : Fin l.length) :
|
||||
l.idList.indexOf (l.idMap i) = l.idListFin.indexOf ((l.getDualInOther? l i).get
|
||||
(getDualInOther?_self_isSome l i)) := by
|
||||
|
|
@ -288,6 +293,7 @@ namespace GetDualCast
|
|||
|
||||
variable {l l2 l3 : IndexList X}
|
||||
|
||||
omit [DecidableEq X] in
|
||||
lemma symm (h : GetDualCast l l2) : GetDualCast l2 l := by
|
||||
apply And.intro h.1.symm
|
||||
intro h'
|
||||
|
|
@ -298,10 +304,12 @@ lemma symm (h : GetDualCast l l2) : GetDualCast l2 l := by
|
|||
rw [h1]
|
||||
simp
|
||||
|
||||
omit [DecidableEq X] in
|
||||
lemma getDual?_isSome_iff (h : GetDualCast l l2) (i : Fin l.length) :
|
||||
(l.getDual? i).isSome ↔ (l2.getDual? (Fin.cast h.1 i)).isSome := by
|
||||
simp [h.2 h.1]
|
||||
|
||||
omit [DecidableEq X]
|
||||
lemma getDual?_get (h : GetDualCast l l2) (i : Fin l.length) (h1 : (l.getDual? i).isSome) :
|
||||
(l.getDual? i).get h1 = Fin.cast h.1.symm ((l2.getDual? (Fin.cast h.1 i)).get
|
||||
((getDual?_isSome_iff h i).mp h1)) := by
|
||||
|
|
@ -504,6 +512,7 @@ end GetDualCast
|
|||
def normalize : IndexList X where
|
||||
val := List.ofFn (fun i => ⟨l.colorMap i, l.idList.indexOf (l.idMap i)⟩)
|
||||
|
||||
omit [DecidableEq X] in
|
||||
lemma normalize_eq_map :
|
||||
l.normalize.val = List.map (fun I => ⟨I.toColor, l.idList.indexOf I.id⟩) l.val := by
|
||||
have hl : l.val = List.map l.val.get (List.finRange l.length) := by
|
||||
|
|
@ -512,19 +521,23 @@ lemma normalize_eq_map :
|
|||
simp [normalize]
|
||||
exact List.ofFn_eq_map
|
||||
|
||||
omit [DecidableEq X] in
|
||||
@[simp]
|
||||
lemma normalize_length : l.normalize.length = l.length := by
|
||||
simp [normalize, idList, length]
|
||||
|
||||
omit [DecidableEq X] in
|
||||
@[simp]
|
||||
lemma normalize_val_length : l.normalize.val.length = l.val.length := by
|
||||
simp [normalize, idList, length]
|
||||
|
||||
omit [DecidableEq X] in
|
||||
@[simp]
|
||||
lemma normalize_colorMap : l.normalize.colorMap = l.colorMap ∘ Fin.cast l.normalize_length := by
|
||||
funext x
|
||||
simp [colorMap, normalize, Index.toColor]
|
||||
|
||||
omit [DecidableEq X] in
|
||||
lemma colorMap_normalize :
|
||||
l.colorMap = l.normalize.colorMap ∘ Fin.cast l.normalize_length.symm := by
|
||||
funext x
|
||||
|
|
@ -590,6 +603,7 @@ lemma normalize_filter_countId_eq_one :
|
|||
rw [normalize_countId_mem]
|
||||
exact hI
|
||||
|
||||
omit [DecidableEq X] in
|
||||
@[simp]
|
||||
lemma normalize_idMap_apply (i : Fin l.normalize.length) :
|
||||
l.normalize.idMap i = l.idList.indexOf (l.val.get ⟨i, by simpa using i.2⟩).id := by
|
||||
|
|
@ -665,10 +679,12 @@ lemma normalize_normalize : l.normalize.normalize = l.normalize := by
|
|||
|
||||
-/
|
||||
|
||||
omit [DecidableEq X] in
|
||||
lemma normalize_length_eq_of_eq_length (h : l.length = l2.length) :
|
||||
l.normalize.length = l2.normalize.length := by
|
||||
rw [normalize_length, normalize_length, h]
|
||||
|
||||
omit [DecidableEq X] in
|
||||
lemma normalize_colorMap_eq_of_eq_colorMap (h : l.length = l2.length)
|
||||
(hc : l.colorMap = l2.colorMap ∘ Fin.cast h) :
|
||||
l.normalize.colorMap = l2.normalize.colorMap ∘
|
||||
|
|
@ -697,6 +713,7 @@ namespace Reindexing
|
|||
|
||||
variable {l l2 l3 : IndexList X}
|
||||
|
||||
omit [DecidableEq X] in
|
||||
lemma iff_getDualCast : Reindexing l l2 ↔ GetDualCast l l2
|
||||
∧ ∀ (h : l.length = l2.length), l.colorMap = l2.colorMap ∘ Fin.cast h := by
|
||||
refine Iff.intro (fun h => ⟨⟨h.1, fun h' => (h.2 h').2⟩, fun h' => (h.2 h').1⟩) (fun h => ?_)
|
||||
|
|
|
|||
|
|
@ -33,6 +33,9 @@ namespace OnlyUniqueDuals
|
|||
|
||||
variable {l l2 l3 : IndexList X}
|
||||
|
||||
omit [IndexNotation X] [Fintype X]
|
||||
|
||||
omit [DecidableEq X] in
|
||||
lemma iff_unique_forall :
|
||||
l.OnlyUniqueDuals ↔
|
||||
∀ (i : l.withDual) j, l.AreDualInSelf i j → j = l.getDual? i := by
|
||||
|
|
@ -48,6 +51,7 @@ lemma iff_unique_forall :
|
|||
true_and]
|
||||
exact And.intro ((mem_withDual_iff_isSome l i).mp hi) (fun j hj => h ⟨i, hi⟩ j hj)
|
||||
|
||||
omit [DecidableEq X] in
|
||||
lemma iff_countId_leq_two :
|
||||
l.OnlyUniqueDuals ↔ ∀ i, l.countId (l.val.get i) ≤ 2 := by
|
||||
refine Iff.intro (fun h i => ?_) (fun h => ?_)
|
||||
|
|
@ -151,11 +155,13 @@ lemma contrIndexList_append (h1 : (l ++ l2).OnlyUniqueDuals) :
|
|||
|
||||
end OnlyUniqueDuals
|
||||
|
||||
omit [IndexNotation X] [Fintype X] in
|
||||
lemma countId_of_OnlyUniqueDuals (h : l.OnlyUniqueDuals) (I : Index X) :
|
||||
l.countId I ≤ 2 := by
|
||||
rw [OnlyUniqueDuals.iff_countId_leq_two'] at h
|
||||
exact h I
|
||||
|
||||
omit [IndexNotation X] [Fintype X] in
|
||||
lemma countId_eq_two_ofcontrIndexList_left_of_OnlyUniqueDuals
|
||||
(h : (l ++ l2).OnlyUniqueDuals) (I : Index X) (h' : (l.contrIndexList ++ l2).countId I = 2) :
|
||||
(l ++ l2).countId I = 2 := by
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@ namespace IndexNotation
|
|||
|
||||
namespace IndexList
|
||||
|
||||
variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
|
||||
variable {X : Type} [DecidableEq X]
|
||||
variable (l l2 l3 : IndexList X)
|
||||
|
||||
/-- An IndexList `l` is a subpermutation of `l2` if there are no duals in `l`, and
|
||||
|
|
|
|||
|
|
@ -31,7 +31,7 @@ variable {d : ℕ} {X Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [
|
|||
{cX cX2 : X → 𝓣.Color} {cY : Y → 𝓣.Color} {cZ : Z → 𝓣.Color}
|
||||
{cW : W → 𝓣.Color} {cY' : Y' → 𝓣.Color} {μ ν η : 𝓣.Color}
|
||||
|
||||
variable [IndexNotation 𝓣.Color] [Fintype 𝓣.Color] [DecidableEq 𝓣.Color]
|
||||
variable [IndexNotation 𝓣.Color]
|
||||
|
||||
/-- The structure an tensor with a index specification e.g. `ᵘ¹ᵤ₂`. -/
|
||||
structure TensorIndex extends ColorIndexList 𝓣.toTensorColor where
|
||||
|
|
@ -42,12 +42,13 @@ namespace TensorIndex
|
|||
|
||||
open TensorColor ColorIndexList
|
||||
|
||||
variable {𝓣 : TensorStructure R} [IndexNotation 𝓣.Color] [Fintype 𝓣.Color] [DecidableEq 𝓣.Color]
|
||||
variable {𝓣 : TensorStructure R} [IndexNotation 𝓣.Color] [DecidableEq 𝓣.Color]
|
||||
variable {n m : ℕ} {cn : Fin n → 𝓣.Color} {cm : Fin m → 𝓣.Color}
|
||||
|
||||
instance : Coe 𝓣.TensorIndex (ColorIndexList 𝓣.toTensorColor) where
|
||||
coe T := T.toColorIndexList
|
||||
|
||||
omit [DecidableEq 𝓣.Color] in
|
||||
lemma colormap_mapIso {T₁ T₂ : 𝓣.TensorIndex} (hi : T₁.toColorIndexList = T₂.toColorIndexList) :
|
||||
ColorMap.MapIso (Fin.castOrderIso (congrArg IndexList.length (congrArg toIndexList hi))).toEquiv
|
||||
T₁.colorMap' T₂.colorMap' := by
|
||||
|
|
@ -65,6 +66,7 @@ lemma colormap_mapIso {T₁ T₂ : 𝓣.TensorIndex} (hi : T₁.toColorIndexList
|
|||
subst hi
|
||||
rfl
|
||||
|
||||
omit [DecidableEq 𝓣.Color] in
|
||||
lemma ext {T₁ T₂ : 𝓣.TensorIndex} (hi : T₁.toColorIndexList = T₂.toColorIndexList)
|
||||
(h : T₁.tensor = 𝓣.mapIso (Fin.castOrderIso (by simp [IndexList.length, hi])).toEquiv
|
||||
(colormap_mapIso hi.symm) T₂.tensor) : T₁ = T₂ := by
|
||||
|
|
@ -75,6 +77,7 @@ lemma ext {T₁ T₂ : 𝓣.TensorIndex} (hi : T₁.toColorIndexList = T₂.toCo
|
|||
subst hi
|
||||
simp_all
|
||||
|
||||
omit [DecidableEq 𝓣.Color] in
|
||||
lemma index_eq_of_eq {T₁ T₂ : 𝓣.TensorIndex} (h : T₁ = T₂) :
|
||||
T₁.toColorIndexList = T₂.toColorIndexList := by
|
||||
cases h
|
||||
|
|
@ -88,6 +91,7 @@ def tensorIso {T₁ T₂ : 𝓣.TensorIndex} (h : T₁ = T₂) :
|
|||
𝓣.mapIso (Fin.castOrderIso (by rw [index_eq_of_eq h])).toEquiv
|
||||
(colormap_mapIso (index_eq_of_eq h).symm)
|
||||
|
||||
omit [DecidableEq 𝓣.Color] in
|
||||
@[simp]
|
||||
lemma tensor_eq_of_eq {T₁ T₂ : 𝓣.TensorIndex} (h : T₁ = T₂) :
|
||||
T₁.tensor = tensorIso h T₂.tensor := by
|
||||
|
|
@ -121,12 +125,14 @@ def contr (T : 𝓣.TensorIndex) : 𝓣.TensorIndex where
|
|||
tensor := 𝓣.mapIso (Equiv.refl _) T.contrEquiv_colorMapIso <|
|
||||
𝓣.contr T.toColorIndexList.contrEquiv T.contrEquiv_contrCond T.tensor
|
||||
|
||||
omit [DecidableEq 𝓣.Color] in
|
||||
@[simp]
|
||||
lemma contr_tensor (T : 𝓣.TensorIndex) :
|
||||
T.contr.tensor = ((𝓣.mapIso (Equiv.refl _) T.contrEquiv_colorMapIso <|
|
||||
𝓣.contr T.toColorIndexList.contrEquiv T.contrEquiv_contrCond T.tensor)) := by
|
||||
rfl
|
||||
|
||||
omit [DecidableEq 𝓣.Color] in
|
||||
/-- Applying contr to a tensor whose indices has no contracts does not do anything. -/
|
||||
@[simp]
|
||||
lemma contr_of_withDual_empty (T : 𝓣.TensorIndex) (h : T.withDual = ∅) :
|
||||
|
|
@ -169,18 +175,22 @@ lemma contr_of_withDual_empty (T : 𝓣.TensorIndex) (h : T.withDual = ∅) :
|
|||
let hl := i.contrEquiv_on_withDual_empty l h
|
||||
exact let_value_heq f hl
|
||||
|
||||
omit [DecidableEq 𝓣.Color] in
|
||||
lemma contr_tensor_of_withDual_empty (T : 𝓣.TensorIndex) (h : T.withDual = ∅) :
|
||||
T.contr.tensor = tensorIso (contr_of_withDual_empty T h) T.tensor := by
|
||||
exact tensor_eq_of_eq (contr_of_withDual_empty T h)
|
||||
|
||||
omit [DecidableEq 𝓣.Color] in
|
||||
@[simp]
|
||||
lemma contr_contr (T : 𝓣.TensorIndex) : T.contr.contr = T.contr :=
|
||||
T.contr.contr_of_withDual_empty (by simp [contr, ColorIndexList.contr])
|
||||
|
||||
omit [DecidableEq 𝓣.Color] in
|
||||
@[simp]
|
||||
lemma contr_toColorIndexList (T : 𝓣.TensorIndex) :
|
||||
T.contr.toColorIndexList = T.toColorIndexList.contr := rfl
|
||||
|
||||
omit [DecidableEq 𝓣.Color] in
|
||||
lemma contr_toIndexList (T : 𝓣.TensorIndex) :
|
||||
T.contr.toIndexList = T.toIndexList.contrIndexList := rfl
|
||||
|
||||
|
|
@ -295,12 +305,15 @@ instance : SMul R 𝓣.TensorIndex where
|
|||
toColorIndexList := T.toColorIndexList
|
||||
tensor := r • T.tensor}
|
||||
|
||||
omit [DecidableEq 𝓣.Color] in
|
||||
@[simp]
|
||||
lemma smul_index (r : R) (T : 𝓣.TensorIndex) : (r • T).toColorIndexList = T.toColorIndexList := rfl
|
||||
|
||||
omit [DecidableEq 𝓣.Color] in
|
||||
@[simp]
|
||||
lemma smul_tensor (r : R) (T : 𝓣.TensorIndex) : (r • T).tensor = r • T.tensor := rfl
|
||||
|
||||
omit [DecidableEq 𝓣.Color] in
|
||||
@[simp]
|
||||
lemma smul_contr (r : R) (T : 𝓣.TensorIndex) : (r • T).contr = r • T.contr := by
|
||||
refine ext rfl ?_
|
||||
|
|
@ -535,6 +548,7 @@ namespace ProdCond
|
|||
|
||||
variable {T₁ T₁' T₂ T₂' : 𝓣.TensorIndex}
|
||||
|
||||
omit [DecidableEq 𝓣.Color] in
|
||||
lemma to_AppendCond (h : ProdCond T₁ T₂) :
|
||||
T₁.AppendCond T₂ := h
|
||||
|
||||
|
|
@ -553,10 +567,12 @@ def prod (T₁ T₂ : 𝓣.TensorIndex) (h : ProdCond T₁ T₂) : 𝓣.TensorIn
|
|||
tensor := 𝓣.mapIso IndexList.appendEquiv (T₁.colorMap_sumELim T₂) <|
|
||||
𝓣.tensoratorEquiv _ _ (T₁.tensor ⊗ₜ[R] T₂.tensor)
|
||||
|
||||
omit [DecidableEq 𝓣.Color] in
|
||||
@[simp]
|
||||
lemma prod_toColorIndexList (T₁ T₂ : 𝓣.TensorIndex) (h : ProdCond T₁ T₂) :
|
||||
(prod T₁ T₂ h).toColorIndexList = T₁.toColorIndexList ++[h] T₂.toColorIndexList := rfl
|
||||
|
||||
omit [DecidableEq 𝓣.Color] in
|
||||
@[simp]
|
||||
lemma prod_toIndexList (T₁ T₂ : 𝓣.TensorIndex) (h : ProdCond T₁ T₂) :
|
||||
(prod T₁ T₂ h).toIndexList = T₁.toIndexList ++ T₂.toIndexList := rfl
|
||||
|
|
|
|||
|
|
@ -138,6 +138,7 @@ lemma repColorModule_colorModuleCast (h : μ = ν) (g : G) :
|
|||
intro x
|
||||
simp [colorModuleCast_equivariant_apply]
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] in
|
||||
@[simp]
|
||||
lemma rep_mapIso (e : X ≃ Y) (h : cX = cY ∘ e) (g : G) :
|
||||
(𝓣.rep g) ∘ₗ (𝓣.mapIso e h).toLinearMap = (𝓣.mapIso e h).toLinearMap ∘ₗ 𝓣.rep g := by
|
||||
|
|
@ -157,6 +158,7 @@ lemma rep_mapIso (e : X ≃ Y) (h : cX = cY ∘ e) (g : G) :
|
|||
subst h
|
||||
simp [colorModuleCast_equivariant_apply]
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] in
|
||||
@[simp]
|
||||
lemma rep_mapIso_apply (e : X ≃ Y) (h : cX = cY ∘ e) (g : G) (x : 𝓣.Tensor cX) :
|
||||
(𝓣.mapIso e h) (g • x) = g • (𝓣.mapIso e h x) := by
|
||||
|
|
@ -164,6 +166,7 @@ lemma rep_mapIso_apply (e : X ≃ Y) (h : cX = cY ∘ e) (g : G) (x : 𝓣.Tenso
|
|||
· simp
|
||||
· rfl
|
||||
|
||||
omit [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] in
|
||||
@[simp]
|
||||
lemma rep_tprod (g : G) (f : (i : X) → 𝓣.ColorModule (cX i)) :
|
||||
g • (PiTensorProduct.tprod R f) = PiTensorProduct.tprod R (fun x =>
|
||||
|
|
@ -178,6 +181,7 @@ lemma rep_tprod (g : G) (f : (i : X) → 𝓣.ColorModule (cX i)) :
|
|||
|
||||
-/
|
||||
|
||||
omit [Fintype X] [Fintype Y] in
|
||||
lemma tensoratorEquiv_equivariant (g : G) :
|
||||
(𝓣.tensoratorEquiv cX cY) ∘ₗ (TensorProduct.map (𝓣.rep g) (𝓣.rep g)) = 𝓣.rep g ∘ₗ
|
||||
(𝓣.tensoratorEquiv cX cY).toLinearMap := by
|
||||
|
|
@ -191,6 +195,7 @@ lemma tensoratorEquiv_equivariant (g : G) :
|
|||
| Sum.inl x => rfl
|
||||
| Sum.inr x => rfl
|
||||
|
||||
omit [Fintype X] [Fintype Y] in
|
||||
@[simp]
|
||||
lemma tensoratorEquiv_equivariant_apply (g : G) (x : 𝓣.Tensor cX ⊗[R] 𝓣.Tensor cY) :
|
||||
(𝓣.tensoratorEquiv cX cY) ((TensorProduct.map (𝓣.rep g) (𝓣.rep g)) x)
|
||||
|
|
@ -200,12 +205,14 @@ lemma tensoratorEquiv_equivariant_apply (g : G) (x : 𝓣.Tensor cX ⊗[R] 𝓣.
|
|||
· rw [tensoratorEquiv_equivariant]
|
||||
rfl
|
||||
|
||||
omit [Fintype X] [Fintype Y] in
|
||||
lemma rep_tensoratorEquiv_tmul (g : G) (x : 𝓣.Tensor cX) (y : 𝓣.Tensor cY) :
|
||||
(𝓣.tensoratorEquiv cX cY) ((g • x) ⊗ₜ[R] (g • y)) =
|
||||
g • ((𝓣.tensoratorEquiv cX cY) (x ⊗ₜ[R] y)) := by
|
||||
nth_rewrite 1 [← tensoratorEquiv_equivariant_apply]
|
||||
rfl
|
||||
|
||||
omit [Fintype X] [Fintype Y] in
|
||||
lemma rep_tensoratorEquiv_symm (g : G) :
|
||||
(𝓣.tensoratorEquiv cX cY).symm ∘ₗ 𝓣.rep g = (TensorProduct.map (𝓣.rep g) (𝓣.rep g)) ∘ₗ
|
||||
(𝓣.tensoratorEquiv cX cY).symm.toLinearMap := by
|
||||
|
|
@ -213,6 +220,7 @@ lemma rep_tensoratorEquiv_symm (g : G) :
|
|||
LinearEquiv.toLinearMap_symm_comp_eq]
|
||||
exact Eq.symm (tensoratorEquiv_equivariant 𝓣 g)
|
||||
|
||||
omit [Fintype X] [Fintype Y] in
|
||||
@[simp]
|
||||
lemma rep_tensoratorEquiv_symm_apply (g : G) (x : 𝓣.Tensor (Sum.elim cX cY)) :
|
||||
(𝓣.tensoratorEquiv cX cY).symm ((𝓣.rep g) x) =
|
||||
|
|
@ -222,14 +230,17 @@ lemma rep_tensoratorEquiv_symm_apply (g : G) (x : 𝓣.Tensor (Sum.elim cX cY))
|
|||
· rw [rep_tensoratorEquiv_symm]
|
||||
rfl
|
||||
|
||||
omit [Fintype X] [DecidableEq X] in
|
||||
@[simp]
|
||||
lemma rep_lid (g : G) : TensorProduct.lid R (𝓣.Tensor cX) ∘ₗ
|
||||
(TensorProduct.map (LinearMap.id) (𝓣.rep g)) = (𝓣.rep g) ∘ₗ
|
||||
(TensorProduct.lid R (𝓣.Tensor cX)).toLinearMap := by
|
||||
apply TensorProduct.ext'
|
||||
intro r y
|
||||
simp
|
||||
simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, map_tmul,
|
||||
LinearMap.id_coe, id_eq, lid_tmul, map_smul]
|
||||
|
||||
omit [Fintype X] [DecidableEq X] in
|
||||
@[simp]
|
||||
lemma rep_lid_apply (g : G) (x : R ⊗[R] 𝓣.Tensor cX) :
|
||||
(TensorProduct.lid R (𝓣.Tensor cX)) ((TensorProduct.map (LinearMap.id) (𝓣.rep g)) x) =
|
||||
|
|
|
|||
|
|
@ -55,6 +55,7 @@ variable {n : ℕ}
|
|||
def boolFin (c₁ c₂ : 𝓒.ColorMap (Fin n)) : Bool :=
|
||||
(Fin.list n).all fun i => if 𝓒.colorQuot (c₁ i) = 𝓒.colorQuot (c₂ i) then true else false
|
||||
|
||||
omit [Fintype 𝓒.Color] in
|
||||
lemma boolFin_DualMap {c₁ c₂ : 𝓒.ColorMap (Fin n)} (h : boolFin c₁ c₂ = true) :
|
||||
DualMap c₁ c₂ := by
|
||||
simp [boolFin] at h
|
||||
|
|
@ -72,6 +73,7 @@ lemma boolFin_DualMap {c₁ c₂ : 𝓒.ColorMap (Fin n)} (h : boolFin c₁ c₂
|
|||
def boolFin' (c₁ c₂ : 𝓒.ColorMap (Fin n)) : Bool :=
|
||||
∀ (i : Fin n), 𝓒.colorQuot (c₁ i) = 𝓒.colorQuot (c₂ i)
|
||||
|
||||
omit [Fintype 𝓒.Color]
|
||||
lemma boolFin'_DualMap {c₁ c₂ : 𝓒.ColorMap (Fin n)} (h : boolFin' c₁ c₂ = true) :
|
||||
DualMap c₁ c₂ := by
|
||||
simp [boolFin'] at h
|
||||
|
|
@ -79,12 +81,15 @@ lemma boolFin'_DualMap {c₁ c₂ : 𝓒.ColorMap (Fin n)} (h : boolFin' c₁ c
|
|||
funext x
|
||||
exact h x
|
||||
|
||||
omit [DecidableEq 𝓒.Color] [Fintype X] [DecidableEq X] in
|
||||
lemma refl : DualMap c₁ c₁ := rfl
|
||||
|
||||
omit [DecidableEq 𝓒.Color] [Fintype X] [DecidableEq X] in
|
||||
lemma symm (h : DualMap c₁ c₂) : DualMap c₂ c₁ := by
|
||||
rw [DualMap] at h ⊢
|
||||
exact h.symm
|
||||
|
||||
omit [DecidableEq 𝓒.Color] [Fintype X] [DecidableEq X] in
|
||||
lemma trans (h : DualMap c₁ c₂) (h' : DualMap c₂ c₃) : DualMap c₁ c₃ := by
|
||||
rw [DualMap] at h h' ⊢
|
||||
exact h.trans h'
|
||||
|
|
@ -93,6 +98,7 @@ lemma trans (h : DualMap c₁ c₂) (h' : DualMap c₂ c₃) : DualMap c₁ c₃
|
|||
def split (c₁ c₂ : 𝓒.ColorMap X) : { x // c₁ x ≠ c₂ x} ⊕ { x // c₁ x = c₂ x} ≃ X :=
|
||||
((Equiv.Set.sumCompl {x | c₁ x = c₂ x}).symm.trans (Equiv.sumComm _ _)).symm
|
||||
|
||||
omit [DecidableEq 𝓒.Color] [Fintype X] [DecidableEq X] in
|
||||
lemma dual_eq_of_neq (h : DualMap c₁ c₂) {x : X} (h' : c₁ x ≠ c₂ x) :
|
||||
𝓒.τ (c₁ x) = c₂ x := by
|
||||
rw [DualMap] at h
|
||||
|
|
@ -101,6 +107,7 @@ lemma dual_eq_of_neq (h : DualMap c₁ c₂) {x : X} (h' : c₁ x ≠ c₂ x) :
|
|||
simp_all only [ne_eq, false_or]
|
||||
exact 𝓒.τ_involutive (c₂ x)
|
||||
|
||||
omit [Fintype X] [DecidableEq X] in
|
||||
@[simp]
|
||||
lemma split_dual (h : DualMap c₁ c₂) : c₁.partDual (split c₁ c₂) = c₂ := by
|
||||
rw [partDual, Equiv.comp_symm_eq]
|
||||
|
|
@ -111,6 +118,7 @@ lemma split_dual (h : DualMap c₁ c₂) : c₁.partDual (split c₁ c₂) = c
|
|||
| Sum.inr x =>
|
||||
exact x.2
|
||||
|
||||
omit [Fintype X] [DecidableEq X] in
|
||||
@[simp]
|
||||
lemma split_dual' (h : DualMap c₁ c₂) : c₂.partDual (split c₁ c₂) = c₁ := by
|
||||
rw [partDual, Equiv.comp_symm_eq]
|
||||
|
|
@ -273,7 +281,7 @@ def dualizeAll : 𝓣.Tensor cX ≃ₗ[R] 𝓣.Tensor (𝓣.τ ∘ cX) := by
|
|||
rw [PiTensorProduct.map_tprod, PiTensorProduct.map_tprod]
|
||||
apply congrArg
|
||||
simp
|
||||
|
||||
omit [Fintype X] [DecidableEq X]
|
||||
@[simp]
|
||||
lemma dualizeAll_equivariant (g : G) : (𝓣.dualizeAll.toLinearMap) ∘ₗ (@rep R _ G _ 𝓣 _ X cX g)
|
||||
= 𝓣.rep g ∘ₗ (𝓣.dualizeAll.toLinearMap) := by
|
||||
|
|
@ -292,6 +300,7 @@ lemma dualizeAll_equivariant (g : G) : (𝓣.dualizeAll.toLinearMap) ∘ₗ (@re
|
|||
rw [PiTensorProduct.map_tprod, PiTensorProduct.map_tprod]
|
||||
simp
|
||||
|
||||
omit [Fintype C] [DecidableEq C] [Fintype P] [DecidableEq P] in
|
||||
lemma dualize_cond (e : C ⊕ P ≃ X) :
|
||||
cX = Sum.elim (cX ∘ e ∘ Sum.inl) (cX ∘ e ∘ Sum.inr) ∘ e.symm := by
|
||||
rw [Equiv.eq_comp_symm]
|
||||
|
|
@ -300,6 +309,7 @@ lemma dualize_cond (e : C ⊕ P ≃ X) :
|
|||
| Sum.inl x => rfl
|
||||
| Sum.inr x => rfl
|
||||
|
||||
omit [Fintype C] [DecidableEq C] [Fintype P] [DecidableEq P] in
|
||||
lemma dualize_cond' (e : C ⊕ P ≃ X) :
|
||||
Sum.elim (𝓣.τ ∘ cX ∘ ⇑e ∘ Sum.inl) (cX ∘ ⇑e ∘ Sum.inr) =
|
||||
(Sum.elim (𝓣.τ ∘ cX ∘ ⇑e ∘ Sum.inl) (cX ∘ ⇑e ∘ Sum.inr) ∘ ⇑e.symm) ∘ ⇑e := by
|
||||
|
|
@ -317,6 +327,7 @@ def dualize (e : C ⊕ P ≃ X) : 𝓣.Tensor cX ≃ₗ[R] 𝓣.Tensor (cX.partD
|
|||
(𝓣.tensoratorEquiv _ _) ≪≫ₗ
|
||||
𝓣.mapIso e (𝓣.dualize_cond' e)
|
||||
|
||||
omit [Fintype C] [Fintype P] in
|
||||
/-- Dualizing indices is equivariant with respect to the group action. This is the
|
||||
applied version of this statement. -/
|
||||
@[simp]
|
||||
|
|
|
|||
|
|
@ -66,9 +66,9 @@ noncomputable def stdBasis : Basis (Fin 1 ⊕ Fin (d)) ℝ (LorentzVector d) :=
|
|||
scoped[LorentzVector] notation "e" => stdBasis
|
||||
|
||||
lemma stdBasis_apply (μ ν : Fin 1 ⊕ Fin d) : e μ ν = if μ = ν then 1 else 0 := by
|
||||
rw [stdBasis]
|
||||
erw [Pi.basisFun_apply]
|
||||
exact LinearMap.stdBasis_apply' ℝ μ ν
|
||||
erw [stdBasis, Pi.basisFun_apply, Pi.single_apply]
|
||||
refine Eq.symm (ite_congr ?h₁ (congrFun rfl) (congrFun rfl))
|
||||
exact Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a)
|
||||
|
||||
lemma decomp_stdBasis (v : LorentzVector d) : ∑ i, v i • e i = v := by
|
||||
funext ν
|
||||
|
|
@ -76,13 +76,13 @@ lemma decomp_stdBasis (v : LorentzVector d) : ∑ i, v i • e i = v := by
|
|||
rw [Finset.sum_eq_single_of_mem ν]
|
||||
· simp [HSMul.hSMul, SMul.smul, stdBasis, Pi.basisFun_apply]
|
||||
erw [Pi.basisFun_apply]
|
||||
simp only [LinearMap.stdBasis_same, mul_one]
|
||||
simp only [Pi.single_eq_same, mul_one]
|
||||
· exact Finset.mem_univ ν
|
||||
· intros b _ hbi
|
||||
simp [HSMul.hSMul, SMul.smul, stdBasis, Pi.basisFun_apply]
|
||||
erw [Pi.basisFun_apply]
|
||||
simp [LinearMap.stdBasis_apply]
|
||||
exact Or.inr hbi
|
||||
simp only [Pi.single]
|
||||
apply Or.inr $ Function.update_noteq (id (Ne.symm hbi)) 1 0
|
||||
|
||||
@[simp]
|
||||
lemma decomp_stdBasis' (v : LorentzVector d) :
|
||||
|
|
|
|||
|
|
@ -74,13 +74,13 @@ lemma contrUpDown_stdBasis_left (x : LorentzVector d) (i : Fin 1 ⊕ Fin d) :
|
|||
rw [Finset.sum_eq_single_of_mem i]
|
||||
· simp only [CovariantLorentzVector.stdBasis]
|
||||
erw [Pi.basisFun_apply]
|
||||
simp only [LinearMap.stdBasis_same, mul_one]
|
||||
simp only [Pi.single_eq_same, mul_one]
|
||||
· exact Finset.mem_univ i
|
||||
· intro b _ hbi
|
||||
simp only [CovariantLorentzVector.stdBasis, mul_eq_zero]
|
||||
erw [Pi.basisFun_apply]
|
||||
simp only [LinearMap.stdBasis_apply', ite_eq_right_iff, one_ne_zero, imp_false]
|
||||
exact Or.inr hbi.symm
|
||||
simp only [Pi.single_apply, ite_eq_right_iff, one_ne_zero, imp_false]
|
||||
apply Or.inr hbi
|
||||
|
||||
@[simp]
|
||||
lemma contrUpDown_stdBasis_right (x : CovariantLorentzVector d) (i : Fin 1 ⊕ Fin d) :
|
||||
|
|
@ -88,13 +88,13 @@ lemma contrUpDown_stdBasis_right (x : CovariantLorentzVector d) (i : Fin 1 ⊕ F
|
|||
simp only [contrUpDown, contrUpDownBi, lift.tmul, LinearMap.coe_mk, AddHom.coe_mk]
|
||||
rw [Finset.sum_eq_single_of_mem i]
|
||||
· erw [Pi.basisFun_apply]
|
||||
simp only [LinearMap.stdBasis_same, one_mul]
|
||||
simp only [Pi.single_eq_same, one_mul]
|
||||
· exact Finset.mem_univ i
|
||||
· intro b _ hbi
|
||||
simp only [CovariantLorentzVector.stdBasis, mul_eq_zero]
|
||||
erw [Pi.basisFun_apply]
|
||||
simp only [LinearMap.stdBasis_apply', ite_eq_right_iff, one_ne_zero, imp_false]
|
||||
exact Or.intro_left (x b = 0) (id (Ne.symm hbi))
|
||||
simp only [Pi.single_apply, ite_eq_right_iff, one_ne_zero, imp_false]
|
||||
exact Or.intro_left (x b = 0) hbi
|
||||
|
||||
/-- The linear map defining the contraction of a covariant Lorentz vector
|
||||
and a contravariant Lorentz vector. -/
|
||||
|
|
@ -247,16 +247,16 @@ lemma asTenProd_contr_asCoTenProd :
|
|||
· change (η μ μ * (η μ μ * e μ μ)) • e μ ⊗ₜ[ℝ] CovariantLorentzVector.stdBasis μ = _
|
||||
rw [LorentzVector.stdBasis]
|
||||
erw [Pi.basisFun_apply]
|
||||
simp only [LinearMap.stdBasis_same, mul_one, η_apply_mul_η_apply_diag, one_smul]
|
||||
simp only [Pi.single_eq_same, mul_one, η_apply_mul_η_apply_diag, one_smul]
|
||||
· exact Finset.mem_univ μ
|
||||
· intro ν _ hμν
|
||||
rw [tmul_smul]
|
||||
change (η ν ν * (η μ μ * e μ ν)) • (e μ ⊗ₜ[ℝ] CovariantLorentzVector.stdBasis ν) = _
|
||||
rw [LorentzVector.stdBasis]
|
||||
erw [Pi.basisFun_apply]
|
||||
simp only [LinearMap.stdBasis_apply', mul_ite, mul_one, mul_zero, ite_smul, zero_smul,
|
||||
simp only [Pi.single_apply, mul_ite, mul_one, mul_zero, ite_smul, zero_smul,
|
||||
ite_eq_right_iff, smul_eq_zero, mul_eq_zero]
|
||||
exact fun a => False.elim (hμν (id (Eq.symm a)))
|
||||
exact fun a => False.elim (hμν a)
|
||||
|
||||
@[simp]
|
||||
lemma asCoTenProd_contr_asTenProd :
|
||||
|
|
@ -273,15 +273,15 @@ lemma asCoTenProd_contr_asTenProd :
|
|||
contrLeft_asTenProd]
|
||||
rw [tmul_sum, Finset.sum_eq_single_of_mem μ, tmul_smul, smul_smul, LorentzVector.stdBasis]
|
||||
· erw [Pi.basisFun_apply]
|
||||
simp only [LinearMap.stdBasis_same, mul_one, η_apply_mul_η_apply_diag, one_smul]
|
||||
simp only [Pi.single_eq_same, mul_one, η_apply_mul_η_apply_diag, one_smul]
|
||||
· exact Finset.mem_univ μ
|
||||
· intro ν _ hμν
|
||||
rw [tmul_smul]
|
||||
rw [LorentzVector.stdBasis]
|
||||
erw [Pi.basisFun_apply]
|
||||
simp only [LinearMap.stdBasis_apply', mul_ite, mul_one, mul_zero, ite_smul, zero_smul,
|
||||
simp only [Pi.single_apply, mul_ite, mul_one, mul_zero, ite_smul, zero_smul,
|
||||
ite_eq_right_iff, smul_eq_zero, mul_eq_zero]
|
||||
exact fun a => False.elim (hμν (id (Eq.symm a)))
|
||||
exact fun a => False.elim (hμν a)
|
||||
|
||||
lemma asTenProd_invariant (g : LorentzGroup d) :
|
||||
TensorProduct.map (LorentzVector.rep g) (LorentzVector.rep g) asTenProd = asTenProd := by
|
||||
|
|
|
|||
|
|
@ -50,13 +50,13 @@ lemma decomp_stdBasis (v : CovariantLorentzVector d) : ∑ i, v i • stdBasis i
|
|||
rw [Finset.sum_apply, Finset.sum_eq_single_of_mem ν]
|
||||
· simp [HSMul.hSMul, SMul.smul, stdBasis, Pi.basisFun_apply]
|
||||
erw [Pi.basisFun_apply]
|
||||
simp only [LinearMap.stdBasis_same, mul_one]
|
||||
simp only [Pi.single_eq_same, mul_one]
|
||||
· exact Finset.mem_univ ν
|
||||
· intros b _ hbi
|
||||
simp [HSMul.hSMul, SMul.smul, stdBasis, Pi.basisFun_apply]
|
||||
simp only [HSMul.hSMul, SMul.smul, stdBasis, mul_eq_zero]
|
||||
erw [Pi.basisFun_apply]
|
||||
simp [LinearMap.stdBasis_apply]
|
||||
exact Or.inr hbi
|
||||
simp only [Pi.single]
|
||||
apply Or.inr (Function.update_noteq (id (Ne.symm hbi)) 1 0)
|
||||
|
||||
@[simp]
|
||||
lemma decomp_stdBasis' (v : CovariantLorentzVector d) :
|
||||
|
|
@ -98,8 +98,8 @@ lemma rep_apply_stdBasis (g : LorentzGroup d) (μ : Fin 1 ⊕ Fin d) :
|
|||
simp only [rep_apply, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
|
||||
Finset.sum_singleton, decomp_stdBasis']
|
||||
funext ν
|
||||
simp [LorentzVector.stdBasis, Pi.basisFun_apply]
|
||||
erw [Pi.basisFun_apply, Matrix.mulVec_stdBasis]
|
||||
simp only [lorentzGroupIsGroup_inv]
|
||||
erw [Pi.basisFun_apply, Matrix.mulVec_single_one]
|
||||
rw [← LorentzGroup.coe_inv]
|
||||
rfl
|
||||
|
||||
|
|
|
|||
|
|
@ -33,7 +33,8 @@ lemma rep_apply_stdBasis (g : LorentzGroup d) (μ : Fin 1 ⊕ Fin d) :
|
|||
Finset.sum_singleton, decomp_stdBasis']
|
||||
funext ν
|
||||
simp [LorentzVector.stdBasis, Pi.basisFun_apply]
|
||||
erw [Pi.basisFun_apply, Matrix.mulVec_stdBasis]
|
||||
erw [Pi.basisFun_apply, Matrix.mulVec_single_one]
|
||||
rfl
|
||||
|
||||
end LorentzVector
|
||||
|
||||
|
|
|
|||
|
|
@ -85,6 +85,7 @@ variable {𝓵 : ℝ}
|
|||
variable (μ2 : ℝ)
|
||||
variable (h𝓵 : 0 < 𝓵)
|
||||
|
||||
include h𝓵
|
||||
/-- The second term of the potential is non-negative. -/
|
||||
lemma snd_term_nonneg (φ : HiggsField) (x : SpaceTime) :
|
||||
0 ≤ 𝓵 * ‖φ‖_H ^ 2 x * ‖φ‖_H ^ 2 x := by
|
||||
|
|
@ -93,11 +94,13 @@ lemma snd_term_nonneg (φ : HiggsField) (x : SpaceTime) :
|
|||
simp_all only [normSq, gt_iff_lt, mul_nonneg_iff_of_pos_left, ge_iff_le, norm_nonneg, pow_nonneg,
|
||||
and_self]
|
||||
|
||||
omit h𝓵
|
||||
lemma as_quad (μ2 𝓵 : ℝ) (φ : HiggsField) (x : SpaceTime) :
|
||||
𝓵 * ‖φ‖_H ^ 2 x * ‖φ‖_H ^ 2 x + (- μ2) * ‖φ‖_H ^ 2 x + (- potential μ2 𝓵 φ x) = 0 := by
|
||||
simp only [normSq, neg_mul, potential, neg_add_rev, neg_neg]
|
||||
ring
|
||||
|
||||
include h𝓵
|
||||
/-- The discriminant of the quadratic formed by the potential is non-negative. -/
|
||||
lemma discrim_nonneg (φ : HiggsField) (x : SpaceTime) :
|
||||
0 ≤ discrim 𝓵 (- μ2) (- potential μ2 𝓵 φ x) := by
|
||||
|
|
@ -141,7 +144,7 @@ lemma bounded_below (φ : HiggsField) (x : SpaceTime) :
|
|||
ring_nf at h1
|
||||
rw [← neg_le_iff_add_nonneg'] at h1
|
||||
rw [show 𝓵 * potential μ2 𝓵 φ x * 4 = (4 * 𝓵) * potential μ2 𝓵 φ x by ring] at h1
|
||||
have h2 := (div_le_iff' (by simp [h𝓵] : 0 < 4 * 𝓵)).mpr h1
|
||||
have h2 := (div_le_iff₀' (by simp [h𝓵] : 0 < 4 * 𝓵)).mpr h1
|
||||
ring_nf at h2 ⊢
|
||||
exact h2
|
||||
|
||||
|
|
@ -164,12 +167,14 @@ variable (h𝓵 : 0 < 𝓵)
|
|||
|
||||
-/
|
||||
|
||||
include h𝓵
|
||||
lemma discrim_eq_zero_of_eq_bound (φ : HiggsField) (x : SpaceTime)
|
||||
(hV : potential μ2 𝓵 φ x = - μ2 ^ 2 / (4 * 𝓵)) :
|
||||
discrim 𝓵 (- μ2) (- potential μ2 𝓵 φ x) = 0 := by
|
||||
rw [discrim, hV]
|
||||
field_simp
|
||||
|
||||
include h𝓵
|
||||
lemma normSq_of_eq_bound (φ : HiggsField) (x : SpaceTime)
|
||||
(hV : potential μ2 𝓵 φ x = - μ2 ^ 2 / (4 * 𝓵)) :
|
||||
‖φ‖_H ^ 2 x = μ2 / (2 * 𝓵) := by
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue