Semantic normal forms for the split trace cover

The iterated monic AdjoinRoot presentation gives every element of the Kummer top algebra a unique rectangular coefficient vector. Composing this representation with the affine and Laurent comparison maps gives semantic normal forms for trace-cover classes, and evaluation of those coefficients recovers the comparison-map image exactly.

This does not identify two source classes with the same semantic normal form. That remaining injectivity statement is the syntactic quotient-division wall and is kept explicit below.

noncomputable def BGS.Markoff.adjoinRootTowerSemanticNormalForm {R : Type u_1} [CommRing R] (f : Polynomial R) (hf : f.Monic) (g : Polynomial (AdjoinRoot f)) (hg : g.Monic) (z : AdjoinRoot g) : Fin f.natDegree × Fin g.natDegree →₀ R

Rectangular coefficients of an element in a two-stage monic AdjoinRoot tower.

Equations

• BGS.Markoff.adjoinRootTowerSemanticNormalForm f hf g hg z = ((AdjoinRoot.powerBasis' hf).basis.smulTower (AdjoinRoot.powerBasis' hg).basis).repr z

noncomputable def BGS.Markoff.adjoinRootTowerSemanticNormalFormEvaluation {R : Type u_1} [CommRing R] (f : Polynomial R) (hf : f.Monic) (g : Polynomial (AdjoinRoot f)) (hg : g.Monic) (c : Fin f.natDegree × Fin g.natDegree →₀ R) : AdjoinRoot g

Evaluate a rectangular coefficient vector in the two-stage AdjoinRoot tower.

Equations

• BGS.Markoff.adjoinRootTowerSemanticNormalFormEvaluation f hf g hg c = ((AdjoinRoot.powerBasis' hf).basis.smulTower (AdjoinRoot.powerBasis' hg).basis).repr.symm c

@[simp]

theorem BGS.Markoff.adjoinRootTowerSemanticNormalForm_evaluation {R : Type u_1} [CommRing R] (f : Polynomial R) (hf : f.Monic) (g : Polynomial (AdjoinRoot f)) (hg : g.Monic) (z : AdjoinRoot g) : adjoinRootTowerSemanticNormalFormEvaluation f hf g hg (adjoinRootTowerSemanticNormalForm f hf g hg z) = z

@[simp]

theorem BGS.Markoff.adjoinRootTowerSemanticNormalForm_evaluation_inverse {R : Type u_1} [CommRing R] (f : Polynomial R) (hf : f.Monic) (g : Polynomial (AdjoinRoot f)) (hg : g.Monic) (c : Fin f.natDegree × Fin g.natDegree →₀ R) : adjoinRootTowerSemanticNormalForm f hf g hg (adjoinRootTowerSemanticNormalFormEvaluation f hf g hg c) = c

@[simp]

theorem BGS.Markoff.adjoinRootTowerSemanticNormalForm_zero {R : Type u_1} [CommRing R] (f : Polynomial R) (hf : f.Monic) (g : Polynomial (AdjoinRoot f)) (hg : g.Monic) : adjoinRootTowerSemanticNormalForm f hf g hg 0 = 0

@[simp]

theorem BGS.Markoff.adjoinRootTowerSemanticNormalFormEvaluation_zero {R : Type u_1} [CommRing R] (f : Polynomial R) (hf : f.Monic) (g : Polynomial (AdjoinRoot f)) (hg : g.Monic) : adjoinRootTowerSemanticNormalFormEvaluation f hf g hg 0 = 0

theorem BGS.Markoff.adjoinRootTowerSemanticNormalForm_injective {R : Type u_1} [CommRing R] (f : Polynomial R) (hf : f.Monic) (g : Polynomial (AdjoinRoot f)) (hg : g.Monic) : Function.Injective (adjoinRootTowerSemanticNormalForm f hf g hg)

noncomputable def BGS.Markoff.splitTraceAffineSemanticNormalForm {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) (a : SplitTraceAffineCoordinateRing K sigma d e) : Fin (splitTraceEtaKummerPolynomial sigma e).natDegree × Fin (splitTraceXiKummerPolynomial sigma e d).natDegree →₀ AdjoinRoot (splitTraceBaseKummerPolynomial sigma)

Semantic rectangular coefficients of an affine trace-cover class.

Equations

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

theorem BGS.Markoff.splitTraceAffineSemanticNormalForm_evaluation {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) (a : SplitTraceAffineCoordinateRing K sigma d e) : adjoinRootTowerSemanticNormalFormEvaluation (splitTraceEtaKummerPolynomial sigma e) ⋯ (splitTraceXiKummerPolynomial sigma e d) ⋯ (splitTraceAffineSemanticNormalForm sigma hsigma e d heOdd hdOdd hde a) = (splitTraceAffineToKummerTop sigma hsigma e d heOdd hdOdd hde) a

Evaluating the affine semantic normal form recovers the affine comparison-map image.

theorem BGS.Markoff.splitTraceAffineSemanticNormalForm_eq_zero_iff {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) (a : SplitTraceAffineCoordinateRing K sigma d e) : splitTraceAffineSemanticNormalForm sigma hsigma e d heOdd hdOdd hde a = 0 ↔ (splitTraceAffineToKummerTop sigma hsigma e d heOdd hdOdd hde) a = 0

The affine semantic normal form has zero coefficients exactly when its Kummer image is zero.

theorem BGS.Markoff.splitTraceAffineSemanticNormalForm_injective_iff {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) : Function.Injective (splitTraceAffineSemanticNormalForm sigma hsigma e d heOdd hdOdd hde) ↔ Function.Injective ⇑(splitTraceAffineToKummerTop sigma hsigma e d heOdd hdOdd hde)

Affine comparison-map injectivity is now exactly injectivity of the semantic coefficient map. The forward implication is useful once a syntactic quotient reduction proves coefficient-map injectivity; the converse prevents semantic coordinates from concealing the original wall.

noncomputable def BGS.Markoff.splitTraceLaurentSemanticNormalForm {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) (a : SplitTraceLaurentCoordinateRing K sigma d e) : Fin (splitTraceEtaKummerPolynomial sigma e).natDegree × Fin (splitTraceXiKummerPolynomial sigma e d).natDegree →₀ AdjoinRoot (splitTraceBaseKummerPolynomial sigma)

Semantic rectangular coefficients of a Laurent trace-cover class.

Equations

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

theorem BGS.Markoff.splitTraceLaurentSemanticNormalForm_evaluation {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) (a : SplitTraceLaurentCoordinateRing K sigma d e) : adjoinRootTowerSemanticNormalFormEvaluation (splitTraceEtaKummerPolynomial sigma e) ⋯ (splitTraceXiKummerPolynomial sigma e d) ⋯ (splitTraceLaurentSemanticNormalForm sigma hsigma e d heOdd hdOdd hde a) = (splitTraceLaurentToKummerTop sigma hsigma e d heOdd hdOdd hde) a

Evaluating the Laurent semantic normal form recovers the Laurent comparison-map image.

theorem BGS.Markoff.splitTraceLaurentSemanticNormalForm_injective_iff {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) : Function.Injective (splitTraceLaurentSemanticNormalForm sigma hsigma e d heOdd hdOdd hde) ↔ Function.Injective ⇑(splitTraceLaurentToKummerTop sigma hsigma e d heOdd hdOdd hde)

Laurent comparison-map injectivity is equivalent to injectivity of its semantic coefficient map. Thus localization introduces no new target-side ambiguity; the unsolved source-side task is still the syntactic quotient normal-form theorem.