Splitting local weights over a new node poset

An order-preserving map to the old nodes pulls back the old flag and its representation. Local pieces dominated by the corresponding old summands can then be rebuilt on their active nodes. This construction permits the two-layer face refinement before the subsequent minimalization.

@[reducible, inline]

noncomputable abbrev EGZ.ConvexFlag.reindex (F : ConvexFlag) {N : Type u_1} [Fintype N] [SemilatticeSup N] [OrderTop N] (node : N →o F.Node) : ConvexFlag

Reindex all fibres along an order-preserving node map.

Equations

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

noncomputable def EGZ.FpRepresentation.reindex {p d : ℕ} {F : ConvexFlag} {N : Type u_1} [Fintype N] [SemilatticeSup N] [OrderTop N] (R : FpRepresentation p d F) (node : N →o F.Node) : FpRepresentation p d (F.reindex node)

Reindex the finite-field representation with the same node map.

Equations

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

theorem EGZ.FlagDecompositionRaw.cumulative_ne_zero_iff {p d : ℕ} {F : ConvexFlag} (pieces : F.Node → FpCoord p d → ℕ) (x : F.Node) (v : FpCoord p d) : cumulativeWeight pieces x v ≠ 0 ↔ ∃ y ≤ x, pieces y v ≠ 0

theorem EGZ.FlagDecompositionRaw.affineFibreMass_ne_zero_iff {p d : ℕ} [NeZero p] {n : ℕ} (w : FpCoord p d → ℕ) (φ : FpCoord p d → FpCoord p n) (c : FpCoord p n) : affineFibreMass w φ c ≠ 0 ↔ ∃ (v : FpCoord p d), φ v = c ∧ w v ≠ 0

