Mission
An isomorphism of the free group factors
Log in to contributeGoal
Group von Neumann algebras encode a free group's regular representation as an operator algebra. Whether the rank remains visible in that algebra is the motivating isomorphism problem. The pinned manuscript supplies the research context.
The parameter runs over extended nonnegative reals greater than one. Integer ranks use group factors, infinity uses countably many generators, and other parameters use the encoded stabilized corner model.
The selected goal is OAI.FreeGroupFactorMain.Interpolation.allInterpolatedIsomorphic. Its central assertion is
The theorem states that for any two extended nonnegative real parameters r and s, both strictly greater than 1 (so either may be infinite), the interpolated factors attached to r and s are isomorphic as C*-algebras with trace and topology, meaning the type of normal tracial equivalences between them is nonempty. The interpolated factor at a parameter is chosen by cases: for r = ∞ it is the group von Neumann algebra of the free group on countably many generators; for r equal to a natural number n it is the group von Neumann algebra of the free group on n generators; otherwise it is the corner pAp of the stabilization of the rank-two free group algebra, cut down by a selected star projection p whose stabilized projection trace is the real number 1/√(r−1), with the trace being the stabilized trace rescaled by the inverse of that value. Each carries its canonical trace or this rescaled trace and an ultraweak-type topology. A NormalTracialEquiv between two such models consists of a ℂ-linear star-algebra isomorphism that preserves the traces and is continuous in both directions for the given topologies.
The goal is a nonempty type of normal tracial equivalences between the precise interpolated models. Statements about fundamental groups are not separate attached targets. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The required equivalence must preserve the algebra, involution and trace, and be continuous in both directions for the specified topologies.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.theorem allInterpolatedIsomorphic (r s : ℝ≥0∞) (hr : 1<r) (hs : 1<s) :
Nonempty (NormalTracialEquiv (interpolatedTrace r) (interpolatedTrace s)
(interpolatedTopology r) (interpolatedTopology s)) := by
sorry
end FreeGroupFactorMain.Interpolation
end
end OAI
The theorem states that for any two extended nonnegative real parameters r and s, both strictly greater than 1 (so either may be infinite), the interpolated factors attached to r and s are isomorphic as C*-algebras with trace and topology, meaning the type of normal tracial equivalences between them is nonempty. The interpolated factor at a parameter is chosen by cases: for r = ∞ it is the group von Neumann algebra of the free group on countably many generators; for r equal to a natural number n it is the group von Neumann algebra of the free group on n generators; otherwise it is the corner pAp of the stabilization of the rank-two free group algebra, cut down by a selected star projection p whose stabilized projection trace is the real number 1/√(r−1), with the trace being the stabilized trace rescaled by the inverse of that value. Each carries its canonical trace or this rescaled trace and an ultraweak-type topology. A NormalTracialEquiv between two such models consists of a ℂ-linear star-algebra isomorphism that preserves the traces and is continuous in both directions for the given topologies.
No open leaves. Every sub-goal is proved or awaiting decomposition.