feat: Add basics for Pure U(1)
This commit is contained in:
jstoobysmith
parent
ffbba6f051
commit
b9119dccf1
3 changed files with 530 additions and 0 deletions
184
HepLean/AnomalyCancellation/PureU1/Basic.lean
Normal file
184
HepLean/AnomalyCancellation/PureU1/Basic.lean
Normal file
|
|
@ -0,0 +1,184 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.AnomalyCancellation.Basic
|
||||
import Mathlib.Algebra.Module.Equiv
|
||||
import Mathlib.Algebra.BigOperators.Ring
|
||||
import Mathlib.Algebra.BigOperators.Fin
|
||||
/-!
|
||||
# Pure U(1) ACC system.
|
||||
|
||||
We define the anomaly cancellation conditions for a pure U(1) gague theory with `n` fermions.
|
||||
|
||||
-/
|
||||
universe v u
|
||||
open Nat
|
||||
|
||||
|
||||
open Finset
|
||||
|
||||
namespace PureU1
|
||||
open BigOperators
|
||||
|
||||
/-- The vector space of charges. -/
|
||||
@[simps!]
|
||||
def PureU1Charges (n : ℕ) : ACCSystemCharges := ACCSystemChargesMk n
|
||||
|
||||
open BigOperators in
|
||||
/-- The gravitational anomaly. -/
|
||||
def accGrav (n : ℕ) : ((PureU1Charges n).charges →ₗ[ℚ] ℚ) where
|
||||
toFun S := ∑ i : Fin n, S i
|
||||
map_add' S T := Finset.sum_add_distrib
|
||||
map_smul' a S := by
|
||||
simp [HSMul.hSMul, SMul.smul]
|
||||
rw [← Finset.mul_sum]
|
||||
|
||||
|
||||
/-- The symmetric trilinear form used to define the cubic anomaly. -/
|
||||
@[simps!]
|
||||
def accCubeTriLinSymm {n : ℕ} : TriLinearSymm (PureU1Charges n).charges where
|
||||
toFun S := ∑ i, S.1 i * S.2.1 i * S.2.2 i
|
||||
map_smul₁' a S L T := by
|
||||
simp [HSMul.hSMul]
|
||||
rw [Finset.mul_sum]
|
||||
apply Fintype.sum_congr
|
||||
intro i
|
||||
ring
|
||||
map_add₁' S L T R := by
|
||||
simp
|
||||
rw [← Finset.sum_add_distrib]
|
||||
apply Fintype.sum_congr
|
||||
intro i
|
||||
ring
|
||||
swap₁' S L T := by
|
||||
simp
|
||||
apply Fintype.sum_congr
|
||||
intro i
|
||||
ring
|
||||
swap₂' S L T := by
|
||||
simp
|
||||
apply Fintype.sum_congr
|
||||
intro i
|
||||
ring
|
||||
|
||||
lemma accCubeTriLinSymm_cast {n m : ℕ} (h : m = n)
|
||||
(S : (PureU1Charges n).charges × (PureU1Charges n).charges × (PureU1Charges n).charges) :
|
||||
accCubeTriLinSymm S = ∑ i : Fin m,
|
||||
S.1 (Fin.cast h i) * S.2.1 (Fin.cast h i) * S.2.2 (Fin.cast h i) := by
|
||||
rw [← accCubeTriLinSymm.toFun_eq_coe, accCubeTriLinSymm]
|
||||
simp
|
||||
rw [Finset.sum_equiv (Fin.castIso h).symm.toEquiv]
|
||||
intro i
|
||||
simp
|
||||
intro i
|
||||
simp
|
||||
|
||||
/-- The cubic anomaly equation. -/
|
||||
@[simp]
|
||||
def accCube (n : ℕ) : HomogeneousCubic ((PureU1Charges n).charges) :=
|
||||
(accCubeTriLinSymm).toCubic
|
||||
|
||||
|
||||
lemma accCube_explicit (n : ℕ) (S : (PureU1Charges n).charges) :
|
||||
accCube n S = ∑ i : Fin n, S i ^ 3:= by
|
||||
rw [accCube, TriLinearSymm.toCubic]
|
||||
change accCubeTriLinSymm.toFun (S, S, S) = _
|
||||
rw [accCubeTriLinSymm]
|
||||
simp
|
||||
apply Finset.sum_congr
|
||||
simp
|
||||
ring_nf
|
||||
simp
|
||||
|
||||
end PureU1
|
||||
|
||||
/-- The ACC system for a pure $U(1)$ gauge theory with $n$ fermions. -/
|
||||
@[simps!]
|
||||
def PureU1 (n : ℕ) : ACCSystem where
|
||||
numberLinear := 1
|
||||
linearACCs := fun i =>
|
||||
match i with
|
||||
| 0 => PureU1.accGrav n
|
||||
numberQuadratic := 0
|
||||
quadraticACCs := Fin.elim0
|
||||
cubicACC := PureU1.accCube n
|
||||
|
||||
/-- An equivalence of vector spaces of charges when the number of fermions is equal. -/
|
||||
def pureU1EqCharges {n m : ℕ} (h : n = m):
|
||||
(PureU1 n).charges ≃ₗ[ℚ] (PureU1 m).charges where
|
||||
toFun f := f ∘ Fin.cast h.symm
|
||||
invFun f := f ∘ Fin.cast h
|
||||
map_add' _ _ := rfl
|
||||
map_smul' _ _:= rfl
|
||||
left_inv _ := rfl
|
||||
right_inv _ := rfl
|
||||
|
||||
open BigOperators
|
||||
|
||||
lemma pureU1_linear {n : ℕ} (S : (PureU1 n.succ).LinSols) :
|
||||
∑ i, S.val i = 0 := by
|
||||
have hS := S.linearSol
|
||||
simp at hS
|
||||
exact hS 0
|
||||
|
||||
lemma pureU1_cube {n : ℕ} (S : (PureU1 n.succ).Sols) :
|
||||
∑ i, (S.val i) ^ 3 = 0 := by
|
||||
have hS := S.cubicSol
|
||||
erw [PureU1.accCube_explicit] at hS
|
||||
exact hS
|
||||
|
||||
lemma pureU1_last {n : ℕ} (S : (PureU1 n.succ).LinSols) :
|
||||
S.val (Fin.last n) = - ∑ i : Fin n, S.val i.castSucc := by
|
||||
have hS := pureU1_linear S
|
||||
simp at hS
|
||||
rw [Fin.sum_univ_castSucc] at hS
|
||||
linear_combination hS
|
||||
|
||||
lemma pureU1_anomalyFree_ext {n : ℕ} {S T : (PureU1 n.succ).LinSols}
|
||||
(h : ∀ (i : Fin n), S.val i.castSucc = T.val i.castSucc) : S = T := by
|
||||
apply ACCSystemLinear.LinSols.ext
|
||||
funext i
|
||||
by_cases hi : i ≠ Fin.last n
|
||||
have hiCast : ∃ j : Fin n, j.castSucc = i := by
|
||||
exact Fin.exists_castSucc_eq.mpr hi
|
||||
obtain ⟨j, hj⟩ := hiCast
|
||||
rw [← hj]
|
||||
exact h j
|
||||
simp at hi
|
||||
rw [hi]
|
||||
rw [pureU1_last, pureU1_last]
|
||||
simp
|
||||
apply Finset.sum_congr
|
||||
simp
|
||||
intro j _
|
||||
exact h j
|
||||
|
||||
namespace PureU1
|
||||
|
||||
lemma sum_of_charges {n : ℕ} (f : Fin k → (PureU1 n).charges) (j : Fin n) :
|
||||
(∑ i : Fin k, (f i)) j = ∑ i : Fin k, (f i) j := by
|
||||
induction k
|
||||
simp
|
||||
rfl
|
||||
rename_i k hl
|
||||
rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
|
||||
have hlt := hl (f ∘ Fin.castSucc)
|
||||
erw [← hlt]
|
||||
simp
|
||||
|
||||
|
||||
lemma sum_of_anomaly_free_linear {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) :
|
||||
(∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) := by
|
||||
induction k
|
||||
simp
|
||||
rfl
|
||||
rename_i k hl
|
||||
rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
|
||||
have hlt := hl (f ∘ Fin.castSucc)
|
||||
erw [← hlt]
|
||||
simp
|
||||
|
||||
|
||||
end PureU1
|
||||
344
HepLean/AnomalyCancellation/PureU1/Permutations.lean
Normal file
344
HepLean/AnomalyCancellation/PureU1/Permutations.lean
Normal file
|
|
@ -0,0 +1,344 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.AnomalyCancellation.PureU1.Basic
|
||||
import HepLean.AnomalyCancellation.GroupActions
|
||||
import Mathlib.Tactic.Polyrith
|
||||
import Mathlib.RepresentationTheory.Basic
|
||||
import Mathlib.Data.Fin.Tuple.Sort
|
||||
/-!
|
||||
# Permutations of Pure U(1) ACC
|
||||
|
||||
We define the permutation group action on the charges of the Pure U(1) ACC system.
|
||||
We further define the action on the ACC System.
|
||||
|
||||
-/
|
||||
|
||||
universe v u
|
||||
|
||||
open Nat
|
||||
open Finset
|
||||
|
||||
namespace PureU1
|
||||
|
||||
/-- The permutation group of the n-fermions. -/
|
||||
@[simp]
|
||||
def permGroup (n : ℕ) := Equiv.Perm (Fin n)
|
||||
|
||||
instance {n : ℕ} : Group (permGroup n) := by
|
||||
simp [permGroup]
|
||||
infer_instance
|
||||
|
||||
section Charges
|
||||
|
||||
/-- The image of an element of `permGroup` under the representation on charges. -/
|
||||
@[simps!]
|
||||
def chargeMap {n : ℕ} (f : permGroup n) :
|
||||
(PureU1 n).charges →ₗ[ℚ] (PureU1 n).charges where
|
||||
toFun S := S ∘ f.toFun
|
||||
map_add' S T := by
|
||||
funext i
|
||||
simp
|
||||
map_smul' a S := by
|
||||
funext i
|
||||
simp [HSMul.hSMul]
|
||||
-- rw [show Rat.cast a = a from rfl]
|
||||
|
||||
open PureU1Charges in
|
||||
|
||||
/-- The representation of `permGroup` acting on the vector space of charges. -/
|
||||
@[simp]
|
||||
def permCharges {n : ℕ} : Representation ℚ (permGroup n) (PureU1 n).charges where
|
||||
toFun f := chargeMap f⁻¹
|
||||
map_mul' f g :=by
|
||||
simp
|
||||
apply LinearMap.ext
|
||||
intro S
|
||||
funext i
|
||||
rfl
|
||||
map_one' := by
|
||||
apply LinearMap.ext
|
||||
intro S
|
||||
funext i
|
||||
rfl
|
||||
|
||||
lemma accGrav_invariant {n : ℕ} (f : (permGroup n)) (S : (PureU1 n).charges) :
|
||||
PureU1.accGrav n (permCharges f S) = accGrav n S := by
|
||||
simp [accGrav, permCharges]
|
||||
apply (Equiv.Perm.sum_comp _ _ _ ?_)
|
||||
simp
|
||||
|
||||
open BigOperators
|
||||
lemma accCube_invariant {n : ℕ} (f : (permGroup n)) (S : (PureU1 n).charges) :
|
||||
accCube n (permCharges f S) = accCube n S := by
|
||||
rw [accCube_explicit, accCube_explicit]
|
||||
change ∑ i : Fin n, ((((fun a => a^3) ∘ S) (f.symm i))) = _
|
||||
apply (Equiv.Perm.sum_comp _ _ _ ?_)
|
||||
simp
|
||||
|
||||
end Charges
|
||||
|
||||
/-- The permutations acting on the ACC system. -/
|
||||
@[simp]
|
||||
def FamilyPermutations (n : ℕ) : ACCSystemGroupAction (PureU1 n) where
|
||||
group := permGroup n
|
||||
groupInst := inferInstance
|
||||
rep := permCharges
|
||||
linearInvariant := by
|
||||
intro i
|
||||
simp at i
|
||||
match i with
|
||||
| 0 => exact accGrav_invariant
|
||||
quadInvariant := by
|
||||
intro i
|
||||
simp at i
|
||||
exact Fin.elim0 i
|
||||
cubicInvariant := accCube_invariant
|
||||
|
||||
|
||||
lemma FamilyPermutations_charges_apply (S : (PureU1 n).charges)
|
||||
(i : Fin n) (f : (FamilyPermutations n).group) :
|
||||
((FamilyPermutations n).rep f S) i = S (f.invFun i) := by
|
||||
rfl
|
||||
|
||||
lemma FamilyPermutations_anomalyFreeLinear_apply (S : (PureU1 n).LinSols)
|
||||
(i : Fin n) (f : (FamilyPermutations n).group) :
|
||||
((FamilyPermutations n).linSolRep f S).val i = S.val (f.invFun i) := by
|
||||
rfl
|
||||
|
||||
|
||||
/-- The permutation which swaps i and j. TODO: Replace with: `Equiv.swap`. -/
|
||||
def pairSwap {n : ℕ} (i j : Fin n) : (FamilyPermutations n).group where
|
||||
toFun s :=
|
||||
if s = i then
|
||||
j
|
||||
else
|
||||
if s = j then
|
||||
i
|
||||
else
|
||||
s
|
||||
invFun s :=
|
||||
if s = i then
|
||||
j
|
||||
else
|
||||
if s = j then
|
||||
i
|
||||
else
|
||||
s
|
||||
left_inv s := by
|
||||
aesop
|
||||
right_inv s := by
|
||||
aesop
|
||||
|
||||
lemma pairSwap_self_inv {n : ℕ} (i j : Fin n) : (pairSwap i j)⁻¹ = (pairSwap i j) := by
|
||||
rfl
|
||||
|
||||
lemma pairSwap_fst {n : ℕ} (i j : Fin n) : (pairSwap i j).toFun i = j := by
|
||||
simp [pairSwap]
|
||||
|
||||
lemma pairSwap_snd {n : ℕ} (i j : Fin n) : (pairSwap i j).toFun j = i := by
|
||||
simp [pairSwap]
|
||||
|
||||
lemma pairSwap_inv_fst {n : ℕ} (i j : Fin n) : (pairSwap i j).invFun i = j := by
|
||||
simp [pairSwap]
|
||||
|
||||
lemma pairSwap_inv_snd {n : ℕ} (i j : Fin n) : (pairSwap i j).invFun j = i := by
|
||||
simp [pairSwap]
|
||||
|
||||
lemma pairSwap_other {n : ℕ} (i j k : Fin n) (hik : i ≠ k) (hjk : j ≠ k) :
|
||||
(pairSwap i j).toFun k = k := by
|
||||
simp [pairSwap]
|
||||
split
|
||||
simp_all
|
||||
split
|
||||
simp_all
|
||||
rfl
|
||||
|
||||
lemma pairSwap_inv_other {n : ℕ} {i j k : Fin n} (hik : i ≠ k) (hjk : j ≠ k) :
|
||||
(pairSwap i j).invFun k = k := by
|
||||
simp [pairSwap]
|
||||
split
|
||||
simp_all
|
||||
split
|
||||
simp_all
|
||||
rfl
|
||||
|
||||
/-- A permutation of fermions which takes one ordered subset into another. -/
|
||||
noncomputable def permOfInjection (f g : Fin m ↪ Fin n) : (FamilyPermutations n).group :=
|
||||
Equiv.extendSubtype (g.toEquivRange.symm.trans f.toEquivRange)
|
||||
|
||||
section permTwo
|
||||
|
||||
variable {i j i' j' : Fin n} (hij : i ≠ j) (hij' : i' ≠ j')
|
||||
|
||||
/-- Given two distinct elements, an embedding of `Fin 2` into `Fin n`. -/
|
||||
def permTwoInj : Fin 2 ↪ Fin n where
|
||||
toFun s := match s with
|
||||
| 0 => i
|
||||
| 1 => j
|
||||
inj' s1 s2 := by
|
||||
aesop
|
||||
|
||||
lemma permTwoInj_fst : i ∈ Set.range ⇑(permTwoInj hij) := by
|
||||
simp
|
||||
use 0
|
||||
rfl
|
||||
|
||||
lemma permTwoInj_fst_apply :
|
||||
(Function.Embedding.toEquivRange (permTwoInj hij)).symm ⟨i, permTwoInj_fst hij⟩ = 0 := by
|
||||
exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permTwoInj hij))).mpr rfl
|
||||
|
||||
lemma permTwoInj_snd : j ∈ Set.range ⇑(permTwoInj hij) := by
|
||||
simp
|
||||
use 1
|
||||
rfl
|
||||
|
||||
lemma permTwoInj_snd_apply :
|
||||
(Function.Embedding.toEquivRange (permTwoInj hij)).symm
|
||||
⟨j, permTwoInj_snd hij⟩ = 1 := by
|
||||
exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permTwoInj hij))).mpr rfl
|
||||
|
||||
/-- A permutation which swaps `i` with `i'` and `j` with `j'`. -/
|
||||
noncomputable def permTwo : (FamilyPermutations n).group :=
|
||||
permOfInjection (permTwoInj hij) (permTwoInj hij')
|
||||
|
||||
lemma permTwo_fst : (permTwo hij hij').toFun i' = i := by
|
||||
rw [permTwo, permOfInjection]
|
||||
have ht := Equiv.extendSubtype_apply_of_mem
|
||||
((permTwoInj hij').toEquivRange.symm.trans
|
||||
(permTwoInj hij).toEquivRange) i' (permTwoInj_fst hij')
|
||||
simp at ht
|
||||
simp [ht, permTwoInj_fst_apply]
|
||||
rfl
|
||||
|
||||
lemma permTwo_snd : (permTwo hij hij').toFun j' = j := by
|
||||
rw [permTwo, permOfInjection]
|
||||
have ht := Equiv.extendSubtype_apply_of_mem
|
||||
((permTwoInj hij' ).toEquivRange.symm.trans
|
||||
(permTwoInj hij).toEquivRange) j' (permTwoInj_snd hij')
|
||||
simp at ht
|
||||
simp [ht, permTwoInj_snd_apply]
|
||||
rfl
|
||||
|
||||
end permTwo
|
||||
|
||||
section permThree
|
||||
|
||||
variable {i j k i' j' k' : Fin n} (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) (hij' : i' ≠ j')
|
||||
(hjk' : j' ≠ k') (hik' : i' ≠ k')
|
||||
|
||||
/-- Given three distinct elements an embedding of `Fin 3` into `Fin n`. -/
|
||||
def permThreeInj : Fin 3 ↪ Fin n where
|
||||
toFun s := match s with
|
||||
| 0 => i
|
||||
| 1 => j
|
||||
| 2 => k
|
||||
inj' s1 s2 := by
|
||||
aesop
|
||||
|
||||
lemma permThreeInj_fst : i ∈ Set.range ⇑(permThreeInj hij hjk hik) := by
|
||||
simp
|
||||
use 0
|
||||
rfl
|
||||
|
||||
lemma permThreeInj_fst_apply :
|
||||
(Function.Embedding.toEquivRange (permThreeInj hij hjk hik)).symm
|
||||
⟨i, permThreeInj_fst hij hjk hik⟩ = 0 := by
|
||||
exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permThreeInj hij hjk hik))).mpr rfl
|
||||
|
||||
|
||||
lemma permThreeInj_snd : j ∈ Set.range ⇑(permThreeInj hij hjk hik) := by
|
||||
simp
|
||||
use 1
|
||||
rfl
|
||||
|
||||
lemma permThreeInj_snd_apply :
|
||||
(Function.Embedding.toEquivRange (permThreeInj hij hjk hik)).symm
|
||||
⟨j, permThreeInj_snd hij hjk hik⟩ = 1 := by
|
||||
exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permThreeInj hij hjk hik))).mpr rfl
|
||||
|
||||
|
||||
lemma permThreeInj_thd : k ∈ Set.range ⇑(permThreeInj hij hjk hik) := by
|
||||
simp
|
||||
use 2
|
||||
rfl
|
||||
|
||||
lemma permThreeInj_thd_apply :
|
||||
(Function.Embedding.toEquivRange (permThreeInj hij hjk hik)).symm
|
||||
⟨k, permThreeInj_thd hij hjk hik⟩ = 2 := by
|
||||
exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permThreeInj hij hjk hik))).mpr rfl
|
||||
|
||||
/-- A permutation which swaps three distinct elements with another three. -/
|
||||
noncomputable def permThree : (FamilyPermutations n).group :=
|
||||
permOfInjection (permThreeInj hij hjk hik) (permThreeInj hij' hjk' hik')
|
||||
|
||||
lemma permThree_fst : (permThree hij hjk hik hij' hjk' hik').toFun i' = i := by
|
||||
rw [permThree, permOfInjection]
|
||||
have ht := Equiv.extendSubtype_apply_of_mem
|
||||
((permThreeInj hij' hjk' hik').toEquivRange.symm.trans
|
||||
(permThreeInj hij hjk hik).toEquivRange) i' (permThreeInj_fst hij' hjk' hik')
|
||||
simp at ht
|
||||
simp [ht, permThreeInj_fst_apply]
|
||||
rfl
|
||||
|
||||
lemma permThree_snd : (permThree hij hjk hik hij' hjk' hik').toFun j' = j := by
|
||||
rw [permThree, permOfInjection]
|
||||
have ht := Equiv.extendSubtype_apply_of_mem
|
||||
((permThreeInj hij' hjk' hik').toEquivRange.symm.trans
|
||||
(permThreeInj hij hjk hik).toEquivRange) j' (permThreeInj_snd hij' hjk' hik')
|
||||
simp at ht
|
||||
simp [ht, permThreeInj_snd_apply]
|
||||
rfl
|
||||
|
||||
lemma permThree_thd : (permThree hij hjk hik hij' hjk' hik').toFun k' = k := by
|
||||
rw [permThree, permOfInjection]
|
||||
have ht := Equiv.extendSubtype_apply_of_mem
|
||||
((permThreeInj hij' hjk' hik').toEquivRange.symm.trans
|
||||
(permThreeInj hij hjk hik).toEquivRange) k' (permThreeInj_thd hij' hjk' hik')
|
||||
simp at ht
|
||||
simp [ht, permThreeInj_thd_apply]
|
||||
rfl
|
||||
|
||||
end permThree
|
||||
|
||||
lemma Prop_two (P : ℚ × ℚ → Prop) {S : (PureU1 n).LinSols}
|
||||
{a b : Fin n} (hab : a ≠ b)
|
||||
(h : ∀ (f : (FamilyPermutations n).group),
|
||||
P ((((FamilyPermutations n).linSolRep f S).val a),
|
||||
(((FamilyPermutations n).linSolRep f S).val b)
|
||||
)) : ∀ (i j : Fin n) (_ : i ≠ j),
|
||||
P (S.val i, S.val j) := by
|
||||
intro i j hij
|
||||
have h1 := h (permTwo hij hab ).symm
|
||||
rw [FamilyPermutations_anomalyFreeLinear_apply, FamilyPermutations_anomalyFreeLinear_apply] at h1
|
||||
simp at h1
|
||||
change P
|
||||
(S.val ((permTwo hij hab ).toFun a),
|
||||
S.val ((permTwo hij hab ).toFun b)) at h1
|
||||
erw [permTwo_fst,permTwo_snd] at h1
|
||||
exact h1
|
||||
|
||||
lemma Prop_three (P : ℚ × ℚ × ℚ → Prop) {S : (PureU1 n).LinSols}
|
||||
{a b c : Fin n} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
|
||||
(h : ∀ (f : (FamilyPermutations n).group),
|
||||
P ((((FamilyPermutations n).linSolRep f S).val a),(
|
||||
(((FamilyPermutations n).linSolRep f S).val b),
|
||||
(((FamilyPermutations n).linSolRep f S).val c)
|
||||
))) : ∀ (i j k : Fin n) (_ : i ≠ j) (_ : j ≠ k) (_ : i ≠ k),
|
||||
P (S.val i, (S.val j, S.val k)) := by
|
||||
intro i j k hij hjk hik
|
||||
have h1 := h (permThree hij hjk hik hab hbc hac).symm
|
||||
rw [FamilyPermutations_anomalyFreeLinear_apply, FamilyPermutations_anomalyFreeLinear_apply,
|
||||
FamilyPermutations_anomalyFreeLinear_apply] at h1
|
||||
simp at h1
|
||||
change P
|
||||
(S.val ((permThree hij hjk hik hab hbc hac).toFun a),
|
||||
S.val ((permThree hij hjk hik hab hbc hac).toFun b),
|
||||
S.val ((permThree hij hjk hik hab hbc hac).toFun c)) at h1
|
||||
erw [permThree_fst,permThree_snd, permThree_thd] at h1
|
||||
exact h1
|
||||
|
||||
|
||||
end PureU1
|
||||
Loading…
Add table
Add a link
Reference in a new issue