theorem EGZ.FlagDecompositionRaw.hat_ne_zero_iff {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (x : F.Node) (q : IntCoord (F.rank x)) : hat R pieces x q ≠ 0 ↔ IsCenteredLift p q ∧ ∃ (v : FpCoord p d), (R.map x) v = IntCoord.mod p q ∧ cumulativeWeight pieces x v ≠ 0

theorem EGZ.FlagDecompositionRaw.localLift_ne_zero_iff {p d : ℕ} [NeZero p] {F : ConvexFlag} (R : FpRepresentation p d F) (pieces : F.Node → FpCoord p d → ℕ) (x : F.Node) (q : IntCoord (F.rank x)) : localLift R pieces x q ≠ 0 ↔ IsCenteredLift p q ∧ ∃ (v : FpCoord p d), (R.map x) v = IntCoord.mod p q ∧ pieces x v ≠ 0

structure EGZ.FlagDecomposition.SplitWeights {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) {N : Type} [Fintype N] [SemilatticeSup N] (node : N →o Φ.flag.Node) : Type

Local weights distributed over a new poset with their old bases recorded.

• weight : N → FpCoord p d → ℕ

  The local multiplicities assigned to the new nodes, bounded by their original node weights.

• weight_le (x : N) (v : FpCoord p d) : self.weight x v ≤ Φ.localWeight (node x) v
• nonzero : ∃ (x : N) (v : FpCoord p d), self.weight x v ≠ 0
• retained_le (v : FpCoord p d) : ∑ x : N, self.weight x v ≤ f v

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.SplitWeights.representation {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {N : Type} [Fintype N] [SemilatticeSup N] [OrderTop N] {node : N →o Φ.flag.Node} (_D : Φ.SplitWeights node) : FpRepresentation p d (Φ.flag.reindex node)

The original finite-field representation reindexed by the split-node map.

Equations

• _D.representation = Φ.representation.reindex node

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.SplitWeights.cumulative {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {N : Type} [Fintype N] [SemilatticeSup N] [OrderTop N] {node : N →o Φ.flag.Node} (D : Φ.SplitWeights node) (x : (Φ.flag.reindex node).Node) (v : FpCoord p d) : ℕ

The split weights accumulated over the lower nodes of the reindexed flag.

Equations

• D.cumulative = EGZ.FlagDecompositionRaw.cumulativeWeight D.weight

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.SplitWeights.hat {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {N : Type} [Fintype N] [SemilatticeSup N] [OrderTop N] {node : N →o Φ.flag.Node} (D : Φ.SplitWeights node) (x : (Φ.flag.reindex node).Node) (q : IntCoord ((Φ.flag.reindex node).rank x)) : ℕ

The cumulative centered lift for the split weights and their reindexed representation.

Equations

• D.hat = EGZ.FlagDecompositionRaw.hat D.representation D.weight

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.SplitWeights.localLift {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {N : Type} [Fintype N] [SemilatticeSup N] [OrderTop N] {node : N →o Φ.flag.Node} (D : Φ.SplitWeights node) (x : (Φ.flag.reindex node).Node) (q : IntCoord ((Φ.flag.reindex node).rank x)) : ℕ

The centered lift of each split node's local weight.

Equations

• D.localLift = EGZ.FlagDecompositionRaw.localLift D.representation D.weight

theorem EGZ.FlagDecomposition.SplitWeights.weight_supported {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {N : Type} [Fintype N] [SemilatticeSup N] [OrderTop N] {node : N →o Φ.flag.Node} (D : Φ.SplitWeights node) (x : N) (v : FpCoord p d) (hv : D.weight x v ≠ 0) : v ∈ D.representation.space x

theorem EGZ.FlagDecomposition.SplitWeights.cumulative_old_nonzero {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {N : Type} [Fintype N] [SemilatticeSup N] [OrderTop N] {node : N →o Φ.flag.Node} (D : Φ.SplitWeights node) (x : N) (v : FpCoord p d) (hv : D.cumulative x v ≠ 0) : Φ.cumulativeWeight (node x) v ≠ 0

theorem EGZ.FlagDecomposition.SplitWeights.cumulative_supported {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {N : Type} [Fintype N] [SemilatticeSup N] [OrderTop N] {node : N →o Φ.flag.Node} (D : Φ.SplitWeights node) (x : N) (v : FpCoord p d) (hv : D.cumulative x v ≠ 0) : v ∈ D.representation.space x

theorem EGZ.FlagDecomposition.SplitWeights.hat_old_nonzero {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {N : Type} [Fintype N] [SemilatticeSup N] [OrderTop N] {node : N →o Φ.flag.Node} (D : Φ.SplitWeights node) (x : N) (q : IntCoord (Φ.flag.rank (node x))) (hq : D.hat x q ≠ 0) : Φ.hat (node x) q ≠ 0

theorem EGZ.FlagDecomposition.SplitWeights.localLift_old_nonzero {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {N : Type} [Fintype N] [SemilatticeSup N] [OrderTop N] {node : N →o Φ.flag.Node} (D : Φ.SplitWeights node) (x : N) (q : IntCoord (Φ.flag.rank (node x))) (hq : D.localLift x q ≠ 0) : Φ.localLift (node x) q ≠ 0

theorem EGZ.FlagDecomposition.SplitWeights.rebuildData {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {N : Type} [Fintype N] [SemilatticeSup N] [OrderTop N] {node : N →o Φ.flag.Node} (D : Φ.SplitWeights node) (hp : Odd p) : FlagDecompositionRaw.RebuildData D.representation D.weight f

Centered support compatibility and visibility survive splitting the old local atoms among new bases.

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.SplitWeights.decomposition {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {N : Type} [Fintype N] [SemilatticeSup N] [OrderTop N] {node : N →o Φ.flag.Node} (D : Φ.SplitWeights node) (hp : Odd p) : FlagDecomposition p d f

The flag decomposition rebuilt from the split weights when the characteristic is odd.

Equations

• D.decomposition hp = ⋯.decomposition

@[simp]

theorem EGZ.FlagDecomposition.SplitWeights.decomposition_retainedWeight {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {N : Type} [Fintype N] [SemilatticeSup N] [OrderTop N] {node : N →o Φ.flag.Node} (D : Φ.SplitWeights node) (hp : Odd p) (v : FpCoord p d) : (D.decomposition hp).retainedWeight v = ∑ x : N, D.weight x v

theorem EGZ.FlagDecomposition.SplitWeights.decomposition_cumulativeWeight {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {N : Type} [Fintype N] [SemilatticeSup N] [OrderTop N] {node : N →o Φ.flag.Node} (D : Φ.SplitWeights node) (hp : Odd p) (x : (D.decomposition hp).flag.Node) : (D.decomposition hp).cumulativeWeight x = D.cumulative ↑x

theorem EGZ.FlagDecomposition.SplitWeights.decomposition_hat {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {N : Type} [Fintype N] [SemilatticeSup N] [OrderTop N] {node : N →o Φ.flag.Node} (D : Φ.SplitWeights node) (hp : Odd p) (x : (D.decomposition hp).flag.Node) : (D.decomposition hp).hat x = D.hat ↑x

theorem EGZ.FlagDecomposition.SplitWeights.decomposition_polytope_subset {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {N : Type} [Fintype N] [SemilatticeSup N] [OrderTop N] {node : N →o Φ.flag.Node} (D : Φ.SplitWeights node) (hp : Odd p) (x : (D.decomposition hp).flag.Node) : ((D.decomposition hp).flag.polytope x).carrier ⊆ (Φ.flag.polytope (node ↑x)).carrier

theorem EGZ.FlagDecomposition.SplitWeights.decomposition_isKBounded {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {N : Type} [Fintype N] [SemilatticeSup N] [OrderTop N] {node : N →o Φ.flag.Node} (D : Φ.SplitWeights node) (hp : Odd p) {K : Φ.flag.Node → ℕ} (hK : Φ.IsKBounded K) : (D.decomposition hp).IsKBounded fun (x : (D.decomposition hp).flag.Node) => K (node ↑x)

theorem EGZ.FlagDecomposition.SplitWeights.decomposition_card_le {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {N : Type} [Fintype N] [SemilatticeSup N] [OrderTop N] {node : N →o Φ.flag.Node} (D : Φ.SplitWeights node) (hp : Odd p) : Fintype.card (D.decomposition hp).flag.Node ≤ Fintype.card N

noncomputable def EGZ.FlagDecomposition.SplitWeights.subdivisionMap {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {Φ : FlagDecomposition p d f} {N : Type} [Fintype N] [SemilatticeSup N] [OrderTop N] {node : N →o Φ.flag.Node} (D : Φ.SplitWeights node) (hp : Odd p) (hsup : ∀ (x y : N), node (x ⊔ y) = node x ⊔ node y) : Φ.SubdivisionMap (D.decomposition hp)

Every surviving split generator is an old local generator.

Equations

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