Splitting the linear solutions in the even case into two ACC-satisfying planes

i. Overview

We split the linear solutions of PureU1 (2 * n.succ) into two planes, where every point in either plane satisfies both the linear and cubic anomaly cancellation conditions.

ii. Key results

• P' : The inclusion of the first plane into linear solutions
• P_accCube : The statement that chares from the first plane satisfy the cubic ACC
• P!' : The inclusion of the second plane.
• P!_accCube : The statement that charges from the second plane satisfy the cubic ACC
• span_basis : Every linear solution is the sum of a point from each plane.

iii. Table of contents

• A. Splitting the charges up into groups
  • A.1. The even split: Spltting the charges up via n.succ + n.succ
  • A.2. The shifted even split: Spltting the charges up via 1 + (n + n + 1)
  • A.3. Lemmas relating the two splittings
• B. The first plane
  • B.1. The basis vectors of the first plane as charges
  • B.2. Components of the basis vectors
  • B.3. The basis vectors satisfy the linear ACCs
  • B.4. The basis vectors satisfy the cubic ACC
  • B.5. The basis vectors as linear solutions
  • B.6. The inclusion of the first plane into charges
  • B.7. Components of the inclusion into charges
  • B.8. The inclusion into charges satisfies the linear and cubic ACCs
  • B.9. Kernel of the inclusion into charges
  • B.10. The inclusion of the plane into linear solutions
  • B.11. The basis vectors are linearly independent
  • B.12. Every vector-like even solution is in the span of the basis of the first plane
• C. The vectors of the basis spanning the second plane, via the shifted even split
  • C.2. Components of the vectors
  • C.3. The vectors satisfy the linear ACCs
  • C.4. The vectors satisfy the cubic ACC
  • C.6. The vectors as linear solutions
  • C.7. The inclusion of the second plane into charges
  • C.8. Components of the inclusion into charges
  • C.9. The inclusion into charges satisfies the cubic ACC
  • C.10. Kernel of the inclusion into charges
  • C.11. The inclusion of the second plane into the span of the basis
  • C.12. The inclusion of the plane into linear solutions
  • C.13. The basis vectors are linearly independent
  • C.14. Properties of the basis vectors relating to the span
  • C.15. Permutations as additions of basis vectors
• D. Mixed cubic ACCs involing points from both planes
• E. The combined basis
  • E.1. As a map into linear solutions
  • E.2. Inclusion of the span of the basis into charges
  • E.3. Components of the inclusion into charges
  • E.4. Kernel of the inclusion into charges
  • E.5. The inclusion of the span of the basis into linear solutions
  • E.6. The combined basis vectors are linearly independent
  • E.7. Injectivity of the inclusion into linear solutions
  • E.8. Cardinality of the basis
  • E.9. The basis vectors as a basis
• F. Every Lienar solution is the sum of a point from each plane
  • F.1. Relation under permutations

iv. References

• https://arxiv.org/pdf/1912.04804.pdf

A. Splitting the charges up into groups

We have 2 * n.succ charges, which we split up in the following ways:

| evenFst j (0 to n) | evenSnd j (n.succ to n + n.succ)|

| evenShiftZero (0) | evenShiftFst j (1 to n) |
  evenShiftSnd j (n.succ to 2 * n) | evenShiftLast (2 * n.succ - 1) |

A.1. The even split: Spltting the charges up via n.succ + n.succ

def PureU1.VectorLikeEvenPlane.evenFst {n : ℕ} (j : Fin n.succ) : Fin (2 * n.succ)

The inclusion of Fin n.succ into Fin (n.succ + n.succ) via the first n.succ, casted into Fin (2 * n.succ).

Equations

• PureU1.VectorLikeEvenPlane.evenFst j = Fin.cast ⋯ (Fin.castAdd n.succ j)

def PureU1.VectorLikeEvenPlane.evenSnd {n : ℕ} (j : Fin n.succ) : Fin (2 * n.succ)

The inclusion of Fin n.succ into Fin (n.succ + n.succ) via the second n.succ, casted into Fin (2 * n.succ).

Equations

• PureU1.VectorLikeEvenPlane.evenSnd j = Fin.cast ⋯ (Fin.natAdd n.succ j)

theorem PureU1.VectorLikeEvenPlane.ext_even {n : ℕ} (S T : Fin (2 * n.succ) → ℚ) (h1 : ∀ (i : Fin n.succ), S (evenFst i) = T (evenFst i)) (h2 : ∀ (i : Fin n.succ), S (evenSnd i) = T (evenSnd i)) : S = T

