# mathlibdocumentation

algebra.star.basic

# Star monoids, rings, and modules #

We introduce the basic algebraic notions of star monoids, star rings, and star modules. A star algebra is simply a star ring that is also a star module.

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
@[class]
structure has_involutive_star (R : Type u) :
Type u
• to_has_star :
• star_involutive :

Typeclass for a star operation with is involutive.

Instances
@[simp]
theorem star_star {R : Type u} (r : R) :
star (star r) = r
theorem star_injective {R : Type u}  :
@[class]
structure star_monoid (R : Type u) [monoid R] :
Type u
• to_has_involutive_star :
• star_mul : ∀ (r s : R), star (r * s) = (star s) * star r

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} [comm_monoid R] [star_monoid R] (x y : R) :
star (x * y) = (star x) * star y

In a commutative ring, make simp prefer leaving the order unchanged.

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_mul_aut_apply {R : Type u} [comm_monoid R] [star_monoid R] (ᾰ : R) :
def star_mul_aut {R : Type u} [comm_monoid R] [star_monoid R] :

star as a mul_aut for commutative R.

Equations
@[simp]
theorem star_one (R : Type u) [monoid R] [star_monoid R] :
star 1 = 1
@[simp]
theorem star_pow {R : Type u} [monoid R] [star_monoid R] (x : R) (n : ) :
star (x ^ n) = star x ^ n
@[simp]
theorem star_inv {R : Type u} [group R] [star_monoid R] (x : R) :
@[simp]
theorem star_zpow {R : Type u} [group R] [star_monoid R] (x : R) (z : ) :
star (x ^ z) = star x ^ z
@[simp]
theorem star_div {R : Type u} [comm_group R] [star_monoid R] (x y : R) :
star (x / y) = star x / star y

When multiplication is commutative, star preserves division.

@[simp]
theorem star_prod {R : Type u} [comm_monoid R] [star_monoid R] {α : Type u_1} (s : finset α) (f : α → R) :
star (∏ (x : α) in s, f x) = ∏ (x : α) in s, star (f x)
def star_monoid_of_comm {R : Type u_1} [comm_monoid R] :

Any commutative monoid admits the trivial *-structure.

Equations
theorem star_id_of_comm {R : Type u_1} {x : R} :
star x = x

Note that since star_monoid_of_comm is reducible, simp can already prove this. -

@[class]
Type u
• to_has_involutive_star :
• star_add : ∀ (r s : R), star (r + s) = star r + star s

A *-additive monoid R is an additive monoid with an involutive star operation which preserves addition.

Instances
@[simp]
theorem star_add_equiv_apply {R : Type u} [add_monoid R] (ᾰ : R) :
R ≃+ R

star as an add_equiv

