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

i. Overview

We split the linear solutions of PureU1 (2 * n + 1) 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 symmetric split: Spltting the charges up via (n + 1) + 1
  • A.2. The shifted split: Spltting the charges up via 1 + n + n
  • A.3. The shifte shifted split: Spltting the charges up via ((1+n)+1) + n.succ
  • A.4. Relating the splittings together
• B. The first plane
  • B.1. The basis vectors of the first plane as charges
  • B.2. Components of the basis vectors as charges
  • B.3. The basis vectors satisfy the linear ACCs
  • B.4. The basis vectors as LinSols
  • B.5. The inclusion of the first plane into charges
  • B.6. Components of the first plane
  • B.7. Points on the first plane satisfies the ACCs
  • B.8. Kernal of the inclusion into charges
  • B.9. The basis vectors are linearly independent
• C. The second plane
  • C.1. The basis vectors of the second plane as charges
  • C.2. Components of the basis vectors as charges
  • C.3. The basis vectors satisfy the linear ACCs
  • C.4. The basis vectors as LinSols
  • C.5. Permutations equal adding basis vectors
  • C.6. The inclusion of the second plane into charges
  • C.7. Components of the second plane
  • C.8. Points on the second plane satisfies the ACCs
  • C.9. Kernal of the inclusion into charges
  • C.10. The inclusion of the second plane into LinSols
  • C.11. The basis vectors are linearly independent
• D. The mixed cubic ACC from points in both planes
• E. The combined basis
  • E.1. The combined basis as LinSols
  • E.2. The inclusion of the span of the combined basis into charges
  • E.3. Components of the inclusion
  • E.4. Kernal of the inclusion into charges
  • E.5. The inclusion of the span of the combined basis into LinSols
  • 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 + 1 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 symmetric split: Spltting the charges up via (n + 1) + 1

theorem PureU1.VectorLikeOddPlane.odd_shift_eq (n : ℕ) : 1 + n + n = 2 * n + 1

def PureU1.VectorLikeOddPlane.oddFst {n : ℕ} (j : Fin n) : Fin (2 * n + 1)

The inclusion of Fin n into Fin ((n + 1) + n) via the first n. This is then casted to Fin (2 * n + 1).

Equations

• PureU1.VectorLikeOddPlane.oddFst j = Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd 1 j))

def PureU1.VectorLikeOddPlane.oddSnd {n : ℕ} (j : Fin n) : Fin (2 * n + 1)

The inclusion of Fin n into Fin ((n + 1) + n) via the second n. This is then casted to Fin (2 * n + 1).

Equations

• PureU1.VectorLikeOddPlane.oddSnd j = Fin.cast ⋯ (Fin.natAdd (n + 1) j)

def PureU1.VectorLikeOddPlane.oddMid {n : ℕ} : Fin (2 * n + 1)

The element representing 1 in Fin ((n + 1) + n). This is then casted to Fin (2 * n + 1).

Equations

• PureU1.VectorLikeOddPlane.oddMid = Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd n 1))

theorem PureU1.VectorLikeOddPlane.sum_odd {n : ℕ} (S : Fin (2 * n + 1) → ℚ) : ∑ i : Fin (2 * n + 1), S i = S oddMid + ∑ i : Fin n, ((S ∘ oddFst) i + (S ∘ oddSnd) i)

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

def PureU1.VectorLikeOddPlane.oddShiftFst {n : ℕ} (j : Fin n) : Fin (2 * n + 1)

The inclusion of Fin n into Fin (1 + n + n) via the first n. This is then casted to Fin (2 * n + 1).

Equations

• PureU1.VectorLikeOddPlane.oddShiftFst j = Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd 1 j))

def PureU1.VectorLikeOddPlane.oddShiftSnd {n : ℕ} (j : Fin n) : Fin (2 * n + 1)

The inclusion of Fin n into Fin (1 + n + n) via the second n. This is then casted to Fin (2 * n + 1).

Equations

• PureU1.VectorLikeOddPlane.oddShiftSnd j = Fin.cast ⋯ (Fin.natAdd (1 + n) j)

def PureU1.VectorLikeOddPlane.oddShiftZero {n : ℕ} : Fin (2 * n + 1)

The element representing the 1 in Fin (1 + n + n). This is then casted to Fin (2 * n + 1).

Equations

• PureU1.VectorLikeOddPlane.oddShiftZero = Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd n 1))

