The saturated atom family (R4 converse piece 3, #107)

The atoms of the coherent basis: one seed family of events per finite tagged vertex set, saturated by the finitely supported relabelings.

The construction

An atom is a pair (seed, τ) where seed is a seed event anchored at some finite A and τ is a finitely supported sortwise permutation. Its anchor is A.image τ and its event is relabel τ ⁻¹' seed. The relabeling action is left multiplication in the second coordinate,

atomAct σ (seed, τ) = (seed, σ * τ),

which is what makes the two action laws group laws rather than anything about events: act_one is one_mul and act_mul is mul_assoc in FinSuppPerm S, the finitely supported subgroup. The anchor law is then Finset.image_image, and the event law is RelStructure.relabel_preimage_relabel_preimage — the orientation matches because relabel is contravariant.

Saturation is built into the index rather than imposed afterwards: every relabel of every seed is already an atom, so the family is closed under the action by construction, with no orbit representatives and no choices to make equivariant.

Contents

• RelSignature.SeedData — a countable family of fixingAlgebra A-events for each finite A, the structural input to the construction, produced from separability of the law by seedDataOf further down this file;
• RelSignature.SaturatedAtom and its anchor / event / act, with the four atom-level laws BasisExpr needs, plus Countable;
• RelSignature.InfiniteRelExchangeableLaw.nonempty_coherentBasis — the assembly: every exchangeable law has a coherent basis.

Countability of the relabeling subgroup

instance RelSignature.instCountableSubtypeForallSrtPermNatMemSubgroupFinSuppPermOfFintype {S : RelSignature} [Fintype S.Srt] : Countable ↥S.FinSuppPerm

The finitely supported sortwise permutations form a countable group under finitely many sorts — the subgroup itself lives beside SortwiseFinSupp in Graphon.RelInvariantAction; countability is recorded here, where Fintype S.Srt is in play.

Seed data

structure RelSignature.SeedData (S : RelSignature) : Type u_1

Seed data: a countable family of events for each finite tagged vertex set, each measurable for the corresponding fixing algebra.

This is the input to the saturated construction, kept abstract so that the algebra below is independent of how the seeds are produced. The seeds that matter come from separability of the law — MeasureTheory.isSeparable_trim applied to fixingAlgebra A — and carry measure density as well; that is supplied separately, since none of the structural laws need it.

• seed : Finset ((s : S.Srt) × S.Vinfinite s) → Set (Set (S.RelStructure S.Vinfinite))

  The seed events available over A.

• countable_seed (A : Finset ((s : S.Srt) × S.Vinfinite s)) : (self.seed A).Countable

  Countably many seeds over each A.

• seed_mem (A : Finset ((s : S.Srt) × S.Vinfinite s)) (E : Set (S.RelStructure S.Vinfinite)) : E ∈ self.seed A → MeasurableSet E

  Each seed over A is a fixingAlgebra A-event.

def RelSignature.SeedData.Index {S : RelSignature} (D : S.SeedData) : Type u_1

The seeds, bundled with the vertex set they are anchored at.

Equations

• D.Index = ((A : Finset ((s : S.Srt) × S.Vinfinite s)) × { E : Set (S.RelStructure S.Vinfinite) // E ∈ D.seed A })

instance RelSignature.SeedData.instCountableIndexOfFintypeSrt {S : RelSignature} (D : S.SeedData) [Fintype S.Srt] : Countable D.Index

Seed data from separability

noncomputable def RelSignature.seedOf {S : RelSignature} [Countable S.Rel] (M : S.InfiniteRelExchangeableLaw) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Set (Set (S.RelStructure S.Vinfinite))

The countable measure-dense family for fixingAlgebra A supplied by separability of the law. [Countable S.Rel] alone gives IsSeparable M.law; isSeparable_trim transports that to each fixing algebra, and this is its chosen witness.

Equations

• RelSignature.seedOf M A = ⋯.choose

theorem RelSignature.countable_seedOf {S : RelSignature} [Countable S.Rel] (M : S.InfiniteRelExchangeableLaw) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : (seedOf M A).Countable

theorem RelSignature.measureDense_seedOf {S : RelSignature} [Countable S.Rel] (M : S.InfiniteRelExchangeableLaw) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : ((↑M.law).trim ⋯).MeasureDense (seedOf M A)

The density carried alongside the seeds. Kept out of SeedData, which stays structural: the atom-level laws never look at the law, and only the final CoherentBasis.density field does.

noncomputable def RelSignature.seedDataOf {S : RelSignature} [Countable S.Rel] (M : S.InfiniteRelExchangeableLaw) : S.SeedData

The seed data of a law: the separability-supplied families, packaged structurally.

Equations

• RelSignature.seedDataOf M = { seed := RelSignature.seedOf M, countable_seed := ⋯, seed_mem := ⋯ }

@[simp]

theorem RelSignature.seedDataOf_seed {S : RelSignature} [Countable S.Rel] (M : S.InfiniteRelExchangeableLaw) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : (seedDataOf M).seed A = seedOf M A

The saturated atoms

def RelSignature.SaturatedAtom {S : RelSignature} (D : S.SeedData) : Type u_1

A saturated atom: a seed together with a finitely supported relabeling of it. Saturation is part of the index, so the atom family is closed under the relabeling action by construction — no orbit representatives, and nothing to make equivariant after the fact.

Equations

• RelSignature.SaturatedAtom D = (D.Index × ↥S.FinSuppPerm)

instance RelSignature.SaturatedAtom.instCountableOfFintypeSrt {S : RelSignature} {D : S.SeedData} [Fintype S.Srt] : Countable (SaturatedAtom D)

noncomputable def RelSignature.SaturatedAtom.anchor {S : RelSignature} {D : S.SeedData} (a : SaturatedAtom D) : Finset ((s : S.Srt) × S.Vinfinite s)

The anchor of an atom: the seed's vertex set, moved by the relabeling.

Equations

• a.anchor = Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑a.2 s)) a.1.fst

def RelSignature.SaturatedAtom.event {S : RelSignature} {D : S.SeedData} (a : SaturatedAtom D) : Set (S.RelStructure S.Vinfinite)

The event of an atom: the seed event, pulled back along the relabeling.

Equations

• a.event = RelSignature.RelStructure.relabel ↑a.2 ⁻¹' ↑a.1.snd

def RelSignature.SaturatedAtom.act {S : RelSignature} {D : S.SeedData} (σ : ↥S.FinSuppPerm) (a : SaturatedAtom D) : SaturatedAtom D

The action: left multiplication in the relabeling coordinate.

Equations

• RelSignature.SaturatedAtom.act σ a = (a.1, σ * a.2)

theorem RelSignature.SaturatedAtom.act_one {S : RelSignature} {D : S.SeedData} (a : SaturatedAtom D) : act 1 a = a

act_one is literally one_mul in the relabeling subgroup.

theorem RelSignature.SaturatedAtom.act_mul {S : RelSignature} {D : S.SeedData} (σ τ : ↥S.FinSuppPerm) (a : SaturatedAtom D) : act (σ * τ) a = act σ (act τ a)

act_mul is literally mul_assoc — the point of putting the relabeling in the index, and of typing the action by the subgroup rather than by raw permutation families.

theorem RelSignature.SaturatedAtom.anchor_act {S : RelSignature} {D : S.SeedData} (σ : ↥S.FinSuppPerm) (a : SaturatedAtom D) : (act σ a).anchor = Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) a.anchor

The anchor transports by the image map: Finset.image_image, since multiplication of permutation families is pointwise composition.

theorem RelSignature.SaturatedAtom.event_act {S : RelSignature} {D : S.SeedData} (σ : ↥S.FinSuppPerm) (a : SaturatedAtom D) : (act σ a).event = RelStructure.relabel ↑σ ⁻¹' a.event

The event transports by preimage, exactly — relabel_preimage_relabel_preimage, whose orientation is exactly the left-multiplication convention.

theorem RelSignature.SaturatedAtom.event_mem {S : RelSignature} {D : S.SeedData} (a : SaturatedAtom D) : MeasurableSet a.event

Every atom event lies in the fixing algebra of its own anchor: the seed lies in fixingAlgebra A, and fixingAlgebra_comap_relabel moves that to the image vertex set.

The coherent basis of a law

theorem RelSignature.InfiniteRelExchangeableLaw.nonempty_coherentBasis {S : RelSignature} [Fintype S.Srt] [Countable S.Rel] (M : S.InfiniteRelExchangeableLaw) : Nonempty (CoherentBasis M)