Genericity polynomials for the equivariant refined prism

The global parameter type from EquivariantPrismVertexParameters already enforces shared-vertex compatibility and prime equivariance. This file records the two algebraic degeneracy families used by the refined prism perturbation.

• For every refined prism simplex and every one of its facets, the facet polynomial is the determinant of the augmented deviation matrix. Its nonvanishing is exactly facet regularity.
• For every refined prism simplex and every ordered codimension-two face, the minor polynomial is the determinant of the deviation vectors at the remaining vertices. Its nonvanishing rules out a deviation zero on that codimension-two face.

Both constructions are literal multivariate polynomials over the finite orbit parameter type. Evaluation lemmas identify them with the corresponding real matrices reconstructed from an assignment. A final sum type packages the two finite families for direct use with FiniteMultivariateGenericPerturbation.exists_small_positive_generic.

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.PolynomialRing {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Type

The multivariate-polynomial ring attached to the finite equivariant prism parameter space.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.PolynomialRing hp N L = MvPolynomial (NRR.FoxNeuwirthOrderComplex.EquivariantPrismVertexParameters.Parameter hp N L) ℝ

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.scalarPolynomial {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (x : EquivariantPrismVertexParameters.GlobalVertex hp N L) (j : Fin p) : PolynomialRing hp N L

The coordinate variable attached to a sampled global vertex and a coordinate label.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.scalarPolynomial hp N L x j = MvPolynomial.X ⟦(x, j)⟧

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.vectorPolynomial {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (x : EquivariantPrismVertexParameters.GlobalVertex hp N L) : Fin p → PolynomialRing hp N L

The polynomial coordinate vector at a sampled global vertex.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.vectorPolynomial hp N L x j = NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.scalarPolynomial hp N L x j

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.localVertexPolynomial {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (i : Fin (p + 1)) : Fin p → PolynomialRing hp N L

The polynomial coordinate vector at one local refined-prism vertex occurrence.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.deviationPolynomial {p : ℕ} (hp : Nat.Prime p) {N L : ℕ} (y : Fin p → PolynomialRing hp N L) (r : Fin (p - 1)) : PolynomialRing hp N L

Fixed difference coordinate in the polynomial ring.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.localVertexMap {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (q : SubdivisionPrismCharts.PrismCell hp N L) : AffinePositiveRayBoundary.VertexMap p

The real vertex map reconstructed on one refined prism simplex.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.assignmentEvalHom {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) : PolynomialRing hp N L →+* ℝ

Evaluation at a parameter assignment, bundled as a ring homomorphism.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.assignmentEvalHom hp N L a = MvPolynomial.eval₂Hom (RingHom.id ℝ) a

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.assignmentEvalHom_apply {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (P : PolynomialRing hp N L) : (assignmentEvalHom hp N L a) P = (MvPolynomial.eval a) P

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.eval_scalarPolynomial {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (x : EquivariantPrismVertexParameters.GlobalVertex hp N L) (j : Fin p) : (MvPolynomial.eval a) (scalarPolynomial hp N L x j) = EquivariantPrismVertexParameters.scalarValue hp N L a x j

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.eval_vectorPolynomial {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (x : EquivariantPrismVertexParameters.GlobalVertex hp N L) (j : Fin p) : (MvPolynomial.eval a) (vectorPolynomial hp N L x j) = EquivariantPrismVertexParameters.vectorValue hp N L a x j

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.eval_localVertexPolynomial {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (q : SubdivisionPrismCharts.PrismCell hp N L) (i : Fin (p + 1)) (j : Fin p) : (MvPolynomial.eval a) (localVertexPolynomial hp N L q i j) = EquivariantPrismVertexParameters.localVertexValue hp N L a q i j

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.eval_deviationPolynomial {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (y : Fin p → PolynomialRing hp N L) (r : Fin (p - 1)) : (MvPolynomial.eval a) (deviationPolynomial hp y r) = AffinePositiveRayBoundary.VertexMap.deviation hp (fun (j : Fin p) => (MvPolynomial.eval a) (y j)) r

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.facetMatrixPolynomial {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (k : Fin (p + 1)) : Matrix (Fin p) (Fin p) (PolynomialRing hp N L)

The polynomial augmented deviation matrix on the facet omitting vertex k.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.facetDeterminantPolynomial {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (k : Fin (p + 1)) : PolynomialRing hp N L

The facet determinant polynomial for one local refined-prism simplex.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.map_facetMatrixPolynomial {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (q : SubdivisionPrismCharts.PrismCell hp N L) (k : Fin (p + 1)) : (assignmentEvalHom hp N L a).mapMatrix (facetMatrixPolynomial hp N L q k) = AffinePositiveRayBoundary.VertexMap.facetMatrix hp (localVertexMap hp N L a q) k

Evaluation of the polynomial facet matrix is the real facet matrix of the reconstructed local vertex map.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.eval_facetDeterminantPolynomial {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (q : SubdivisionPrismCharts.PrismCell hp N L) (k : Fin (p + 1)) : (MvPolynomial.eval a) (facetDeterminantPolynomial hp N L q k) = AffinePositiveRayBoundary.VertexMap.facetDeterminant hp (localVertexMap hp N L a q) k

The facet determinant polynomial evaluates to the actual local facet determinant.

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.CodimTwoFace (p : ℕ) : Type

An ordered codimension-two face is encoded by first omitting one vertex and then omitting one vertex of the resulting facet. This representation is finite and avoids choosing an ordering on unordered pairs.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.CodimTwoFace p = (Fin (p + 1) × Fin p)

@[instance_reducible]

instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.codimTwoFaceFintype (p : ℕ) : Fintype (CodimTwoFace p)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.codimTwoFaceFintype p = inferInstance

@[instance_reducible]

instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.codimTwoFaceDecidableEq (p : ℕ) : DecidableEq (CodimTwoFace p)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.codimTwoFaceDecidableEq p = inferInstance

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.secondOmissionIndex {p : ℕ} (hp : Nat.Prime p) (f : CodimTwoFace p) : Fin (p - 1 + 1)

The second omission index, cast to the syntactic successor form needed by Fin.succAbove.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.secondOmissionIndex hp f = Fin.cast ⋯ f.2

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.codimTwoVertex {p : ℕ} (hp : Nat.Prime p) (f : CodimTwoFace p) (i : Fin (p - 1)) : Fin (p + 1)

The vertex retained in an ordered codimension-two face after the two omissions.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.codimTwoVertex_ne_first {p : ℕ} (hp : Nat.Prime p) (f : CodimTwoFace p) (i : Fin (p - 1)) : codimTwoVertex hp f i ≠ f.1

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.codimTwoDeviationMatrixPolynomial {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (f : CodimTwoFace p) : Matrix (Fin (p - 1)) (Fin (p - 1)) (PolynomialRing hp N L)

The polynomial deviation matrix on the vertices of an ordered codimension-two face. Rows are fixed deviation coordinates and columns are the p-1 retained vertices.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.codimTwoMinorPolynomial {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (f : CodimTwoFace p) : PolynomialRing hp N L

The codimension-two deviation-minor polynomial.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.codimTwoDeviationMatrix {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (q : SubdivisionPrismCharts.PrismCell hp N L) (f : CodimTwoFace p) : Matrix (Fin (p - 1)) (Fin (p - 1)) ℝ

The corresponding real deviation matrix reconstructed from an assignment.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.map_codimTwoDeviationMatrixPolynomial {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (q : SubdivisionPrismCharts.PrismCell hp N L) (f : CodimTwoFace p) : (assignmentEvalHom hp N L a).mapMatrix (codimTwoDeviationMatrixPolynomial hp N L q f) = codimTwoDeviationMatrix hp N L a q f

Evaluation of the polynomial codimension-two matrix gives the corresponding real matrix.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.eval_codimTwoMinorPolynomial {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (q : SubdivisionPrismCharts.PrismCell hp N L) (f : CodimTwoFace p) : (MvPolynomial.eval a) (codimTwoMinorPolynomial hp N L q f) = (codimTwoDeviationMatrix hp N L a q f).det

The codimension-two minor polynomial evaluates to the corresponding real determinant.

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.GenericityIndex {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Type

Finite indices for all facet-determinant and codimension-two-minor degeneracies.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.genericityIndexFintype {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : Fintype (GenericityIndex hp N L)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.genericityIndexFintype hp N L = inferInstance

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.genericityIndexDecidableEq {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : DecidableEq (GenericityIndex hp N L)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.genericityIndexDecidableEq hp N L = inferInstance

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.genericityPolynomial {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) : GenericityIndex hp N L → PolynomialRing hp N L

The combined finite polynomial family used by the generic perturbation theorem.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismGenericityPolynomials.eval_genericityPolynomial {p : ℕ} (hp : Nat.Prime p) (N L : ℕ) (a : EquivariantPrismVertexParameters.Assignment hp N L) (i : GenericityIndex hp N L) : (MvPolynomial.eval a) (genericityPolynomial hp N L i) = match i with | Sum.inl qk => AffinePositiveRayBoundary.VertexMap.facetDeterminant hp (localVertexMap hp N L a qk.1) qk.2 | Sum.inr qf => (codimTwoDeviationMatrix hp N L a qf.1 qf.2).det

Evaluation of the combined family, split into its two geometric meanings.