Multiplicities and relative thickness

The expansion argument counts positions in a multiset. Natural-valued weights retain these multiplicities when several positions have the same vector. Affine changes of coordinates preserve zero sums of length p.

noncomputable def EGZ.Expansion.pushWeight {α : Type u_1} {β : Type u_2} [Fintype α] (f : α → β) (w : α → ℕ) (b : β) : ℕ

Push a finite multiplicity function through an arbitrary map.

Equations

• EGZ.Expansion.pushWeight f w b = ∑ a : α, if f a = b then w a else 0

theorem EGZ.Expansion.pushWeight_mono {α : Type u_1} {β : Type u_2} [Fintype α] (f : α → β) {w u : α → ℕ} (h : w ≤ u) : pushWeight f w ≤ pushWeight f u

theorem EGZ.Expansion.sum_pushWeight {α : Type u_1} {β : Type u_2} {M : Type u_3} [Fintype α] [Fintype β] [AddCommMonoid M] (f : α → β) (w : α → ℕ) (g : β → M) : ∑ b : β, pushWeight f w b • g b = ∑ a : α, w a • g (f a)

theorem EGZ.Expansion.natMass_pushWeight {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : α → β) (w : α → ℕ) : natMass (pushWeight f w) = natMass w

theorem EGZ.Expansion.natMassOn_pushWeight {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : α → β) (w : α → ℕ) (S : Set β) : natMassOn (pushWeight f w) S = natMassOn w (f ⁻¹' S)

theorem EGZ.Expansion.pushWeight_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Fintype β] (f : α → β) (g : β → γ) (w : α → ℕ) : pushWeight g (pushWeight f w) = pushWeight (g ∘ f) w

theorem EGZ.Expansion.pushWeight_pullback {α : Type u_1} {β : Type u_2} [Fintype α] (f : α → β) (hf : Function.Injective f) (w : β → ℕ) (hs : ∀ (b : β), w b ≠ 0 → b ∈ Set.range f) : pushWeight f (w ∘ f) = w

Pulling a supported weight back along an injection and pushing it forward recovers every multiplicity.

theorem EGZ.Expansion.affine_sum_eq_zero {p m n : ℕ} [NeZero p] (A : FpCoord p m →ᵃ[ZMod p] FpCoord p n) (w : FpCoord p m → ℕ) (hm : natMass w = p) (hz : ∑ v : FpCoord p m, w v • v = 0) : ∑ v : FpCoord p m, w v • A v = 0

Affine maps preserve a zero sum when its total multiplicity is p.

theorem EGZ.Expansion.hasZeroSumMultiplicity_pushWeight {p m n : ℕ} [NeZero p] (A : FpCoord p m →ᵃ[ZMod p] FpCoord p n) {w : FpCoord p m → ℕ} (h : HasZeroSumMultiplicity w) : HasZeroSumMultiplicity (pushWeight (⇑A) w)

def EGZ.Expansion.NonconstantOnFibers {p n r : ℕ} (φ : FpCoord p n → FpCoord p r) (ξ : FpCoord p n →ᵃ[ZMod p] ZMod p) : Prop

Two points in one fibre of φ are distinguished by ξ.

Equations

• EGZ.Expansion.NonconstantOnFibers φ ξ = ∃ (v : EGZ.FpCoord p n) (u : EGZ.FpCoord p n), φ v = φ u ∧ ξ v ≠ ξ u

def EGZ.Expansion.IsThickRelative {p n r : ℕ} [NeZero p] (w : FpCoord p n → ℕ) (φ : FpCoord p n → FpCoord p r) (T : ℕ) (δ : ℝ) : Prop

The thickness assumption of the relative expansion theorem.

Equations

• EGZ.Expansion.IsThickRelative w φ T δ = ∀ (ξ : EGZ.FpCoord p n →ᵃ[ZMod p] ZMod p), EGZ.Expansion.NonconstantOnFibers φ ξ → EGZ.IsThickAlong w ξ T δ

theorem EGZ.Expansion.IsThickRelative.mono {p n r T T' : ℕ} [NeZero p] {w : FpCoord p n → ℕ} {φ : FpCoord p n → FpCoord p r} {δ δ' : ℝ} (h : IsThickRelative w φ T δ) (hT : T' ≤ T) (hδ : δ' ≤ δ) : IsThickRelative w φ T' δ'

theorem EGZ.Expansion.nonconstantOnFibers_iff_kernel {p n r : ℕ} (φ : FpCoord p n →ₗ[ZMod p] FpCoord p r) (ξ : FpCoord p n →ᵃ[ZMod p] ZMod p) : NonconstantOnFibers (⇑φ) ξ ↔ ∃ (v : FpCoord p n) (u : FpCoord p n), φ v = 0 ∧ φ u = 0 ∧ ξ v ≠ ξ u

For a linear projection, nonconstancy on its fibres is exactly nonconstancy on the fibre through zero, even for affine functionals.