theorem PureU1.VectorLikeEvenPlane.sum_even {n : ℕ} (S : Fin (2 * n.succ) → ℚ) : ∑ i : Fin (2 * n.succ), S i = ∑ i : Fin n.succ, ((S ∘ evenFst) i + (S ∘ evenSnd) i)

A.2. The shifted even split: Spltting the charges up via 1 + (n + n + 1)

theorem PureU1.VectorLikeEvenPlane.n_cond₂ (n : ℕ) : 1 + (n + n + 1) = 2 * n.succ

def PureU1.VectorLikeEvenPlane.evenShiftFst {n : ℕ} (j : Fin n) : Fin (2 * n.succ)

The inclusion of Fin n into Fin (1 + (n + n + 1)) via the first n, casted into Fin (2 * n.succ).

Equations

• PureU1.VectorLikeEvenPlane.evenShiftFst j = Fin.cast ⋯ (Fin.natAdd 1 (Fin.castAdd 1 (Fin.castAdd n j)))

def PureU1.VectorLikeEvenPlane.evenShiftSnd {n : ℕ} (j : Fin n) : Fin (2 * n.succ)

The inclusion of Fin n into Fin (1 + (n + n + 1)) via the second n, casted into Fin (2 * n.succ).

Equations

• PureU1.VectorLikeEvenPlane.evenShiftSnd j = Fin.cast ⋯ (Fin.natAdd 1 (Fin.castAdd 1 (Fin.natAdd n j)))

def PureU1.VectorLikeEvenPlane.evenShiftZero {n : ℕ} : Fin (2 * n.succ)

The element of Fin (1 + (n + n + 1)) corresponding to the first 1, casted into Fin (2 * n.succ).

Equations

• PureU1.VectorLikeEvenPlane.evenShiftZero = Fin.cast ⋯ (Fin.castAdd (n + n + 1) 0)

def PureU1.VectorLikeEvenPlane.evenShiftLast {n : ℕ} : Fin (2 * n.succ)

The element of Fin (1 + (n + n + 1)) corresponding to the second 1, casted into Fin (2 * n.succ).

Equations

• PureU1.VectorLikeEvenPlane.evenShiftLast = Fin.cast ⋯ (Fin.natAdd 1 (Fin.natAdd (n + n) 0))

theorem PureU1.VectorLikeEvenPlane.sum_evenShift {n : ℕ} (S : Fin (2 * n.succ) → ℚ) : ∑ i : Fin (2 * n.succ), S i = S evenShiftZero + S evenShiftLast + ∑ i : Fin n, ((S ∘ evenShiftFst) i + (S ∘ evenShiftSnd) i)

A.3. Lemmas relating the two splittings

theorem PureU1.VectorLikeEvenPlane.evenShiftZero_eq_evenFst_zero {n : ℕ} : evenShiftZero = evenFst 0

theorem PureU1.VectorLikeEvenPlane.evenShiftLast_eq_evenSnd_last {n : ℕ} : evenShiftLast = evenSnd (Fin.last n)

theorem PureU1.VectorLikeEvenPlane.evenShiftFst_eq_evenFst_succ {n : ℕ} (j : Fin n) : evenShiftFst j = evenFst j.succ

theorem PureU1.VectorLikeEvenPlane.evenShiftSnd_eq_evenSnd_castSucc {n : ℕ} (j : Fin n) : evenShiftSnd j = evenSnd j.castSucc

B. The first plane

B.1. The basis vectors of the first plane as charges

def PureU1.VectorLikeEvenPlane.basisAsCharges {n : ℕ} (j : Fin n.succ) : (PureU1 (2 * n.succ)).Charges

The first part of the basis as charges.

Equations

• PureU1.VectorLikeEvenPlane.basisAsCharges j i = if i = PureU1.VectorLikeEvenPlane.evenFst j then 1 else if i = PureU1.VectorLikeEvenPlane.evenSnd j then -1 else 0

B.2. Components of the basis vectors

theorem PureU1.VectorLikeEvenPlane.basis_on_evenFst_self {n : ℕ} (j : Fin n.succ) : basisAsCharges j (evenFst j) = 1

