OAI/Analysis/KadisonKastler/SequenceTransport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonKastler.boundedSequenceMapHom line 14

   Source documentation

   Apply a contractive star homomorphism at every coordinate.

   def boundedSequenceMapHom (φ : A →⋆ₐ[ℂ] B) : BoundedSequence A →⋆ₐ[ℂ] BoundedSequence B where
   …

   Mentions: OAI.KadisonKastler.BoundedSequence

2. theorem OAI.KadisonKastler.boundedSequenceMapHom_apply line 30
3. def OAI.KadisonKastler.boundedSequenceMapEquiv line 33
4. def OAI.KadisonKastler.TraceQuotientMap.comapEquiv line 54

   Source documentation

   A change of the concrete model for the source changes neither the represented quotient nor its trace.

   def comapEquiv (Q : TraceQuotientMap τB σ ω) (e : A ≃⋆ₐ[ℂ] B)
       (hτ : ∀ a, τB.toLinearMap (e a) = τA.toLinearMap a) :
       TraceQuotientMap τA σ ω where
   …

   Mentions: OAI.KadisonKastler.TraceQuotientMap

5. theorem OAI.KadisonKastler.TraceQuotientMap.comapEquiv_quotient line 65