Remaining multiset positions in each fibre

Deletion is performed on labelled positions, so coincident vectors retain their separate multiplicities. The remaining fibres reconstruct exactly the remaining natural-valued weight.

@[reducible, inline]

abbrev EGZ.Expansion.FibreSlots.Atom {G : Type u_1} (w : G → ℕ) : Type u_1

A labelled copy of a group element, with one copy for each unit of its multiplicity.

Equations

• EGZ.Expansion.FibreSlots.Atom w = ((v : G) × Fin (w v))

noncomputable def EGZ.Expansion.FibreSlots.remaining {G : Type u_1} [Fintype G] (w : G → ℕ) (U : Finset (Atom w)) : G → ℕ

The multiplicity function remaining after the selected atoms are removed.

Equations

• EGZ.Expansion.FibreSlots.remaining w U = EGZ.Expansion.pushWeight Sigma.fst fun (a : EGZ.Expansion.FibreSlots.Atom w) => if a ∉ U then 1 else 0

@[reducible, inline]

abbrev EGZ.Expansion.FibreSlots.Fibre {G : Type u_1} {H : Type u_2} (w : G → ℕ) (U : Finset (Atom w)) (π : G → H) (q : H) : Type u_1

The retained atoms whose group elements project to the specified fibre label.

Equations

• EGZ.Expansion.FibreSlots.Fibre w U π q = { a : EGZ.Expansion.FibreSlots.Atom w // π a.fst = q ∧ a ∉ U }

@[instance_reducible]

noncomputable instance EGZ.Expansion.FibreSlots.fibreFintype {G : Type u_1} {H : Type u_2} [Fintype G] (w : G → ℕ) (U : Finset (Atom w)) (π : G → H) (q : H) : Fintype (Fibre w U π q)

Equations

• EGZ.Expansion.FibreSlots.fibreFintype w U π q = Fintype.ofFinite (EGZ.Expansion.FibreSlots.Fibre w U π q)

@[reducible, inline]

abbrev EGZ.Expansion.FibreSlots.Retained {G : Type u_1} (w : G → ℕ) (U : Finset (Atom w)) : Type u_1

The subtype of atoms that have not been removed.

Equations

• EGZ.Expansion.FibreSlots.Retained w U = { a : EGZ.Expansion.FibreSlots.Atom w // a ∉ U }

@[instance_reducible]

noncomputable instance EGZ.Expansion.FibreSlots.retainedFintype {G : Type u_1} [Fintype G] (w : G → ℕ) (U : Finset (Atom w)) : Fintype (Retained w U)

Equations

• EGZ.Expansion.FibreSlots.retainedFintype w U = Fintype.ofFinite (EGZ.Expansion.FibreSlots.Retained w U)

theorem EGZ.Expansion.FibreSlots.pushWeight_atoms {G : Type u_1} [Fintype G] (w : G → ℕ) : (pushWeight Sigma.fst fun (x : Atom w) => 1) = w

theorem EGZ.Expansion.FibreSlots.card_atoms {G : Type u_1} [Fintype G] (w : G → ℕ) : Fintype.card (Atom w) = natMass w

theorem EGZ.Expansion.FibreSlots.remaining_le {G : Type u_1} [Fintype G] (w : G → ℕ) (U : Finset (Atom w)) : remaining w U ≤ w

theorem EGZ.Expansion.FibreSlots.mass_remaining_add_card {G : Type u_1} [Fintype G] (w : G → ℕ) (U : Finset (Atom w)) : natMass (remaining w U) + U.card = natMass w

theorem EGZ.Expansion.FibreSlots.mass_loss {G : Type u_1} [Fintype G] (w : G → ℕ) (U : Finset (Atom w)) : natMass w - natMass (remaining w U) = U.card

theorem EGZ.Expansion.FibreSlots.card_fibre_eq {G : Type u_1} {H : Type u_2} [Fintype G] (w : G → ℕ) (U : Finset (Atom w)) (π : G → H) (q : H) : Fintype.card (Fibre w U π q) = pushWeight π (remaining w U) q

noncomputable def EGZ.Expansion.FibreSlots.removedInFibre {G : Type u_1} {H : Type u_2} (w : G → ℕ) (U : Finset (Atom w)) (π : G → H) (q : H) : ℕ

The number of removed atoms lying over a specified fibre label.

Equations

• EGZ.Expansion.FibreSlots.removedInFibre w U π q = {a ∈ U | π a.fst = q}.card

theorem EGZ.Expansion.FibreSlots.card_fibre_eq_sub_removed {G : Type u_1} {H : Type u_2} [Fintype G] (w : G → ℕ) (U : Finset (Atom w)) (π : G → H) (q : H) : Fintype.card (Fibre w U π q) = pushWeight π w q - removedInFibre w U π q

theorem EGZ.Expansion.FibreSlots.card_fibre_lower {G : Type u_1} {H : Type u_2} [Fintype G] (w : G → ℕ) (U : Finset (Atom w)) (π : G → H) (q : H) : pushWeight π w q - U.card ≤ Fintype.card (Fibre w U π q)

theorem EGZ.Expansion.FibreSlots.sum_retained {G : Type u_1} [Fintype G] [DecidableEq G] {M : Type u_4} [AddCommMonoid M] (w : G → ℕ) (U : Finset (Atom w)) (f : Atom w → M) : ∑ a : Retained w U, f ↑a = ∑ a : Atom w, if a ∉ U then f a else 0

noncomputable def EGZ.Expansion.FibreSlots.labelledEquiv {G : Type u_1} {H : Type u_2} {S : Type u_3} (w : G → ℕ) (U : Finset (Atom w)) (π : G → H) (label : S → H) (hinj : Function.Injective label) (hcover : ∀ (v : G), w v ≠ 0 → ∃ (s : S), π v = label s) : (s : S) × Fibre w U π (label s) ≃ Retained w U

The equivalence reassembling disjoint labelled fibres into all retained atoms.

Equations

• EGZ.Expansion.FibreSlots.labelledEquiv w U π label hinj hcover = Equiv.ofBijective (fun (z : (s : S) × EGZ.Expansion.FibreSlots.Fibre w U π (label s)) => ⟨↑z.snd, ⋯⟩) ⋯

theorem EGZ.Expansion.FibreSlots.reassemble_remaining {G : Type u_1} {H : Type u_2} {S : Type u_3} [Fintype G] [Fintype S] (w : G → ℕ) (U : Finset (Atom w)) (π : G → H) (label : S → H) (hinj : Function.Injective label) (hcover : ∀ (v : G), w v ≠ 0 → ∃ (s : S), π v = label s) : (pushWeight (fun (z : (s : S) × Fibre w U π (label s)) => (↑z.snd).fst) fun (x : (s : S) × Fibre w U π (label s)) => 1) = remaining w U

Reassembling all surviving labelled fibres recovers exactly the remaining multiplicities, without identifying coincident positions.

theorem EGZ.Expansion.FibreSlots.remaining_isThickRelative {p d r T : ℕ} [NeZero p] (w : FpCoord p d → ℕ) (U : Finset (Atom w)) (π : FpCoord p d → FpCoord p r) {δ : ℝ} (hδ : 0 ≤ δ) (hmass : p ≤ natMass w) (hU : ↑U.card ≤ δ * ↑p / 2) (hthick : IsThickRelative w π T δ) : IsThickRelative (remaining w U) π T (δ / 2)