theorem PureU1.VectorLikeEvenPlane.basis_on_evenFst_other {n : ℕ} {k j : Fin n.succ} (h : k ≠ j) : basisAsCharges k (evenFst j) = 0

theorem PureU1.VectorLikeEvenPlane.basis_on_other {n : ℕ} {k : Fin n.succ} {j : Fin (2 * n.succ)} (h1 : j ≠ evenFst k) (h2 : j ≠ evenSnd k) : basisAsCharges k j = 0

theorem PureU1.VectorLikeEvenPlane.basis_evenSnd_eq_neg_evenFst {n : ℕ} (j i : Fin n.succ) : basisAsCharges j (evenSnd i) = -basisAsCharges j (evenFst i)

theorem PureU1.VectorLikeEvenPlane.basis_on_evenSnd_self {n : ℕ} (j : Fin n.succ) : basisAsCharges j (evenSnd j) = -1

theorem PureU1.VectorLikeEvenPlane.basis_on_evenSnd_other {n : ℕ} {k j : Fin n.succ} (h : k ≠ j) : basisAsCharges k (evenSnd j) = 0

B.3. The basis vectors satisfy the linear ACCs

theorem PureU1.VectorLikeEvenPlane.basis_linearACC {n : ℕ} (j : Fin n.succ) : (accGrav (2 * n.succ)) (basisAsCharges j) = 0

B.4. The basis vectors satisfy the cubic ACC

theorem PureU1.VectorLikeEvenPlane.basis_accCube {n : ℕ} (j : Fin n.succ) : (accCube (2 * n.succ)) (basisAsCharges j) = 0

B.5. The basis vectors as linear solutions

def PureU1.VectorLikeEvenPlane.basis {n : ℕ} (j : Fin n.succ) : (PureU1 (2 * n.succ)).LinSols

The first part of the basis as LinSols.

Equations

• PureU1.VectorLikeEvenPlane.basis j = { val := PureU1.VectorLikeEvenPlane.basisAsCharges j, linearSol := ⋯ }

@[simp]

theorem PureU1.VectorLikeEvenPlane.basis_val {n : ℕ} (j : Fin n.succ) : (basis j).val = basisAsCharges j

B.6. The inclusion of the first plane into charges

def PureU1.VectorLikeEvenPlane.P {n : ℕ} (f : Fin n.succ → ℚ) : (PureU1 (2 * n.succ)).Charges

A point in the span of the first part of the basis as a charge.

Equations

• PureU1.VectorLikeEvenPlane.P f = ∑ i : Fin n.succ, f i • PureU1.VectorLikeEvenPlane.basisAsCharges i

B.7. Components of the inclusion into charges

