# Star projections #

This file defines star projections, which are self-adjoint idempotents.

In star-ordered rings, star projections are non-negative. (See `IsStarProjection.nonneg` in `Mathlib/Algebra/Order/Star/Basic.lean`.)

source
structure IsStarProjection {R : Type u_1} [Mul R] [Star R] (p : R) :
Prop

A star projection is a self-adjoint idempotent.

- isIdempotentElem : IsIdempotentElem p
- isSelfAdjoint : IsSelfAdjoint p

Instances For

source
theorem isStarProjection_iff {R : Type u_1} [Mul R] [Star R] (p : R) :
IsStarProjection p ↔ IsIdempotentElem p ∧ IsSelfAdjoint p
source
theorem isStarProjection_iff' {R : Type u_1} {p : R} [Mul R] [Star R] :
IsStarProjection p ↔ p * p = p ∧ star p = p
source
theorem IsStarProjection.isStarNormal {R : Type u_1} {p : R} [Mul R] [Star R] (hp : IsStarProjection p) :
IsStarNormal p
source
@[simp]
theorem IsStarProjection.zero (R : Type u_1) [NonUnitalNonAssocSemiring R] [StarAddMonoid R] :
IsStarProjection 0
source
@[simp]
theorem IsStarProjection.one (R : Type u_1) [MulOneClass R] [StarMul R] :
IsStarProjection 1
source
theorem IsStarProjection.pow_eq {R : Type u_1} {p : R} [Monoid R] [Star R] (hp : IsStarProjection p) {n : ℕ} (hn : n ≠ 0) :
p ^ n = p
source
theorem IsStarProjection.pow_succ_eq {R : Type u_1} {p : R} [Monoid R] [Star R] (hp : IsStarProjection p) (n : ℕ) :
p ^ (n + 1) = p
source
theorem IsStarProjection.one_sub {R : Type u_1} {p : R} [NonAssocRing R] [StarRing R] (hp : IsStarProjection p) :
IsStarProjection (1 - p)
source
theorem isStarProjection_one_sub_iff {R : Type u_1} {p : R} [NonAssocRing R] [StarRing R] :
IsStarProjection (1 - p) ↔ IsStarProjection p
source
theorem IsStarProjection.of_one_sub {R : Type u_1} {p : R} [NonAssocRing R] [StarRing R] :
IsStarProjection (1 - p) → IsStarProjection p

Alias of the forward direction of `isStarProjection_one_sub_iff`.

source
theorem IsStarProjection.mul_one_sub_self {R : Type u_1} {p : R} [NonAssocRing R] [Star R] (hp : IsStarProjection p) :
p * (1 - p) = 0
source
theorem IsStarProjection.one_sub_mul_self {R : Type u_1} {p : R} [NonAssocRing R] [Star R] (hp : IsStarProjection p) :
(1 - p) * p = 0
source
theorem IsStarProjection.add {R : Type u_1} {p q : R} [NonUnitalNonAssocSemiring R] [StarRing R] (hp : IsStarProjection p) (hq : IsStarProjection q) (hpq : p * q = 0) :
IsStarProjection (p + q)

The sum of star projections is a star projection if their product is `0`.

source
theorem IsStarProjection.mul {R : Type u_1} {p q : R} [NonUnitalSemiring R] [StarRing R] (hp : IsStarProjection p) (hq : IsStarProjection q) (hpq : Commute p q) :
IsStarProjection (p * q)

The product of star projections is a star projection if they commute.

source
theorem IsStarProjection.sub_of_mul_eq_left {R : Type u_1} {p q : R} [NonUnitalNonAssocRing R] [StarRing R] (hp : IsStarProjection p) (hq : IsStarProjection q) (hpq : p * q = p) :
IsStarProjection (q - p)

`q - p` is a star projection when `p * q = p`.

source
theorem IsStarProjection.sub_of_mul_eq_right {R : Type u_1} {p q : R} [NonUnitalNonAssocRing R] [StarRing R] (hp : IsStarProjection p) (hq : IsStarProjection q) (hqp : q * p = p) :
IsStarProjection (q - p)

`q - p` is a star projection when `q * p = p`.

source
theorem IsStarProjection.sub_iff_mul_eq_left {R : Type u_1} [NonUnitalRing R] [StarRing R] [IsAddTorsionFree R] {p q : R} (hp : IsStarProjection p) (hq : IsStarProjection q) :
IsStarProjection (q - p) ↔ p * q = p

`q - p` is a star projection iff `p * q = p`.

source
theorem IsStarProjection.sub_iff_mul_eq_right {R : Type u_1} [NonUnitalRing R] [StarRing R] [IsAddTorsionFree R] {p q : R} (hp : IsStarProjection p) (hq : IsStarProjection q) :
IsStarProjection (q - p) ↔ q * p = p

`q - p` is a star projection iff `q * p = p`.

source
theorem IsStarProjection.add_sub_mul_of_commute {R : Type u_1} {p q : R} [NonUnitalRing R] [StarRing R] (hpq : Commute p q) (hp : IsStarProjection p) (hq : IsStarProjection q) :
IsStarProjection (p + q - p * q)