Minimal finite-field representations after changing lattice coordinates

Restrict each ambient affine space to the span of its cumulative support. An affine left inverse of the modular lattice chart then gives a surjective representation in the new coordinates, compatible with all transitions.

def EGZ.FlagDecomposition.Rechart.space {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) : AffineSubspace (ZMod p) (FpCoord p d)

The minimal ambient affine space at a node.

Equations

• EGZ.FlagDecomposition.Rechart.space Φ x = affineSpan (ZMod p) {v : EGZ.FpCoord p d | Φ.cumulativeWeight x v ≠ 0}

noncomputable def EGZ.FlagDecomposition.Rechart.map {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (x : Φ.flag.Node) : FpCoord p d →ᵃ[ZMod p] FpCoord p (C x).rank

The old representation expressed through an affine left inverse of the modular chart. The definition is an affine map on the whole ambient space.

Equations

• EGZ.FlagDecomposition.Rechart.map Φ C x = (EGZ.affineLeftInverse ((EGZ.FlagDecomposition.Rechart.chart Φ C x).modp p)).comp (Φ.representation.map x)

theorem EGZ.FlagDecomposition.Rechart.space_mono {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) {x y : Φ.flag.Node} (h : x ≤ y) : space Φ x ≤ space Φ y

theorem EGZ.FlagDecomposition.Rechart.space_le_original {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) : space Φ x ≤ Φ.representation.space x

theorem EGZ.FlagDecomposition.Rechart.localWeight_supported {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (v : FpCoord p d) (hv : Φ.localWeight x v ≠ 0) : v ∈ space Φ x

theorem EGZ.FlagDecomposition.Rechart.exists_liftedSupport_of_cumulative_ne_zero {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : Φ.flag.Node) (v : FpCoord p d) (hv : Φ.cumulativeWeight x v ≠ 0) : ∃ z ∈ Φ.liftedSupport x, IntCoord.mod p z = (Φ.representation.map x) v

theorem EGZ.FlagDecomposition.Rechart.exists_cumulative_of_liftedSupport {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (x : Φ.flag.Node) (z : IntCoord (Φ.flag.rank x)) (hz : z ∈ Φ.liftedSupport x) : ∃ (v : FpCoord p d), Φ.cumulativeWeight x v ≠ 0 ∧ (Φ.representation.map x) v = IntCoord.mod p z

theorem EGZ.FlagDecomposition.Rechart.original_map_mem_chart_range {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (x : Φ.flag.Node) (v : FpCoord p d) (hv : Φ.cumulativeWeight x v ≠ 0) : (Φ.representation.map x) v ∈ Set.range ⇑((chart Φ C x).modp p)

theorem EGZ.FlagDecomposition.Rechart.chart_map {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) (x : Φ.flag.Node) (v : FpCoord p d) (hv : v ∈ space Φ x) : ((chart Φ C x).modp p) ((map Φ C x) v) = (Φ.representation.map x) v

Retraction through a chart recovers the original representation on the full minimal ambient affine space.

theorem EGZ.FlagDecomposition.Rechart.map_eq_mod {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) (x : Φ.flag.Node) (v : FpCoord p d) (q : IntCoord (C x).rank) (hv : (Φ.representation.map x) v = IntCoord.mod p ((C x).map q)) : (map Φ C x) v = IntCoord.mod p q

The new representation takes the residue of a charted support point to its new finite-field coordinates.

theorem EGZ.FlagDecomposition.Rechart.image_cumulative_support {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) (x : Φ.flag.Node) : ⇑(map Φ C x) '' {v : FpCoord p d | Φ.cumulativeWeight x v ≠ 0} = IntCoord.mod p '' ↑(C x).coordinateSupport

The representation image of the old cumulative support is exactly the reduction of the coordinate support of the lattice chart.

theorem EGZ.FlagDecomposition.Rechart.map_surjective {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) (x : Φ.flag.Node) : Set.SurjOn (⇑(map Φ C x)) (↑(space Φ x)) Set.univ

theorem EGZ.FlagDecomposition.Rechart.map_compatible {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) {x y : Φ.flag.Node} (h : x ≤ y) {v : FpCoord p d} (hv : v ∈ space Φ x) : (map Φ C y) v = ((transition Φ C h).modp p) ((map Φ C x) v)

noncomputable def EGZ.FlagDecomposition.Rechart.representation {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (C : (x : Φ.flag.Node) → IntegerLatticeChart (Φ.liftedSupport x)) (hp : Odd p) (hinj : ∀ (x : Φ.flag.Node), Function.Injective ⇑((chart Φ C x).modp p)) : FpRepresentation p d (flag Φ C)

The finite-field representation in minimal lattice and ambient affine coordinates. Modular injectivity is the only chart hypothesis.

Equations

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