mathlib documentation

algebra.star.basic

Star monoids and star rings #

We introduce the basic algebraic notions of star monoids, and star rings. Star algebras are introduced in algebra.algebra.star.

These are implemented as "mixin" typeclasses, so to summon a star ring (for example) one needs to write (R : Type) [ring R] [star_ring R]. This avoids difficulties with diamond inheritance.

For now we simply do not introduce notations, as different users are expected to feel strongly about the relative merits of r^*, r†, rᘁ, and so on.

Our star rings are actually star semirings, but of course we can prove star_neg : star (-r) = - star r when the underlying semiring is a ring.

@[class]
structure has_star (R : Type u) :
Type u
  • star : R → R

Notation typeclass (with no default notation!) for an algebraic structure with a star operation.

Instances
def star {R : Type u} [has_star R] (r : R) :
R

A star operation (e.g. complex conjugate).

Equations
@[class]
structure has_involutive_star (R : Type u) :
Type u

Typeclass for a star operation with is involutive.

Instances
@[simp]
theorem star_star {R : Type u} [has_involutive_star R] (r : R) :
star (star r) = r
@[class]
structure star_monoid (R : Type u) [monoid R] :
Type u

A *-monoid is a monoid R with an involutive operations star so star (r * s) = star s * star r.

Instances
@[simp]
theorem star_mul {R : Type u} [monoid R] [star_monoid R] (r s : R) :
star (r * s) = (star s) * star r
def star_mul_equiv {R : Type u} [monoid R] [star_monoid R] :

star as an mul_equiv from R to Rᵒᵖ

Equations
@[simp]
theorem star_mul_equiv_apply {R : Type u} [monoid R] [star_monoid R] (x : R) :
@[simp]
theorem star_one (R : Type u) [monoid R] [star_monoid R] :
star 1 = 1
@[class]
structure star_ring (R : Type u) [semiring R] :
Type u

A *-ring R is a (semi)ring with an involutive star operation which is additive which makes R with its multiplicative structure into a *-monoid (i.e. star (r * s) = star s * star r).

Instances
@[simp]
theorem star_add {R : Type u} [semiring R] [star_ring R] (r s : R) :
star (r + s) = star r + star s
@[simp]
theorem star_add_equiv_apply {R : Type u} [semiring R] [star_ring R] (r : R) :
@[simp]
theorem star_zero (R : Type u) [semiring R] [star_ring R] :
star 0 = 0
@[simp]
theorem star_ring_equiv_apply {R : Type u} [semiring R] [star_ring R] (x : R) :
def star_ring_equiv {R : Type u} [semiring R] [star_ring R] :

star as an ring_equiv from R to Rᵒᵖ

Equations
@[simp]
theorem star_sum {R : Type u} [semiring R] [star_ring R] {α : Type u_1} (s : finset α) (f : α → R) :
star (∑ (x : α) in s, f x) = ∑ (x : α) in s, star (f x)
@[simp]
theorem star_neg {R : Type u} [ring R] [star_ring R] (r : R) :
star (-r) = -star r
@[simp]
theorem star_sub {R : Type u} [ring R] [star_ring R] (r s : R) :
star (r - s) = star r - star s
@[simp]
theorem star_bit0 {R : Type u} [ring R] [star_ring R] (r : R) :
star (bit0 r) = bit0 (star r)
@[simp]
theorem star_bit1 {R : Type u} [ring R] [star_ring R] (r : R) :
star (bit1 r) = bit1 (star r)
def star_ring_of_comm {R : Type u_1} [comm_semiring R] :

Any commutative semiring admits the trivial *-structure.

Equations
@[simp]
theorem star_id_of_comm {R : Type u_1} [comm_semiring R] {x : R} :
star x = x
@[class]
structure star_ordered_ring (R : Type u) [ordered_semiring R] :
Type u

An ordered *-ring is a ring which is both an ordered ring and a *-ring, and 0 ≤ star r * r for every r.

(In a Banach algebra, the natural ordering is given by the positive cone which is the closure of the sums of elements star r * r. This ordering makes the Banach algebra an ordered *-ring.)

Instances
theorem star_mul_self_nonneg {R : Type u} [ordered_semiring R] [star_ordered_ring R] {r : R} :
0 (star r) * r