Documentation

LeanPool.NandakumarRamanaRao.NRR.PrimePolyhedron.FoxNeuwirth.RelativeCollarThinSlabsEndpoints

Endpoint identification for thin-time stacks #

The external lower face of the first slab and external upper face of the last slab carry exactly the original level-N Fox--Neuwirth orbit chain. All intermediate mesh faces were already cancelled by the telescoping boundary theorem. This module supplies the endpoint quotient-facet maps, chain pairing identities, exhaustiveness, and representative geometry required by EndpointIdentifiedRelativeAffineCollar.

source
def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.firstSlab (m : ℕ) (hm : 0 < m) :
Fin m

First slab of a positive stack.

Equations
Instances For
    source
    def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.lastSlab (m : ℕ) (hm : 0 < m) :
    Fin m

    Last slab of a positive stack.

    Equations
    Instances For
      source
      @[simp]
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.firstSlab_val (m : ℕ) (hm : 0 < m) :
      ↑(firstSlab m hm) = 0
      source
      @[simp]
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.lastSlab_succ_eq_last (m : ℕ) (hm : 0 < m) :
      (lastSlab m hm).succ = Fin.last m
      source
      noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.lowerOccurrence {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (q : RefinedAffineMap.TopCell hp N) :
      (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).FacetOccurrence

      Canonical lower occurrence of a level-N spatial top cell in the first slab.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.upperOccurrence {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (q : RefinedAffineMap.TopCell hp N) :
        (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).FacetOccurrence

        Canonical upper occurrence of a level-N spatial top cell in the last slab.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.lowerFacet {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (q : RefinedAffineMap.TopCell hp N) :
          (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).Facet

          Canonical lower quotient facet.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.upperFacet {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (q : RefinedAffineMap.TopCell hp N) :
            (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).Facet

            Canonical upper quotient facet.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.lowerOccurrence_facetSignature {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (q : RefinedAffineMap.TopCell hp N) (i : Fin p) :
              (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).facetSignature (lowerOccurrence hp N m hm q) i = ExplicitAffineRelativeCollar.lowerCylinderPoint (RefinedAffineMap.vertex hp N q (Fin.cast ⋯ i))

              Ordered vertices of the canonical lower occurrence are exactly the level-N lower endpoint vertices.

              source
              theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.upperOccurrence_facetSignature {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (q : RefinedAffineMap.TopCell hp N) (i : Fin p) :
              (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).facetSignature (upperOccurrence hp N m hm q) i = ExplicitAffineRelativeCollar.upperCylinderPoint (RefinedAffineMap.vertex hp N q (Fin.cast ⋯ i))

              Ordered vertices of the canonical upper occurrence are exactly the level-N upper endpoint vertices.

              source
              theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.lowerFacet_isLower {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (q : RefinedAffineMap.TopCell hp N) :
              (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).IsLowerFacet (lowerFacet hp N m hm q)

              Canonical lower facets are lower horizontal.

              source
              theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.upperFacet_isUpper {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (q : RefinedAffineMap.TopCell hp N) :
              (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).IsUpperFacet (upperFacet hp N m hm q)

              Canonical upper facets are upper horizontal.

              source
              theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.mapVertexSignature_meshLower {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (q : RefinedAffineMap.TopCell hp N) :
              EquivariantPrismNonhorizontalCancellation.mapVertexSignature (RelativeCollarThinSlabsBoundary.meshEndpointMap m hm 0 ⇑(RefinedAffineMap.chart hp N q)) = (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).facetSignature (lowerOccurrence hp N m hm q)

              Vertex-map signature of the canonical lower occurrence.

              source
              theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.mapVertexSignature_meshUpper {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (q : RefinedAffineMap.TopCell hp N) :
              EquivariantPrismNonhorizontalCancellation.mapVertexSignature (RelativeCollarThinSlabsBoundary.meshEndpointMap m hm (Fin.last m) ⇑(RefinedAffineMap.chart hp N q)) = (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).facetSignature (upperOccurrence hp N m hm q)

              Vertex-map signature of the canonical upper occurrence.

              source
              theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.stackFacetOrbitIndicator_meshLower {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).Facet) (q : RefinedAffineMap.TopCell hp N) :
              RelativeCollarThinSlabsBoundary.stackFacetOrbitIndicator hp N m hm s (RelativeCollarThinSlabsBoundary.meshEndpointMap m hm 0 ⇑(RefinedAffineMap.chart hp N q)) = if lowerFacet hp N m hm q = s then 1 else 0

              External lower mesh indicators are the Kronecker weights of canonical lower quotient facets.

              source
              theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.stackFacetOrbitIndicator_meshUpper {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).Facet) (q : RefinedAffineMap.TopCell hp N) :
              RelativeCollarThinSlabsBoundary.stackFacetOrbitIndicator hp N m hm s (RelativeCollarThinSlabsBoundary.meshEndpointMap m hm (Fin.last m) ⇑(RefinedAffineMap.chart hp N q)) = if upperFacet hp N m hm q = s then 1 else 0

              External upper mesh indicators are the Kronecker weights of canonical upper quotient facets.

              source
              theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.lowerBoundaryPairing_eq {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (W : (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).Facet → ZMod p) :
              ∑ s : (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).Facet, RelativeCollarThinSlabsBoundary.lowerBoundaryCoefficient hp N m hm s * W s = ∑ q : RefinedAffineMap.TopCell hp N, RefinedAffineMap.coefficient hp N q * W (lowerFacet hp N m hm q)

              Chain-level lower endpoint pairing identity.

              source
              theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.upperBoundaryPairing_eq {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (W : (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).Facet → ZMod p) :
              ∑ s : (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).Facet, RelativeCollarThinSlabsBoundary.upperBoundaryCoefficient hp N m hm s * W s = ∑ q : RefinedAffineMap.TopCell hp N, RefinedAffineMap.coefficient hp N q * W (upperFacet hp N m hm q)

              Chain-level upper endpoint pairing identity.

              source
              theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.stackFacetClass_eq_of_baseFacetClass_eq {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (r : Fin m) {o o' : (RelativeCollarThinSlabsBoundary.BaseCells hp N).FacetOccurrence} (h : (RelativeCollarThinSlabsBoundary.BaseCells hp N).facetClass o = (RelativeCollarThinSlabsBoundary.BaseCells hp N).facetClass o') :
              (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).facetClass (RelativeCollarThinSlabsBoundary.stackOccurrence hp N m hm r o) = (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).facetClass (RelativeCollarThinSlabsBoundary.stackOccurrence hp N m hm r o')

              Equality of base quotient facets lifts to equality of their copies in one fixed slab.

              source
              theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.lowerOccurrence_reduction {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (r : Fin m) (o : (RelativeCollarThinSlabsBoundary.BaseCells hp N).FacetOccurrence) (h : (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).IsLowerFacetOccurrence (RelativeCollarThinSlabsBoundary.stackOccurrence hp N m hm r o)) :
              r = firstSlab m hm ∧ (RelativeCollarThinSlabsBoundary.BaseCells hp N).IsLowerFacetOccurrence o

              A lower-horizontal stack occurrence necessarily belongs to the first slab and its underlying base occurrence is lower horizontal.

              source
              theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.upperOccurrence_reduction {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (r : Fin m) (o : (RelativeCollarThinSlabsBoundary.BaseCells hp N).FacetOccurrence) (h : (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).IsUpperFacetOccurrence (RelativeCollarThinSlabsBoundary.stackOccurrence hp N m hm r o)) :
              r = lastSlab m hm ∧ (RelativeCollarThinSlabsBoundary.BaseCells hp N).IsUpperFacetOccurrence o

              An upper-horizontal stack occurrence necessarily belongs to the last slab and its underlying base occurrence is upper horizontal.

              source
              theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.lowerFacet_exhaustive {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).Facet) (hs : (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).IsLowerFacet s) :
              ∃ (q : RefinedAffineMap.TopCell hp N), lowerFacet hp N m hm q = s

              Every lower horizontal quotient facet is represented by a canonical level-N lower facet.

              source
              theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.upperFacet_exhaustive {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (s : (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).Facet) (hs : (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).IsUpperFacet s) :
              ∃ (q : RefinedAffineMap.TopCell hp N), upperFacet hp N m hm q = s

              Every upper horizontal quotient facet is represented by a canonical level-N upper facet.

              source
              theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.lowerFacetOccurrenceVertex_eq {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (q : RefinedAffineMap.TopCell hp N) (o : (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).FacetOccurrence) (ho : (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).facetClass o = lowerFacet hp N m hm q) :
              ∃ (g : ↥(PrimeSymmetry p)), ∀ (i : Fin p), (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).facetSignature o i = g • ExplicitAffineRelativeCollar.lowerCylinderPoint (RefinedAffineMap.vertex hp N q (Fin.cast ⋯ i))

              Every representative of a canonical lower quotient facet has the prescribed endpoint vertices, up to one simultaneous prime relabelling.

              source
              theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.upperFacetOccurrenceVertex_eq {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) (q : RefinedAffineMap.TopCell hp N) (o : (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).FacetOccurrence) (ho : (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).facetClass o = upperFacet hp N m hm q) :
              ∃ (g : ↥(PrimeSymmetry p)), ∀ (i : Fin p), (RelativeCollarThinSlabsBoundary.StackCells hp N m hm).facetSignature o i = g • ExplicitAffineRelativeCollar.upperCylinderPoint (RefinedAffineMap.vertex hp N q (Fin.cast ⋯ i))

              Every representative of a canonical upper quotient facet has the prescribed endpoint vertices, up to one simultaneous prime relabelling.

              source
              noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RelativeCollarThinSlabsEndpoints.endpointIdentifiedCollar {p : ℕ} (hp : Nat.Prime p) (N m : ℕ) (hm : 0 < m) :
              ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N N N m

              A positive thin-time stack is a complete endpoint-identified relative affine collar with the original spatial level fixed at both endpoints.

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