Basis of LinSols

We give a basis of vector space LinSols, and find the rank thereof.

def PureU1.BasisLinear.asCharges {n : ℕ} (j : Fin n) : (PureU1 n.succ).Charges

The basis elements as charges, defined to have a 1 in the jth position and a -1 in the last position.

Equations

• PureU1.BasisLinear.asCharges j i = if i = j.castSucc then 1 else if i = Fin.last n then -1 else 0

theorem PureU1.BasisLinear.asCharges_eq_castSucc {n : ℕ} (j : Fin n) : asCharges j j.castSucc = 1

theorem PureU1.BasisLinear.asCharges_ne_castSucc {n : ℕ} {k j : Fin n} (h : k ≠ j) : asCharges k j.castSucc = 0

def PureU1.BasisLinear.asLinSols {n : ℕ} (j : Fin n) : (PureU1 n.succ).LinSols

The basis elements as LinSols.

Equations

• PureU1.BasisLinear.asLinSols j = { val := PureU1.BasisLinear.asCharges j, linearSol := ⋯ }

@[simp]

theorem PureU1.BasisLinear.asLinSols_val {n : ℕ} (j : Fin n) : (asLinSols j).val = asCharges j

theorem PureU1.BasisLinear.sum_of_vectors {k n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) : (∑ i : Fin k, f i).val j = ∑ i : Fin k, (f i).val j

noncomputable def PureU1.BasisLinear.coordinateMap {n : ℕ} : (PureU1 n.succ).LinSols ≃ₗ[ℚ] Fin n →₀ ℚ

The coordinate map for the basis.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PureU1.BasisLinear.asBasis {n : ℕ} : Module.Basis (Fin n) ℚ (PureU1 n.succ).LinSols

The basis of LinSols.

Equations

• PureU1.BasisLinear.asBasis = { repr := PureU1.BasisLinear.coordinateMap }

instance PureU1.BasisLinear.instFiniteRatLinSolsSucc {n : ℕ} : Module.Finite ℚ (PureU1 n.succ).LinSols

The module over ℚ defined by linear solutions to the pure U(1) ACCs is finite.

theorem PureU1.BasisLinear.finrank_AnomalyFreeLinear {n : ℕ} : Module.finrank ℚ (PureU1 n.succ).LinSols = n

The module of solutions to the linear pure-U(1) acc has rank equal to n.