The raw fixing σ-algebras of finite tagged vertex sets (R4 converse piece 2a, #107)

The law-independent factor-algebra layer of the converse representation theorem: for a finite set A of tagged vertices, the σ-algebra of events invariant under every finitely supported sortwise permutation fixing every tagged vertex of A — the A-relativized RelStructure.invariantAlgebra. Crucially this is not "generated by the relation coordinates inside A" (that loses hidden vertex information — a vertex latent carries more than the relations observed at the vertex); the invariance definition captures everything the ambient randomness outside A cannot move.

Everything here is raw and measure-free — no completions, no conditional expectations, no law. The conditional-independence theorem built on this layer lives in Graphon.RelFixingCondIndep, with [Countable S.Rel] supplying StandardBorelSpace (RelStructure S (Vinfinite S)): CondIndep (fixingAlgebra (A ∩ B)) (fixingAlgebra A) (fixingAlgebra B) (fixingAlgebra_le _) M.law for every exchangeable M — dissociation is not required. Sanity specializations: at A = B, and likewise at A = ∅ or B = ∅, one outer algebra equals the conditioning algebra fixingAlgebra (A ∩ B), so the statement is tautological — conditional independence of an algebra from anything given itself; the content is at disjoint nonempty A, B. The standard-Borel factor realizations (stated modulo the law) remain a deliberately separate, later PR.

• RelSignature.SortwiseFixing — the A-fixing stabilizer (finitely supported + fixes A pointwise), closed under 1, *, ⁻¹, and conjugation (SortwiseFixing.conj);
• RelStructure.fixingAlgebra — the raw fixing σ-algebra, with fixingAlgebra_le;
• RelStructure.fixingAlgebra_mono — monotone: A ⊆ B → fixingAlgebra A ≤ fixingAlgebra B (a larger fixed set is a smaller stabilizer, hence more invariant events);
• RelStructure.fixingAlgebra_empty — fixingAlgebra ∅ = invariantAlgebra (near-definitional: the same finitary action);
• RelStructure.fixingAlgebra_comap_relabel — transport: pulling back along a finitely supported relabeling is an equality of measurable spaces comap (relabel σ) (fixingAlgebra A) = fixingAlgebra (image σ A), by conjugating stabilizers.

The fixing stabilizer

def RelSignature.SortwiseFixing {S : RelSignature} (A : Finset ((s : S.Srt) × S.Vinfinite s)) (σ : S.Srt → Equiv.Perm ℕ) : Prop

The A-fixing stabilizer: a sortwise permutation family with common finite support fixing every tagged vertex of A. At A = ∅ this is SortwiseFinSupp — the acting group of RelStructure.invariantAlgebra.

Equations

• RelSignature.SortwiseFixing A σ = (RelSignature.SortwiseFinSupp σ ∧ ∀ v ∈ A, (σ v.fst) v.snd = v.snd)

theorem RelSignature.SortwiseFixing.one {S : RelSignature} {A : Finset ((s : S.Srt) × S.Vinfinite s)} : SortwiseFixing A fun (x : S.Srt) => 1

theorem RelSignature.SortwiseFixing.mul {S : RelSignature} {A : Finset ((s : S.Srt) × S.Vinfinite s)} {σ τ : S.Srt → Equiv.Perm ℕ} (hσ : SortwiseFixing A σ) (hτ : SortwiseFixing A τ) : SortwiseFixing A fun (s : S.Srt) => σ s * τ s

theorem RelSignature.SortwiseFixing.inv {S : RelSignature} {A : Finset ((s : S.Srt) × S.Vinfinite s)} {σ : S.Srt → Equiv.Perm ℕ} (hσ : SortwiseFixing A σ) : SortwiseFixing A fun (s : S.Srt) => (σ s)⁻¹

theorem RelSignature.SortwiseFixing.conj {S : RelSignature} {A : Finset ((s : S.Srt) × S.Vinfinite s)} {σ τ : S.Srt → Equiv.Perm ℕ} (hσ : SortwiseFinSupp σ) (hτ : SortwiseFixing (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(σ s)) A) τ) : SortwiseFixing A fun (s : S.Srt) => (σ s)⁻¹ * τ s * σ s

Conjugation moves the fixed set: conjugating a stabilizer of the image vertex set by σ gives a stabilizer of A — the group-theoretic heart of the transport theorem. Finite support survives because a common bound for σ and τ bounds the conjugate.

