Basis of LinSols in the even case

We give a basis of LinSols in the even case. This basis has the special property that splits into two planes on which every point is a solution to the ACCs.

theorem PureU1.VectorLikeEvenPlane.n_cond₂ (n : ℕ) : 1 + (n + n + 1) = 2 * 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)

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.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)

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)

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

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

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

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

theorem PureU1.VectorLikeEvenPlane.basis!_on_evenShiftFst_self {n : ℕ} (j : Fin n) : basis!AsCharges j (evenShiftFst 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!_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_evenSnd_eq_neg_evenFst {n : ℕ} (j i : Fin n.succ) : basisAsCharges j (evenSnd i) = -basisAsCharges j (evenFst i)

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_evenSnd_self {n : ℕ} (j : Fin n.succ) : basisAsCharges j (evenSnd j) = -1

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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.P_evenSnd {n : ℕ} (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (evenSnd j) = -f j

theorem PureU1.VectorLikeEvenPlane.P!_evenShiftSnd {n : ℕ} (f : Fin n → ℚ) (j : Fin n) : P! f (evenShiftSnd j) = -f 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.P!_evenShiftZero {n : ℕ} (f : Fin n → ℚ) : P! f evenShiftZero = 0

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

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

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

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

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

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

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

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

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

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

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

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

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)

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

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

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

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

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

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

def PureU1.VectorLikeEvenPlane.join {n : ℕ} (g : Fin n.succ → ℚ) (f : Fin n → ℚ) : Fin n.succ ⊕ Fin n → ℚ

A helper function for what follows.

Equations

• PureU1.VectorLikeEvenPlane.join g f (Sum.inl i_2) = g i_2
• PureU1.VectorLikeEvenPlane.join g f (Sum.inr i_2) = f i_2

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

theorem PureU1.VectorLikeEvenPlane.join_Pa {n : ℕ} (g g' : Fin n.succ → ℚ) (f f' : Fin n → ℚ) : Pa' (join g f) = Pa' (join 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'

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

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

The basis formed out of our basisa vectors.

Equations

• PureU1.VectorLikeEvenPlane.basisaAsBasis = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

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

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

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)

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

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)