Representing a charted support diagram

The old affine maps need only realize the support residues and commute on supported atoms. Injective modular lattice charts then give a surjective representation of the charted flag on its minimal ambient affine spaces.

noncomputable def EGZ.LatticeSupportDiagram.coordinateMap {p d : ℕ} [Fact (Nat.Prime p)] (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) (φ : (x : D.Node) → FpCoord p d →ᵃ[ZMod p] FpCoord p (D.rank x)) (x : D.Node) : FpCoord p d →ᵃ[ZMod p] FpCoord p (C x).rank

Express the old coordinate map through the modular chart's left inverse.

Equations

• D.coordinateMap C φ x = (C x).rechartMap (φ x)

theorem EGZ.LatticeSupportDiagram.coordinateMap_eq_mod {p d : ℕ} [Fact (Nat.Prime p)] (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) (φ : (x : D.Node) → FpCoord p d →ᵃ[ZMod p] FpCoord p (D.rank x)) (hinj : ∀ (x : D.Node), Function.Injective ⇑((D.chart C x).modp p)) (x : D.Node) (v : FpCoord p d) (q : IntCoord (C x).rank) (hv : (φ x) v = IntCoord.mod p ((C x).map q)) : (D.coordinateMap C φ x) v = IntCoord.mod p q

theorem EGZ.LatticeSupportDiagram.coordinateMap_image_support {p d : ℕ} [Fact (Nat.Prime p)] (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) (w : D.Node → FpCoord p d → ℕ) (φ : (x : D.Node) → FpCoord p d →ᵃ[ZMod p] FpCoord p (D.rank x)) (hinj : ∀ (x : D.Node), Function.Injective ⇑((D.chart C x).modp p)) (himage : ∀ (x : D.Node), ⇑(φ x) '' {v : FpCoord p d | FlagDecompositionRaw.cumulativeWeight w x v ≠ 0} = IntCoord.mod p '' ↑(D.support x)) (x : D.Node) : ⇑(D.coordinateMap C φ x) '' {v : FpCoord p d | FlagDecompositionRaw.cumulativeWeight w x v ≠ 0} = IntCoord.mod p '' ↑(C x).coordinateSupport

theorem EGZ.LatticeSupportDiagram.chart_coordinateMap {p d : ℕ} [Fact (Nat.Prime p)] (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) (w : D.Node → FpCoord p d → ℕ) (φ : (x : D.Node) → FpCoord p d →ᵃ[ZMod p] FpCoord p (D.rank x)) (hinj : ∀ (x : D.Node), Function.Injective ⇑((D.chart C x).modp p)) (himage : ∀ (x : D.Node), ⇑(φ x) '' {v : FpCoord p d | FlagDecompositionRaw.cumulativeWeight w x v ≠ 0} = IntCoord.mod p '' ↑(D.support x)) (x : D.Node) (v : FpCoord p d) (hv : FlagDecompositionRaw.cumulativeWeight w x v ≠ 0) : ((D.chart C x).modp p) ((D.coordinateMap C φ x) v) = (φ x) v

theorem EGZ.LatticeSupportDiagram.coordinateMap_compatible {p d : ℕ} [Fact (Nat.Prime p)] (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) (w : D.Node → FpCoord p d → ℕ) (φ : (x : D.Node) → FpCoord p d →ᵃ[ZMod p] FpCoord p (D.rank x)) (hinj : ∀ (x : D.Node), Function.Injective ⇑((D.chart C x).modp p)) (himage : ∀ (x : D.Node), ⇑(φ x) '' {v : FpCoord p d | FlagDecompositionRaw.cumulativeWeight w x v ≠ 0} = IntCoord.mod p '' ↑(D.support x)) (hcompat : ∀ {x y : D.Node} (h : x ≤ y) {v : FpCoord p d}, FlagDecompositionRaw.cumulativeWeight w x v ≠ 0 → (φ y) v = ((D.transition h).modp p) ((φ x) v)) {x y : D.Node} (h : x ≤ y) {v : FpCoord p d} (hv : FlagDecompositionRaw.cumulativeWeight w x v ≠ 0) : (D.coordinateMap C φ y) v = ((D.chartedTransition C h).modp p) ((D.coordinateMap C φ x) v)

noncomputable def EGZ.LatticeSupportDiagram.chartedRepresentation {p d : ℕ} [Fact (Nat.Prime p)] (D : LatticeSupportDiagram) (C : (x : D.Node) → IntegerLatticeChart (D.support x)) (w : D.Node → FpCoord p d → ℕ) (φ : (x : D.Node) → FpCoord p d →ᵃ[ZMod p] FpCoord p (D.rank x)) (hinj : ∀ (x : D.Node), Function.Injective ⇑((D.chart C x).modp p)) (himage : ∀ (x : D.Node), ⇑(φ x) '' {v : FpCoord p d | FlagDecompositionRaw.cumulativeWeight w x v ≠ 0} = IntCoord.mod p '' ↑(D.support x)) (hcompat : ∀ {x y : D.Node} (h : x ≤ y) {v : FpCoord p d}, FlagDecompositionRaw.cumulativeWeight w x v ≠ 0 → (φ y) v = ((D.transition h).modp p) ((φ x) v)) : FpRepresentation p d (D.chartedFlag C)

The actual representation of the charted support diagram.

Equations

• D.chartedRepresentation C w φ hinj himage hcompat = EGZ.FpRepresentation.ofCumulativeSupport w (D.coordinateMap C φ) (fun (x : (D.chartedFlag C).Node) => (C x).coordinateSupport) ⋯ ⋯ ⋯ ⋯