The Boolean syntax layer for a coherent basis (R4 converse piece 3, #107)

The index type of a RelSignature.CoherentBasis must be closed under finite Boolean operations and carry a strict action of the finitely supported relabelings. Both are obtained here by taking the indices to be formal expressions over a set of atoms, rather than a set of events closed under the operations.

Why syntax rather than a closed family of events

Two things go wrong if the index is a family of events:

• The anchor is not determined by the event. The same set can arise anchored at different finite vertex sets, so an event-indexed family forces a choice of anchor, and then anchor_act demands that choice be equivariant — which is the coherence problem again.
• The action laws stop being strict. Closing a family of events under complement and intersection and then acting on it requires choosing representatives of equal events, and act_one / act_mul hold only up to that choice.

With syntax both problems vanish: anchor and event are computed by recursion, so the anchor travels with the expression, and act acts on the syntax tree, so its laws follow by structural induction from the corresponding laws on atoms.

Contents

• RelSignature.BasisExpr — formal Boolean expressions over an atom type;
• BasisExpr.eval / BasisExpr.anchorOf — the event and anchor of an expression, by recursion;
• BasisExpr.act — the relabeling action on expressions, with act_one and act_mul proved by induction from the atom-level laws;
• BasisExpr.instCountable — countability, so the resulting index type is countable.

The syntax

inductive RelSignature.BasisExpr (α : Type u_1) : Type u_1

Formal Boolean expressions over an atom type α: the formal Boolean-expression syntax with ⊥, complement, and intersection — unquotiented terms, not the free Boolean ring itself. Union and difference are derived, so the image of eval is a set ring.

The index of a CoherentBasis is built from this rather than from a closed family of events, so that the anchor is computed from the expression and the relabeling action is structural.

• bot {α : Type u_1} : BasisExpr α

  The empty event, anchored at ∅.

• atom {α : Type u_1} : α → BasisExpr α

  An atom.

• compl {α : Type u_1} : BasisExpr α → BasisExpr α

  Complement; the anchor is unchanged.

• inter {α : Type u_1} : BasisExpr α → BasisExpr α → BasisExpr α

  Intersection; the anchor is the union of the two anchors.

@[implicit_reducible]

instance RelSignature.instEncodableBasisExpr {α✝ : Type u_1} [Encodable α✝] : Encodable (BasisExpr α✝)

Equations

• RelSignature.instEncodableBasisExpr = Encodable.ofLeftInjection RelSignature.instEncodableBasisExpr.encodable_toS✝ RelSignature.instEncodableBasisExpr.encodable_fromS✝ ⋯

instance RelSignature.BasisExpr.instCountable {α : Type u_1} [Countable α] : Countable (BasisExpr α)

Evaluation

noncomputable def RelSignature.BasisExpr.anchorOf {α : Type u_1} {S : RelSignature} (atomAnchor : α → Finset ((s : S.Srt) × S.Vinfinite s)) : BasisExpr α → Finset ((s : S.Srt) × S.Vinfinite s)

The anchor of an expression, computed structurally: ⊥ is anchored at ∅, complement preserves the anchor, and intersection takes the union — which is exactly what keeps the indices anchored inside A closed under the operations.

Equations

• RelSignature.BasisExpr.anchorOf atomAnchor RelSignature.BasisExpr.bot = ∅
• RelSignature.BasisExpr.anchorOf atomAnchor (RelSignature.BasisExpr.atom a) = atomAnchor a
• RelSignature.BasisExpr.anchorOf atomAnchor a.compl = RelSignature.BasisExpr.anchorOf atomAnchor a
• RelSignature.BasisExpr.anchorOf atomAnchor (a.inter a_1) = RelSignature.BasisExpr.anchorOf atomAnchor a ∪ RelSignature.BasisExpr.anchorOf atomAnchor a_1

def RelSignature.BasisExpr.eval {α : Type u_1} {S : RelSignature} (atomEvent : α → Set (S.RelStructure S.Vinfinite)) : BasisExpr α → Set (S.RelStructure S.Vinfinite)

The event of an expression, computed structurally.

Equations

• RelSignature.BasisExpr.eval atomEvent RelSignature.BasisExpr.bot = ∅
• RelSignature.BasisExpr.eval atomEvent (RelSignature.BasisExpr.atom a) = atomEvent a
• RelSignature.BasisExpr.eval atomEvent a.compl = (RelSignature.BasisExpr.eval atomEvent a)ᶜ
• RelSignature.BasisExpr.eval atomEvent (a.inter a_1) = RelSignature.BasisExpr.eval atomEvent a ∩ RelSignature.BasisExpr.eval atomEvent a_1

theorem RelSignature.BasisExpr.eval_mem {α : Type u_1} {S : RelSignature} {atomAnchor : α → Finset ((s : S.Srt) × S.Vinfinite s)} {atomEvent : α → Set (S.RelStructure S.Vinfinite)} (hatom : ∀ (a : α), MeasurableSet (atomEvent a)) (e : BasisExpr α) : MeasurableSet (eval atomEvent e)

Every expression evaluates into the fixing algebra of its own anchor, provided the atoms do. The intersection case is where the anchor-as-union convention pays: both sides are pushed up to the union by fixingAlgebra_mono.

The relabeling action

def RelSignature.BasisExpr.act {α : Type u_1} {S : RelSignature} (atomAct : ↥S.FinSuppPerm → α → α) (σ : ↥S.FinSuppPerm) : BasisExpr α → BasisExpr α

The action on expressions, induced by an action on atoms. Typed by the finitely supported subgroup, matching CoherentBasis.act.

Equations

• RelSignature.BasisExpr.act atomAct σ RelSignature.BasisExpr.bot = RelSignature.BasisExpr.bot
• RelSignature.BasisExpr.act atomAct σ (RelSignature.BasisExpr.atom a) = RelSignature.BasisExpr.atom (atomAct σ a)
• RelSignature.BasisExpr.act atomAct σ a.compl = (RelSignature.BasisExpr.act atomAct σ a).compl
• RelSignature.BasisExpr.act atomAct σ (a.inter a_1) = (RelSignature.BasisExpr.act atomAct σ a).inter (RelSignature.BasisExpr.act atomAct σ a_1)

theorem RelSignature.BasisExpr.act_one {α : Type u_1} {S : RelSignature} {atomAct : ↥S.FinSuppPerm → α → α} (hone : ∀ (a : α), atomAct 1 a = a) (e : BasisExpr α) : act atomAct 1 e = e

The action is trivial at the identity, by induction from the atom-level law.

theorem RelSignature.BasisExpr.act_mul {α : Type u_1} {S : RelSignature} {atomAct : ↥S.FinSuppPerm → α → α} {σ τ : ↥S.FinSuppPerm} (hmul : ∀ (a : α), atomAct (σ * τ) a = atomAct σ (atomAct τ a)) (e : BasisExpr α) : act atomAct (σ * τ) e = act atomAct σ (act atomAct τ e)

The action is multiplicative, by induction from the atom-level law. The orientation matches the contravariance of RelStructure.relabel.

theorem RelSignature.BasisExpr.anchorOf_act {α : Type u_1} {S : RelSignature} {atomAnchor : α → Finset ((s : S.Srt) × S.Vinfinite s)} {atomAct : ↥S.FinSuppPerm → α → α} {σ : ↥S.FinSuppPerm} (hanchor : ∀ (a : α), atomAnchor (atomAct σ a) = Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) (atomAnchor a)) (e : BasisExpr α) : anchorOf atomAnchor (act atomAct σ e) = Finset.image (Sigma.map id fun (s : S.Srt) => ⇑(↑σ s)) (anchorOf atomAnchor e)

The action transports anchors by the image map, provided the atoms do.

theorem RelSignature.BasisExpr.eval_act {α : Type u_1} {S : RelSignature} {atomEvent : α → Set (S.RelStructure S.Vinfinite)} {atomAct : ↥S.FinSuppPerm → α → α} {σ : ↥S.FinSuppPerm} (hevent : ∀ (a : α), atomEvent (atomAct σ a) = RelStructure.relabel ↑σ ⁻¹' atomEvent a) (e : BasisExpr α) : eval atomEvent (act atomAct σ e) = RelStructure.relabel ↑σ ⁻¹' eval atomEvent e

The action transports events by preimage — exactly, with no null sets, provided the atoms do. Complement and intersection commute with preimage on the nose, which is the whole reason the syntax layer keeps the action strict.