Imports
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.QFT.QED.AnomalyCancellation.Basic
public import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
Basis of LinSols
We give a basis of vector space LinSols, and find the rank thereof.
@[expose] public section
The basis elements as charges, defined to have a 1 in the jth position and a -1 in the
last position.
def asCharges (j : Fin n) : (PureU1 n.succ).Charges :=
(fun i =>
if i = j.castSucc then 1
else if i = Fin.last n then
- 1
else 0)lemma asCharges_eq_castSucc (j : Fin n) :
asCharges j (Fin.castSucc j) = 1 := n:ℕj:Fin n⊢ asCharges j j.castSucc = 1
All goals completed! 🐙lemma asCharges_ne_castSucc {k j : Fin n} (h : k ≠ j) :
asCharges k ⟨j, n:ℕk:Fin nj:Fin nh:k ≠ j⊢ ↑j < (PureU1 n.succ).numberCharges All goals completed! 🐙⟩= 0 := n:ℕk:Fin nj:Fin nh:k ≠ j⊢ asCharges k ⟨↑j, ⋯⟩ = 0
n:ℕk:Fin nj:Fin nh:k ≠ j⊢ (if ↑j = ↑k then 1 else if ↑j = n then -1 else 0) = 0
All goals completed! 🐙
The basis elements as LinSols.
set_option backward.isDefEq.respectTransparency false inn:ℕj:Fin ni:Fin (PureU1 n.succ).numberLinearisLt✝:0 < (PureU1 n.succ).numberLinear⊢ asCharges j j.castSucc + asCharges j (Fin.last n) = 0n:ℕj:Fin ni:Fin (PureU1 n.succ).numberLinearisLt✝:0 < (PureU1 n.succ).numberLinear⊢ ∀ b ∈ Finset.univ, b ≠ j → asCharges j b.castSucc = 0n:ℕj:Fin ni:Fin (PureU1 n.succ).numberLinearisLt✝:0 < (PureU1 n.succ).numberLinear⊢ j ∉ Finset.univ → asCharges j j.castSucc = 0
n:ℕj:Fin ni:Fin (PureU1 n.succ).numberLinearisLt✝:0 < (PureU1 n.succ).numberLinear⊢ asCharges j j.castSucc + asCharges j (Fin.last n) = 0 n:ℕj:Fin ni:Fin (PureU1 n.succ).numberLinearisLt✝:0 < (PureU1 n.succ).numberLinear⊢ (1 + if Fin.last n = j.castSucc then 1 else -1) = 0
n:ℕj:Fin ni:Fin (PureU1 n.succ).numberLinearisLt✝:0 < (PureU1 n.succ).numberLinearhn:¬Fin.last n = j.castSucc⊢ (1 + if Fin.last n = j.castSucc then 1 else -1) = 0
n:ℕj:Fin ni:Fin (PureU1 n.succ).numberLinearisLt✝:0 < (PureU1 n.succ).numberLinearhn:¬Fin.last n = j.castSucch✝:Fin.last n = j.castSucc⊢ 1 + 1 = 0n:ℕj:Fin ni:Fin (PureU1 n.succ).numberLinearisLt✝:0 < (PureU1 n.succ).numberLinearhn:¬Fin.last n = j.castSucch✝:¬Fin.last n = j.castSucc⊢ 1 + -1 = 0
n:ℕj:Fin ni:Fin (PureU1 n.succ).numberLinearisLt✝:0 < (PureU1 n.succ).numberLinearhn:¬Fin.last n = j.castSucch✝:Fin.last n = j.castSucc⊢ 1 + 1 = 0 n:ℕj:Fin ni:Fin (PureU1 n.succ).numberLinearisLt✝:0 < (PureU1 n.succ).numberLinearhn:¬Fin.last n = j.castSuccht:Fin.last n = j.castSucc⊢ 1 + 1 = 0
All goals completed! 🐙
n:ℕj:Fin ni:Fin (PureU1 n.succ).numberLinearisLt✝:0 < (PureU1 n.succ).numberLinearhn:¬Fin.last n = j.castSucch✝:¬Fin.last n = j.castSucc⊢ 1 + -1 = 0 with_unfolding_all All goals completed! 🐙
n:ℕj:Fin ni:Fin (PureU1 n.succ).numberLinearisLt✝:0 < (PureU1 n.succ).numberLinear⊢ ∀ b ∈ Finset.univ, b ≠ j → asCharges j b.castSucc = 0 n:ℕj:Fin ni:Fin (PureU1 n.succ).numberLinearisLt✝:0 < (PureU1 n.succ).numberLineark:Fin na✝:k ∈ Finset.univhkj:k ≠ j⊢ asCharges j k.castSucc = 0
All goals completed! 🐙
n:ℕj:Fin ni:Fin (PureU1 n.succ).numberLinearisLt✝:0 < (PureU1 n.succ).numberLinear⊢ j ∉ Finset.univ → asCharges j j.castSucc = 0 n:ℕj:Fin ni:Fin (PureU1 n.succ).numberLinearisLt✝:0 < (PureU1 n.succ).numberLinearhk:j ∉ Finset.univ⊢ asCharges j j.castSucc = 0
All goals completed! 🐙⟩lemma sum_of_vectors {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) :
(∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) :=
sum_of_anomaly_free_linear (fun i => f i) j
The module over ℚ defined by linear solutions to the pure U(1) ACCs is finite.
The module of solutions to the linear pure-U(1) acc has rank equal to n.
lemma finrank_AnomalyFreeLinear :
Module.finrank ℚ (((PureU1 n.succ).LinSols)) = n := n:ℕ⊢ finrank ℚ (PureU1 n.succ).LinSols = n
n:ℕh:↑(finrank ℚ (PureU1 n.succ).LinSols) = Cardinal.mk (Fin n)⊢ finrank ℚ (PureU1 n.succ).LinSols = n
n:ℕh:Module.rank ℚ (PureU1 (n + 1)).LinSols = ↑n⊢ finrank ℚ (PureU1 n.succ).LinSols = n
All goals completed! 🐙