The coherent-basis interface for the fixing σ-algebras (R4 converse piece 3, #107)

The interface for a simultaneous, coherent family of factors for fixingAlgebra A, as A ranges over the finite sets of tagged vertices. This file defines the interface and derives its formal consequences, including the relabeling equivalence basisIndexEquiv; it does not construct an instance — that is RelSignature.InfiniteRelExchangeableLaw.nonempty_coherentBasis, in Graphon.RelBasisSaturation.

Why not one factor per A

Graphon.SeparableFactor already produces a factor map for a single sub-σ-algebra, via MeasurableSpace.mapNatBool. That map cannot be used family-wide: its generating sequence is chosen by the CountablyGenerated instance, so factors for different A have no relation to one another — no literal inclusion when C ⊆ A, and no equivariance under relabeling. Choosing per-A maps and repairing the relations afterwards leads straight back into coherence choices, because independently chosen transports need not respect a given inclusion.

The design

A single global countable index type ι, each index carrying an explicit finite anchor and an event:

• anchor : ι → Finset (Σ s, Vinfinite S s) and event : ι → Set (RelStructure S (Vinfinite S)), with event i measurable for fixingAlgebra (anchor i);
• the indices available over A are BasisIndex A := {i // anchor i ⊆ A}, so C ⊆ A induces a literal embedding BasisIndex C ↪ BasisIndex A;
• the factor space is BasisIndex A → Bool — a varying index, not ℕ → Bool. It is still standard Borel because the index is countable, and unlike a Cantor coding it keeps the inclusions literal, so the factor projection is ordinary coordinate restriction and its cocycle law is definitional;
• the finitely supported relabelings act on ι — an action proper, with identity and multiplicativity laws, not merely a map — transporting anchors by the image map and events by exact preimage equality, with no null sets. The action is typed by the subgroup FinSuppPerm S rather than by raw permutation families with a side condition: closure under finitely supported relabelings is all this layer provides and all it needs, whereas closure of the chosen event family under the full permutation group is neither constructed nor countable in general. So the subgroup is precisely the symmetry the interface can honestly guarantee, and its group inverses are what let basisIndexEquiv, below, upgrade a relabeling to an equivalence BasisIndex A ≃ BasisIndex (A.image σ);
• the family is closed under finite Boolean operations, so it is a countable set ring. This is demanded up front rather than derived later: the conditional-law and Dynkin arguments downstream are far easier over a ring than over an arbitrary dense family;
• measure density: for each A, the events indexed by BasisIndex A approximate every fixingAlgebra A-event modulo the law. Combined with Measure.MeasureDense.exists_generateFrom_ae_eq this is what turns approximation into a.e. representatives.

Contents

• RelSignature.CoherentBasis — the interface;
• CoherentBasis.BasisIndex / basisIndexEmbedding / factorMap / factorProjection — the derived objects, with the coordinate-restriction cocycle factorProjection_comp and the compatibility factorProjection_factorMap;
• CoherentBasis.measurable_factorMap and CoherentBasis.comap_factorMap_le — the factor map is fixingAlgebra A-measurable, so its pullback lands inside fixingAlgebra A;
• CoherentBasis.exists_comap_factorMap_ae_eq — the payoff: every fixingAlgebra A-event has an a.e. representative in the pullback of the factor map;
• CoherentBasis.FactorSpace — the factor space at A, standard Borel because the index is countable, with the measurability of the factor maps and projections, and factorSpaceEquiv, a relabeling as a measurable equivalence of factor spaces;
• CoherentBasis.basisIndexEquiv — a relabeling as an equivalence BasisIndex A ≃ BasisIndex (A.image σ), with factorMap_basisIndexEquiv / factorMap_comp_relabel (naturality against relabel, orientation forced by event_act being a preimage equality) and the two definitional compatibilities with basisIndexEmbedding and factorProjection.

The interface

structure RelSignature.CoherentBasis {S : RelSignature} (M : S.InfiniteRelExchangeableLaw) : Type (u + 1)

A coherent basis for the fixing σ-algebras of M: one global countable family of anchored events, from which a factor for every finite tagged vertex set A is read off by restricting to the indices anchored inside A.

The point of the single global index is that all the coherence is structural: the inclusion for C ⊆ A is a literal subtype inclusion, the relabeling action is an action on indices with exact anchor and event transport, and the factor projections are coordinate restrictions. Only density refers to the law.

• ι : Type u

  The global index type. It lives in the signature's universe: the anchors are Finsets of tagged vertices and the events are sets of structures, both of which do.

• countable_ι : Countable self.ι

  The index type is countable, so each factor space is standard Borel.

• anchor : self.ι → Finset ((s : S.Srt) × S.Vinfinite s)

  The finite tagged vertex set an index is anchored at.

• event : self.ι → Set (S.RelStructure S.Vinfinite)

  The event an index names.

• event_mem (i : self.ι) : MeasurableSet (self.event i)

  Each event is measurable for the fixing algebra of its own anchor — hence for fixingAlgebra A whenever the anchor sits inside A.

• bot : self.ι

  An index naming the empty event, anchored at ∅ — hence available over every A.

• anchor_bot : self.anchor self.bot = ∅
• event_bot : self.event self.bot = ∅
• compl : self.ι → self.ι

  Complementation on indices, fixing the anchor.

• anchor_compl (i : self.ι) : self.anchor (self.compl i) = self.anchor i
• event_compl (i : self.ι) : self.event (self.compl i) = (self.event i)ᶜ
• inter : self.ι → self.ι → self.ι

  Intersection on indices; the anchor is the union, which is exactly what keeps BasisIndex A closed under the operation.

• anchor_inter (i j : self.ι) : self.anchor (self.inter i j) = self.anchor i ∪ self.anchor j
• event_inter (i j : self.ι) : self.event (self.inter i j) = self.event i ∩ self.event j
• act : ↥S.FinSuppPerm → self.ι → self.ι

  A finitely supported sortwise relabeling acts on indices.

  The field is typed by the subgroup FinSuppPerm S, not by a raw permutation family with a SortwiseFinSupp side condition. That is deliberate: closure under finitely supported relabelings is what the construction supplies and what the downstream arguments use, while closure of the chosen event family under the full permutation group is neither constructed here nor countable in general. Typing the field by the subgroup states exactly the symmetry guaranteed, and makes inverses available for free.

• act_one (i : self.ι) : self.act 1 i = i

  The identity relabeling acts trivially.

• act_mul (σ τ : ↥S.FinSuppPerm) (i : self.ι) : self.act (σ * τ) i = self.act σ (self.act τ i)

  The action is multiplicative. The orientation matches event_act and the contravariance of relabel: relabel (σ * τ) ⁻¹' E = relabel σ ⁻¹' (relabel τ ⁻¹' E), by RelStructure.relabel_preimage_relabel_preimage.

  With act_one this makes act an action rather than a bare map, which is what lets basisIndexEquiv turn a relabeling into an equivalence BasisIndex A ≃ BasisIndex (A.image σ): the group inverse supplies the two-sided inverse via act σ⁻¹ ∘ act σ = act 1 = id.

• anchor_act (σ : ↥S.FinSuppPerm) (i : self.ι) : self.anchor (self.act σ i) = Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) (self.anchor i)

  The action transports anchors by the image map, exactly.

• event_act (σ : ↥S.FinSuppPerm) (i : self.ι) : self.event (self.act σ i) = RelStructure.relabel ↑σ ⁻¹' self.event i

  The action transports events by preimage, exactly — no null sets.

• density (A : Finset ((s : S.Srt) × S.Vinfinite s)) : ((↑M.law).trim ⋯).MeasureDense {E : Set (S.RelStructure S.Vinfinite) | ∃ (i : self.ι), self.anchor i ⊆ A ∧ self.event i = E}

  Measure density: over each A, the events anchored inside A approximate every fixingAlgebra A-event. This is the only field that mentions the law.

instance RelSignature.CoherentBasis.instCountableι {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) : Countable B.ι

The derived factors

def RelSignature.CoherentBasis.BasisIndex {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Type u

The indices available over A: those anchored inside A. Countable, so BasisIndex A → Bool is standard Borel.

Equations

• B.BasisIndex A = { i : B.ι // B.anchor i ⊆ A }

instance RelSignature.CoherentBasis.instCountableBasisIndex {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Countable (B.BasisIndex A)

The factor spaces

@[reducible, inline]

abbrev RelSignature.CoherentBasis.FactorSpace {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Type u

The factor space at A: the Boolean cube over the indices anchored inside A.

Standard Borel, because the index is countable — this is what the conditional-kernel step will need, and it is the reason for indexing by BasisIndex A rather than coding every factor into ℕ → Bool: the varying index keeps the inclusions literal without giving up the measurable structure.

Equations

• B.FactorSpace A = (B.BasisIndex A → Bool)

instance RelSignature.CoherentBasis.instStandardBorelSpaceFactorSpace {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : StandardBorelSpace (B.FactorSpace A)

def RelSignature.CoherentBasis.basisIndexEmbedding {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {C A : Finset ((s : S.Srt) × S.Vinfinite s)} (hCA : C ⊆ A) : B.BasisIndex C → B.BasisIndex A

The inclusion of sub-indices, for C ⊆ A: a literal subtype inclusion, which is the whole reason for anchoring indices at finite sets rather than coding each factor separately.

Equations

• B.basisIndexEmbedding hCA i = ⟨↑i, ⋯⟩

noncomputable def RelSignature.CoherentBasis.factorMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : S.RelStructure S.Vinfinite → B.FactorSpace A

The factor map at A: evaluate every event anchored inside A.

Equations

• B.factorMap A X i = decide (X ∈ B.event ↑i)

def RelSignature.CoherentBasis.factorProjection {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {C A : Finset ((s : S.Srt) × S.Vinfinite s)} (hCA : C ⊆ A) : B.FactorSpace A → B.FactorSpace C

The factor projection from A down to C ⊆ A: precomposition with the index inclusion, i.e. ordinary coordinate restriction.

Equations

• B.factorProjection hCA f = f ∘ B.basisIndexEmbedding hCA

theorem RelSignature.CoherentBasis.factorProjection_factorMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {C A : Finset ((s : S.Srt) × S.Vinfinite s)} (hCA : C ⊆ A) : B.factorProjection hCA ∘ B.factorMap A = B.factorMap C

The projections are compatible with the factor maps — by definition, since both sides evaluate the same events.

theorem RelSignature.CoherentBasis.factorProjection_comp {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {D C A : Finset ((s : S.Srt) × S.Vinfinite s)} (hDC : D ⊆ C) (hCA : C ⊆ A) : B.factorProjection hDC ∘ B.factorProjection hCA = B.factorProjection ⋯

The cocycle law, definitional: restricting through an intermediate set is the same as restricting directly.

@[simp]

theorem RelSignature.CoherentBasis.factorMap_eq_true {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {A : Finset ((s : S.Srt) × S.Vinfinite s)} (X : S.RelStructure S.Vinfinite) (i : B.BasisIndex A) : B.factorMap A X i = true ↔ X ∈ B.event ↑i

A coordinate of the factor map reads membership in the corresponding event.

theorem RelSignature.CoherentBasis.measurable_factorProjection {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {C A : Finset ((s : S.Srt) × S.Vinfinite s)} (hCA : C ⊆ A) : Measurable (B.factorProjection hCA)

The factor projections are measurable — they are coordinate restrictions.

Measurability and generation

theorem RelSignature.CoherentBasis.measurable_factorMap {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Measurable (B.factorMap A)

The factor map at A is measurable for fixingAlgebra A: each coordinate is the indicator of an event whose anchor lies inside A, and fixingAlgebra is monotone.

theorem RelSignature.CoherentBasis.measurable_factorMap' {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Measurable (B.factorMap A)

The factor map is measurable for the ambient σ-algebra too, by fixingAlgebra_le.

theorem RelSignature.CoherentBasis.comap_factorMap_le {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : MeasurableSpace.comap (B.factorMap A) inferInstance ≤ RelStructure.fixingAlgebra A

Consequently the pullback of the factor σ-algebra sits inside fixingAlgebra A.

theorem RelSignature.CoherentBasis.exists_comap_factorMap_ae_eq {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) {E : Set (S.RelStructure S.Vinfinite)} (hE : MeasurableSet E) : ∃ (E' : Set (S.RelStructure S.Vinfinite)), MeasurableSet E' ∧ E' =ᵐ[↑M.law] E

The payoff: every fixingAlgebra A-event has an a.e. representative in the pullback of the factor map at A. Stated eventwise, like everything else in this layer — never as an equality of σ-algebras "modulo null sets".

Together with comap_factorMap_le this says the factor captures fixingAlgebra A exactly modulo the law, while factorProjection_factorMap and factorProjection_comp say the family of factors is coherent on the nose.

Relabeling equivariance

theorem RelSignature.CoherentBasis.image_image_inv {S : RelSignature} (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ⁻¹ s)) (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A) = A

Relabeling by σ and then by σ⁻¹ returns a vertex set to itself.

noncomputable def RelSignature.CoherentBasis.basisIndexEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : B.BasisIndex A ≃ B.BasisIndex (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A)

A relabeling is an equivalence of index sets: BasisIndex A ≃ BasisIndex (A.image σ).

The two-sided inverse is the group inverse of σ, available because the action is typed by the subgroup: act σ⁻¹ ∘ act σ = act 1 = id by act_mul and act_one.

Equations

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

@[simp]

theorem RelSignature.CoherentBasis.basisIndexEquiv_apply_coe {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) (i : B.BasisIndex A) : ↑((B.basisIndexEquiv σ A) i) = B.act σ ↑i

@[simp]

theorem RelSignature.CoherentBasis.basisIndexEquiv_symm_apply_coe {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) (j : B.BasisIndex (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A)) : ↑((B.basisIndexEquiv σ A).symm j) = B.act σ⁻¹ ↑j

@[simp]

theorem RelSignature.CoherentBasis.basisIndexEquiv_one_coe {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (A : Finset ((s : S.Srt) × S.Vinfinite s)) (i : B.BasisIndex A) : ↑((B.basisIndexEquiv 1 A) i) = ↑i

Identity, at the level of underlying indices. The equivalence at σ = 1 does not have type BasisIndex A ≃ BasisIndex A on the nose — its codomain is BasisIndex (A.image id) — so the law is stated where no transport is needed.

@[simp]

theorem RelSignature.CoherentBasis.basisIndexEquiv_mul_coe {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ τ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) (i : B.BasisIndex A) : ↑((B.basisIndexEquiv (σ * τ) A) i) = B.act σ ↑((B.basisIndexEquiv τ A) i)

Composition, likewise at the level of underlying indices: the codomains BasisIndex (A.image (σ * τ)) and BasisIndex ((A.image τ).image σ) agree only after Finset.image_image.

theorem RelSignature.CoherentBasis.factorMap_basisIndexEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) (X : S.RelStructure S.Vinfinite) (i : B.BasisIndex A) : B.factorMap (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A) X ((B.basisIndexEquiv σ A) i) = B.factorMap A (RelStructure.relabel (↑σ) X) i

Naturality of the factor map, with the orientation explicit: evaluating the factor at the image vertex set, on the index transported by σ, is evaluating the factor at A on the relabeled structure.

The direction is forced by event_act being a preimage equality: X ∈ event (act σ i) iff relabel σ X ∈ event i.

noncomputable def RelSignature.CoherentBasis.factorSpaceEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : B.FactorSpace (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A) ≃ᵐ B.FactorSpace A

A relabeling as a measurable equivalence of factor spaces. The forward map is precomposition with basisIndexEquiv σ A; both directions are coordinate reindexings, hence measurable.

This is the form the conditional kernels consume: transporting a kernel across a relabeling needs the measurable equivalence, not just the underlying bijection of indices.

Equations

• B.factorSpaceEquiv σ A = { toEquiv := (B.basisIndexEquiv σ A).symm.arrowCongr (Equiv.refl Bool), measurable_toFun := ⋯, measurable_invFun := ⋯ }

@[simp]

theorem RelSignature.CoherentBasis.factorSpaceEquiv_apply {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) (f : B.FactorSpace (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A)) : (B.factorSpaceEquiv σ A) f = f ∘ ⇑(B.basisIndexEquiv σ A)

theorem RelSignature.CoherentBasis.factorMap_comp_relabel {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) (σ : ↥S.FinSuppPerm) (A : Finset ((s : S.Srt) × S.Vinfinite s)) : ⇑(B.factorSpaceEquiv σ A) ∘ B.factorMap (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A) = B.factorMap A ∘ RelStructure.relabel ↑σ

The naturality equation as a commuting square, through the named measurable equivalence: the factor at the image vertex set, transported back along σ, is the factor at A precomposed with the relabeling.

theorem RelSignature.CoherentBasis.basisIndexEmbedding_basisIndexEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {C A : Finset ((s : S.Srt) × S.Vinfinite s)} (hCA : C ⊆ A) (σ : ↥S.FinSuppPerm) : B.basisIndexEmbedding ⋯ ∘ ⇑(B.basisIndexEquiv σ C) = ⇑(B.basisIndexEquiv σ A) ∘ B.basisIndexEmbedding hCA

The index equivalence commutes with the sub-index inclusions — and definitionally, since both routes act by σ and only the containment proof differs.

theorem RelSignature.CoherentBasis.factorProjection_basisIndexEquiv {S : RelSignature} {M : S.InfiniteRelExchangeableLaw} (B : CoherentBasis M) {C A : Finset ((s : S.Srt) × S.Vinfinite s)} (hCA : C ⊆ A) (σ : ↥S.FinSuppPerm) (f : B.FactorSpace (Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) A)) : B.factorProjection hCA (f ∘ ⇑(B.basisIndexEquiv σ A)) = B.factorProjection ⋯ f ∘ ⇑(B.basisIndexEquiv σ C)

Dually, the factor projection commutes with precomposition by the index equivalence — again definitionally, so the relabeling action descends along the tower of factors with no coherence condition to check.