theorem PureU1.VectorLikeOddPlane.sum_oddShift {n : ℕ} (S : Fin (2 * n + 1) → ℚ) : ∑ i : Fin (2 * n + 1), S i = S oddShiftZero + ∑ i : Fin n, ((S ∘ oddShiftFst) i + (S ∘ oddShiftSnd) i)

A.3. The shifte shifted split: Spltting the charges up via ((1+n)+1) + n.succ

theorem PureU1.VectorLikeOddPlane.odd_shift_shift_eq (n : ℕ) : 1 + n + 1 + n.succ = 2 * n.succ + 1

def PureU1.VectorLikeOddPlane.oddShiftShiftZero {n : ℕ} : Fin (2 * n.succ + 1)

The element representing the first 1 in Fin (1 + n + 1 + n.succ) casted to Fin (2 * n.succ + 1).

Equations

• PureU1.VectorLikeOddPlane.oddShiftShiftZero = Fin.cast ⋯ (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.castAdd n 1)))

def PureU1.VectorLikeOddPlane.oddShiftShiftFst {n : ℕ} (j : Fin n) : Fin (2 * n.succ + 1)

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

Equations

• PureU1.VectorLikeOddPlane.oddShiftShiftFst j = Fin.cast ⋯ (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.natAdd 1 j)))

def PureU1.VectorLikeOddPlane.oddShiftShiftMid {n : ℕ} : Fin (2 * n.succ + 1)

The element representing the second 1 in Fin (1 + n + 1 + n.succ) casted to 2 * n.succ + 1.

Equations

• PureU1.VectorLikeOddPlane.oddShiftShiftMid = Fin.cast ⋯ (Fin.castAdd n.succ (Fin.natAdd (1 + n) 1))

def PureU1.VectorLikeOddPlane.oddShiftShiftSnd {n : ℕ} (j : Fin n.succ) : Fin (2 * n.succ + 1)

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

Equations

• PureU1.VectorLikeOddPlane.oddShiftShiftSnd j = Fin.cast ⋯ (Fin.natAdd (1 + n + 1) j)

A.4. Relating the splittings together

theorem PureU1.VectorLikeOddPlane.oddShiftShiftZero_eq_oddFst_zero {n : ℕ} : oddShiftShiftZero = oddFst 0

theorem PureU1.VectorLikeOddPlane.oddShiftShiftZero_eq_oddShiftZero {n : ℕ} : oddShiftShiftZero = oddShiftZero

theorem PureU1.VectorLikeOddPlane.oddShiftShiftFst_eq_oddFst_succ {n : ℕ} (j : Fin n) : oddShiftShiftFst j = oddFst j.succ

theorem PureU1.VectorLikeOddPlane.oddShiftShiftFst_eq_oddShiftFst_castSucc {n : ℕ} (j : Fin n) : oddShiftShiftFst j = oddShiftFst j.castSucc

theorem PureU1.VectorLikeOddPlane.oddShiftShiftMid_eq_oddMid {n : ℕ} : oddShiftShiftMid = oddMid

theorem PureU1.VectorLikeOddPlane.oddShiftShiftMid_eq_oddShiftFst_last {n : ℕ} : oddShiftShiftMid = oddShiftFst (Fin.last n)

theorem PureU1.VectorLikeOddPlane.oddShiftShiftSnd_eq_oddSnd {n : ℕ} (j : Fin n.succ) : oddShiftShiftSnd j = oddSnd j

theorem PureU1.VectorLikeOddPlane.oddShiftShiftSnd_eq_oddShiftSnd {n : ℕ} (j : Fin n.succ) : oddShiftShiftSnd j = oddShiftSnd j

theorem PureU1.VectorLikeOddPlane.oddSnd_eq_oddShiftSnd {n : ℕ} (j : Fin n) : oddSnd j = oddShiftSnd j

B. The first plane

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

def PureU1.VectorLikeOddPlane.basisAsCharges {n : ℕ} (j : Fin n) : (PureU1 (2 * n + 1)).Charges

The first part of the basis as charge assignments.

Equations

• PureU1.VectorLikeOddPlane.basisAsCharges j i = if i = PureU1.VectorLikeOddPlane.oddFst j then 1 else if i = PureU1.VectorLikeOddPlane.oddSnd j then -1 else 0

B.2. Components of the basis vectors as charges

