TracialUltrapowerHom.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Trace-preserving homomorphisms induce homomorphisms of the actual tracial quotients. In particular this realizes Q^ω inside P^ω.

def OAI.KadisonSimilarity.boundedSequenceStarHom line 18
Source documentation
Apply a star homomorphism at every coordinate of a bounded sequence.
```
def boundedSequenceStarHom (φ : A →⋆ₐ[ℂ] B) : (ℕ →ᵇ A) →⋆ₐ[ℂ] (ℕ →ᵇ B) where
…
```
theorem OAI.KadisonSimilarity.boundedSequenceStarHom_apply line 28
theorem OAI.KadisonSimilarity.boundedSequenceStarHom_null line 39
def OAI.KadisonSimilarity.tracialUltrapowerMap line 51
Source documentation
The induced star homomorphism of tracial ultrapowers.
```
def tracialUltrapowerMap : Ultrapower τA hA ω trA →⋆ₐ[ℂ] Ultrapower τB hB ω trB where
…
```
theorem OAI.KadisonSimilarity.tracialUltrapowerMap_mk line 61

theorem OAI.KadisonSimilarity.tracialUltrapowerMap_trace line 66

Source documentation

The induced map preserves the actual quotient trace.

theorem tracialUltrapowerMap_trace (x : Ultrapower τA hA ω trA) :
    quotientTrace τB hB ω trB (tracialUltrapowerMap τA τB hA hB ω trA trB φ hφ x) =
      quotientTrace τA hA ω trA x := by
…

Mentions: OAI.KadisonSimilarity.tracialUltrapowerMap

theorem OAI.KadisonSimilarity.tracialUltrapowerMap_injective line 76
Source documentation
Faithfulness of the quotient trace makes the induced map injective.
```
theorem tracialUltrapowerMap_injective :
    Function.Injective (tracialUltrapowerMap τA τB hA hB ω trA trB φ hφ) := by
…
```
Mentions: OAI.KadisonSimilarity.tracialUltrapowerMap