Solutions from quad solutions

We use $B-L$ to form a surjective map from quad solutions to solutions. The main reference for this material is:

• https://arxiv.org/abs/2006.03588

def SMRHN.PlusU1.QuadSolToSol.α₁ {n : ℕ} (S : (PlusU1 n).QuadSols) : ℚ

A helper function for what follows.

Equations

• SMRHN.PlusU1.QuadSolToSol.α₁ S = -3 * ((SMνACCs.cubeTriLin S.val) S.val) (SMRHN.PlusU1.BL n).val

def SMRHN.PlusU1.QuadSolToSol.α₂ {n : ℕ} (S : (PlusU1 n).QuadSols) : ℚ

A helper function for what follows.

Equations

• SMRHN.PlusU1.QuadSolToSol.α₂ S = SMνACCs.accCube S.val

theorem SMRHN.PlusU1.QuadSolToSol.cube_α₁_α₂_zero {n : ℕ} (S : (PlusU1 n).QuadSols) (a b : ℚ) (h1 : α₁ S = 0) (h2 : α₂ S = 0) : SMνACCs.accCube (BL.addQuad S a b).val = 0

theorem SMRHN.PlusU1.QuadSolToSol.α₂_AF {n : ℕ} (S : (PlusU1 n).Sols) : α₂ S.toQuadSols = 0

theorem SMRHN.PlusU1.QuadSolToSol.BL_add_α₁_α₂_cube {n : ℕ} (S : (PlusU1 n).QuadSols) : SMνACCs.accCube (BL.addQuad S (α₁ S) (α₂ S)).val = 0

theorem SMRHN.PlusU1.QuadSolToSol.BL_add_α₁_α₂_AF {n : ℕ} (S : (PlusU1 n).Sols) : BL.addQuad S.toQuadSols (α₁ S.toQuadSols) (α₂ S.toQuadSols) = α₁ S.toQuadSols • S.toQuadSols

def SMRHN.PlusU1.QuadSolToSol.generic {n : ℕ} (S : (PlusU1 n).QuadSols) : (PlusU1 n).Sols

The construction of a Sol from a QuadSol in the generic case.

Equations

• SMRHN.PlusU1.QuadSolToSol.generic S = SMRHN.PlusU1.quadToAF (SMRHN.PlusU1.BL.addQuad S (SMRHN.PlusU1.QuadSolToSol.α₁ S) (SMRHN.PlusU1.QuadSolToSol.α₂ S)) ⋯

theorem SMRHN.PlusU1.QuadSolToSol.generic_on_AF {n : ℕ} (S : (PlusU1 n).Sols) : generic S.toQuadSols = α₁ S.toQuadSols • S

theorem SMRHN.PlusU1.QuadSolToSol.generic_on_AF_α₁_ne_zero {n : ℕ} (S : (PlusU1 n).Sols) (h : α₁ S.toQuadSols ≠ 0) : (α₁ S.toQuadSols)⁻¹ • generic S.toQuadSols = S

def SMRHN.PlusU1.QuadSolToSol.special {n : ℕ} (S : (PlusU1 n).QuadSols) (a b : ℚ) (h1 : α₁ S = 0) (h2 : α₂ S = 0) : (PlusU1 n).Sols

The construction of a Sol from a QuadSol in the case when α₁ S = 0 and α₂ S = 0.

Equations

• SMRHN.PlusU1.QuadSolToSol.special S a b h1 h2 = SMRHN.PlusU1.quadToAF (SMRHN.PlusU1.BL.addQuad S a b) ⋯

theorem SMRHN.PlusU1.QuadSolToSol.special_on_AF {n : ℕ} (S : (PlusU1 n).Sols) (h1 : α₁ S.toQuadSols = 0) : special S.toQuadSols 1 0 h1 ⋯ = S

def SMRHN.PlusU1.quadSolToSol {n : ℕ} : (PlusU1 n).QuadSols × ℚ × ℚ → (PlusU1 n).Sols

A map from QuadSols × ℚ × ℚ to Sols taking account of the special and generic cases. We will show that this map is a surjection.

Equations

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

def SMRHN.PlusU1.quadSolToSolInv {n : ℕ} : (PlusU1 n).Sols → (PlusU1 n).QuadSols × ℚ × ℚ

A map from Sols to QuadSols × ℚ × ℚ which forms a right-inverse to quadSolToSol, as shown in quadSolToSolInv_rightInverse.

Equations

• SMRHN.PlusU1.quadSolToSolInv S = if SMRHN.PlusU1.QuadSolToSol.α₁ S.toQuadSols = 0 then (S.toQuadSols, 1, 0) else (S.toQuadSols, (SMRHN.PlusU1.QuadSolToSol.α₁ S.toQuadSols)⁻¹, 0)

theorem SMRHN.PlusU1.quadSolToSolInv_1 {n : ℕ} (S : (PlusU1 n).Sols) : (quadSolToSolInv S).1 = S.toQuadSols

theorem SMRHN.PlusU1.quadSolToSolInv_α₁_α₂_zero {n : ℕ} (S : (PlusU1 n).Sols) (h : QuadSolToSol.α₁ S.toQuadSols = 0) : QuadSolToSol.α₁ (quadSolToSolInv S).1 = 0 ∧ QuadSolToSol.α₂ (quadSolToSolInv S).1 = 0

theorem SMRHN.PlusU1.quadSolToSolInv_α₁_α₂_neq_zero {n : ℕ} (S : (PlusU1 n).Sols) (h : QuadSolToSol.α₁ S.toQuadSols ≠ 0) : ¬(QuadSolToSol.α₁ (quadSolToSolInv S).1 = 0 ∧ QuadSolToSol.α₂ (quadSolToSolInv S).1 = 0)

theorem SMRHN.PlusU1.quadSolToSolInv_special {n : ℕ} (S : (PlusU1 n).Sols) (h : QuadSolToSol.α₁ S.toQuadSols = 0) : QuadSolToSol.special (quadSolToSolInv S).1 (quadSolToSolInv S).2.1 (quadSolToSolInv S).2.2 ⋯ ⋯ = S

theorem SMRHN.PlusU1.quadSolToSolInv_generic {n : ℕ} (S : (PlusU1 n).Sols) (h : QuadSolToSol.α₁ S.toQuadSols ≠ 0) : (quadSolToSolInv S).2.1 • QuadSolToSol.generic (quadSolToSolInv S).1 = S

theorem SMRHN.PlusU1.quadSolToSolInv_rightInverse {n : ℕ} : Function.RightInverse quadSolToSolInv quadSolToSol

theorem SMRHN.PlusU1.quadSolToSol_surjective {n : ℕ} : Function.Surjective quadSolToSol