Documentation

LeanPool.NandakumarRamanaRao.NRR.PrimePolyhedron.FoxNeuwirth.ExplicitAffineRelativeCollarCompose

Composition of endpoint-identified 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.internalFacet_eq {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (q : RefinedAffineMap.TopCell hp Nmid) :
Combined.leftFacet C.cells D.cells (C.upperFacet q) = Combined.rightFacet C.cells D.cells (D.lowerFacet q)

The two copies of every common endpoint facet define the same combined quotient facet.

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

External lower coefficient of the composed collar.

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

    External upper coefficient of the composed collar.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.internalPairings_eq {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (s : (combinedCells C.cells D.cells).Facet) :
      ∑ t : C.cells.Facet, C.upperBoundaryCoefficient t * Combined.leftIndicator C.cells D.cells s t = ∑ t : D.cells.Facet, D.lowerBoundaryCoefficient t * Combined.rightIndicator C.cells D.cells s t

      The common endpoint contributions of the two component collars cancel pointwise.

      source
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.incidence_eq_boundary {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (s : (combinedCells C.cells D.cells).Facet) :
      (combinedCells C.cells D.cells).facetIncidence s = upperBoundaryCoefficient C D s - lowerBoundaryCoefficient C D s

      Pointwise boundary formula for the composed collar.

      source
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.lowerFacet_isLower {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (q : RefinedAffineMap.TopCell hp N₀) :
      (combinedCells C.cells D.cells).IsLowerFacet (Combined.leftFacet C.cells D.cells (C.lowerFacet q))

      Canonical lower endpoint facets are lower horizontal in the combined cylinder.

      source
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.upperFacet_isUpper {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (q : RefinedAffineMap.TopCell hp N₁) :
      (combinedCells C.cells D.cells).IsUpperFacet (Combined.rightFacet C.cells D.cells (D.upperFacet q))

      Canonical upper endpoint facets are upper horizontal in the combined cylinder.

      source
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.lowerBoundaryCoefficient_zero_of_not_lower {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (s : (combinedCells C.cells D.cells).Facet) (hs : ¬(combinedCells C.cells D.cells).IsLowerFacet s) :
      lowerBoundaryCoefficient C D s = 0

      External lower coefficients vanish away from the lower horizontal boundary.

      source
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.upperBoundaryCoefficient_zero_of_not_upper {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (s : (combinedCells C.cells D.cells).Facet) (hs : ¬(combinedCells C.cells D.cells).IsUpperFacet s) :
      upperBoundaryCoefficient C D s = 0

      External upper coefficients vanish away from the upper horizontal boundary.

      source
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.lowerFacet_exhaustive {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (s : (combinedCells C.cells D.cells).Facet) (hs : (combinedCells C.cells D.cells).IsLowerFacet s) :
      ∃ (q : RefinedAffineMap.TopCell hp N₀), Combined.leftFacet C.cells D.cells (C.lowerFacet q) = s

      Every lower-horizontal combined quotient facet comes from the external lower boundary.

      source
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.upperFacet_exhaustive {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (s : (combinedCells C.cells D.cells).Facet) (hs : (combinedCells C.cells D.cells).IsUpperFacet s) :
      ∃ (q : RefinedAffineMap.TopCell hp N₁), Combined.rightFacet C.cells D.cells (D.upperFacet q) = s

      Every upper-horizontal combined quotient facet comes from the external upper boundary.

      source
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.lowerBoundaryPairing_eq {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (W : (combinedCells C.cells D.cells).Facet → ZMod p) :
      ∑ s : (combinedCells C.cells D.cells).Facet, lowerBoundaryCoefficient C D s * W s = ∑ q : RefinedAffineMap.TopCell hp N₀, RefinedAffineMap.coefficient hp N₀ q * W (Combined.leftFacet C.cells D.cells (C.lowerFacet q))

      Chain-level lower endpoint identity for the composed collar.

      source
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.upperBoundaryPairing_eq {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (W : (combinedCells C.cells D.cells).Facet → ZMod p) :
      ∑ s : (combinedCells C.cells D.cells).Facet, upperBoundaryCoefficient C D s * W s = ∑ q : RefinedAffineMap.TopCell hp N₁, RefinedAffineMap.coefficient hp N₁ q * W (Combined.rightFacet C.cells D.cells (D.upperFacet q))

      Chain-level upper endpoint identity for the composed collar.

      source
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.lowerFacetOccurrenceVertex_eq {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (q : RefinedAffineMap.TopCell hp N₀) (o : (combinedCells C.cells D.cells).FacetOccurrence) (ho : (combinedCells C.cells D.cells).facetClass o = Combined.leftFacet C.cells D.cells (C.lowerFacet q)) :
      ∃ (g : ↥(PrimeSymmetry p)), ∀ (i : Fin p), (combinedCells C.cells D.cells).facetSignature o i = g • ExplicitAffineRelativeCollar.lowerCylinderPoint (RefinedAffineMap.vertex hp N₀ q (Fin.cast ⋯ i))

      Representatives of external lower facets have the prescribed level-N₀ geometry.

      source
      theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.upperFacetOccurrenceVertex_eq {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp Nmid N₁ M₁ L₁) (q : RefinedAffineMap.TopCell hp N₁) (o : (combinedCells C.cells D.cells).FacetOccurrence) (ho : (combinedCells C.cells D.cells).facetClass o = Combined.rightFacet C.cells D.cells (D.upperFacet q)) :
      ∃ (g : ↥(PrimeSymmetry p)), ∀ (i : Fin p), (combinedCells C.cells D.cells).facetSignature o i = g • ExplicitAffineRelativeCollar.upperCylinderPoint (RefinedAffineMap.vertex hp N₁ q (Fin.cast ⋯ i))

      Representatives of external upper facets have the prescribed level-N₁ geometry.

      source
      noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.relativeCollar {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp Nmid N₁ M₁ L₁) :
      ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar hp N₀ N₁ (max M₀ M₁) (L₀ + L₁ + 1)

      Pointwise composed relative collar.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollarCompose.endpointIdentifiedCollar {p N₀ Nmid N₁ M₀ M₁ L₀ L₁ : ℕ} {hp : Nat.Prime p} (C : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp Nmid N₁ M₁ L₁) :
        ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar hp N₀ N₁ (max M₀ M₁) (L₀ + L₁ + 1)

        Composition of endpoint-identified relative affine collars.

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