Representations generated by cumulative supports

Affine coordinate maps compatible on the nonzero cumulative atoms extend to compatible maps on their affine spans. If their support images are reductions of integer affine generators, these maps are surjective on the spans. This constructs a representation without assuming surjectivity of the original coordinate maps on the ambient space.

theorem EGZ.FlagDecompositionRaw.localWeight_le_cumulative {p d : ℕ} {F : ConvexFlag} (w : F.Node → FpCoord p d → ℕ) (x : F.Node) (v : FpCoord p d) : w x v ≤ cumulativeWeight w x v

Local weights contribute to the cumulative weight at their own node.

theorem EGZ.FlagDecompositionRaw.cumulativeWeight_node_mono {p d : ℕ} {F : ConvexFlag} (w : F.Node → FpCoord p d → ℕ) {x y : F.Node} (h : x ≤ y) (v : FpCoord p d) : cumulativeWeight w x v ≤ cumulativeWeight w y v

Cumulative weight is monotone in its node.

def EGZ.FpRepresentation.cumulativeSpace {p d : ℕ} {F : ConvexFlag} (w : F.Node → FpCoord p d → ℕ) (x : F.Node) : AffineSubspace (ZMod p) (FpCoord p d)

The smallest ambient affine space containing the cumulative support.

Equations

• EGZ.FpRepresentation.cumulativeSpace w x = affineSpan (ZMod p) {v : EGZ.FpCoord p d | EGZ.FlagDecompositionRaw.cumulativeWeight w x v ≠ 0}

theorem EGZ.FpRepresentation.cumulativeSpace_mono {p d : ℕ} {F : ConvexFlag} (w : F.Node → FpCoord p d → ℕ) {x y : F.Node} (h : x ≤ y) : cumulativeSpace w x ≤ cumulativeSpace w y

theorem EGZ.FpRepresentation.local_supported_cumulativeSpace {p d : ℕ} {F : ConvexFlag} (w : F.Node → FpCoord p d → ℕ) (x : F.Node) (v : FpCoord p d) (hv : w x v ≠ 0) : v ∈ cumulativeSpace w x

theorem EGZ.FpRepresentation.compatible_on_cumulativeSpace {p d : ℕ} {F : ConvexFlag} (w : F.Node → FpCoord p d → ℕ) (ψ : (x : F.Node) → FpCoord p d →ᵃ[ZMod p] FpCoord p (F.rank x)) (hcompat : ∀ {x y : F.Node} (h : x ≤ y) {v : FpCoord p d}, FlagDecompositionRaw.cumulativeWeight w x v ≠ 0 → (ψ y) v = ((F.transition h).modp p) ((ψ x) v)) {x y : F.Node} (h : x ≤ y) {v : FpCoord p d} (hv : v ∈ cumulativeSpace w x) : (ψ y) v = ((F.transition h).modp p) ((ψ x) v)

Compatibility on nonzero cumulative atoms extends to the full affine space generated by those atoms.

noncomputable def EGZ.FpRepresentation.ofCumulativeSupport {p d : ℕ} {F : ConvexFlag} [Fact (Nat.Prime p)] (w : F.Node → FpCoord p d → ℕ) (ψ : (x : F.Node) → FpCoord p d →ᵃ[ZMod p] FpCoord p (F.rank x)) (S : (x : F.Node) → Finset (IntCoord (F.rank x))) (hS : ∀ (x : F.Node), FlagDecomposition.AffineIntSpans (S x)) (himage : ∀ (x : F.Node), ⇑(ψ x) '' {v : FpCoord p d | FlagDecompositionRaw.cumulativeWeight w x v ≠ 0} = IntCoord.mod p '' ↑(S x)) (hcompat : ∀ {x y : F.Node} (h : x ≤ y) {v : FpCoord p d}, FlagDecompositionRaw.cumulativeWeight w x v ≠ 0 → (ψ y) v = ((F.transition h).modp p) ((ψ x) v)) (hlattice : ∀ (x : F.Node) (q : RealCoord (F.rank x)), q ∈ F.lattice x ↔ IsIntegral q) : FpRepresentation p d F

Construct a representation from its cumulative support images. Integer affine generation supplies surjectivity, and compatibility is needed only on the nonzero cumulative atoms.

Equations

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