theorem PureU1.VectorLikeEvenPlane.P_evenFst {n : ℕ} (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (evenFst j) = f j

theorem PureU1.VectorLikeEvenPlane.P_evenSnd {n : ℕ} (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (evenSnd j) = -f j

theorem PureU1.VectorLikeEvenPlane.P_evenSnd_evenFst {n : ℕ} (f : Fin n.succ → ℚ) : P f ∘ evenSnd = -P f ∘ evenFst

B.8. The inclusion into charges satisfies the linear and cubic ACCs

theorem PureU1.VectorLikeEvenPlane.P_linearACC {n : ℕ} (f : Fin n.succ → ℚ) : (accGrav (2 * n.succ)) (P f) = 0

theorem PureU1.VectorLikeEvenPlane.P_accCube {n : ℕ} (f : Fin n.succ → ℚ) : (accCube (2 * n.succ)) (P f) = 0

B.9. Kernel of the inclusion into charges

theorem PureU1.VectorLikeEvenPlane.P_zero {n : ℕ} (f : Fin n.succ → ℚ) (h : P f = 0) (i : Fin n.succ) : f i = 0

B.10. The inclusion of the plane into linear solutions

def PureU1.VectorLikeEvenPlane.P' {n : ℕ} (f : Fin n.succ → ℚ) : (PureU1 (2 * n.succ)).LinSols

A point in the span of the first part of the basis.

Equations

• PureU1.VectorLikeEvenPlane.P' f = ∑ i : Fin n.succ, f i • PureU1.VectorLikeEvenPlane.basis i

theorem PureU1.VectorLikeEvenPlane.P'_val {n : ℕ} (f : Fin n.succ → ℚ) : (P' f).val = P f

B.11. The basis vectors are linearly independent

theorem PureU1.VectorLikeEvenPlane.basis_linear_independent {n : ℕ} : LinearIndependent ℚ basis

B.12. Every vector-like even solution is in the span of the basis of the first plane

theorem PureU1.VectorLikeEvenPlane.vectorLikeEven_in_span {n : ℕ} (S : (PureU1 (2 * n.succ)).LinSols) (hS : VectorLikeEven S.val) : ∃ (M : (FamilyPermutations (2 * n.succ)).group), ((FamilyPermutations (2 * n.succ)).linSolRep M) S ∈ Submodule.span ℚ (Set.range basis)

C. The vectors of the basis spanning the second plane, via the shifted even split

def PureU1.VectorLikeEvenPlane.basis!AsCharges {n : ℕ} (j : Fin n) : (PureU1 (2 * n.succ)).Charges

The second part of the basis as charges.

Equations

• PureU1.VectorLikeEvenPlane.basis!AsCharges j i = if i = PureU1.VectorLikeEvenPlane.evenShiftFst j then 1 else if i = PureU1.VectorLikeEvenPlane.evenShiftSnd j then -1 else 0

C.2. Components of the vectors

theorem PureU1.VectorLikeEvenPlane.basis!_on_evenShiftFst_self {n : ℕ} (j : Fin n) : basis!AsCharges j (evenShiftFst j) = 1

theorem PureU1.VectorLikeEvenPlane.basis!_on_other {n : ℕ} {k : Fin n} {j : Fin (2 * n.succ)} (h1 : j ≠ evenShiftFst k) (h2 : j ≠ evenShiftSnd k) : basis!AsCharges k j = 0

theorem PureU1.VectorLikeEvenPlane.basis!_on_evenShiftFst_other {n : ℕ} {k j : Fin n} (h : k ≠ j) : basis!AsCharges k (evenShiftFst j) = 0

theorem PureU1.VectorLikeEvenPlane.basis!_evenShftSnd_eq_neg_evenShiftFst {n : ℕ} (j i : Fin n) : basis!AsCharges j (evenShiftSnd i) = -basis!AsCharges j (evenShiftFst i)

theorem PureU1.VectorLikeEvenPlane.basis!_on_evenShiftSnd_self {n : ℕ} (j : Fin n) : basis!AsCharges j (evenShiftSnd j) = -1

theorem PureU1.VectorLikeEvenPlane.basis!_on_evenShiftSnd_other {n : ℕ} {k j : Fin n} (h : k ≠ j) : basis!AsCharges k (evenShiftSnd j) = 0

theorem PureU1.VectorLikeEvenPlane.basis!_on_evenShiftZero {n : ℕ} (j : Fin n) : basis!AsCharges j evenShiftZero = 0

theorem PureU1.VectorLikeEvenPlane.basis!_on_evenShiftLast {n : ℕ} (j : Fin n) : basis!AsCharges j evenShiftLast = 0

C.3. The vectors satisfy the linear ACCs

theorem PureU1.VectorLikeEvenPlane.basis!_linearACC {n : ℕ} (j : Fin n) : (accGrav (2 * n.succ)) (basis!AsCharges j) = 0

C.4. The vectors satisfy the cubic ACC

theorem PureU1.VectorLikeEvenPlane.basis!_accCube {n : ℕ} (j : Fin n) : (accCube (2 * n.succ)) (basis!AsCharges j) = 0

C.6. The vectors as linear solutions

def PureU1.VectorLikeEvenPlane.basis! {n : ℕ} (j : Fin n) : (PureU1 (2 * n.succ)).LinSols

The second part of the basis as LinSols.

Equations

• PureU1.VectorLikeEvenPlane.basis! j = { val := PureU1.VectorLikeEvenPlane.basis!AsCharges j, linearSol := ⋯ }

@[simp]

theorem PureU1.VectorLikeEvenPlane.basis!_val {n : ℕ} (j : Fin n) : (basis! j).val = basis!AsCharges j

C.7. The inclusion of the second plane into charges

def PureU1.VectorLikeEvenPlane.P! {n : ℕ} (f : Fin n → ℚ) : (PureU1 (2 * n.succ)).Charges

A point in the span of the second part of the basis as a charge.

Equations

• PureU1.VectorLikeEvenPlane.P! f = ∑ i : Fin n, f i • PureU1.VectorLikeEvenPlane.basis!AsCharges i

C.8. Components of the inclusion into charges

theorem PureU1.VectorLikeEvenPlane.P!_evenShiftFst {n : ℕ} (f : Fin n → ℚ) (j : Fin n) : P! f (evenShiftFst j) = f j

theorem PureU1.VectorLikeEvenPlane.P!_evenShiftSnd {n : ℕ} (f : Fin n → ℚ) (j : Fin n) : P! f (evenShiftSnd j) = -f j

theorem PureU1.VectorLikeEvenPlane.P!_evenShiftZero {n : ℕ} (f : Fin n → ℚ) : P! f evenShiftZero = 0

theorem PureU1.VectorLikeEvenPlane.P!_evenShiftLast {n : ℕ} (f : Fin n → ℚ) : P! f evenShiftLast = 0

C.9. The inclusion into charges satisfies the cubic ACC

theorem PureU1.VectorLikeEvenPlane.P!_accCube {n : ℕ} (f : Fin n → ℚ) : (accCube (2 * n.succ)) (P! f) = 0

C.10. Kernel of the inclusion into charges

theorem PureU1.VectorLikeEvenPlane.P!_zero {n : ℕ} (f : Fin n → ℚ) (h : P! f = 0) (i : Fin n) : f i = 0

C.11. The inclusion of the second plane into the span of the basis

theorem PureU1.VectorLikeEvenPlane.P!_in_span {n : ℕ} (f : Fin n → ℚ) : P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges)

