Computational probe: is extend_sup true (deterministic Function.End model)?

fvP_extend_sup (over the kernel monoid) is sorry'd; the question is whether it is even true. The kernel monoid is infinite, but its obstruction is the corner double-commutant identity u '' (CC W) = CC (u '' W), which already makes sense in the finite deterministic model Function.End (the Dirac part). This file brute-forces that model:

• focus Foc = Fin 2, state St = Fin 2 × Fin 2, lens fst,
• u f = fun p => (f p.1, p.2) is the lens-corner embedding (= Lens.update fst),
• cen / cc are the centralizer / bicommutant under composition,
• a "range" is a bicommutant-closed set (cc S = S); extend r = cc (u '' r).

We then check extend (r₁ ⊔ r₂) = extend r₁ ⊔ extend r₂ for every pair of ranges and report any counterexample. (A failure here strongly suggests the probabilistic fvP_extend_sup is false; no failure suggests it is true and my earlier pessimism was wrong.)

@[reducible, inline]

abbrev Foc : Type

Equations

• Foc = Fin 2

@[reducible, inline]

abbrev St : Type

Equations

• St = (Fin 2 × Fin 2)

@[reducible, inline]

abbrev Ma : Type

Equations

• Ma = (Foc → Foc)

@[reducible, inline]

abbrev Mb : Type

Equations

• Mb = (St → St)

def cen {α : Type} [DecidableEq α] [Fintype α] (S : Finset (α → α)) : Finset (α → α)

Centralizer of S (under composition) inside the full endomorphism monoid.

Equations

• cen S = {h : α → α | ∀ g ∈ S, g ∘ h = h ∘ g}

def cc {α : Type} [DecidableEq α] [Fintype α] (S : Finset (α → α)) : Finset (α → α)

Bicommutant closure.

Equations

• cc S = cen (cen S)

def u (f : Ma) : Mb

The lens-corner embedding Foc-endo ↦ St-endo (act on the first coordinate).

Equations

• u f p = (f p.1, p.2)

def uimg (S : Finset Ma) : Finset Mb

Equations

• uimg S = Finset.image u S

def extendUpd (r : Finset Ma) : Finset Mb

extend r's updates: bicommutant of the localized image.

Equations

• extendUpd r = cc (uimg r)

def joinA (r₁ r₂ : Finset Ma) : Finset Ma

Join of two ranges (= bicommutant of the union of updates).

Equations

• joinA r₁ r₂ = cc (r₁ ∪ r₂)

def joinB (s₁ s₂ : Finset Mb) : Finset Mb

Equations

• joinB s₁ s₂ = cc (s₁ ∪ s₂)

def rangesA : Finset (Finset Ma)

The ranges of Ma: bicommutant-closed subsets.

Equations

• rangesA = {S ∈ Finset.univ.powerset | cc S = S}

def extendSupHolds (r₁ r₂ : Finset Ma) : Bool

extend_sup for one pair, as a Bool.

Equations

• extendSupHolds r₁ r₂ = decide (extendUpd (joinA r₁ r₂) = joinB (extendUpd r₁) (extendUpd r₂))

def counterexamples : Finset (Finset Ma × Finset Ma)

All range pairs violating extend_sup.

Equations

• counterexamples = {p ∈ rangesA ×ˢ rangesA | (!extendSupHolds p.1 p.2) = true}

def coreIdentityHolds (W : Finset Ma) : Bool

The underlying identity extend_sup needs, for an arbitrary set W: u '' (CC W) = CC (u '' W).

Equations

• coreIdentityHolds W = decide (uimg (cc W) = cc (uimg W))

def coreCounterexamples : Finset (Finset Ma)

All subsets W ⊆ Ma violating the core identity.

Equations

• coreCounterexamples = {W ∈ Finset.univ.powerset | (!coreIdentityHolds W) = true}

Proof-strategy probe: does extend have a right adjoint?

extend r ≤ R ⟺ r.updates ⊆ u⁻¹'(R.updates). So extend has a right adjoint (hence preserves all joins, giving extend_sup and reduce_sup for free) iff u⁻¹'(R.updates) is bicommutant-closed for every range R. We test that on the corner ranges that actually arise.

def uPre (R : Finset Mb) : Finset Ma

Preimage of a set of Mb-endos under u.

Equations

• uPre R = {f : Ma | u f ∈ R}

def uPreClosed (R : Finset Mb) : Bool

Is u⁻¹'(R) bicommutant-closed in Ma?

Equations

• uPreClosed R = decide (cc (uPre R) = uPre R)

def cornerRanges : Finset (Finset Mb)

The corner ranges appearing in extend_sup: extend r and extend r₁ ⊔ extend r₂.

Equations

• cornerRanges = Finset.image extendUpd rangesA ∪ Finset.image (fun (p : Finset Ma × Finset Ma) => joinB (extendUpd p.1) (extendUpd p.2)) (rangesA ×ˢ rangesA)