Documentation

Mathlib.Algebra.Star.StarProjection

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.

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
    theorem IsStarProjection.map {A : Type u_2} {B : Type u_3} [Mul A] [Star A] [Mul B] [Star B] {F : Type u_4} [FunLike F A B] [StarHomClass F A B] [MulHomClass F A B] {x : A} (hx : IsStarProjection x) (f : F) :
    IsStarProjection (f x)
    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] [HasUniqueDiv 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] [HasUniqueDiv 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)