Composed geometric and mass transport along low-level lineages

A transport bundles a subdivision with compatible stable mass maps. These data compose without changing parent-node identifications. Iterating them gives the geometric and measure comparison between any two stages, while the parent agrees with the abstract lineage ancestor.

def EGZ.FlagDecomposition.SubdivisionMap.refl {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) : Φ.SubdivisionMap Φ

The identity subdivision of a flag decomposition.

Equations

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

@[simp]

theorem EGZ.FlagDecomposition.SubdivisionMap.refl_comp {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} (M : Φ.SubdivisionMap Ψ) : (refl Φ).comp M = M

@[simp]

theorem EGZ.FlagDecomposition.SubdivisionMap.comp_refl {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ Ψ : FlagDecomposition p d f} (M : Φ.SubdivisionMap Ψ) : M.comp (refl Ψ) = M

theorem EGZ.FlagDecomposition.SubdivisionMap.comp_assoc {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ Ψ Ω Θ : FlagDecomposition p d f} (M : Φ.SubdivisionMap Ψ) (N : Ψ.SubdivisionMap Ω) (Q : Ω.SubdivisionMap Θ) : (M.comp N).comp Q = M.comp (N.comp Q)

structure EGZ.FlagDecomposition.LineageMassMaps {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : ℕ → FlagDecomposition p d f) : Type

Stepwise geometric and measure data for an iteration of minimal decompositions. Stability and parent injectivity are required only below the cutoff at that step.

• minimal (i : ℕ) : (Φ i).IsMinimal
• step (i : ℕ) : (Φ i).SubdivisionMap (Φ (i + 1))

  The subdivision map for each successive pair of decompositions.

• cutoff : ℕ → ℕ

  The level up to which node maps must be stable at each step.

• level_parent (i : ℕ) (x : (Φ (i + 1)).flag.Node) : (Φ i).level ((self.step i).node x) ≤ (Φ (i + 1)).level x
• stable (i : ℕ) (y : (Φ (i + 1)).flag.Node) : (Φ (i + 1)).level y ≤ self.cutoff i → (Φ i).StableNodeMap (Φ (i + 1)) ((self.step i).node y) y

  Stable node maps below the cutoff of each successive subdivision.

• stable_real (i : ℕ) (y : (Φ (i + 1)).flag.Node) (h : (Φ (i + 1)).level y ≤ self.cutoff i) : (self.stable i y h).coord.real = (self.step i).fibre y
• injective_below (i L : ℕ) : L ≤ self.cutoff i → Set.InjOn ⇑(self.step i).node {y : (Φ (i + 1)).flag.Node | (Φ (i + 1)).level y ≤ L}

structure EGZ.FlagDecomposition.LineageMassMaps.Transport {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : ℕ → FlagDecomposition p d f) (L i j : ℕ) : Type

All comparisons needed between two times at a fixed level cutoff.

• subdivision : (Φ i).SubdivisionMap (Φ j)

  The subdivision map transporting nodes across the interval of stages.