theorem PureU1.VectorLikeOddPlane.basis_on_oddFst_self {n : ℕ} (j : Fin n) : basisAsCharges j (oddFst j) = 1

theorem PureU1.VectorLikeOddPlane.basis_on_oddFst_other {n : ℕ} {k j : Fin n} (h : k ≠ j) : basisAsCharges k (oddFst j) = 0

theorem PureU1.VectorLikeOddPlane.basis_on_other {n : ℕ} {k : Fin n} {j : Fin (2 * n + 1)} (h1 : j ≠ oddFst k) (h2 : j ≠ oddSnd k) : basisAsCharges k j = 0

theorem PureU1.VectorLikeOddPlane.basis_oddSnd_eq_minus_oddFst {n : ℕ} (j i : Fin n) : basisAsCharges j (oddSnd i) = -basisAsCharges j (oddFst i)

theorem PureU1.VectorLikeOddPlane.basis_on_oddSnd_self {n : ℕ} (j : Fin n) : basisAsCharges j (oddSnd j) = -1

theorem PureU1.VectorLikeOddPlane.basis_on_oddSnd_other {n : ℕ} {k j : Fin n} (h : k ≠ j) : basisAsCharges k (oddSnd j) = 0

theorem PureU1.VectorLikeOddPlane.basis_on_oddMid {n : ℕ} (j : Fin n) : basisAsCharges j oddMid = 0

B.3. The basis vectors satisfy the linear ACCs

theorem PureU1.VectorLikeOddPlane.basis_linearACC {n : ℕ} (j : Fin n) : (accGrav (2 * n + 1)) (basisAsCharges j) = 0

B.4. The basis vectors as LinSols

def PureU1.VectorLikeOddPlane.basis {n : ℕ} (j : Fin n) : (PureU1 (2 * n + 1)).LinSols

The first part of the basis as LinSols.

Equations

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

@[simp]

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

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

