MATHLIBANNEX / CANONICAL DECLARATION CARD

Sphere isometries preserve the Plücker body

MathlibAnnex.PluckerBody.eq_of_sphereIsometry

theorem

Combines generator transport and its inverse for every finite output dimension.

Statement

Let , put , and give and their coordinate sup norms. Let be the fixed coordinate Lebesgue measure on . Let be continuous real seminorms with specified positive constants such that

Both and are norms. For each define the closed unit ball, unit sphere, and real reference volume by The finite measure is read as a real number when used as a scalar.

Let be the finite set of increasing -tuples of distinct rows from . The minor-coordinate space carries its sup norm. For a linear map , put in the standard coordinate basis. Write for its maximal-minor vector and for its two volume-scaled versions. Their coordinates and scaling are

For each , let consist of linear maps with for all . Set If is a bijection with for all , then

Assumptions

The source dimension is positive, . Both seminorms have the specified positive norm comparisons and are continuous. The sphere map is a bijective chord-distance isometry. The output dimension is arbitrary, including zero.

Conclusion

The two bodies agree for each finite . This statement does not classify the norms or assert that the given sphere map itself has a linear extension.

Proof route

Transport both signs, take convex hulls, and repeat for the inverse isometry.

Proof steps

  1. Place every signed target generator in the source body. For each ,

    The first membership is generator transport through the sphere isometry applied to and this -contraction . The second is sign symmetry of the same source body. Consequently,

    This is the signed-generator inclusion.

  2. Pass to convex hulls. Since is convex, the preceding inclusion implies

    Equivalently, every finite convex combination of its generators stays in the source body. This is the body inclusion.

  3. Use the inverse isometry for the reverse inclusion. The bijection satisfies the same chord-distance condition with interchanged. Applying Steps 1–2 to that map gives

    The two inclusions are for the same output dimension and the same reference minor coordinates, so they yield the asserted equality.

Main citations

Lean source signature (exact)

/-- Equality follows from the two inclusions furnished by the isometry and its inverse. -/
theorem eq_of_sphereIsometry {m N : ℕ}
    {MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)}
    (Δ : sphere (0 : Space MX) 1 ≃ᵢ sphere (0 : Space MY) 1) :
    body MX N = body MY N

The two expressions after the final colon are sets, and = asserts that they contain exactly the same minor-coordinate vectors.

In the source Mathematical meaning
{m N : ℕ}; Fin (m + 1) → ℝ; Fin N → ℝ , , , . Coordinate vectors have the sup norm; braces mark parameters Lean can infer.
MX; MY The continuous seminorms and , with their positive lower and upper comparison constants stated in this Card.
Space MX; Space MY The same vectors of , now with norms and , respectively.
sphere (0 : Space MX) 1; sphere (0 : Space MY) 1 and . The arguments are center and radius .
Δ : ... ≃ᵢ ... A bijective isometry : for all . The symbol in the code asserts both bijectivity and distance preservation.
Matrix.MaximalMinorIndex (m + 1) (Fin N) The row selections with rows from . Both bodies lie in the same space .
Matrix.ballVolumeScaledMaximalMinors MX B; ... MY B and , where and .
generators MX N , where .
generators MY N . This uses and , instead of and .
body MX N The source body , a set of minor-coordinate vectors.
In the source Mathematical meaning
body MY N The target body .
body MX N = body MY N The conclusion . The same arbitrary output dimension is used on both sides; no linear extension of is asserted.

Exact definitions used in this reading: Signed generator set; Convex-body definition.

Exact surrounding binder context (separate excerpts)

Exact source lines 15–18:

noncomputable section
open Set Metric Function MeasureTheory
open scoped NNReal ENNReal BigOperators
namespace MathlibAnnex.PluckerBody

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

Exact content identity

Declaration: MathlibAnnex.PluckerBody.eq_of_sphereIsometry

Accepted content SHA-256: aeded10096a0d780b78a532d3c609f27b4e08e9215fb29d6377b3c4cc99382b5

Accepted source guide SHA-256: aad4287bcfc0e0bfe21426313cdf86c427e7d5db183d4bab61808c77aef4593a

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