RelativeGeneration
DefinitionFor a complex Hilbert space H, WOTClosed(A) says a unital star subalgebra A of the bounded operators on H is closed in the weak operator topology, and wstar(S) is the infimum (intersection) of all weakly closed unital star subalgebras containing the operator set S. IsII1Factor(A) packages the following conditions: the zero operator differs from the identity, A is weakly closed, every element of A commuting with all of A is a scalar multiple of the identity, every isometry in A (star(v)v=1) is unitary, and every nonzero projection p in A has a nonzero proper subprojection q in A with pq=qp=q. HasSeparablePredual(A) means there is a separable complete complex normed space, in the same universe as H, whose strong dual is conjugate-linearly isometrically equivalent to A; no separability of H or of the operator norm topology is imposed. The ultraweak topology on operators is generated by the functionals T ↦ Σₙ ⟨xₙ, T yₙ⟩ for sequences with Σ‖xₙ‖‖yₙ‖ finite, and algebras carry the induced topology. IsNormalizedTrace(A,τ) asks a continuous linear functional τ on A to satisfy τ(1)=1, τ(xx) has nonnegative real part, τ(x)=conj τ(x), τ(xy)=τ(yx), faithfulness (τ(xx)=0 forces x=0), and ultraweak continuity. traceDistance(τ,u,v) is the square root of the real part of τ((u−v)(u−v)) for unitaries u,v of A, and traceTopology is the topology generated by open balls for this distance on the unitary group. relativeGeneratorLocus(B,A) is the set of unitaries u of A for which the weakly closed unital star algebra generated by B together with u equals A. MainTarget is a defined proposition, not an established theorem: for every Hilbert space H and every pair of subalgebras B ≤ A of operators on H that are both II₁ factors, if the relative commutant of B in A is only the scalars (an irreducible inclusion) and A has separable predual, then there exists a normalized faithful normal trace τ on A such that relativeGeneratorLocus(B,A) is both a Gδ set and dense in the unitary group of A under traceTopology.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/RelativeGeneration.lean; bytes 16..5898
-- Kind: block; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.
import Mathlib
namespace OAI
noncomputable section
universe level
namespace RelativeGeneration
variable {Hilbert : Type level} [NormedAddCommGroup Hilbert]
[InnerProductSpace ℂ Hilbert] [CompleteSpace Hilbert]
/-- Weak operator closedness of a concrete unital star subalgebra. -/
def WOTClosed (algebra : StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert)) : Prop :=
IsClosed {operator : Hilbert →WOT[ℂ] Hilbert | operator.toCLM ∈ algebra}
/-- The weakly closed unital star algebra generated by a set of operators. -/
def wstar (operators : Set (Hilbert →L[ℂ] Hilbert)) :
StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert) :=
sInf {algebra | WOTClosed algebra ∧ operators ⊆ algebra}
/-- A nonzero, weakly closed, finite diffuse algebra with scalar center. -/
structure IsII1Factor (algebra : StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert)) : Prop where
nonzero : (0 : Hilbert →L[ℂ] Hilbert) ≠ 1
weaklyClosed : WOTClosed algebra
factor : ∀ element : algebra, (∀ other : algebra, other * element = element * other) →
∃ scalar : ℂ, element = algebraMap ℂ algebra scalar
finite : ∀ isometry : algebra, star isometry * isometry = 1 → isometry * star isometry = 1
diffuse : ∀ projection : algebra, IsStarProjection projection → projection ≠ 0 →
∃ subprojection : algebra, IsStarProjection subprojection ∧ subprojection ≠ 0 ∧
subprojection ≠ projection ∧ projection * subprojection = subprojection ∧
subprojection * projection = subprojection
/-- A same-universe separable Banach predual, with the conjugate-linear dual convention.
This imposes no separability on the Hilbert representation or the operator norm topology. -/
def HasSeparablePredual (algebra : StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert)) : Prop :=
∃ (Banach : Type level) (_ : NormedAddCommGroup Banach) (_ : NormedSpace ℂ Banach)
(_ : CompleteSpace Banach) (_ : TopologicalSpace.SeparableSpace Banach),
Nonempty (StrongDual ℂ Banach ≃ₗᵢ⋆[ℂ] algebra)
/-- The ultraweak topology is generated by absolutely summable vector functionals. -/
abbrev ultraweakTopology (Hilbert : Type level) [NormedAddCommGroup Hilbert]
[InnerProductSpace ℂ Hilbert] [CompleteSpace Hilbert] :
TopologicalSpace (Hilbert →L[ℂ] Hilbert) :=
⨅ (left : ℕ → Hilbert) (right : ℕ → Hilbert)
(_ : Summable (fun index => ‖left index‖ * ‖right index‖)),
TopologicalSpace.induced
(fun operator : Hilbert →L[ℂ] Hilbert =>
∑' index, inner ℂ (left index) (operator (right index))) inferInstance
/-- The concrete algebra carries the induced ultraweak topology. -/
abbrev algebraUltraweakTopology (algebra : StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert)) :
TopologicalSpace algebra :=
TopologicalSpace.induced (fun operator : algebra => (operator : Hilbert →L[ℂ] Hilbert))
(ultraweakTopology Hilbert)
/-- A faithful normal normalized trace, not an additional hypothesis on the inclusion. -/
structure IsNormalizedTrace (algebra : StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert))
(trace : algebra →L[ℂ] ℂ) : Prop where
normalized : trace 1 = 1
positive : ∀ element : algebra, 0 ≤ (trace (star element * element)).re
star_preserving : ∀ element : algebra, trace (star element) = star (trace element)
tracial : ∀ left right : algebra, trace (left * right) = trace (right * left)
faithful : ∀ element : algebra, trace (star element * element) = 0 → element = 0
normal : @Continuous algebra ℂ (algebraUltraweakTopology algebra) inferInstance trace
/-- The normalized trace two-distance between genuine unitaries of the original algebra. -/
def traceDistance (algebra : StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert))
(trace : algebra →L[ℂ] ℂ) (left right : unitary algebra) : ℝ :=
Real.sqrt (trace (star ((left : algebra) - (right : algebra)) *
((left : algebra) - (right : algebra)))).re
/-- The topology generated by trace two-distance balls, not the inherited operator norm topology. -/
abbrev traceTopology (algebra : StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert))
(trace : algebra →L[ℂ] ℂ) : TopologicalSpace (unitary algebra) :=
TopologicalSpace.generateFrom {ball | ∃ center : unitary algebra, ∃ radius : ℝ,
0 < radius ∧ ball = {point | traceDistance algebra trace center point < radius}}
/-- The entire relative-generator locus in the original unitary group. -/
def relativeGeneratorLocus (small large : StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert)) :
Set (unitary large) :=
{element | wstar ((small : Set (Hilbert →L[ℂ] Hilbert)) ∪
{((element : large) : Hilbert →L[ℂ] Hilbert)}) = large}
/-- Every irreducible inclusion of concrete type II₁ factors with separable predual
of the larger factor has a dense Gδ full relative-generator locus in the normalized
trace two-topology. The normalized faithful normal trace is asserted to exist;
no representation, transport, cyclicity, or perturbation premise is imposed. -/
def MainTarget : Prop :=
∀ (Hilbert : Type level) [NormedAddCommGroup Hilbert] [InnerProductSpace ℂ Hilbert]
[CompleteSpace Hilbert] (small large : StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert)),
IsII1Factor small → IsII1Factor large → ∀ inclusion : small ≤ large,
(∀ element : large,
(∀ member : small, StarSubalgebra.inclusion inclusion member * element =
element * StarSubalgebra.inclusion inclusion member) →
∃ scalar : ℂ, element = algebraMap ℂ large scalar) →
HasSeparablePredual large →
∃ trace : large →L[ℂ] ℂ, IsNormalizedTrace large trace ∧
@IsGδ (unitary large) (traceTopology large trace) (relativeGeneratorLocus small large) ∧
@Dense (unitary large) (traceTopology large trace) (relativeGeneratorLocus small large)
end RelativeGeneration
end
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.