Physlib

PhyslibAlpha.ProbabilisticTheory.Channel.Weight

Weight pushforward along a channel

i. Overview

A channel from system `A` to system `B` is, in the Schrödinger picture, an affine map on states. Dualizing gives a unital positive linear map on effects in the other direction (the Heisenberg picture): that map is already `UnitalPositiveLinearMap`, so a channel's adjoint needs no new structure. What *is* new is pushing a weight forward along that adjoint, and the fact that a state pushes forward to a state.

Read `φ : Channel E₂ E₁` here as the adjoint of a channel `A → B` with effect algebras `E₁ = E_A`, `E₂ = E_B`: it pulls an effect of `B` back to an effect of `A`. Precomposing a weight on `A` with `φ` gives a weight on `B` — the Schrödinger-picture pushforward — and `Weight.comp_id`, `Weight.comp_comp` show this assignment respects identities and composition, so pushforward is a functor from unital positive linear maps to weights, contravariant in `φ`.

ii. Key definitions and results

  • `Weight.comp`, `Weight.IsFinite.comp`, `Weight.IsState.comp`

iii. Table of contents

  • A. Pushforward of weights
  • B. Functoriality
  • C. Preservation of finite weights and states

A. Pushforward of weights

B. Functoriality

C. Preservation of finite weights and states

6 declarations

definition

Pushforward of a weight ww along a channel ϕ\phi

Given a weight ww on an effect algebra E1E_1 and a channel ϕ:E2→E1\phi : E_2 \to E_1 (representing the adjoint of a channel in the Heisenberg picture), the pushforward weight w∘ϕw \circ \phi on E2E_2 is defined by precomposing ww with ϕ\phi. For any positive element yy in the positive cone of E2E_2, the value of the new weight is given by (w∘ϕ)(y)=w(ϕ(y))(w \circ \phi)(y) = w(\phi(y)).

theorem

Evaluation of the pushforward weight (w∘ϕ)(y)=w(ϕ(y))(w \circ \phi)(y) = w(\phi(y))

Let E1E_1 and E2E_2 be effect algebras. Given a weight ww on E1E_1 and a channel ϕ:E2→E1\phi: E_2 \to E_1, the value of the pushforward weight w∘ϕw \circ \phi at an element yy in the positive cone of E2E_2 is equal to the weight ww applied to the image ϕ(y)\phi(y), which is an element of the positive cone of E1E_1. That is, (w∘ϕ)(y)=w(ϕ(y))(w \circ \phi)(y) = w(\phi(y)).

theorem

Pushforward of a weight ww along the identity channel is ww

Let E1E_1 be an effect algebra and ww be a weight on E1E_1. The pushforward of ww along the identity channel idE1\text{id}_{E_1} is equal to ww itself.

theorem

Associativity of weight pushforward: w∘(ϕ∘ψ)=(w∘ϕ)∘ψw \circ (\phi \circ \psi) = (w \circ \phi) \circ \psi

Let E1,E2E_1, E_2, and E3E_3 be effect algebras. Let ww be a weight on E1E_1, and let ϕ:E2→E1\phi : E_2 \to E_1 and ψ:E3→E2\psi : E_3 \to E_2 be channels (representing unital positive linear maps in the Heisenberg picture). The pushforward of the weight ww along the composed channel ϕ∘ψ\phi \circ \psi is equal to the pushforward of the weight (w∘ϕ)(w \circ \phi) along the channel ψ\psi: w∘(ϕ∘ψ)=(w∘ϕ)∘ψ w \circ (\phi \circ \psi) = (w \circ \phi) \circ \psi

theorem

If a weight ww is finite, then its pushforward w∘ϕw \circ \phi along a channel ϕ\phi is finite.

Let ww be a finite weight on an effect algebra E1E_1. For any channel ϕ:E2→E1\phi : E_2 \to E_1 (representing the adjoint of a channel in the Heisenberg picture), the pushforward weight w∘ϕw \circ \phi on E2E_2 is also a finite weight.

theorem

The pushforward of a state along a channel is a state

Let ww be a weight on an effect algebra F1F_1, and let ϕ:F2→F1\phi : F_2 \to F_1 be a channel (the adjoint of a channel in the Heisenberg picture). If ww is a state, then the pushforward weight w∘ϕw \circ \phi on F2F_2 is also a state.