Monoid.lean`

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

The ordered Cuntz monoid and compression by its order unit.

abbrev OAI.Kaplansky.CuntzMonoid line 18
Source documentation
The ordered Cuntz monoid of actual positive finite matrices over A. The order is rectangular norm comparison, not an assumed abstract relation.
```
abbrev CuntzMonoid (A : Type*) [CStarAlgebra A] :=
…
```
def OAI.Kaplansky.cuntzClass line 21
theorem OAI.Kaplansky.cuntzClass_le line 24
theorem OAI.Kaplansky.cuntzClass_eq line 28
instance OAI.Kaplansky.(instance at line 33) line 33
instance OAI.Kaplansky.(instance at line 34) line 34
theorem OAI.Kaplansky.cuntzClass_add line 38
instance OAI.Kaplansky.(instance at line 41) line 41
instance OAI.Kaplansky.(instance at line 70) line 70
theorem OAI.Kaplansky.cuntzMonoid_nonneg line 78
def OAI.Kaplansky.cuntzUnit line 83
Source documentation
Class of the n-by-n identity.
```
def cuntzUnit (A : Type*) [CStarAlgebra A] (n : ℕ) : CuntzMonoid A :=
…
```
Mentions: OAI.Kaplansky.CuntzMonoid
theorem OAI.Kaplansky.cuntzUnit_zero line 86
theorem OAI.Kaplansky.cuntzUnit_add line 95
theorem OAI.Kaplansky.cuntzUnit_nsmul line 105
theorem OAI.Kaplansky.cuntzMonoid_orderUnit line 111
Source documentation
Every class is bounded by a natural multiple of [1_A].
```
theorem cuntzMonoid_orderUnit (x : CuntzMonoid A) : ∃ n : ℕ, x ≤ n • cuntzUnit A 1 := by
…
```
Mentions: OAI.Kaplansky.CuntzMonoid, OAI.Kaplansky.cuntzUnit
theorem OAI.Kaplansky.properlyInfinite_of_coisometry_half line 131
Source documentation
A coisometry supported on the first half of the columns gives two orthogonal isometries in the undoubled algebra.
```
theorem properlyInfinite_of_coisometry_half
    (Y : CStarMatrix (ι ⊕ ι) (ι ⊕ ι) A) (hY : Y * star Y = 1)
    (hzero : ∀ i j, Y i (Sum.inr j) = 0) :
    ProperlyInfinite (CStarMatrix ι ι A) := by
…
```
Mentions: OAI.Kaplansky.ProperlyInfinite
theorem OAI.Kaplansky.properlyInfinite_of_invertible_rectangular_gram line 157
Source documentation
Invertible rectangular row Gram gives a genuine coisometry by inverse square-root normalization. The zero column block is retained.
```
theorem properlyInfinite_of_invertible_rectangular_gram
    (v : Matrix (ι ⊕ ι) ι A)
    (hv : IsUnit (CStarMatrix.ofMatrix (v * v.conjTranspose))) :
    ProperlyInfinite (CStarMatrix ι ι A) := by
…
```
Mentions: OAI.Kaplansky.ProperlyInfinite
theorem OAI.Kaplansky.properlyInfinite_of_cuntzLE_double_unit line 190
Source documentation
Approximate compression of a doubled identity already forces proper infiniteness, using the radius-one invertibility criterion.
```
theorem properlyInfinite_of_cuntzLE_double_unit
    (h : CuntzLE (1 : Matrix (ι ⊕ ι) (ι ⊕ ι) A) (1 : Matrix ι ι A)) :
    ProperlyInfinite (CStarMatrix ι ι A) := by
…
```
Mentions: OAI.Kaplansky.CuntzLE, OAI.Kaplansky.ProperlyInfinite
theorem OAI.Kaplansky.properlyInfinite_of_cuntzUnit_compression line 201