Documentation

LeanPool.NandakumarRamanaRao.NRR.PrimePolyhedron.FoxNeuwirth.ExplicitAffineRelativeCollarComposeCells

Cell system for composing relative affine collars #

Two collars with a common intermediate endpoint are placed in the lower and upper half of the realization cylinder. Their cell families are joined by disjoint union. The quotient-facet relation then identifies the two copies of every intermediate endpoint facet. The upper boundary pairing of the first collar and lower boundary pairing of the second collar are the same refined Fox--Neuwirth chain, hence cancel pointwise after regrouping by combined quotient facets.

source
theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.cylinderPoint_ext {p : ℕ} {z w : EquivariantPrismVertexParameters.CylinderPoint p} (hs : z.spatial = w.spatial) (ht : ↑z.time = ↑w.time) :
z = w

Two cylinder points agree when their spatial and interval coordinates agree.

source
noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.leftPoint {p : ℕ} (z : EquivariantPrismVertexParameters.CylinderPoint p) :
EquivariantPrismVertexParameters.CylinderPoint p

Place a cylinder point in the lower half-cylinder.

Equations
Instances For
    source
    noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.rightPoint {p : ℕ} (z : EquivariantPrismVertexParameters.CylinderPoint p) :
    EquivariantPrismVertexParameters.CylinderPoint p

    Place a cylinder point in the upper half-cylinder.

    Equations
    Instances For
      source
      @[simp]
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.leftPoint_spatial {p : ℕ} (z : EquivariantPrismVertexParameters.CylinderPoint p) :
      (leftPoint z).spatial = z.spatial
      source
      @[simp]
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.rightPoint_spatial {p : ℕ} (z : EquivariantPrismVertexParameters.CylinderPoint p) :
      (rightPoint z).spatial = z.spatial
      source
      @[simp]
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.leftPoint_time {p : ℕ} (z : EquivariantPrismVertexParameters.CylinderPoint p) :
      ↑(leftPoint z).time = ↑z.time / 2
      source
      @[simp]
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.rightPoint_time {p : ℕ} (z : EquivariantPrismVertexParameters.CylinderPoint p) :
      ↑(rightPoint z).time = (1 + ↑z.time) / 2
      source
      @[simp]
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.leftPoint_smul {p : ℕ} (g : ↥(PrimeSymmetry p)) (z : EquivariantPrismVertexParameters.CylinderPoint p) :
      leftPoint (g • z) = g • leftPoint z
      source
      @[simp]
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.rightPoint_smul {p : ℕ} (g : ↥(PrimeSymmetry p)) (z : EquivariantPrismVertexParameters.CylinderPoint p) :
      rightPoint (g • z) = g • rightPoint z
      source
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.leftPoint_injective {p : ℕ} :
      Function.Injective leftPoint

      Both half-cylinder embeddings are injective.

      source
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.rightPoint_injective {p : ℕ} :
      Function.Injective rightPoint

      Both half-cylinder embeddings are injective.

      source
      noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.middlePoint {p : ℕ} (x : Realization p) :
      EquivariantPrismVertexParameters.CylinderPoint p

      Common interface point at time 1/2.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.left_upper_eq_middle {p : ℕ} (x : Realization p) :
        leftPoint (ExplicitAffineRelativeCollar.upperCylinderPoint x) = middlePoint x
        source
        @[simp]
        theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.right_lower_eq_middle {p : ℕ} (x : Realization p) :
        rightPoint (ExplicitAffineRelativeCollar.lowerCylinderPoint x) = middlePoint x
        source
        @[simp]
        theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.left_lower_eq_lower {p : ℕ} (x : Realization p) :
        leftPoint (ExplicitAffineRelativeCollar.lowerCylinderPoint x) = ExplicitAffineRelativeCollar.lowerCylinderPoint x
        source
        @[simp]
        theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.right_upper_eq_upper {p : ℕ} (x : Realization p) :
        rightPoint (ExplicitAffineRelativeCollar.upperCylinderPoint x) = ExplicitAffineRelativeCollar.upperCylinderPoint x
        source
        noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.combinedCells {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) :
        ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ (max M₀ M₁) (L₀ + L₁ + 1)

        Combined affine cell system.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.Combined.leftOccurrence {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (o : C.FacetOccurrence) :
          (combinedCells C D).FacetOccurrence

          Embed a left local facet occurrence into the combined cell family.

          Equations
          Instances For
            source
            def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.Combined.rightOccurrence {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (o : D.FacetOccurrence) :
            (combinedCells C D).FacetOccurrence

            Embed a right local facet occurrence into the combined cell family.

            Equations
            Instances For
              source
              @[simp]
              theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.Combined.left_facetSignature {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (o : C.FacetOccurrence) :
              (combinedCells C D).facetSignature (leftOccurrence C D o) = fun (i : Fin p) => leftPoint (C.facetSignature o i)
              source
              @[simp]
              theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.Combined.right_facetSignature {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (o : D.FacetOccurrence) :
              (combinedCells C D).facetSignature (rightOccurrence C D o) = fun (i : Fin p) => rightPoint (D.facetSignature o i)
              source
              noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.Combined.leftFacet {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (s : C.Facet) :
              (combinedCells C D).Facet

              Push a left quotient facet into the combined quotient.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.Combined.rightFacet {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (s : D.Facet) :
                (combinedCells C D).Facet

                Push a right quotient facet into the combined quotient.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.Combined.leftFacet_facetClass {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (o : C.FacetOccurrence) :
                  leftFacet C D (C.facetClass o) = (combinedCells C D).facetClass (leftOccurrence C D o)
                  source
                  @[simp]
                  theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.Combined.rightFacet_facetClass {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (o : D.FacetOccurrence) :
                  rightFacet C D (D.facetClass o) = (combinedCells C D).facetClass (rightOccurrence C D o)
                  source
                  theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.Combined.leftFacet_injective {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) :
                  Function.Injective (leftFacet C D)

                  The left quotient-facet embedding is injective.

                  source
                  theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.Combined.rightFacet_injective {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) :
                  Function.Injective (rightFacet C D)

                  The right quotient-facet embedding is injective.

                  source
                  noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.Combined.leftIndicator {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (s : (combinedCells C D).Facet) (t : C.Facet) :
                  ZMod p

                  Kronecker weight for the image of one combined quotient facet.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.Combined.rightIndicator {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (s : (combinedCells C D).Facet) (t : D.Facet) :
                    ZMod p

                    Kronecker weight for the right image.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.Combined.occurrencePairing_eq_facetPairing {p : ℕ} {hp : Nat.Prime p} {A B E T : ℕ} (K : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp A B E T) (W : K.Facet → ZMod p) :
                      ∑ o : K.FacetOccurrence, K.coefficient o.1 * ExplicitAffineRelativeCollar.RelativeAffineCellSystem.alternatingSign o.2 * W (K.facetClass o) = ∑ s : K.Facet, K.facetIncidence s * W s

                      Generic finite regrouping of occurrence weights by quotient-facet incidence.

                      source
                      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.Combined.sum_combinedOccurrence {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (f : (combinedCells C D).FacetOccurrence → ZMod p) :
                      ∑ o : (combinedCells C D).FacetOccurrence, f o = ∑ o : C.FacetOccurrence, f (leftOccurrence C D o) + ∑ o : D.FacetOccurrence, f (rightOccurrence C D o)

                      Split a finite sum over combined facet occurrences into its two components.

                      source
                      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.Combined.combined_facetIncidence {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (s : (combinedCells C D).Facet) :
                      (combinedCells C D).facetIncidence s = ∑ t : C.Facet, C.facetIncidence t * leftIndicator C D s t + ∑ t : D.Facet, D.facetIncidence t * rightIndicator C D s t

                      Combined pointwise incidence is the sum of the two pushed-forward incidence pairings.