• level_parent (y : (Φ j).flag.Node) : (Φ i).level (self.subdivision.node y) ≤ (Φ j).level y
• stable (y : { y : (Φ j).flag.Node // (Φ j).level y ≤ L }) : (Φ i).StableNodeMap (Φ j) (self.subdivision.node ↑y) ↑y

  Stable node maps for transported nodes of level at most L.

• stable_real (y : { y : (Φ j).flag.Node // (Φ j).level y ≤ L }) : (self.stable y).coord.real = self.subdivision.fibre ↑y

def EGZ.FlagDecomposition.LineageMassMaps.Transport.refl {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : ℕ → FlagDecomposition p d f) (L i : ℕ) : Transport Φ L i i

Identity transport at a single stage.

Equations

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

def EGZ.FlagDecomposition.LineageMassMaps.Transport.lowParent {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} {L i j : ℕ} (M : Transport Φ L i j) (y : { y : (Φ j).flag.Node // (Φ j).level y ≤ L }) : { x : (Φ i).flag.Node // (Φ i).level x ≤ L }

The parent of a low-level node is still below the cutoff.

Equations

• M.lowParent y = ⟨M.subdivision.node ↑y, ⋯⟩

def EGZ.FlagDecomposition.LineageMassMaps.Transport.comp {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} {L i j k : ℕ} (M : Transport Φ L i j) (N : Transport Φ L j k) : Transport Φ L i k

Compose transports across two consecutive intervals of stages.

Equations

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

@[simp]

theorem EGZ.FlagDecomposition.LineageMassMaps.Transport.refl_comp {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} {L i j : ℕ} (M : Transport Φ L i j) : (refl Φ L i).comp M = M

@[simp]

theorem EGZ.FlagDecomposition.LineageMassMaps.Transport.comp_refl {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} {L i j : ℕ} (M : Transport Φ L i j) : M.comp (refl Φ L j) = M

theorem EGZ.FlagDecomposition.LineageMassMaps.Transport.comp_assoc {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} {L i j k l : ℕ} (M : Transport Φ L i j) (N : Transport Φ L j k) (Q : Transport Φ L k l) : (M.comp N).comp Q = M.comp (N.comp Q)

@[simp]

theorem EGZ.FlagDecomposition.LineageMassMaps.Transport.comp_stable_coord {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} {L i j k : ℕ} (M : Transport Φ L i j) (N : Transport Φ L j k) (y : { y : (Φ k).flag.Node // (Φ k).level y ≤ L }) : ((M.comp N).stable y).coord = (M.stable (N.lowParent y)).coord.comp (N.stable y).coord

def EGZ.FlagDecomposition.LineageMassMaps.Transport.stableAt {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} {L i j : ℕ} (M : Transport Φ L i j) (y : { y : (Φ j).flag.Node // (Φ j).level y ≤ L }) (x : (Φ i).flag.Node) (h : M.subdivision.node ↑y = x) : (Φ i).StableNodeMap (Φ j) x ↑y

A stable map whose target is named by an equal node.

Equations

• M.stableAt y x h = h ▸ M.stable y

theorem EGZ.FlagDecomposition.LineageMassMaps.Transport.stableAt_coord_congr {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} {L i j : ℕ} (M N : Transport Φ L i j) (hMN : M = N) (y : { y : (Φ j).flag.Node // (Φ j).level y ≤ L }) (x : (Φ i).flag.Node) (hM : M.subdivision.node ↑y = x) (hN : N.subdivision.node ↑y = x) : (M.stableAt y x hM).coord = (N.stableAt y x hN).coord

theorem EGZ.FlagDecomposition.LineageMassMaps.Transport.stableAt_comp_coord {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} {L i j k : ℕ} (M : Transport Φ L i j) (N : Transport Φ L j k) (z : { z : (Φ k).flag.Node // (Φ k).level z ≤ L }) (y : { y : (Φ j).flag.Node // (Φ j).level y ≤ L }) (x : (Φ i).flag.Node) (hy : N.subdivision.node ↑z = ↑y) (hx : M.subdivision.node ↑y = x) (hxz : (M.comp N).subdivision.node ↑z = x) : ((M.comp N).stableAt z x hxz).coord = (M.stableAt y x hx).coord.comp (N.stableAt z (↑y) hy).coord

theorem EGZ.FlagDecomposition.LineageMassMaps.Transport.stableAt_real_preimage {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} {L i j : ℕ} (M : Transport Φ L i j) (y : { y : (Φ j).flag.Node // (Φ j).level y ≤ L }) (x : (Φ i).flag.Node) (h : M.subdivision.node ↑y = x) (S : Set (RealCoord ((Φ i).flag.rank x))) : ⇑(M.stableAt y x h).coord.real ⁻¹' S = ⇑(M.subdivision.fibre ↑y) ⁻¹' (⋯ ▸ S)

@[reducible, inline]

noncomputable abbrev EGZ.FlagDecomposition.LineageMassMaps.system {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (D : LineageMassMaps Φ) : Lineages.System

Forget the geometry and masses to obtain the abstract lineage system.

Equations

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

theorem EGZ.FlagDecomposition.LineageMassMaps.system_injectiveBelow {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (D : LineageMassMaps Φ) {L : ℕ} (hL : ∀ (i : ℕ), L ≤ D.cutoff i) : D.system.InjectiveBelow L

def EGZ.FlagDecomposition.LineageMassMaps.stepTransport {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (D : LineageMassMaps Φ) {L : ℕ} (hL : ∀ (i : ℕ), L ≤ D.cutoff i) (i : ℕ) : Transport Φ L i (i + 1)

A one-step comparison at a cutoff below the current selected level.

Equations

• D.stepTransport hL i = { subdivision := D.step i, level_parent := ⋯, stable := fun (y : { y : (Φ (i + 1)).flag.Node // (Φ (i + 1)).level y ≤ L }) => D.stable i ↑y ⋯, stable_real := ⋯ }

def EGZ.FlagDecomposition.LineageMassMaps.transport {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (D : LineageMassMaps Φ) {L : ℕ} (hL : ∀ (i : ℕ), L ≤ D.cutoff i) {i j : ℕ} (h : i ≤ j) : Transport Φ L i j

Compose the subdivisions and stable mass maps from any time i to any later time j.

Equations

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

@[simp]

theorem EGZ.FlagDecomposition.LineageMassMaps.transport_self {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (D : LineageMassMaps Φ) {L : ℕ} (hL : ∀ (i : ℕ), L ≤ D.cutoff i) (i : ℕ) : D.transport hL ⋯ = Transport.refl Φ L i

theorem EGZ.FlagDecomposition.LineageMassMaps.transport_succ {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (D : LineageMassMaps Φ) {L : ℕ} (hL : ∀ (i : ℕ), L ≤ D.cutoff i) {i j : ℕ} (h : i ≤ j) : D.transport hL ⋯ = (D.transport hL h).comp (D.stepTransport hL j)

theorem EGZ.FlagDecomposition.LineageMassMaps.transport_trans {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (D : LineageMassMaps Φ) {L : ℕ} (hL : ∀ (i : ℕ), L ≤ D.cutoff i) {i j k : ℕ} (hij : i ≤ j) (hjk : j ≤ k) : D.transport hL ⋯ = (D.transport hL hij).comp (D.transport hL hjk)

Pairwise comparisons compose coherently, including their integer coordinates, their real fibres, and all stable mass estimates.

theorem EGZ.FlagDecomposition.LineageMassMaps.transport_node_eq_ancestor {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (D : LineageMassMaps Φ) {L : ℕ} (hL : ∀ (i : ℕ), L ≤ D.cutoff i) {i j : ℕ} (h : i ≤ j) (y : D.system.LowNode L j) : (D.transport hL h).subdivision.node ↑y = ↑((D.system.ancestor ⋯ h) y)

The composed geometric parent is exactly the abstract low-level ancestor, so geometric and counting arguments use the same lineage.

def EGZ.FlagDecomposition.LineageMassMaps.ancestorMap {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (D : LineageMassMaps Φ) {L : ℕ} (hL : ∀ (i : ℕ), L ≤ D.cutoff i) {i j : ℕ} (h : i ≤ j) (y : D.system.LowNode L j) : (Φ i).StableNodeMap (Φ j) ↑((D.system.ancestor ⋯ h) y) ↑y

The stable map to the actual abstract ancestor.

Equations

• D.ancestorMap hL h y = ⋯.mpr ((D.transport hL h).stable y)

theorem EGZ.FlagDecomposition.LineageMassMaps.transport_node_eq_of_ancestry_eq {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (D : LineageMassMaps Φ) {L : ℕ} (hL : ∀ (i : ℕ), L ≤ D.cutoff i) {i j : ℕ} (h : i ≤ j) (x : D.system.LowNode L i) (y : D.system.LowNode L j) (heq : (D.system.ancestry ⋯ i) x = (D.system.ancestry ⋯ j) y) : (D.transport hL h).subdivision.node ↑y = ↑x

Selected nodes with the same initial lineage label are related by the composed parent map at any two ordered times.

def EGZ.FlagDecomposition.LineageMassMaps.mapOfSameAncestry {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (D : LineageMassMaps Φ) {L : ℕ} (hL : ∀ (i : ℕ), L ≤ D.cutoff i) {i j : ℕ} (h : i ≤ j) (x : D.system.LowNode L i) (y : D.system.LowNode L j) (heq : (D.system.ancestry ⋯ i) x = (D.system.ancestry ⋯ j) y) : (Φ i).StableNodeMap (Φ j) ↑x ↑y

The mass map between two selected nodes on the same persistent lineage.

Equations

• D.mapOfSameAncestry hL h x y heq = (D.transport hL h).stableAt y ↑x ⋯

theorem EGZ.FlagDecomposition.LineageMassMaps.mapOfSameAncestry_comp_coord {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (D : LineageMassMaps Φ) {L : ℕ} (hL : ∀ (i : ℕ), L ≤ D.cutoff i) {i j k : ℕ} (hij : i ≤ j) (hjk : j ≤ k) (x : D.system.LowNode L i) (y : D.system.LowNode L j) (z : D.system.LowNode L k) (hxy : (D.system.ancestry ⋯ i) x = (D.system.ancestry ⋯ j) y) (hyz : (D.system.ancestry ⋯ j) y = (D.system.ancestry ⋯ k) z) (hxz : (D.system.ancestry ⋯ i) x = (D.system.ancestry ⋯ k) z) : (D.mapOfSameAncestry hL ⋯ x z hxz).coord = (D.mapOfSameAncestry hL hij x y hxy).coord.comp (D.mapOfSameAncestry hL hjk y z hyz).coord

Coordinate transport is coherent even when each intermediate node is specified by its persistent ancestry label.

theorem EGZ.FlagDecomposition.LineageMassMaps.mapOfSameAncestry_real_preimage {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (D : LineageMassMaps Φ) {L : ℕ} (hL : ∀ (i : ℕ), L ≤ D.cutoff i) {i j : ℕ} (h : i ≤ j) (x : D.system.LowNode L i) (y : D.system.LowNode L j) (heq : (D.system.ancestry ⋯ i) x = (D.system.ancestry ⋯ j) y) (S : Set (RealCoord ((Φ i).flag.rank ↑x))) : ⇑(D.mapOfSameAncestry hL h x y heq).coord.real ⁻¹' S = ⇑((D.transport hL h).subdivision.fibre ↑y) ⁻¹' (⋯ ▸ S)

theorem EGZ.FlagDecomposition.LineageMassMaps.transport_real_bijective_of_level_eq {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (D : LineageMassMaps Φ) {L : ℕ} (hL : ∀ (i : ℕ), L ≤ D.cutoff i) {i j : ℕ} (h : i ≤ j) (y : D.system.LowNode L j) (heq : (Φ i).level ((D.transport hL h).subdivision.node ↑y) = (Φ j).level ↑y) : Function.Bijective ⇑((D.transport hL h).subdivision.fibre ↑y)

Equal levels along a lineage make the composed real coordinate map an affine isomorphism.

theorem EGZ.FlagDecomposition.LineageMassMaps.transport_isRealizedFace {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {Φ : ℕ → FlagDecomposition p d f} (D : LineageMassMaps Φ) {L : ℕ} (hL : ∀ (i : ℕ), L ≤ D.cutoff i) {i j : ℕ} (h : i ≤ j) (y : (Φ j).flag.Node) (Γ : ((Φ i).flag.polytope ((D.transport hL h).subdivision.node y)).Face) (hne : (((Φ j).flag.polytope y).carrier ∩ ⇑((D.transport hL h).subdivision.fibre y) ⁻¹' Γ.carrier).Nonempty) (hΓ : (Φ i).IsRealizedFace ((D.transport hL h).subdivision.node y) Γ) : (Φ j).IsRealizedFace y ((D.transport hL h).subdivision.face y Γ hne)

A realized face stays realized throughout any number of subdivision steps whenever its final pullback is nonempty.