mathlib documentation

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.

We also define the class star_ordered_ring R, which says that the order on R respects the star operation, i.e. an element r is nonnegative iff there exists an s such that r = star s * s.

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.

TODO #

In a Banach star algebra without a well-defined square root, the natural ordering is given by the positive cone which is the closure of the sums of elements star r * r. A weaker version of star_ordered_ring could be defined for this case. Note that the current definition has the advantage of not requiring a topology.

@[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 : has_star R
star_involutive : function.involutive star

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

theorem star_injective {R : Type u} [has_involutive_star R] :

function.injective star

@[protected]

def equiv.star {R : Type u} [has_involutive_star R] :

star as an equivalence when it is involutive.

Equations

equiv.star = function.involutive.to_perm star star_involutive

theorem eq_star_of_eq_star {R : Type u} [has_involutive_star R] {r s : R} (h : r = star s) :

s = star r

theorem eq_star_iff_eq_star {R : Type u} [has_involutive_star R] {r s : R} :

r = star s ↔ s = star r

theorem star_eq_iff_star_eq {R : Type u} [has_involutive_star R] {r s : R} :

star r = s ↔ star s = r

@[class]

structure has_trivial_star (R : Type u) [has_star R] :

Prop

star_trivial : ∀ (r : R), star r = r

Typeclass for a trivial star operation. This is mostly meant for ℝ.

Instances

real.has_trivial_star

@[class]

structure star_semigroup (R : Type u) [semigroup R] :

Type u

to_has_involutive_star : has_involutive_star R
star_mul : ∀ (r s : R), star (r * s) = (star s) * star r

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

Instances

@[simp]

theorem star_mul' {R : Type u} [comm_semigroup R] [star_semigroup 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} [semigroup R] [star_semigroup R] :

R ≃* Rᵐᵒᵖ

star as an mul_equiv from R to Rᵐᵒᵖ

Equations

star_mul_equiv = {to_fun := λ (x : R), mul_opposite.op (star x), inv_fun := (equiv.trans (function.involutive.to_perm star star_mul_equiv._proof_1) mul_opposite.op_equiv).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

@[simp]

theorem star_mul_equiv_apply {R : Type u} [semigroup R] [star_semigroup R] (x : R) :

⇑star_mul_equiv x = mul_opposite.op (star x)

@[simp]

theorem star_mul_aut_apply {R : Type u} [comm_semigroup R] [star_semigroup R] (ᾰ : R) :

⇑star_mul_aut ᾰ = star ᾰ

def star_mul_aut {R : Type u} [comm_semigroup R] [star_semigroup R] :

star as a mul_aut for commutative R.

Equations

star_mul_aut = {to_fun := star has_involutive_star.to_has_star, inv_fun := (function.involutive.to_perm star star_mul_aut._proof_1).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

@[simp]

theorem star_one (R : Type u) [monoid R] [star_semigroup R] :

star 1 = 1

@[simp]

theorem star_pow {R : Type u} [monoid R] [star_semigroup R] (x : R) (n : ℕ) :

star (x ^ n) = star x ^ n

@[simp]

theorem star_inv {R : Type u} [group R] [star_semigroup R] (x : R) :

star x⁻¹ = (star x)⁻¹

@[simp]

theorem star_zpow {R : Type u} [group R] [star_semigroup R] (x : R) (z : ℤ) :

star (x ^ z) = star x ^ z

@[simp]

theorem star_div {R : Type u} [comm_group R] [star_semigroup 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_semigroup R] {α : Type u_1} (s : finset α) (f : α → R) :

star (∏ (x : α) in s, f x) = ∏ (x : α) in s, star (f x)

def star_semigroup_of_comm {R : Type u_1} [comm_monoid R] :

star_semigroup R

Any commutative monoid admits the trivial *-structure.

See note [reducible non-instances].

Equations

star_semigroup_of_comm = {to_has_involutive_star := {to_has_star := {star := id R}, star_involutive := _}, star_mul := _}

theorem star_id_of_comm {R : Type u_1} [comm_semiring R] {x : R} :

star x = x

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

@[class]

structure star_add_monoid (R : Type u) [add_monoid R] :

Type u

to_has_involutive_star : has_involutive_star R
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] [star_add_monoid R] (ᾰ : R) :

⇑star_add_equiv ᾰ = star ᾰ

def star_add_equiv {R : Type u} [add_monoid R] [star_add_monoid R] :

R ≃+ R

star as an add_equiv

Equations

star_add_equiv = {to_fun := star has_involutive_star.to_has_star, inv_fun := (function.involutive.to_perm star star_add_equiv._proof_1).inv_fun, left_inv := _, right_inv := _, map_add' := _}

@[simp]

theorem star_zero (R : Type u) [add_monoid R] [star_add_monoid R] :

star 0 = 0

@[simp]

theorem star_eq_zero {R : Type u} [add_monoid R] [star_add_monoid R] {x : R} :

star x = 0 ↔ x = 0

theorem star_ne_zero {R : Type u} [add_monoid R] [star_add_monoid R] {x : R} :

star x ≠ 0 ↔ x ≠ 0

@[simp]

theorem star_neg {R : Type u} [add_group R] [star_add_monoid R] (r : R) :

star (-r) = -star r

@[simp]

theorem star_sub {R : Type u} [add_group R] [star_add_monoid R] (r s : R) :

star (r - s) = star r - star s

@[simp]

theorem star_nsmul {R : Type u} [add_comm_monoid R] [star_add_monoid R] (x : R) (n : ℕ) :

star (n • x) = n • star x

@[simp]

theorem star_zsmul {R : Type u} [add_comm_group R] [star_add_monoid R] (x : R) (n : ℤ) :

star (n • x) = n • star x

@[simp]

theorem star_sum {R : Type u} [add_comm_monoid R] [star_add_monoid R] {α : 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) [non_unital_semiring R] :

Type u

to_star_semigroup : star_semigroup R
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 *-semigroup (i.e. star (r * s) = star s * star r).

Instances

@[protected, instance]

def star_ring.to_star_add_monoid {R : Type u} [non_unital_semiring R] [star_ring R] :

star_add_monoid R

Equations

star_ring.to_star_add_monoid = {to_has_involutive_star := star_semigroup.to_has_involutive_star star_ring.to_star_semigroup, star_add := _}

@[simp]

theorem star_ring_equiv_apply {R : Type u} [non_unital_semiring R] [star_ring R] (x : R) :

⇑star_ring_equiv x = mul_opposite.op (star x)

def star_ring_equiv {R : Type u} [non_unital_semiring R] [star_ring R] :

R ≃+* Rᵐᵒᵖ

star as an ring_equiv from R to Rᵐᵒᵖ

Equations

star_ring_equiv = {to_fun := λ (x : R), mul_opposite.op (star x), inv_fun := (star_add_equiv.trans mul_opposite.op_add_equiv).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

@[simp, norm_cast]

theorem star_nat_cast {R : Type u} [semiring R] [star_ring R] (n : ℕ) :

star ↑n = ↑n

@[simp, norm_cast]

theorem star_int_cast {R : Type u} [ring R] [star_ring R] (z : ℤ) :

star ↑z = ↑z

@[simp, norm_cast]

theorem star_rat_cast {R : Type u} [division_ring R] [char_zero R] [star_ring R] (r : ℚ) :

star ↑r = ↑r

@[simp]

theorem star_ring_aut_apply {R : Type u} [comm_semiring R] [star_ring R] (ᾰ : R) :

⇑star_ring_aut ᾰ = star ᾰ

def star_ring_aut {R : Type u} [comm_semiring R] [star_ring R] :

star as a ring automorphism, for commutative R.

Equations

star_ring_aut = {to_fun := star has_involutive_star.to_has_star, inv_fun := star_add_equiv.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

def star_ring_end (R : Type u) [comm_semiring R] [star_ring R] :

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

Note that this is the preferred form (over star_ring_aut, available under the same hypotheses) because the notation E →ₗ⋆[R] F for an R-conjugate-linear map (short for E →ₛₗ[star_ring_end R] F) does not pretty-print if there is a coercion involved, as would be the case for (↑star_ring_aut : R →* R).

Equations

conj = ↑star_ring_aut

theorem star_ring_end_apply {R : Type u} [comm_semiring R] [star_ring R] {x : R} :

⇑conj x = star x

This is not a simp lemma, since we usually want simp to keep star_ring_end 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_end_self_apply {R : Type u} [comm_semiring R] [star_ring R] (x : R) :

⇑conj (⇑conj x) = x

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

⇑conj (⇑conj x) = x

Alias of star_ring_end_self_apply.

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

⇑conj (⇑conj x) = x

Alias of star_ring_end_self_apply.

@[simp]

theorem star_inv' {R : Type u} [division_ring R] [star_ring R] (x : R) :

star x⁻¹ = (star x)⁻¹

@[simp]

theorem star_zpow₀ {R : Type u} [division_ring R] [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} [add_monoid R] [star_add_monoid R] (r : R) :

star (bit0 r) = bit0 (star r)

@[simp]

theorem star_bit1 {R : Type u} [semiring 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.

See note [reducible non-instances].

Equations

star_ring_of_comm = {to_star_semigroup := {to_has_involutive_star := {to_has_star := {star := id R}, star_involutive := _}, star_mul := _}, star_add := _}

@[class]

structure star_ordered_ring (R : Type u) [non_unital_semiring R] [partial_order R] :

Type u

to_star_ring : star_ring R
add_le_add_left : ∀ (a b : R), a ≤ b → ∀ (c : R), c + a ≤ c + b
nonneg_iff : ∀ (r : R), 0 ≤ r ↔ ∃ (s : R), r = (star s) * s

An ordered *-ring is a ring which is both an ordered_add_comm_group and a *-ring, and 0 ≤ r ↔ ∃ s, r = star s * s.

Instances

@[protected, instance]

def star_ordered_ring.ordered_add_comm_group {R : Type u} [ring R] [partial_order R] [star_ordered_ring R] :

ordered_add_comm_group R

Equations

star_ordered_ring.ordered_add_comm_group = {add := ring.add (show ring R, from _inst_1), add_assoc := _, zero := ring.zero (show ring R, from _inst_1), zero_add := _, add_zero := _, nsmul := ring.nsmul (show ring R, from _inst_1), nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (show ring R, from _inst_1), sub := ring.sub (show ring R, from _inst_1), sub_eq_add_neg := _, zsmul := ring.zsmul (show ring R, from _inst_1), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := partial_order.le (show partial_order R, from _inst_2), lt := partial_order.lt (show partial_order R, from _inst_2), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}

theorem star_mul_self_nonneg {R : Type u} [non_unital_semiring R] [partial_order R] [star_ordered_ring R] {r : R} :

0 ≤ (star r) * r

theorem star_mul_self_nonneg' {R : Type u} [non_unital_semiring R] [partial_order R] [star_ordered_ring R] {r : R} :

0 ≤ r * star r

@[class]

structure star_module (R : Type u) (A : Type v) [has_star R] [has_star A] [has_scalar R A] :

Prop

star_smul : ∀ (r : R) (a : A), star (r • a) = star r • star a

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_semigroup.to_star_module {R : Type u} [comm_monoid R] [star_semigroup R] :

star_module R R

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

@[protected, instance]

def ring_hom_inv_pair.star_ring_end.ring_hom_inv_pair {R : Type u} [comm_semiring R] [star_ring R] :

ring_hom_inv_pair conj conj

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

Instances #

@[protected, instance]

def units.star_semigroup {R : Type u} [monoid R] [star_semigroup R] :

star_semigroup Rˣ

Equations

units.star_semigroup = {to_has_involutive_star := {to_has_star := {star := λ (u : Rˣ), {val := star ↑u, inv := star ↑u⁻¹, val_inv := _, inv_val := _}}, star_involutive := _}, star_mul := _}

@[simp]

theorem units.coe_star {R : Type u} [monoid R] [star_semigroup R] (u : Rˣ) :

↑(star u) = star ↑u

@[simp]

theorem units.coe_star_inv {R : Type u} [monoid R] [star_semigroup R] (u : Rˣ) :

↑(star u)⁻¹ = star ↑u⁻¹

@[protected, instance]

def units.star_module {R : Type u} [monoid R] [star_semigroup R] {A : Type u_1} [has_star A] [has_scalar R A] [star_module R A] :

star_module Rˣ A

theorem is_unit.star {R : Type u} [monoid R] [star_semigroup R] {a : R} :

is_unit a → is_unit (star a)

@[simp]

theorem is_unit_star {R : Type u} [monoid R] [star_semigroup R] {a : R} :

is_unit (star a) ↔ is_unit a

theorem ring.inverse_star {R : Type u} [semiring R] [star_ring R] (a : R) :

ring.inverse (star a) = star (ring.inverse a)

@[protected, instance]

def invertible.star {R : Type u_1} [monoid R] [star_semigroup R] (r : R) [invertible r] :

invertible (star r)

Equations

invertible.star r = {inv_of := star (⅟ r), inv_of_mul_self := _, mul_inv_of_self := _}

theorem star_inv_of {R : Type u_1} [monoid R] [star_semigroup R] (r : R) [invertible r] [invertible (star r)] :

star (⅟ r) = ⅟ (star r)

@[protected, instance]

def mul_opposite.has_star {R : Type u} [has_star R] :

has_star Rᵐᵒᵖ

The opposite type carries the same star operation.

Equations

mul_opposite.has_star = {star := λ (r : Rᵐᵒᵖ), mul_opposite.op (star (mul_opposite.unop r))}

@[simp]

theorem mul_opposite.unop_star {R : Type u} [has_star R] (r : Rᵐᵒᵖ) :

mul_opposite.unop (star r) = star (mul_opposite.unop r)

@[simp]

theorem mul_opposite.op_star {R : Type u} [has_star R] (r : R) :

mul_opposite.op (star r) = star (mul_opposite.op r)

@[protected, instance]

def mul_opposite.has_involutive_star {R : Type u} [has_involutive_star R] :

has_involutive_star Rᵐᵒᵖ

Equations

mul_opposite.has_involutive_star = {to_has_star := mul_opposite.has_star has_involutive_star.to_has_star, star_involutive := _}

@[protected, instance]

def mul_opposite.star_semigroup {R : Type u} [monoid R] [star_semigroup R] :

star_semigroup Rᵐᵒᵖ

Equations

mul_opposite.star_semigroup = {to_has_involutive_star := mul_opposite.has_involutive_star star_semigroup.to_has_involutive_star, star_mul := _}

@[protected, instance]

def mul_opposite.star_add_monoid {R : Type u} [add_monoid R] [star_add_monoid R] :

star_add_monoid Rᵐᵒᵖ

Equations

mul_opposite.star_add_monoid = {to_has_involutive_star := mul_opposite.has_involutive_star star_add_monoid.to_has_involutive_star, star_add := _}

@[protected, instance]

def mul_opposite.star_ring {R : Type u} [semiring R] [star_ring R] :

star_ring Rᵐᵒᵖ

Equations

mul_opposite.star_ring = {to_star_semigroup := mul_opposite.star_semigroup star_ring.to_star_semigroup, star_add := _}

@[protected, instance]

def star_semigroup.to_opposite_star_module {R : Type u} [comm_monoid R] [star_semigroup R] :

star_module Rᵐᵒᵖ R

A commutative star monoid is a star module over its opposite via monoid.to_opposite_mul_action.