Equations
@[simp]
theorem star_zero (R : Type u) [add_monoid R]  :
star 0 = 0
@[simp]
theorem star_neg {R : Type u} [add_group R] (r : R) :
star (-r) = -star r
@[simp]
theorem star_sub {R : Type u} [add_group R] (r s : R) :
star (r - s) = star r - star s
@[simp]
theorem star_nsmul {R : Type u} (x : R) (n : ) :
star (n x) = n star x
@[simp]
theorem star_zsmul {R : Type u} (x : R) (n : ) :
star (n x) = n star x
@[simp]
theorem star_sum {R : Type u} {α : Type u_1} (s : finset α) (f : α → R) :
star (∑ (x : α) in s, f x) = ∑ (x : α) in s, star (f x)
@[class]
structure star_ring (R : Type u) [semiring R] :
Type u
• to_star_monoid :
• star_add : ∀ (r s : R), star (r + s) = star r + star s

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
@[protected, instance]
def star_ring.to_star_add_monoid {R : Type u} [semiring R] [star_ring R] :
Equations
@[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
def star_ring_aut {R : Type u} [star_ring R] :

star as a ring_aut for commutative R. This is used to denote complex conjugation, and is available under the notation conj in the locale complex_conjugate

Equations
theorem star_ring_aut_apply {R : Type u} [star_ring R] {x : R} :
= star x

This is not a simp lemma, since we usually want simp to keep star_ring_aut bundled. For example, for complex conjugation, we don't want simp to turn conj x into the bare function star x automatically since most lemmas are about conj x.

@[simp]
theorem star_ring_aut_self_apply {R : Type u} [star_ring R] (x : R) :
theorem complex.conj_conj {R : Type u} [star_ring R] (x : R) :

Alias of star_ring_aut_self_apply.

theorem is_R_or_C.conj_conj {R : Type u} [star_ring R] (x : R) :

Alias of star_ring_aut_self_apply.

@[simp]
theorem star_inv' {R : Type u} [star_ring R] (x : R) :
@[simp]
theorem star_zpow₀ {R : Type u} [star_ring R] (x : R) (z : ) :
star (x ^ z) = star x ^ z
@[simp]
theorem star_div' {R : Type u} [field R] [star_ring R] (x y : R) :
star (x / y) = star x / star y

When multiplication is commutative, star preserves division.

@[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}  :

Any commutative semiring admits the trivial *-structure.

Equations
@[class]
structure star_ordered_ring (R : Type u)  :
Type u
• to_star_ring :
• star_mul_self_nonneg : ∀ (r : R), 0 (star r) * r

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} {r : R} :
0 (star r) * r
@[class]
structure star_module (R : Type u) (A : Type v) [has_star R] [has_star A] [ A] :
Type

A star module A over a star ring R is a module which is a star add monoid, and the two star structures are compatible in the sense star (r • a) = star r • star a.

Note that it is up to the user of this typeclass to enforce [semiring R] [star_ring R] [add_comm_monoid A] [star_add_monoid A] [module R A], and that the statement only requires [has_star R] [has_star A] [has_scalar R A].

If used as [comm_ring R] [star_ring R] [semiring A] [star_ring A] [algebra R A], this represents a star algebra.

Instances
@[protected, instance]
def star_monoid.to_star_module {R : Type u} [comm_monoid R] [star_monoid R] :
R

A commutative star monoid is a star module over itself via monoid.to_mul_action.

Equations
@[protected, instance]

Instance needed to define star-linear maps over a commutative star ring (ex: conjugate-linear maps when R = ℂ).

### Instances #

@[protected, instance]
def units.star_monoid {R : Type u} [monoid R] [star_monoid R] :
Equations
@[simp]
theorem units.coe_star {R : Type u} [monoid R] [star_monoid R] (u : units R) :
(star u) =
@[simp]
theorem units.coe_star_inv {R : Type u} [monoid R] [star_monoid R] (u : units R) :
@[protected, instance]
def units.star_module {R : Type u} [monoid R] [star_monoid R] {A : Type u_1} [has_star A] [ A] [ A] :
Equations
theorem is_unit.star {R : Type u} [monoid R] [star_monoid R] {a : R} :
is_unit (star a)
@[simp]
theorem is_unit_star {R : Type u} [monoid R] [star_monoid R] {a : R} :
theorem ring.inverse_star {R : Type u} [semiring R] [star_ring R] (a : R) :
@[protected, instance]
def mul_opposite.has_star {R : Type u} [has_star R] :

The opposite type carries the same star operation.

Equations
@[simp]
theorem mul_opposite.unop_star {R : Type u} [has_star R] (r : Rᵐᵒᵖ) :
@[simp]
theorem mul_opposite.op_star {R : Type u} [has_star R] (r : R) :
=
@[protected, instance]
def mul_opposite.has_involutive_star {R : Type u}  :
Equations
@[protected, instance]
def mul_opposite.star_monoid {R : Type u} [monoid R] [star_monoid R] :
Equations
@[protected, instance]
A commutative star monoid is a star module over its opposite via monoid.to_opposite_mul_action.