VaryingQuotient.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Trace-preserving embeddings of varying tracial products

Coordinate embeddings descend to the represented tracial quotients. Faithfulness and the trace ultralimit formula supply the kernel inclusion; no additional ultraproduct embedding principle is assumed.

theorem OAI.KadisonKastler.descent_eq line 28
def OAI.KadisonKastler.descentValue line 34
theorem OAI.KadisonKastler.descentValue_map line 36
def OAI.KadisonKastler.starAlgHomDescend line 41
Source documentation
Descent through a surjective star homomorphism with smaller kernel.
```
def starAlgHomDescend : B →⋆ₐ[ℂ] C where
…
```
theorem OAI.KadisonKastler.starAlgHomDescend_apply_map line 70
structure OAI.KadisonKastler.VaryingTraceQuotient line 79
Source documentation
The quotient and its canonical trace formula for a varying product.
```
structure VaryingTraceQuotient (τ : ∀ j, FaithfulTracialState (B j))
    (σ : FaithfulTracialState C) (ω : Ultrafilter ℕ) where
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
theorem OAI.KadisonKastler.VaryingTraceQuotient.mapped_trace line 97
Source documentation
Coordinate trace preservation gives trace preservation before descent.
```
theorem mapped_trace (s : VaryingBoundedSequence B) :
    σD.toLinearMap (R.quotient (varyingSequenceMap φ s)) =
      σ.toLinearMap (Q.quotient s) := by
…
```
Mentions: OAI.KadisonKastler.VaryingBoundedSequence, OAI.KadisonKastler.varyingSequenceMap
theorem OAI.KadisonKastler.VaryingTraceQuotient.mapped_zero line 105
Source documentation
Faithfulness gives the kernel inclusion for the induced map.
```
theorem mapped_zero (s : VaryingBoundedSequence B) (hs : Q.quotient s = 0) :
    R.quotient (varyingSequenceMap φ s) = 0 := by
…
```
Mentions: OAI.KadisonKastler.VaryingBoundedSequence, OAI.KadisonKastler.varyingSequenceMap
def OAI.KadisonKastler.VaryingTraceQuotient.inducedMap line 112
Source documentation
The trace-preserving embedding induced by the coordinate embeddings.
```
def inducedMap : C →⋆ₐ[ℂ] D :=
…
```
theorem OAI.KadisonKastler.VaryingTraceQuotient.inducedMap_quotient line 117
theorem OAI.KadisonKastler.VaryingTraceQuotient.trace_inducedMap line 121
theorem OAI.KadisonKastler.VaryingTraceQuotient.inducedMap_injective line 127