theorem RelSignature.SortwiseFixing.conj_of_fintype {S : RelSignature} {A : Finset ((s : S.Srt) × S.Vinfinite s)} {σ τ : S.Srt → Equiv.Perm ℕ} [Fintype S.Srt] (hτ : SortwiseFixing (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(σ s)) A) τ) : SortwiseFixing A fun (s : S.Srt) => (σ s)⁻¹ * τ s * σ s

Conjugation under finitely many sorts needs no support bound on σ: with [Fintype S.Srt] the sortwise suprema of the finitely many inverse images of the bound of τ give a common finite bound for the conjugate — the hypothesis dropped from SortwiseFixing.conj, which is genuinely necessary over infinitely many sorts.

The raw fixing σ-algebra

@[implicit_reducible]

def RelSignature.RelStructure.fixingAlgebra {S : RelSignature} (A : Finset ((s : S.Srt) × S.Vinfinite s)) : MeasurableSpace (S.RelStructure S.Vinfinite)

The raw fixing σ-algebra of a finite tagged vertex set A: measurable events invariant under every finitely supported sortwise relabeling fixing every tagged vertex of A. Law-independent by construction — completions, conditional expectations, and mod-null factor realizations explicitly carry a law and live in later layers.

Equations

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

theorem RelSignature.RelStructure.fixingAlgebra_le {S : RelSignature} (A : Finset ((s : S.Srt) × S.Vinfinite s)) : fixingAlgebra A ≤ inferInstance

theorem RelSignature.RelStructure.fixingAlgebra_mono {S : RelSignature} {A B : Finset ((s : S.Srt) × S.Vinfinite s)} (hAB : A ⊆ B) : fixingAlgebra A ≤ fixingAlgebra B

Monotonicity: a larger fixed set is a smaller stabilizer, hence more invariant events.

theorem RelSignature.RelStructure.fixingAlgebra_empty {S : RelSignature} : fixingAlgebra ∅ = invariantAlgebra

The bottom factor is the invariant σ-algebra — near-definitional: at A = ∅ the fixing condition is vacuous and the stabilizer is the full finitely supported group, so dissociation/ergodicity (R3, #106) trivializes exactly this factor.

Transport

theorem RelSignature.RelStructure.relabel_comp_relabel {S : RelSignature} (σ τ : S.Srt → Equiv.Perm ℕ) : relabel σ ∘ relabel τ = relabel fun (s : S.Srt) => τ s * σ s

Relabelings compose contravariantly (permutation product acts inner-first).

theorem RelSignature.RelStructure.relabel_preimage_relabel_preimage {S : RelSignature} (τ σ : S.Srt → Equiv.Perm ℕ) (E : Set (S.RelStructure S.Vinfinite)) : relabel τ ⁻¹' relabel σ ⁻¹' E = (relabel fun (s : S.Srt) => τ s * σ s) ⁻¹' E

theorem RelSignature.RelStructure.fixingAlgebra_comap_relabel {S : RelSignature} {σ : S.Srt → Equiv.Perm ℕ} (hσ : SortwiseFinSupp σ) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : MeasurableSpace.comap (relabel σ) (fixingAlgebra A) = fixingAlgebra (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(σ s)) A)

Transport of the fixing σ-algebra along a finitely supported sortwise relabeling — an equality of pulled-back measurable spaces, not merely an event-membership equivalence: the pullback of the A-fixing algebra is the fixing algebra of the image vertex set. Stabilizers conjugate (SortwiseFixing.conj); the reverse inclusion is the forward one for σ⁻¹ transported through comap composition. Over infinitely many sorts the finite-support hypothesis is genuinely necessary; under [Fintype S.Srt] see fixingAlgebra_comap_relabel_of_fintype.

theorem RelSignature.RelStructure.fixingAlgebra_comap_relabel_of_fintype {S : RelSignature} [Fintype S.Srt] (σ : S.Srt → Equiv.Perm ℕ) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : MeasurableSpace.comap (relabel σ) (fixingAlgebra A) = fixingAlgebra (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(σ s)) A)

Transport under finitely many sorts holds for an arbitrary sortwise permutation family: finite sorts let conjugation recover a common finite bound (SortwiseFixing.conj_of_fintype), so no support hypothesis on σ is needed.