Support diagrams with additional slab coordinates

At each node append an initial segment of a common sequence of affine functionals to the old coordinate map. An antitone number of additional coordinates ensures that transitions retain exactly the available prefix. Centered lifts of cumulative atoms give a finite support diagram, even when the augmented finite-field maps are not surjective.

def EGZ.FlagDecomposition.Augmented.lift {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (x : Φ.flag.Node) (v : FpCoord p d) : IntCoord (Φ.flag.rank x + e x)

The integer lift of one ambient atom with its extra slab coordinates.

Equations

• EGZ.FlagDecomposition.Augmented.lift Φ e ξ x v = Fin.append ((Φ.representation.map x) v).centeredLift (EGZ.slabCoordinates (e x) ξ v)

@[simp]

theorem EGZ.FlagDecomposition.Augmented.lift_first {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (x : Φ.flag.Node) (v : FpCoord p d) : (Coord.first (Φ.flag.rank x) (e x)) (lift Φ e ξ x v) = ((Φ.representation.map x) v).centeredLift

@[simp]

theorem EGZ.FlagDecomposition.Augmented.lift_last {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (x : Φ.flag.Node) (v : FpCoord p d) : (Coord.last (Φ.flag.rank x) (e x)) (lift Φ e ξ x v) = slabCoordinates (e x) ξ v

def EGZ.FlagDecomposition.Augmented.map {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (x : Φ.flag.Node) : FpCoord p d →ᵃ[ZMod p] FpCoord p (Φ.flag.rank x + e x)

The finite-field affine map augmented by the same sequence of directions.

Equations

• EGZ.FlagDecomposition.Augmented.map Φ e ξ x = EGZ.Coord.append (Φ.representation.map x) (AffineMap.pi fun (i : Fin (e x)) => ξ ↑i)

@[simp]

theorem EGZ.FlagDecomposition.Augmented.lift_mod {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (x : Φ.flag.Node) (v : FpCoord p d) : IntCoord.mod p (lift Φ e ξ x v) = (map Φ e ξ x) v

noncomputable def EGZ.FlagDecomposition.Augmented.support {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (x : Φ.flag.Node) : Finset (IntCoord (Φ.flag.rank x + e x))

The augmented support consists of lifts of the nonzero cumulative atoms.

Equations

• EGZ.FlagDecomposition.Augmented.support Φ e ξ x = Finset.image (EGZ.FlagDecomposition.Augmented.lift Φ e ξ x) {v : EGZ.FpCoord p d | Φ.cumulativeWeight x v ≠ 0}

@[simp]

theorem EGZ.FlagDecomposition.Augmented.mem_support {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (x : Φ.flag.Node) (q : IntCoord (Φ.flag.rank x + e x)) : q ∈ support Φ e ξ x ↔ ∃ (v : FpCoord p d), Φ.cumulativeWeight x v ≠ 0 ∧ lift Φ e ξ x v = q

theorem EGZ.FlagDecomposition.Augmented.support_nonempty {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (x : Φ.flag.Node) : (support Φ e ξ x).Nonempty

theorem EGZ.FlagDecomposition.Augmented.support_mod {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (x : Φ.flag.Node) : IntCoord.mod p '' ↑(support Φ e ξ x) = ⇑(map Φ e ξ x) '' {v : FpCoord p d | Φ.cumulativeWeight x v ≠ 0}

Reducing the augmented integer support gives precisely the finite-field image of the cumulative support.

theorem EGZ.FlagDecomposition.Augmented.first_image_support {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (hp : Odd p) (x : Φ.flag.Node) : Finset.image (⇑(Coord.first (Φ.flag.rank x) (e x))) (support Φ e ξ x) = Φ.liftedSupport x

Projection of the augmented support recovers the entire old lifted support.

noncomputable def EGZ.FlagDecomposition.Augmented.transition {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (he : Antitone e) {x y : Φ.flag.Node} (h : x ≤ y) : IntegralAffineMap (Φ.flag.rank x + e x) (Φ.flag.rank y + e y)

Along an order relation keep only the upper node's prefix of directions.

Equations

• EGZ.FlagDecomposition.Augmented.transition Φ e he h = (Φ.flag.transition h).extendPrefix (e x) (e y) ⋯

theorem EGZ.FlagDecomposition.Augmented.transition_lift {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (hp : Odd p) (he : Antitone e) {x y : Φ.flag.Node} (h : x ≤ y) (v : FpCoord p d) (hv : Φ.cumulativeWeight x v ≠ 0) : (transition Φ e he h).integer (lift Φ e ξ x v) = lift Φ e ξ y v

theorem EGZ.FlagDecomposition.Augmented.transition_support {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (hp : Odd p) (he : Antitone e) {x y : Φ.flag.Node} (h : x ≤ y) {q : IntCoord (Φ.flag.rank x + e x)} (hq : q ∈ support Φ e ξ x) : (transition Φ e he h).integer q ∈ support Φ e ξ y

theorem EGZ.FlagDecomposition.Augmented.transition_refl {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (he : Antitone e) (x : Φ.flag.Node) : transition Φ e he ⋯ = IntegralAffineMap.id (Φ.flag.rank x + e x)

theorem EGZ.FlagDecomposition.Augmented.transition_trans {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (he : Antitone e) {x y z : Φ.flag.Node} (hxy : x ≤ y) (hyz : y ≤ z) : transition Φ e he ⋯ = (transition Φ e he hyz).comp (transition Φ e he hxy)

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.Augmented.diagram {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (hp : Odd p) (he : Antitone e) : LatticeSupportDiagram

The actual support diagram used before minimalizing augmented fibres.

Equations

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

theorem EGZ.FlagDecomposition.Augmented.first_image_polytope {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (hp : Odd p) (he : Antitone e) (x : Φ.flag.Node) : ⇑(IntegralAffineMap.first (Φ.flag.rank x) (e x)).real '' ((diagram Φ e ξ hp he).polytope x).carrier = (Φ.flag.polytope x).carrier

The old-coordinate projection maps the augmented support hull onto the original node polytope.

theorem EGZ.FlagDecomposition.Augmented.map_compatible {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (he : Antitone e) {x y : Φ.flag.Node} (h : x ≤ y) {v : FpCoord p d} (hv : v ∈ Φ.representation.space x) : (map Φ e ξ y) v = ((transition Φ e he h).modp p) ((map Φ e ξ x) v)

The augmented affine maps commute with the augmented transitions on the old represented affine spaces.

theorem EGZ.FlagDecomposition.Augmented.first_comp_transition {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (he : Antitone e) {x y : Φ.flag.Node} (h : x ≤ y) : (IntegralAffineMap.first (Φ.flag.rank y) (e y)).comp (transition Φ e he h) = (Φ.flag.transition h).comp (IntegralAffineMap.first (Φ.flag.rank x) (e x))

Forgetting the slab coordinates commutes with diagram transitions.

theorem EGZ.FlagDecomposition.Augmented.lift_centered {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (hp : Odd p) (x : Φ.flag.Node) (v : FpCoord p d) : IsCenteredLift p (lift Φ e ξ x v)

theorem EGZ.FlagDecomposition.Augmented.support_centered {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (hp : Odd p) (x : Φ.flag.Node) (q : IntCoord (Φ.flag.rank x + e x)) (hq : q ∈ support Φ e ξ x) : IsCenteredLift p q

theorem EGZ.FlagDecomposition.Augmented.support_bound {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (e : Φ.flag.Node → ℕ) (ξ : ℕ → FpCoord p d →ᵃ[ZMod p] ZMod p) (hp : Odd p) {K L : Φ.flag.Node → ℕ} (hK : Φ.IsKBounded K) (hL : ∀ (x : Φ.flag.Node) (v : FpCoord p d), Φ.cumulativeWeight x v ≠ 0 → latticeSupNorm (slabCoordinates (e x) ξ v) ≤ L x) (x : Φ.flag.Node) (q : IntCoord (Φ.flag.rank x + e x)) (hq : q ∈ support Φ e ξ x) : latticeSupNorm q ≤ max (K x) (L x)

Bounds for the old support and slab block give a uniform bound for every augmented support point.