PhysLean Documentation

Mathlib.Algebra.Algebra.StrictPositivity

Strictly positive elements of an algebra #

This file introduces strictly positive elements of an algebra (also known as positive definite elements). This is mostly used for C⋆-algebras, but the basic definition makes sense in a more general context.

Implementation notes #

Note that, while the current definition is adequate in the unital case, it will eventually be replaced by a definition that makes sense in the non-unital case (an element is strictly positive if the hereditary C⋆-subalgebra generated by that element is the whole algebra). Thus, it is best to avoid unfolding the definition and only use the API provided.

TODO #

source
def IsStrictlyPositive {A : Type u_1} [LE A] [Monoid A] [Zero A] (a : A) :
Prop

An element of an ordered algebra is strictly positive if it is nonnegative and invertible.

NOTE: This definition will be generalized to the non-unital case in the future; do not unfold the definition and use the API provided instead to avoid breakage when the refactor happens.

Equations
Instances For
    source
    theorem IsStrictlyPositive.iff_of_unital {A : Type u_1} [LE A] [Monoid A] [Zero A] {a : A} :
    IsStrictlyPositive a ↔ 0 ≤ a ∧ IsUnit a
    source
    theorem IsStrictlyPositive.nonneg {A : Type u_1} [LE A] [Monoid A] [Zero A] {a : A} (ha : IsStrictlyPositive a) :
    0 ≤ a
    source
    theorem IsStrictlyPositive.isUnit {A : Type u_1} [LE A] [Monoid A] [Zero A] {a : A} (ha : IsStrictlyPositive a) :
    IsUnit a
    source
    theorem IsUnit.isStrictlyPositive {A : Type u_1} [LE A] [Monoid A] [Zero A] {a : A} (ha : IsUnit a) (ha₀ : 0 ≤ a) :
    IsStrictlyPositive a
    source
    theorem IsStrictlyPositive.isSelfAdjoint {A : Type u_1} [Semiring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] {a : A} (ha : IsStrictlyPositive a) :
    IsSelfAdjoint a
    source
    @[simp]
    theorem isStrictlyPositive_one {A : Type u_1} [LE A] [Monoid A] [Zero A] [ZeroLEOneClass A] :
    IsStrictlyPositive 1
    source
    theorem IsStrictlyPositive.smul {A : Type u_1} {𝕜 : Type u_2} [Ring A] [PartialOrder A] [Semifield 𝕜] [PartialOrder 𝕜] [Algebra 𝕜 A] [PosSMulMono 𝕜 A] {c : 𝕜} (hc : 0 < c) {a : A} (ha : IsStrictlyPositive a) :
    IsStrictlyPositive (c • a)
    source
    theorem isStrictlyPositive_algebraMap {A : Type u_1} {𝕜 : Type u_2} [Ring A] [PartialOrder A] [ZeroLEOneClass A] [Semifield 𝕜] [PartialOrder 𝕜] [Algebra 𝕜 A] [PosSMulMono 𝕜 A] {c : 𝕜} (hc : 0 < c) :
    IsStrictlyPositive ((algebraMap 𝕜 A) c)
    source
    theorem IsStrictlyPositive.spectrum_pos {A : Type u_1} {𝕜 : Type u_2} [Ring A] [PartialOrder A] [CommSemiring 𝕜] [PartialOrder 𝕜] [Algebra 𝕜 A] [NonnegSpectrumClass 𝕜 A] {a : A} (ha : IsStrictlyPositive a) {x : 𝕜} (hx : x ∈ spectrum 𝕜 a) :
    0 < x