PopaConjugatePosition.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The conjugacy form of Popa's free-position construction: a unitary in an irreducibly included subfactor's tracial ultrapower conjugates a prescribed constant subfactor to a copy free from the ambient constant algebra. The conjugating unitary remains in the prescribed subfactor ultrapower, and trace preservation transports the matrix presentation to its conjugated copy.

def OAI.KadisonSimilarity.conjugatedConstantEmbedding line 30
Source documentation
The prescribed subfactor is embedded as constants, conjugated inside A^ω, then included in B^ω. Thus membership in the prescribed ultrapower is retained.
```
def conjugatedConstantEmbedding (ρ : R →⋆ₐ[ℂ] A)
    (u : unitary (Ultrapower τA hA ω trA)) : R →⋆ₐ[ℂ] Ultrapower τB hB ω trB :=
…
```
def OAI.KadisonSimilarity.Popa1995ConjugateFreenessInput line 39
Source documentation
Local published specialization for a fixed irreducible inclusion of separable II₁ factors A⊂B and a fixed separable subfactor ρ(R)⊂A. The two free algebras are concrete ranges, rather than unspecified copies.
```
def Popa1995ConjugateFreenessInput
    (_hω : (ω : Filter ℕ) ≤ Filter.cofinite) (ρ : R →⋆ₐ[ℂ] A) : Prop :=
…
```
theorem OAI.KadisonSimilarity.quotientTrace_unitary_conjugate line 46

theorem OAI.KadisonSimilarity.conjugatedConstantEmbedding_trace line 56

Source documentation

The conjugated constant copy has exactly its original trace.

theorem conjugatedConstantEmbedding_trace (ρ : R →⋆ₐ[ℂ] A)
    (u : unitary (Ultrapower τA hA ω trA)) (x : R) :
    quotientTrace τB hB ω trB
      (conjugatedConstantEmbedding τA τB hA hB ω trA trB φ hφ ρ u x) = τA (ρ x) := by
…

Mentions: OAI.KadisonSimilarity.conjugatedConstantEmbedding

theorem OAI.KadisonSimilarity.conjugatedConstantEmbedding_range_le line 68
Source documentation
Its range lies inside the included A-ultrapower, as required by the coordinate small-corner transfer.
```
theorem conjugatedConstantEmbedding_range_le (ρ : R →⋆ₐ[ℂ] A)
    (u : unitary (Ultrapower τA hA ω trA)) :
    (conjugatedConstantEmbedding τA τB hA hB ω trA trB φ hφ ρ u).range ≤
      (tracialUltrapowerMap τA τB hA hB ω trA trB φ hφ).range := by
…
```
Mentions: OAI.KadisonSimilarity.conjugatedConstantEmbedding, OAI.KadisonSimilarity.tracialUltrapowerMap

theorem OAI.KadisonSimilarity.conjugatedConstantEmbedding_injective line 76

Source documentation

Faithfulness survives the constant embedding, conjugation, and inclusion.

theorem conjugatedConstantEmbedding_injective (ρ : R →⋆ₐ[ℂ] A)
    (hρ : Function.Injective ρ)
    (hfA : ∀ a : A, τA (star a * a) = 0 → a = 0)
    (u : unitary (Ultrapower τA hA ω trA)) :
    Function.Injective (conjugatedConstantEmbedding τA τB hA hB ω trA trB φ hφ ρ u) :=
…

Mentions: OAI.KadisonSimilarity.conjugatedConstantEmbedding

theorem OAI.KadisonSimilarity.conjugatedConstantEmbedding_range_isClosed line 87

Source documentation

An embedded C-star algebra has closed range; this supplies the actual closed subalgebra used for the matrix-tower transport.

theorem conjugatedConstantEmbedding_range_isClosed (ρ : R →⋆ₐ[ℂ] A)
    (hρ : Function.Injective ρ)
    (hfA : ∀ a : A, τA (star a * a) = 0 → a = 0)
    (u : unitary (Ultrapower τA hA ω trA)) :
    IsClosed ((conjugatedConstantEmbedding τA τB hA hB ω trA trB φ hφ ρ u).range :
      Set (Ultrapower τB hB ω trB)) :=
…

Mentions: OAI.KadisonSimilarity.conjugatedConstantEmbedding