class ResourceTheory (ι : Type u_1) extends FreeStateTheory ι : Type (max u_1 (u_2 + 1))

A quantum resource theory extends a FreeStateTheory with a collection of free operations. It is required that any state we can always prepare for free must be free, and this is all then the resource theory is "minimal", but we can have a more restricted set of operations.

• H : ι → Type u_2
• FinH (i : ι) : Fintype (H i)
• DecEqH (i : ι) : DecidableEq (H i)
• NonemptyH (i : ι) : Nonempty (H i)
• prod : ι → ι → ι
• prodEquiv (i j : ι) : H (prod i j) ≃ H i × H j
• IsFree {i : ι} : Set (MState (ResourcePretheory.H i))
• free_closed {i : ι} : IsClosed IsFree
• free_convex {i : ι} : Convex ℝ (MState.m '' IsFree)
• free_prod {i j : ι} {ρ₁ : MState (ResourcePretheory.H i)} {ρ₂ : MState (ResourcePretheory.H j)} (h₁ : IsFree ρ₁) (h₂ : IsFree ρ₂) : IsFree (ResourcePretheory.prodRelabel ρ₁ ρ₂)
• free_fullRank (i : ι) : ∃ (ρ : MState (ResourcePretheory.H i)), 0 < ↑ρ ∧ IsFree ρ
• freeOps (i j : ι) : Set (CPTPMap (ResourcePretheory.H i) (ResourcePretheory.H j))
• nongenerating {i j : ι} {f : CPTPMap (ResourcePretheory.H i) (ResourcePretheory.H j)} (h : f ∈ freeOps i j) (ρ : MState (ResourcePretheory.H i)) : FreeStateTheory.IsFree ρ → FreeStateTheory.IsFree (f ρ)

  Free operations in a ResourceTheory are nongenerating: they only create a free states from a free state.

• free_id (i : ι) : CPTPMap.id ∈ freeOps i i

  The identity operation is free

• free_comp {i j k : ι} (Y : ↑(freeOps j k)) (X : ↑(freeOps i j)) : (↑Y).compose ↑X ∈ freeOps i k

  Free operations are closed under composition

def ResourceTheory.maximal {ι : Type u_1} [FreeStateTheory ι] : ResourceTheory ι

Given a FreeStateTheory, there is a maximal set of free operations compatible with the free states. That is the set of all operations that don't generate non-free states from free states. We call this the maximal resource theory.

Equations

• One or more equations did not get rendered due to their size.

def ResourceTheory.IsMaximal {ι : Type u_1} (r : ResourceTheory ι) : Prop

A resource theory IsMaximal if it includes all non-generating operations.

Equations

• One or more equations did not get rendered due to their size.

structure ResourceTheory.IsTensorial {ι : Type u_1} [ResourceTheory ι] [ResourcePretheory.Unital ι] : Prop

A resource theory IsTensorial if it includes tensor products of operations, creating free states, and discarding. This implies that includes a unit object.

• prod {i j k l : ι} {f : CPTPMap (ResourcePretheory.H i) (ResourcePretheory.H k)} {g : CPTPMap (ResourcePretheory.H j) (ResourcePretheory.H l)} : f ∈ freeOps i k → g ∈ freeOps j l → ResourcePretheory.prodCPTPMap f g ∈ freeOps (ResourcePretheory.prod i j) (ResourcePretheory.prod k l)
• create {i : ι} (ρ : MState (ResourcePretheory.H i)) : FreeStateTheory.IsFree ρ → CPTPMap.const_state ρ ∈ freeOps ResourcePretheory.Unital.unit i
• destroy (i : ι) : CPTPMap.destroy ∈ freeOps i ResourcePretheory.Unital.unit

theorem ResourceTheory.maximal_IsMaximal {ι : Type u_1} [FreeStateTheory ι] : maximal.IsMaximal

The theory ResourceTheory.maximal always IsMaximal.

def ResourceTheory.mk_of_ops {ι : Type u_1} [ResourcePretheory ι] (O : (i j : ι) → Set (CPTPMap (ResourcePretheory.H i) (ResourcePretheory.H j))) (h_id : ∀ (i : ι), CPTPMap.id ∈ O i i) (h_comp : ∀ {i j k : ι} (Y : ↑(O j k)) (X : ↑(O i j)), (↑Y).compose ↑X ∈ O i k) (h_closed : ∀ {i j : ι}, IsClosed (O i j)) (h_convex : ∀ {i j : ι}, Convex ℝ (CPTPMap.choi '' O i j)) (h_prod : ∀ {i j k l : ι} {f : CPTPMap (ResourcePretheory.H i) (ResourcePretheory.H k)} {g : CPTPMap (ResourcePretheory.H j) (ResourcePretheory.H l)}, f ∈ O i k → g ∈ O j l → ResourcePretheory.prodCPTPMap f g ∈ O (ResourcePretheory.prod i j) (ResourcePretheory.prod k l)) (h_fullRank : {i : ι} → sorry) (h_appendFree : {i j k : ι} → sorry) : ResourceTheory ι

A ResourceTheory can be constructed from a set of operations (satisfying appropriate axioms of closure), and then the free states are taken to be the set of states that can be prepared from any initial state.

Equations

• ResourceTheory.mk_of_ops O h_id h_comp h_closed h_convex h_prod h_fullRank h_appendFree = ResourceTheory.mk O ⋯ h_id ⋯

instance ResourceTheory.instQRTCategory (ι : Type u_2) [ResourceTheory ι] : CategoryTheory.Category.{u_3, u_2} ι

A ResourceTheory provides a category structure

Equations

• ResourceTheory.instQRTCategory ι = CategoryTheory.Category.mk ⋯ ⋯ ⋯

noncomputable def ResourceTheory.fullyFreeQRT : ResourceTheory { ι : Type // Finite ι ∧ Nonempty ι }

The 'fully free' quantum resource theory: the category is all finite Hilbert spaces, all maps are free and all states are free. Marked noncomputable because we assume that all types have DecidableEq.

Equations

• ResourceTheory.fullyFreeQRT = ResourceTheory.mk (fun (x x_1 : { ι : Type // Finite ι ∧ Nonempty ι }) => Set.univ) ⋯ ResourceTheory.fullyFreeQRT.proof_9 @ResourceTheory.fullyFreeQRT.proof_10