One finite character-fusion stage

This module turns the bounded-deletion conclusion into the exact short-relation compatibility required by the uniform Kronecker lemma. It is the finite algebraic heart of one fusion stage.

theorem Wallace.disjoint_of_mixedRelationFree {G : Type u} [AddCommGroup G] {A Y : Finset G} {Q : ℕ} (hQ : 1 ≤ Q) (hfree : FiniteCombinatorics.MixedRelationFree Q A Y) : Disjoint A Y

A short-relation-free old/new pair is disjoint as soon as the height bound contains 1.

@[reducible, inline]

noncomputable abbrev Wallace.unionEquiv {G : Type u} [DecidableEq G] (A Y : Finset G) : Fin (A ∪ Y).card ≃ ↥(A ∪ Y)

Enumerate the union of two finite sets by a finite index type.

Equations

• Wallace.unionEquiv A Y = (A ∪ Y).equivFin.symm

noncomputable def Wallace.unionTuple {G : Type u} [DecidableEq G] (A Y : Finset G) : Fin (A ∪ Y).card → G

The tuple enumerating the union of the two finite sets.

Equations

• Wallace.unionTuple A Y i = ↑((Wallace.unionEquiv A Y) i)

noncomputable def Wallace.stageTarget {G : Type u} [AddCommGroup G] [DecidableEq G] (A Y : Finset G) (old : G →+ UnitAddCircle) : Fin (A ∪ Y).card → UnitAddCircle

The target which keeps the old character on A and is zero on the new set Y.

Equations

• Wallace.stageTarget A Y old i = if Wallace.unionTuple A Y i ∈ A then old (Wallace.unionTuple A Y i) else 0

theorem Wallace.stageTarget_respectsRelationsUpTo {G : Type u} [AddCommGroup G] [DecidableEq G] {A Y : Finset G} {Q : ℕ} (hQ : 1 ≤ Q) (hfree : FiniteCombinatorics.MixedRelationFree Q A Y) (old : G →+ UnitAddCircle) : RespectsRelationsUpTo Q (unionTuple A Y) (stageTarget A Y old)

Bounded deletion makes the finite fusion target compatible with every relation up to Q.

theorem Wallace.exists_character_fusion_stage {G : Type u} [AddCommGroup G] [DecidableEq G] {A Y : Finset G} {Q : ℕ} (hQ : 1 ≤ Q) (hfree : FiniteCombinatorics.MixedRelationFree Q A Y) (old : G →+ UnitAddCircle) {eps : ℝ} (hbound : IsUniformKroneckerBound (A ∪ Y).card eps Q) : ∃ (next : G →+ UnitAddCircle), (∀ x ∈ A, ‖next x - old x‖ < eps) ∧ ∀ y ∈ Y, ‖next y‖ < eps

One application of uniform Kronecker performs a finite fusion stage.