MATHLIBANNEX / CANONICAL DECLARATION CARD

The satellite polynomial is linear in the maximal-minor vector

MathlibAnnex.PluckerSupport.pluckerPairing_satelliteCoefficients_maximalMinors

theorem

Expresses the configuration polynomial as a linear pairing with maximal minors.

Statement

Let and let be finite, possibly empty. On fix real linear functionals and . Put in the standard basis, and let replace row by . Set Enumerate to place its rows after the base rows. For a real linear map , let . For each increasing -row index , put . Let select all base rows and select all base rows except , followed by satellite . Let denote a minor-coordinate unit vector. Given any and coefficients , put Then the finite dot product satisfies

Assumptions

The finite families, arbitrary real weight and coefficients are the only inputs. No norm model, admissibility or maximizing condition is assumed.

Conclusion

The same configuration appears in the map and polynomial. The parity corrects increasing-row order to row-replacement order.

Proof route

Read the row sign, expand both finite sums, and substitute their determinant identities.

Proof steps

  1. Correct the selected row order. Moving the last selected satellite row into position crosses rows. Therefore

    The inverse cycle in the source maps position to the last selected row. the parity-corrected minor lemma applies to this same configuration, and . In zero-based source indexing , the parity is . The pinned row-permutation determinant formula says ; substitute the inverse cycle that moves the last selected row to .

  2. Show both sums in the pairing. Bilinearity gives

    The first equality expands the coefficient vector RHS; the second substitutes Step 1. If is empty the sums vanish and the identity reduces to .

The product-indexed map and finite-coordinate map both send to its base and satellite evaluations, as in the displayed definition of . Extracting the rows of a linear map and reassembling them gives that same map, by the reconstruction identity.

For the later volume-scaled application, let be a norm, and its reference Lebesgue volume. The volume-scaling identity gives Neither the norm nor the volume factor is an input to the unscaled theorem above.

Main citations

Lean source signature (exact)

theorem pluckerPairing_satelliteCoefficients_maximalMinors
    (weight : ℝ) (coeff : J → Coord (m + 1))
    (C : SatelliteConfiguration (m + 1) J) :
    dotProduct (satellitePluckerCoefficients weight coeff)
      (maximalMinors (clmMatrix (configurationFinMap C))) =
      configurationPolynomial weight coeff C
In the source Mathematical meaning
m; [Fintype J] and finite , whose enumeration orders the satellite coordinates.
C : SatelliteConfiguration (m + 1) J; C.1; C.2 a The pair ; C.1 is the base family and C.2 a is the functional . The pair type imposes no admissibility.
configurationFinMap C; clmMatrix (configurationFinMap C) The map and its matrix in standard coordinates.
maximalMinors (clmMatrix (configurationFinMap C)) The vector , with coordinate for each increasing -row index.
replacementParity; baseMinorIndex; replacementMinorIndex The sign and the row indices ; source index corresponds to formula index .
weight; coeff a; coeff a i , the vector , and its coordinate , respectively.
In the source Mathematical meaning
satellitePluckerCoefficients weight coeff The full vector .
dotProduct (…) (…) = configurationPolynomial weight coeff C The whole equality .

Surrounding assumptions and aliases.

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Exact content identity

Declaration: MathlibAnnex.PluckerSupport.pluckerPairing_satelliteCoefficients_maximalMinors

Accepted content SHA-256: 6e0ca039827a0b6cb429f09633300fba57157e6ded5ee257f28f89a65861dcc9

Accepted source guide SHA-256: f27d35366b349169534b09e4b62851a73ff429d3cef0c28c2b98fbb2eed96c5c

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