Documentation

LeanPool.NandakumarRamanaRao.NRR.PrimePolyhedron.FoxNeuwirth.ReferenceSubdivisionRegular

Regularity of the S5 reference map on every barycentric refinement #

The S5 reference coordinate map is affine on each original maximal order-complex simplex. On a refined simplex its augmented difference matrix is the original augmented matrix multiplied by the barycentric vertex matrix of the subdivision chart. Both factors have nonzero determinant.

source
noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.originalAugmentedMatrix {p : ℕ} (hp : Nat.Prime p) (F : CoordinateAffineVertexMap p) (s : Simplex p (p - 1)) :
Matrix (Fin (p - 1 + 1)) (Fin (p - 1 + 1)) ℝ

Augmented matrix of an original affine vertex map on one maximal simplex.

Equations
Instances For
    source
    theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.CoordinateAffineVertexMap.globalValue_realizationPoint {p : ℕ} (F : CoordinateAffineVertexMap p) (s : Simplex p (p - 1)) (w : StandardSimplex (p - 1)) :
    F.globalValue (s.realizationPoint w) = F.value s w

    Global affine interpolation on the realization chart of a simplex is the barycentric interpolation of the vertex data on that simplex.

    source
    theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.augmentedMatrix_ofCoordinateAffineVertexMap_eq_mul {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F : CoordinateAffineVertexMap p) (q : TopCell hp N) :
    augmentedMatrix hp N (ofCoordinateAffineVertexMap F) q = originalAugmentedMatrix hp F (ReferenceAffineOrbitCount.topRepr hp q.1) * AffineSubdivisionDeterminant.iterVertexMatrix (p - 1) N fun (k : Fin N) => Simplex.refinementIndexPerm (q.2 k)

    Sampling an original affine map on a refined simplex multiplies the original augmented matrix by the subdivision vertex matrix.

    source
    theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.determinant_ofCoordinateAffineVertexMap {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F : CoordinateAffineVertexMap p) (q : TopCell hp N) :
    determinant hp N (ofCoordinateAffineVertexMap F) q = (CoordinateAffineVertexMap.deviation hp F).determinant (ReferenceAffineOrbitCount.topRepr hp q.1) * (AffineSubdivisionDeterminant.iterVertexMatrix (p - 1) N fun (k : Fin N) => Simplex.refinementIndexPerm (q.2 k)).det

    Determinant factorization for an original affine map on a refined simplex.

    source
    theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.regular_on_refinement_of_regular {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (F : CoordinateAffineVertexMap p) (hF : (CoordinateAffineVertexMap.deviation hp F).IsRegular) (q : TopCell hp N) :
    determinant hp N (ofCoordinateAffineVertexMap F) q ≠ 0

    Any original regular affine deviation map remains regular on every iterated subdivision.