Documentation

LeanPool.NandakumarRamanaRao.NRR.PrimePolyhedron.FoxNeuwirth.StableFullCollarOriginMarginAffinePullback

Unconditional full-collar origin margin from the affine-pullback construction #

This file instantiates the generic compactness theorem of StableFullCollarOriginMargin with the concrete Step 4 collar constructed in StableFullCollarConstructionAffinePullback.

source
noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarOriginMarginAffinePullback.fullCollarOriginMarginDataAffinePullback {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) :
StableFullCollarOriginMargin.FullCollarOriginMarginData hp H A₀ A₁

Concrete quantitative origin-margin data attached to the affine-pullback full collar.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarOriginMarginAffinePullback.fullCollarOriginMargin_affinePullback {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) :
    Nonempty (StableFullCollarOriginMargin.FullCollarOriginMarginData hp H A₀ A₁)

    Step 5, specialized to the concrete Step 4 construction.

    source
    theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.StableFullCollarOriginMarginAffinePullback.affinePullback_margin_pos {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp) (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.StableRegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.StableRegularApproximation hp F₁.map) :
    0 < (fullCollarOriginMarginDataAffinePullback hp F₀ F₁ H A₀ A₁).margin

    The concrete collar has a positive coordinate norm margin.