def PureU1.VectorLikeOddPlane.P {n : ℕ} (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges

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

Equations

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

B.6. Components of the first plane

theorem PureU1.VectorLikeOddPlane.P_oddFst {n : ℕ} (f : Fin n → ℚ) (j : Fin n) : P f (oddFst j) = f j

theorem PureU1.VectorLikeOddPlane.P_oddSnd {n : ℕ} (f : Fin n → ℚ) (j : Fin n) : P f (oddSnd j) = -f j

theorem PureU1.VectorLikeOddPlane.P_oddMid {n : ℕ} (f : Fin n → ℚ) : P f oddMid = 0

B.7. Points on the first plane satisfies the ACCs

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

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

B.8. Kernal of the inclusion into charges

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

def PureU1.VectorLikeOddPlane.P' {n : ℕ} (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).LinSols

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

Equations

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

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

B.9. The basis vectors are linearly independent

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

C. The second plane

C.1. The basis vectors of the second plane as charges

def PureU1.VectorLikeOddPlane.basis!AsCharges {n : ℕ} (j : Fin n) : (PureU1 (2 * n + 1)).Charges

The second part of the basis as charge assignments.

Equations

• PureU1.VectorLikeOddPlane.basis!AsCharges j i = if i = PureU1.VectorLikeOddPlane.oddShiftFst j then 1 else if i = PureU1.VectorLikeOddPlane.oddShiftSnd j then -1 else 0

C.2. Components of the basis vectors as charges

theorem PureU1.VectorLikeOddPlane.basis!_on_oddShiftFst_self {n : ℕ} (j : Fin n) : basis!AsCharges j (oddShiftFst j) = 1

theorem PureU1.VectorLikeOddPlane.basis!_on_oddShiftFst_other {n : ℕ} {k j : Fin n} (h : k ≠ j) : basis!AsCharges k (oddShiftFst j) = 0

theorem PureU1.VectorLikeOddPlane.basis!_on_other {n : ℕ} {k : Fin n} {j : Fin (2 * n + 1)} (h1 : j ≠ oddShiftFst k) (h2 : j ≠ oddShiftSnd k) : basis!AsCharges k j = 0

theorem PureU1.VectorLikeOddPlane.basis!_oddShiftSnd_eq_minus_oddShiftFst {n : ℕ} (j i : Fin n) : basis!AsCharges j (oddShiftSnd i) = -basis!AsCharges j (oddShiftFst i)

theorem PureU1.VectorLikeOddPlane.basis!_on_oddShiftSnd_self {n : ℕ} (j : Fin n) : basis!AsCharges j (oddShiftSnd j) = -1

theorem PureU1.VectorLikeOddPlane.basis!_on_oddShiftSnd_other {n : ℕ} {k j : Fin n} (h : k ≠ j) : basis!AsCharges k (oddShiftSnd j) = 0

theorem PureU1.VectorLikeOddPlane.basis!_on_oddShiftZero {n : ℕ} (j : Fin n) : basis!AsCharges j oddShiftZero = 0

C.3. The basis vectors satisfy the linear ACCs

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

C.4. The basis vectors as LinSols

def PureU1.VectorLikeOddPlane.basis! {n : ℕ} (j : Fin n) : (PureU1 (2 * n + 1)).LinSols

The second part of the basis as LinSols.

Equations

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

@[simp]

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

C.5. Permutations equal adding basis vectors

theorem PureU1.VectorLikeOddPlane.swap!_as_add {n : ℕ} {S S' : (PureU1 (2 * n + 1)).LinSols} (j : Fin n) (hS : ((FamilyPermutations (2 * n + 1)).linSolRep (pairSwap (oddShiftFst j) (oddShiftSnd j))) S = S') : S'.val = S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j

Swapping the elements oddShiftFst j and oddShiftSnd j is equivalent to adding a vector basis!AsCharges j.

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

def PureU1.VectorLikeOddPlane.P! {n : ℕ} (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges

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

Equations

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

C.7. Components of the second plane

theorem PureU1.VectorLikeOddPlane.P!_oddShiftFst {n : ℕ} (f : Fin n → ℚ) (j : Fin n) : P! f (oddShiftFst j) = f j

theorem PureU1.VectorLikeOddPlane.P!_oddShiftSnd {n : ℕ} (f : Fin n → ℚ) (j : Fin n) : P! f (oddShiftSnd j) = -f j

theorem PureU1.VectorLikeOddPlane.P!_oddShiftZero {n : ℕ} (f : Fin n → ℚ) : P! f oddShiftZero = 0

C.8. Points on the second plane satisfies the ACCs

theorem PureU1.VectorLikeOddPlane.P!_linearACC {n : ℕ} (f : Fin n → ℚ) : (accGrav (2 * n + 1)) (P! f) = 0

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

C.9. Kernal of the inclusion into charges

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

C.10. The inclusion of the second plane into LinSols

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

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

Equations

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

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

C.11. The basis vectors are linearly independent

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

D. The mixed cubic ACC from points in both planes

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

E. The combined basis

E.1. The combined basis as LinSols

def PureU1.VectorLikeOddPlane.basisa {n : ℕ} : Fin n ⊕ Fin n → (PureU1 (2 * n + 1)).LinSols

The whole basis as LinSols.

Equations

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

E.2. The inclusion of the span of the combined basis into charges

def PureU1.VectorLikeOddPlane.Pa {n : ℕ} (f g : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges

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

Equations

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

E.3. Components of the inclusion

theorem PureU1.VectorLikeOddPlane.Pa_oddShiftShiftZero {n : ℕ} (f g : Fin n.succ → ℚ) : Pa f g oddShiftShiftZero = f 0

theorem PureU1.VectorLikeOddPlane.Pa_oddShiftShiftFst {n : ℕ} (f g : Fin n.succ → ℚ) (j : Fin n) : Pa f g (oddShiftShiftFst j) = f j.succ + g j.castSucc

theorem PureU1.VectorLikeOddPlane.Pa_oddShiftShiftMid {n : ℕ} (f g : Fin n.succ → ℚ) : Pa f g oddShiftShiftMid = g (Fin.last n)

theorem PureU1.VectorLikeOddPlane.Pa_oddShiftShiftSnd {n : ℕ} (f g : Fin n.succ → ℚ) (j : Fin n.succ) : Pa f g (oddShiftShiftSnd j) = -f j - g j

E.4. Kernal of the inclusion into charges

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

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

E.5. The inclusion of the span of the combined basis into LinSols

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

A point in the span of the whole basis.

Equations

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

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

E.6. The combined basis vectors are linearly independent

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

E.7. Injectivity of the inclusion into linear solutions

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

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

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

E.8. Cardinality of the basis

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

E.9. The basis vectors as a basis

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

The basis formed out of our basisa vectors.

Equations

• PureU1.VectorLikeOddPlane.basisaAsBasis = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

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

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

F.1. Relation under permutations

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