Levels of represented flag nodes

The lexicographic pair consisting of representation codimension and lattice rank is encoded by a natural number. Levels are antitone along flag nodes and increase under restriction of the represented space when the old map factors through the new map. This includes minimalization.

def EGZ.LevelCode.code (d a b : ℕ) : ℕ

Encode two coordinates in the square [0,d]² in lexicographic order.

Equations

• EGZ.LevelCode.code d a b = (d + 1) * a + b

theorem EGZ.LevelCode.lt_of_first_lt {d a b a' b' : ℕ} (h : a < a') (hb : b ≤ d) : code d a b < code d a' b'

theorem EGZ.LevelCode.le_of_first_le {d a b a' b' : ℕ} (ha : a ≤ a') (hb : b ≤ d) (heq : a = a' → b ≤ b') : code d a b ≤ code d a' b'

theorem EGZ.LevelCode.eq_iff {d a b a' b' : ℕ} (hb : b ≤ d) (hb' : b' ≤ d) : code d a b = code d a' b' ↔ a = a' ∧ b = b'

theorem EGZ.LevelCode.lt_square {d a b : ℕ} (ha : a ≤ d) (hb : b ≤ d) : code d a b < (d + 1) ^ 2

noncomputable def EGZ.FpRepresentation.spaceDimension {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) : ℕ

Dimension of the represented affine space.

Equations

• R.spaceDimension x = Module.finrank (ZMod p) ↥(R.space x).direction

noncomputable def EGZ.FpRepresentation.codimension {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) : ℕ

Codimension of the represented affine space in the ambient space.

Equations

• R.codimension x = d - R.spaceDimension x

noncomputable def EGZ.FpRepresentation.level {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) : ℕ

Natural-number encoding of (codim V_x, rank Λ_x).

Equations

• R.level x = EGZ.LevelCode.code d (R.codimension x) (F.rank x)

theorem EGZ.FpRepresentation.space_nonempty {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) : (↑(R.space x)).Nonempty

theorem EGZ.FpRepresentation.spaceDimension_le {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) : R.spaceDimension x ≤ d

theorem EGZ.FpRepresentation.codimension_le {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) : R.codimension x ≤ d

theorem EGZ.FpRepresentation.level_lt {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) : R.level x < (d + 1) ^ 2

theorem EGZ.FpRepresentation.level_le {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) (x : F.Node) : R.level x ≤ (d + 1) ^ 2 - 1

theorem EGZ.FpRepresentation.codimension_le_of_space_le {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} {G : ConvexFlag} (R : FpRepresentation p d F) (T : FpRepresentation p d G) (x : F.Node) (y : G.Node) (h : T.space y ≤ R.space x) : R.codimension x ≤ T.codimension y

theorem EGZ.FpRepresentation.space_eq_of_codimension_eq_of_le {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} {G : ConvexFlag} (R : FpRepresentation p d F) (T : FpRepresentation p d G) (x : F.Node) (y : G.Node) (h : T.space y ≤ R.space x) (heq : R.codimension x = T.codimension y) : T.space y = R.space x

theorem EGZ.FpRepresentation.factor_surjective_of_space_eq {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} {G : ConvexFlag} (R : FpRepresentation p d F) (T : FpRepresentation p d G) (x : F.Node) (y : G.Node) (A : FpCoord p (G.rank y) →ᵃ[ZMod p] FpCoord p (F.rank x)) (hspace : T.space y = R.space x) (hfactor : ∀ v ∈ T.space y, (R.map x) v = A ((T.map y) v)) : Function.Surjective ⇑A

Factoring a surjective represented map gives a surjective coordinate map when the two represented affine spaces coincide.

theorem EGZ.FpRepresentation.rank_le_of_factor_of_space_eq {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} {G : ConvexFlag} (R : FpRepresentation p d F) (T : FpRepresentation p d G) (x : F.Node) (y : G.Node) (A : FpCoord p (G.rank y) →ᵃ[ZMod p] FpCoord p (F.rank x)) (hspace : T.space y = R.space x) (hfactor : ∀ v ∈ T.space y, (R.map x) v = A ((T.map y) v)) : F.rank x ≤ G.rank y

theorem EGZ.FpRepresentation.level_le_of_space_le_of_factor {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} {G : ConvexFlag} (R : FpRepresentation p d F) (T : FpRepresentation p d G) (x : F.Node) (y : G.Node) (A : FpCoord p (G.rank y) →ᵃ[ZMod p] FpCoord p (F.rank x)) (hspace : T.space y ≤ R.space x) (hfactor : ∀ v ∈ T.space y, (R.map x) v = A ((T.map y) v)) : R.level x ≤ T.level y

The basic level comparison used by all support refinements.

theorem EGZ.FpRepresentation.level_lt_of_space_lt {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} {G : ConvexFlag} (R : FpRepresentation p d F) (T : FpRepresentation p d G) (x : F.Node) (y : G.Node) (hspace : T.space y < R.space x) : R.level x < T.level y

theorem EGZ.FpRepresentation.level_lt_of_space_eq_of_rank_lt {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} {G : ConvexFlag} (R : FpRepresentation p d F) (T : FpRepresentation p d G) (x : F.Node) (y : G.Node) (hspace : T.space y = R.space x) (hrank : F.rank x < G.rank y) : R.level x < T.level y

theorem EGZ.FpRepresentation.level_lt_of_rank_lt_of_factor {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} {G : ConvexFlag} (R : FpRepresentation p d F) (T : FpRepresentation p d G) (x : F.Node) (y : G.Node) (A : FpCoord p (G.rank y) →ᵃ[ZMod p] FpCoord p (F.rank x)) (hspace : T.space y ≤ R.space x) (hfactor : ∀ v ∈ T.space y, (R.map x) v = A ((T.map y) v)) (hrank : G.rank y < F.rank x) : R.level x < T.level y

Losing lattice rank under a factorization forces loss of represented space, and therefore a strict increase in level.

theorem EGZ.FpRepresentation.level_lt_of_nonconstant_factor {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} {G : ConvexFlag} (R : FpRepresentation p d F) (T : FpRepresentation p d G) (x : F.Node) (y : G.Node) (A : FpCoord p (G.rank y) →ᵃ[ZMod p] FpCoord p (F.rank x)) (hspace : T.space y ≤ R.space x) (hfactor : ∀ v ∈ T.space y, (R.map x) v = A ((T.map y) v)) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) (hξ : R.NonconstantOnFibers x ξ) (B : FpCoord p (G.rank y) →ᵃ[ZMod p] ZMod p) (hB : ∀ v ∈ T.space y, ξ v = B ((T.map y) v)) : R.level x < T.level y

A newly represented functional which is nonconstant on an old fibre forces a strict level increase. Only one such functional is needed.

theorem EGZ.FpRepresentation.level_antitone {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) : Antitone R.level

theorem EGZ.FpRepresentation.codimension_eq_and_rank_eq_of_level_eq {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} {G : ConvexFlag} (R : FpRepresentation p d F) (T : FpRepresentation p d G) (x : F.Node) (y : G.Node) (h : R.level x = T.level y) : R.codimension x = T.codimension y ∧ F.rank x = G.rank y

Equal levels determine both coordinates of the lexicographic pair.

theorem EGZ.FpRepresentation.space_eq_of_le_of_level_eq {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) {y x : F.Node} (h : y ≤ x) (heq : R.level y = R.level x) : R.space y = R.space x

theorem EGZ.FpRepresentation.transition_modp_injective_of_level_eq {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) {y x : F.Node} (h : y ≤ x) (heq : R.level y = R.level x) : Function.Injective ⇑((F.transition h).modp p)

A transition between comparable nodes of equal level is injective over the represented field.

theorem EGZ.FpRepresentation.fiberConstantSubmodule_eq_of_level_eq {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} (R : FpRepresentation p d F) {y x : F.Node} (h : y ≤ x) (heq : R.level y = R.level x) : R.fiberConstantSubmodule y = R.fiberConstantSubmodule x

Comparable equal-level nodes have exactly the same fibre-constant functionals. This is the equality case needed by complete refinement.

theorem EGZ.FpRepresentation.level_lt_of_nonconstant_factor_at_upper {p d : ℕ} [Fact (Nat.Prime p)] {F : ConvexFlag} {G : ConvexFlag} (R : FpRepresentation p d F) (T : FpRepresentation p d G) {x y : F.Node} (h : y ≤ x) (z : G.Node) (A : FpCoord p (G.rank z) →ᵃ[ZMod p] FpCoord p (F.rank y)) (hspace : T.space z ≤ R.space y) (hfactor : ∀ v ∈ T.space z, (R.map y) v = A ((T.map z) v)) (ξ : FpCoord p d →ᵃ[ZMod p] ZMod p) (hξ : R.NonconstantOnFibers x ξ) (B : FpCoord p (G.rank z) →ᵃ[ZMod p] ZMod p) (hB : ∀ v ∈ T.space z, ξ v = B ((T.map z) v)) : R.level x < T.level z

Representing a functional nonconstant on an upper node's fibres gives a strict increase over that upper level at every retained lower node.

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.level {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) : Φ.flag.Node → ℕ

Level of a node of a flag decomposition.

Equations

• Φ.level = Φ.representation.level

theorem EGZ.FlagDecomposition.level_antitone {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) : Antitone Φ.level

@[simp]

theorem EGZ.FlagDecomposition.reduced_level {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (hp : Odd p) (x : (Φ.reduced hp).flag.Node) : (Φ.reduced hp).level x = Φ.level ↑x

@[simp]

theorem EGZ.FlagDecomposition.PrunedWeights.rebuilt_level {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (x : (D.rebuilt hp).flag.Node) : (D.rebuilt hp).level x = Φ.level ↑x

@[simp]

theorem EGZ.FlagDecomposition.PrunedWeights.cleaned_level {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} (D : Φ.PrunedWeights) (hp : Odd p) (x : (D.cleaned hp).flag.Node) : (D.cleaned hp).level x = Φ.level ↑↑x

theorem EGZ.FlagDecomposition.Rechart.decomposition_level_le {p d : ℕ} [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)) (hcenter : ∀ (x : Φ.flag.Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q) (x : Φ.flag.Node) : Φ.level x ≤ (decomposition Φ C hp hinj hcenter).level x

Minimalization cannot lower a node's level. A decrease in lattice rank forces a strict decrease in its represented affine space.