This definition gives the library's named construction or computation for “system lift”. Lift a system-register matrix through coefficient and selector identities.
def systemLift
{coefficient selector system : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(operator : _root_.Matrix system system ℂ) :
_root_.Matrix
(LCUIndex coefficient selector system)
(LCUIndex coefficient selector system) ℂ :=
(1 : _root_.Matrix coefficient coefficient ℂ) ⊗ₖ
((1 : _root_.Matrix selector selector ℂ) ⊗ₖ operator)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “system lift unitary”; the hypotheses and conclusion in the code panel fix its exact scope. A unitary system operation remains unitary after the identity lifts.
theorem systemLift_unitary
{coefficient selector system : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(operator : _root_.Matrix system system ℂ)
(unitary : operator ∈ _root_.Matrix.unitaryGroup system ℂ) :
systemLift (coefficient := coefficient) (selector := selector) operator ∈
_root_.Matrix.unitaryGroup
(LCUIndex coefficient selector system) ℂ := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “system lift apply”; the hypotheses and conclusion in the code panel fix its exact scope. Entry formula: coefficient and selector are Kronecker deltas.
@[simp] theorem systemLift_apply
{coefficient selector system : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(operator : _root_.Matrix system system ℂ)
(row column : LCUIndex coefficient selector system) :
systemLift (coefficient := coefficient) (selector := selector) operator
row column =
if row.1 = column.1 ∧ row.2.1 = column.2.1 then
operator row.2.2 column.2.2
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “star system lift apply”; the hypotheses and conclusion in the code panel fix its exact scope. Entry formula for the adjoint system lift.
@[simp] theorem star_systemLift_apply
{coefficient selector system : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(operator : _root_.Matrix system system ℂ)
(row column : LCUIndex coefficient selector system) :
star (systemLift (coefficient := coefficient) (selector := selector) operator)
row column =
if row.1 = column.1 ∧ row.2.1 = column.2.1 then
star (operator column.2.2 row.2.2)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “system lift mul clean row”; the hypotheses and conclusion in the code panel fix its exact scope. Left multiplication by a lifted system matrix on a clean row.
theorem systemLift_mul_cleanRow
{coefficient selector system columnType : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
[Fintype columnType]
(systemOperator : _root_.Matrix system system ℂ)
(operator : _root_.Matrix
(LCUIndex coefficient selector system) columnType ℂ)
(cleanCoefficient : coefficient) (cleanSelector : selector)
(systemRow : system) (column : columnType) :
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “mul star system lift clean column”; the hypotheses and conclusion in the code panel fix its exact scope. Right multiplication by the adjoint lift on a clean column.
theorem mul_star_systemLift_cleanColumn
{rowType coefficient selector system : Type*}
[Fintype rowType]
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(operator : _root_.Matrix rowType
(LCUIndex coefficient selector system) ℂ)
(systemOperator : _root_.Matrix system system ℂ)
(row : rowType)
(cleanCoefficient : coefficient) (cleanSelector : selector)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “clean system block”. Extract the coefficient/selector clean block as a system matrix.
noncomputable def cleanSystemBlock
{coefficient selector system : Type*}
(operator : _root_.Matrix
(LCUIndex coefficient selector system)
(LCUIndex coefficient selector system) ℂ)
(cleanCoefficient : coefficient) (cleanSelector : selector) :
_root_.Matrix system system ℂ := fun row column =>
operator (cleanCoefficient, (cleanSelector, row))
(cleanCoefficient, (cleanSelector, column))
/-- Conjugate a full logical matrix only on its system register. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “conjugate system”. Conjugate a full logical matrix only on its system register.
noncomputable def conjugateSystem
{coefficient selector system : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(systemOperator : _root_.Matrix system system ℂ)
(operator : _root_.Matrix
(LCUIndex coefficient selector system)
(LCUIndex coefficient selector system) ℂ) :
_root_.Matrix
(LCUIndex coefficient selector system)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “conjugate system unitary”; the hypotheses and conclusion in the code panel fix its exact scope. System conjugation preserves unitarity.
theorem conjugateSystem_unitary
{coefficient selector system : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(systemOperator : _root_.Matrix system system ℂ)
(operator : _root_.Matrix
(LCUIndex coefficient selector system)
(LCUIndex coefficient selector system) ℂ)
(systemUnitary : systemOperator ∈
_root_.Matrix.unitaryGroup system ℂ)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “clean system block conjugate system”; the hypotheses and conclusion in the code panel fix its exact scope. Conjugating the full logical matrix conjugates exactly its clean system block.
theorem cleanSystemBlock_conjugateSystem
{coefficient selector system : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(systemOperator : _root_.Matrix system system ℂ)
(operator : _root_.Matrix
(LCUIndex coefficient selector system)
(LCUIndex coefficient selector system) ℂ)
(cleanCoefficient : coefficient) (cleanSelector : selector) :
cleanSystemBlock (conjugateSystem systemOperator operator)
commit-pinned source · Verso Blueprint panel