C.12. The inclusion of the plane into linear solutions

def PureU1.VectorLikeEvenPlane.P!' {n : ℕ} (f : Fin n → ℚ) : (PureU1 (2 * n.succ)).LinSols

A point in the span of the second part of the basis.

Equations

• PureU1.VectorLikeEvenPlane.P!' f = ∑ i : Fin n, f i • PureU1.VectorLikeEvenPlane.basis! i

theorem PureU1.VectorLikeEvenPlane.P!'_val {n : ℕ} (f : Fin n → ℚ) : (P!' f).val = P! f

C.13. The basis vectors are linearly independent

theorem PureU1.VectorLikeEvenPlane.basis!_linear_independent {n : ℕ} : LinearIndependent ℚ basis!

C.14. Properties of the basis vectors relating to the span

theorem PureU1.VectorLikeEvenPlane.smul_basis!AsCharges_in_span {n : ℕ} (S : (PureU1 (2 * n.succ)).LinSols) (j : Fin n) : (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∈ Submodule.span ℚ (Set.range basis!AsCharges)

C.15. Permutations as additions of basis vectors

theorem PureU1.VectorLikeEvenPlane.swap!_as_add {n : ℕ} {S S' : (PureU1 (2 * n.succ)).LinSols} (j : Fin n) (hS : ((FamilyPermutations (2 * n.succ)).linSolRep (pairSwap (evenShiftFst j) (evenShiftSnd j))) S = S') : S'.val = S.val + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j

Swapping the elements evenShiftFst j and evenShiftSnd j is equivalent to adding a vector basis!AsCharges j.

D. Mixed cubic ACCs involing points from both planes

theorem PureU1.VectorLikeEvenPlane.P_P_P!_accCube {n : ℕ} (g : Fin n.succ → ℚ) (j : Fin n) : ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = g j.succ ^ 2 - g j.castSucc ^ 2

theorem PureU1.VectorLikeEvenPlane.P_P!_P!_accCube {n : ℕ} (g : Fin n → ℚ) (j : Fin n.succ) : ((accCubeTriLinSymm (P! g)) (P! g)) (basisAsCharges j) = P! g (evenFst j) ^ 2 - P! g (evenSnd j) ^ 2

E. The combined basis

E.1. As a map into linear solutions

def PureU1.VectorLikeEvenPlane.basisa {n : ℕ} : Fin n.succ ⊕ Fin n → (PureU1 (2 * n.succ)).LinSols

The whole basis as LinSols.

Equations

• PureU1.VectorLikeEvenPlane.basisa (Sum.inl i_2) = PureU1.VectorLikeEvenPlane.basis i_2
• PureU1.VectorLikeEvenPlane.basisa (Sum.inr i_2) = PureU1.VectorLikeEvenPlane.basis! i_2

E.2. Inclusion of the span of the basis into charges

def PureU1.VectorLikeEvenPlane.Pa {n : ℕ} (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : (PureU1 (2 * n.succ)).Charges

A point in the span of the basis as a charge.

Equations

• PureU1.VectorLikeEvenPlane.Pa f g = PureU1.VectorLikeEvenPlane.P f + PureU1.VectorLikeEvenPlane.P! g

E.3. Components of the inclusion into charges

theorem PureU1.VectorLikeEvenPlane.Pa_evenShiftFst {n : ℕ} (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) : Pa f g (evenShiftFst j) = f j.succ + g j

theorem PureU1.VectorLikeEvenPlane.Pa_evenShiftSnd {n : ℕ} (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) : Pa f g (evenShiftSnd j) = -f j.castSucc - g j

theorem PureU1.VectorLikeEvenPlane.Pa_evenShitZero {n : ℕ} (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : Pa f g evenShiftZero = f 0

theorem PureU1.VectorLikeEvenPlane.Pa_evenShiftLast {n : ℕ} (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : Pa f g evenShiftLast = -f (Fin.last n)

E.4. Kernel of the inclusion into charges

theorem PureU1.VectorLikeEvenPlane.Pa_zero {n : ℕ} (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) (i : Fin n.succ) : f i = 0

theorem PureU1.VectorLikeEvenPlane.Pa_zero! {n : ℕ} (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) (i : Fin n) : g i = 0

E.5. The inclusion of the span of the basis into linear solutions

def PureU1.VectorLikeEvenPlane.Pa' {n : ℕ} (f : Fin n.succ ⊕ Fin n → ℚ) : (PureU1 (2 * n.succ)).LinSols

A point in the span of the whole basis.

Equations

• PureU1.VectorLikeEvenPlane.Pa' f = ∑ i : Fin n.succ ⊕ Fin n, f i • PureU1.VectorLikeEvenPlane.basisa i

theorem PureU1.VectorLikeEvenPlane.Pa'_P'_P!' {n : ℕ} (f : Fin n.succ ⊕ Fin n → ℚ) : Pa' f = P' (f ∘ Sum.inl) + P!' (f ∘ Sum.inr)

E.6. The combined basis vectors are linearly independent

theorem PureU1.VectorLikeEvenPlane.basisa_linear_independent {n : ℕ} : LinearIndependent ℚ basisa

E.7. Injectivity of the inclusion into linear solutions

theorem PureU1.VectorLikeEvenPlane.Pa'_eq {n : ℕ} (f f' : Fin n.succ ⊕ Fin n → ℚ) : Pa' f = Pa' f' ↔ f = f'

theorem PureU1.VectorLikeEvenPlane.Pa'_elim_eq_iff {n : ℕ} (g g' : Fin n.succ → ℚ) (f f' : Fin n → ℚ) : Pa' (Sum.elim g f) = Pa' (Sum.elim g' f') ↔ Pa g f = Pa g' f'

theorem PureU1.VectorLikeEvenPlane.Pa_eq {n : ℕ} (g g' : Fin n.succ → ℚ) (f f' : Fin n → ℚ) : Pa g f = Pa g' f' ↔ g = g' ∧ f = f'

E.8. Cardinality of the basis

theorem PureU1.VectorLikeEvenPlane.basisa_card {n : ℕ} : Fintype.card (Fin n.succ ⊕ Fin n) = Module.finrank ℚ (PureU1 (2 * n.succ)).LinSols

E.9. The basis vectors as a basis

noncomputable def PureU1.VectorLikeEvenPlane.basisaAsBasis {n : ℕ} : Module.Basis (Fin n.succ ⊕ Fin n) ℚ (PureU1 (2 * n.succ)).LinSols

The basis formed out of our basisa vectors.

Equations

• PureU1.VectorLikeEvenPlane.basisaAsBasis = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

F. Every Lienar solution is the sum of a point from each plane

theorem PureU1.VectorLikeEvenPlane.span_basis {n : ℕ} (S : (PureU1 (2 * n.succ)).LinSols) : ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = P g + P! f

F.1. Relation under permutations

theorem PureU1.VectorLikeEvenPlane.span_basis_swap! {n : ℕ} {S' S : (PureU1 (2 * n.succ)).LinSols} (j : Fin n) (hS : ((FamilyPermutations (2 * n.succ)).linSolRep (pairSwap (evenShiftFst j) (evenShiftSnd j))) S = S') (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (h : S.val = P g + P! f) : ∃ (g' : Fin n.succ → ℚ) (f' : Fin n → ℚ), S'.val = P g' + P! f' ∧ P! f' = P! f + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∧ g' = g