No subspace of ℂ is in two of the polynomial, involution and real pencil classes of conjugation hulls
ProvedDiazModulus.laurent_conj_hull_configuration_classes_disjointLet and with (so is real), and put , so that . Let be any -subspace. Then no two of the following hold:
- (P) for some , not both zero;
- (Q) for some with , and ;
- (R) with , for some with and some with and .
Proof. As is real, is transcendental with , and , so a relation in and with algebraic coefficients clears to a polynomial identity and can be compared coefficientwise. (P) against (Q): writing in the (Q) basis and multiplying by gives a degree- identity whose coefficients at force the (Q) coordinates, and then , to vanish. For (R), with and , so that and , evaluating a cleared identity at kills the coordinate of , and then clearing by kills that of . So (P) and (R) exclude each other, since both coordinates of vanish and then ; and so do (Q) and (R), since applied to and its conjugate both coordinates vanish, while .
Novelty. Not found in the sources read; routine.
import Definitions.Def_DiazModulus
open Complex ComplexConjugate
namespace DiazModulus
theorem laurent_conj_hull_configuration_classes_disjoint
(u s : ℂ) (hu : u ∉ Qbar) (hs : s ∈ Qbar) (hss : s * s = u * conj u) (W : Submodule (↥Qbar) ℂ) :
¬ ((∃ α β : ℂ, α ∈ Qbar ∧ β ∈ Qbar ∧ (α ≠ 0 ∨ β ≠ 0) ∧ α * u ^ 2 + β * u ^ 3 ∈ W) ∧
(∃ e β ζ : ℂ, e ∈ Qbar ∧ β ∈ Qbar ∧ ζ ∈ Qbar ∧ e * conj e = 1 ∧ β * conj β = 1 ∧
ζ = -(β * e ^ 2 * conj ζ) ∧
W =
Submodule.span Qbar ({1, u, conj u, conj (u / s) ^ 2 + e * (u / s) ^ 2, β * conj (u / s) ^ 3 + ζ * (u / s) ^ 2 + e * (u / s) ^ 3} : Set ℂ))) ∧
¬ ((∃ α β : ℂ, α ∈ Qbar ∧ β ∈ Qbar ∧ (α ≠ 0 ∨ β ≠ 0) ∧ α * u ^ 2 + β * u ^ 3 ∈ W) ∧
(∃ κ : ℂ, κ ∈ Qbar ∧ κ * conj κ = 1 ∧ ∃ G : Polynomial ↥Qbar, G.coeff 0 = 0 ∧ 2 ≤ G.natDegree ∧
W =
Submodule.span Qbar ({1, u, conj u, Polynomial.aeval (u / s) G + κ * conj ((u / s) * Polynomial.aeval (u / s) G), conj (Polynomial.aeval (u / s) G + κ * conj ((u / s) * Polynomial.aeval (u / s) G))} : Set ℂ))) ∧
¬ ((∃ e β ζ : ℂ, e ∈ Qbar ∧ β ∈ Qbar ∧ ζ ∈ Qbar ∧ e * conj e = 1 ∧ β * conj β = 1 ∧
ζ = -(β * e ^ 2 * conj ζ) ∧
W =
Submodule.span Qbar ({1, u, conj u, conj (u / s) ^ 2 + e * (u / s) ^ 2, β * conj (u / s) ^ 3 + ζ * (u / s) ^ 2 + e * (u / s) ^ 3} : Set ℂ)) ∧
(∃ κ : ℂ, κ ∈ Qbar ∧ κ * conj κ = 1 ∧ ∃ G : Polynomial ↥Qbar, G.coeff 0 = 0 ∧ 2 ≤ G.natDegree ∧
W =
Submodule.span Qbar ({1, u, conj u, Polynomial.aeval (u / s) G + κ * conj ((u / s) * Polynomial.aeval (u / s) G), conj (Polynomial.aeval (u / s) G + κ * conj ((u / s) * Polynomial.aeval (u / s) G))} : Set ℂ))) := by
sorry
end DiazModulus