LeanPool.Monlib4.LinearAlgebra.QuantumSet.DeltaForm

Imported Lean Pool material for LeanPool.Monlib4.LinearAlgebra.QuantumSet.DeltaForm.

class QuantumSetDeltaForm (A : Type u_1) [starAlgebra A] [QuantumSet A] [CoalgebraStruct ℂ A] : Type

Delta-form quantum sets satisfy m ∘ comul = δ • 1 for a positive scalar δ.

• delta : ℂ

  The positive delta scalar.

• delta_pos : 0 < delta A

  Positivity of the delta scalar.

• mul_comp_comul_eq : LinearMap.mul' ℂ A ∘ₗ CoalgebraStruct.comul = delta A • 1

  Multiplication after comultiplication is scalar multiplication by delta.

@[reducible]

noncomputable instance QuantumSet.DeltaForm.mulCompComulIsInvertible {A : Type u_1} [starAlgebra A] [QuantumSet A] [CoalgebraStruct ℂ A] [FiniteDimensional ℂ A] [hA2 : QuantumSetDeltaForm A] : Invertible (LinearMap.mul' ℂ A ∘ₗ CoalgebraStruct.comul)

In delta form, m ∘ comul is invertible.

Equations

• QuantumSet.DeltaForm.mulCompComulIsInvertible = ⋯.invertible