A 2×3 configuration whose ratio is a Möbius function of u gives three independent y′ with y′ and u·y′ in W
ProvedDiazModulus.mobius_ratio_configuration_u_multiplier_tripleLet be transcendental, that is, (the algebraic numbers); spans and linear independence are over . Let be any -subspace of , let be linearly independent and linearly independent, with for all (a configuration in ), and let be coprime with and , so the ratio is a Möbius function of . Then there are linearly independent with and for every .
So is a configuration in , with ratio .
Proof. Write and . To begin, : otherwise , so ( is transcendental) and are not coprime; hence . Next . If , gives , so , and the independence of forces . If , then , so forces , and neither nor has a term in , against . Put , a non-zero multiple of the independent family , so is independent. As and , inverting the matrix of in the basis gives and ; both lie in , and so do and after dividing by .
Novelty. Not found in the sources read; routine.
import Definitions.Def_DiazModulus
open Complex ComplexConjugate
namespace DiazModulus
open Polynomial in
theorem mobius_ratio_configuration_u_multiplier_triple (u : ℂ) (hu : u ∉ Qbar) (W : Submodule (↥Qbar) ℂ)
(x : Fin 2 → ℂ) (y : Fin 3 → ℂ) (hx : LinearIndependent (↥Qbar) x)
(hy : LinearIndependent (↥Qbar) y) (hxy : ∀ i j, x i * y j ∈ W)
(p q : (↥Qbar)[X]) (hcop : IsCoprime p q) (hdeg : max p.natDegree q.natDegree = 1)
(hpq : x 1 * aeval u q = x 0 * aeval u p) :
∃ y' : Fin 3 → ℂ, LinearIndependent (↥Qbar) y' ∧ ∀ j, y' j ∈ W ∧ u * y' j ∈ W := by
sorry
end DiazModulus