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