mathlib3 documentation

algebra.star.basic

Star monoids, rings, and modules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
@[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 of this typeclass
Instances of other typeclasses for has_star
  • has_star.has_sizeof_inst
source
@[class]
structure star_mem_class (S : Type u_1) (R : Type u_2) [has_star R] [set_like S R] :
Type

star_mem_class S G states S is a type of subsets s ⊆ G closed under star.

Instances of this typeclass
Instances of other typeclasses for star_mem_class
  • star_mem_class.has_sizeof_inst
source
@[protected, instance]
def star_mem_class.has_star {R S : Type u} [has_star R] [set_like S R] [hS : star_mem_class S R] (s : S) :
has_star ↥s
Equations
source
@[class]
structure has_involutive_star (R : Type u) :
Type u

Typeclass for a star operation with is involutive.

Instances of this typeclass
Instances of other typeclasses for has_involutive_star
  • has_involutive_star.has_sizeof_inst
source
@[simp]
theorem star_star {R : Type u} [has_involutive_star R] (r : R) :
has_star.star (has_star.star r) = r
source
theorem star_injective {R : Type u} [has_involutive_star R] :
function.injective has_star.star
source
@[simp]
theorem star_inj {R : Type u} [has_involutive_star R] {x y : R} :
has_star.star x = has_star.star y ↔ x = y
source
@[protected]
def equiv.star {R : Type u} [has_involutive_star R] :
equiv.perm R

star as an equivalence when it is involutive.

Equations
source
theorem eq_star_of_eq_star {R : Type u} [has_involutive_star R] {r s : R} (h : r = has_star.star s) :
s = has_star.star r
source
theorem eq_star_iff_eq_star {R : Type u} [has_involutive_star R] {r s : R} :
r = has_star.star s ↔ s = has_star.star r
source
theorem star_eq_iff_star_eq {R : Type u} [has_involutive_star R] {r s : R} :
has_star.star r = s ↔ has_star.star s = r
source
@[class]
structure has_trivial_star (R : Type u) [has_star R] :
Prop

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

Instances of this typeclass
source
@[class]
structure star_semigroup (R : Type u) [semigroup R] :
Type u

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

Instances of this typeclass
Instances of other typeclasses for star_semigroup
  • star_semigroup.has_sizeof_inst
source
theorem star_star_mul {R : Type u} [semigroup R] [star_semigroup R] (x y : R) :
has_star.star (has_star.star x * y) = has_star.star y * x
source
theorem star_mul_star {R : Type u} [semigroup R] [star_semigroup R] (x y : R) :
has_star.star (x * has_star.star y) = y * has_star.star x
source
@[simp]
theorem semiconj_by_star_star_star {R : Type u} [semigroup R] [star_semigroup R] {x y z : R} :
semiconj_by (has_star.star x) (has_star.star z) (has_star.star y) ↔ semiconj_by x y z
source
theorem semiconj_by.star_star_star {R : Type u} [semigroup R] [star_semigroup R] {x y z : R} :
semiconj_by x y z → semiconj_by (has_star.star x) (has_star.star z) (has_star.star y)

Alias of the reverse direction of semiconj_by_star_star_star.

source
@[simp]
theorem commute_star_star {R : Type u} [semigroup R] [star_semigroup R] {x y : R} :
commute (has_star.star x) (has_star.star y) ↔ commute x y
source
theorem commute.star_star {R : Type u} [semigroup R] [star_semigroup R] {x y : R} :
commute x y → commute (has_star.star x) (has_star.star y)

Alias of the reverse direction of commute_star_star.

source
theorem commute_star_comm {R : Type u} [semigroup R] [star_semigroup R] {x y : R} :
commute (has_star.star x) y ↔ commute x (has_star.star y)
source
@[simp]
theorem star_mul' {R : Type u} [comm_semigroup R] [star_semigroup R] (x y : R) :
has_star.star (x * y) = has_star.star x * has_star.star y

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

source
def star_mul_equiv {R : Type u} [semigroup R] [star_semigroup R] :
R ≃* Rᵐᵒᵖ

star as an mul_equiv from R to Rᵐᵒᵖ

Equations
source
@[simp]
theorem star_mul_equiv_apply {R : Type u} [semigroup R] [star_semigroup R] (x : R) :
⇑star_mul_equiv x = mul_opposite.op (has_star.star x)
source
@[simp]
theorem star_mul_aut_apply {R : Type u} [comm_semigroup R] [star_semigroup R] (ᾰ : R) :
⇑star_mul_aut ᾰ = has_star.star ᾰ
source
def star_mul_aut {R : Type u} [comm_semigroup R] [star_semigroup R] :
mul_aut R

star as a mul_aut for commutative R.

Equations
source
@[simp]
theorem star_one (R : Type u) [monoid R] [star_semigroup R] :
has_star.star 1 = 1
source
@[simp]
theorem star_pow {R : Type u} [monoid R] [star_semigroup R] (x : R) (n : ℕ) :
has_star.star (x ^ n) = has_star.star x ^ n
source
@[simp]
theorem star_inv {R : Type u} [group R] [star_semigroup R] (x : R) :
has_star.star x⁻¹ = (has_star.star x)⁻¹
source
@[simp]
theorem star_zpow {R : Type u} [group R] [star_semigroup R] (x : R) (z : ℤ) :
has_star.star (x ^ z) = has_star.star x ^ z
source
@[simp]
theorem star_div {R : Type u} [comm_group R] [star_semigroup R] (x y : R) :
has_star.star (x / y) = has_star.star x / has_star.star y

When multiplication is commutative, star preserves division.

source
@[reducible]
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
source
theorem star_id_of_comm {R : Type u_1} [comm_semiring R] {x : R} :
has_star.star x = x

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

source
@[class]
structure star_add_monoid (R : Type u) [add_monoid R] :
Type u

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

Instances of this typeclass
Instances of other typeclasses for star_add_monoid
  • star_add_monoid.has_sizeof_inst
source
@[simp]
theorem star_add_equiv_apply {R : Type u} [add_monoid R] [star_add_monoid R] (ᾰ : R) :
⇑star_add_equiv ᾰ = has_star.star ᾰ
source
def star_add_equiv {R : Type u} [add_monoid R] [star_add_monoid R] :
R ≃+ R

star as an add_equiv

Equations
source
@[simp]
theorem star_zero (R : Type u) [add_monoid R] [star_add_monoid R] :
has_star.star 0 = 0
source
@[simp]
theorem star_eq_zero {R : Type u} [add_monoid R] [star_add_monoid R] {x : R} :
has_star.star x = 0 ↔ x = 0
source
theorem star_ne_zero {R : Type u} [add_monoid R] [star_add_monoid R] {x : R} :
has_star.star x ≠ 0 ↔ x ≠ 0
source
@[simp]
theorem star_neg {R : Type u} [add_group R] [star_add_monoid R] (r : R) :
has_star.star (-r) = -has_star.star r
source
@[simp]
theorem star_sub {R : Type u} [add_group R] [star_add_monoid R] (r s : R) :
has_star.star (r - s) = has_star.star r - has_star.star s
source
@[simp]
theorem star_nsmul {R : Type u} [add_monoid R] [star_add_monoid R] (x : R) (n : ℕ) :
has_star.star (n • x) = n • has_star.star x
source
@[simp]
theorem star_zsmul {R : Type u} [add_group R] [star_add_monoid R] (x : R) (n : ℤ) :
has_star.star (n • x) = n • has_star.star x
source
@[class]
structure star_ring (R : Type u) [non_unital_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 *-semigroup (i.e. star (r * s) = star s * star r).

Instances of this typeclass
Instances of other typeclasses for star_ring
  • star_ring.has_sizeof_inst
source
@[protected, instance]
def star_ring.to_star_add_monoid {R : Type u} [non_unital_semiring R] [star_ring R] :
star_add_monoid R
Equations
source
@[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 (has_star.star x)
source
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
source
@[simp, norm_cast]
theorem star_nat_cast {R : Type u} [semiring R] [star_ring R] (n : ℕ) :
has_star.star ↑n = ↑n
source
@[simp, norm_cast]
theorem star_int_cast {R : Type u} [ring R] [star_ring R] (z : ℤ) :
has_star.star ↑z = ↑z
source
@[simp, norm_cast]
theorem star_rat_cast {R : Type u} [division_ring R] [star_ring R] (r : ℚ) :
has_star.star ↑r = ↑r
source
@[simp]
theorem star_ring_aut_apply {R : Type u} [comm_semiring R] [star_ring R] (ᾰ : R) :
⇑star_ring_aut ᾰ = has_star.star ᾰ
source
def star_ring_aut {R : Type u} [comm_semiring R] [star_ring R] :
ring_aut R

star as a ring automorphism, for commutative R.

Equations
source
def star_ring_end (R : Type u) [comm_semiring R] [star_ring R] :
R →+* 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
Instances for star_ring_end
source
theorem star_ring_end_apply {R : Type u} [comm_semiring R] [star_ring R] {x : R} :
⇑(star_ring_end R) x = has_star.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.

source
@[simp]
theorem star_ring_end_self_apply {R : Type u} [comm_semiring R] [star_ring R] (x : R) :
⇑(star_ring_end R) (⇑(star_ring_end R) x) = x
source
@[protected, instance]
def ring_hom.has_involutive_star {R : Type u} {S : Type u_1} [non_assoc_semiring S] [comm_semiring R] [star_ring R] :
has_involutive_star (S →+* R)
Equations
source
theorem ring_hom.star_def {R : Type u} {S : Type u_1} [non_assoc_semiring S] [comm_semiring R] [star_ring R] (f : S →+* R) :
has_star.star f = (star_ring_end R).comp f
source
theorem ring_hom.star_apply {R : Type u} {S : Type u_1} [non_assoc_semiring S] [comm_semiring R] [star_ring R] (f : S →+* R) (s : S) :
⇑(has_star.star f) s = has_star.star (⇑f s)
source
theorem complex.conj_conj {R : Type u} [comm_semiring R] [star_ring R] (x : R) :
⇑(star_ring_end R) (⇑(star_ring_end R) x) = x

Alias of star_ring_end_self_apply.

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

Alias of star_ring_end_self_apply.

source
@[simp]
theorem star_inv' {R : Type u} [division_semiring R] [star_ring R] (x : R) :
has_star.star x⁻¹ = (has_star.star x)⁻¹
source
@[simp]
theorem star_zpow₀ {R : Type u} [division_semiring R] [star_ring R] (x : R) (z : ℤ) :
has_star.star (x ^ z) = has_star.star x ^ z
source
@[simp]
theorem star_div' {R : Type u} [semifield R] [star_ring R] (x y : R) :
has_star.star (x / y) = has_star.star x / has_star.star y

When multiplication is commutative, star preserves division.

source
@[simp]
theorem star_bit0 {R : Type u} [add_monoid R] [star_add_monoid R] (r : R) :
has_star.star (bit0 r) = bit0 (has_star.star r)
source
@[simp]
theorem star_bit1 {R : Type u} [semiring R] [star_ring R] (r : R) :
has_star.star (bit1 r) = bit1 (has_star.star r)
source
@[reducible]
def star_ring_of_comm {R : Type u_1} [comm_semiring R] :
star_ring R

Any commutative semiring admits the trivial *-structure.

See note [reducible non-instances].

Equations
source
@[class]
structure star_module (R : Type u) (A : Type v) [has_star R] [has_star A] [has_smul R A] :
Prop

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_smul 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 of this typeclass
source
@[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.

source
@[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 (star_ring_end R) (star_ring_end R)

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

source
@[class]
structure star_hom_class (F : Type u_1) (R : out_param (Type u_2)) (S : out_param (Type u_3)) [has_star R] [has_star S] :
Type (max u_1 u_2 u_3)

star_hom_class F R S states that F is a type of star-preserving maps from R to S.

Instances of this typeclass
Instances of other typeclasses for star_hom_class
  • star_hom_class.has_sizeof_inst
source
@[instance]
def star_hom_class.to_fun_like (F : Type u_1) (R : out_param (Type u_2)) (S : out_param (Type u_3)) [has_star R] [has_star S] [self : star_hom_class F R S] :
fun_like F R (λ (_x : R), S)

Instances #

source
@[protected, instance]
def units.star_semigroup {R : Type u} [monoid R] [star_semigroup R] :
star_semigroup Rˣ
Equations
source
@[simp]
theorem units.coe_star {R : Type u} [monoid R] [star_semigroup R] (u : Rˣ) :
↑(has_star.star u) = has_star.star ↑u
source
@[simp]
theorem units.coe_star_inv {R : Type u} [monoid R] [star_semigroup R] (u : Rˣ) :
↑(has_star.star u)⁻¹ = has_star.star ↑u⁻¹
source
@[protected, instance]
def units.star_module {R : Type u} [monoid R] [star_semigroup R] {A : Type u_1} [has_star A] [has_smul R A] [star_module R A] :
star_module Rˣ A
source
theorem is_unit.star {R : Type u} [monoid R] [star_semigroup R] {a : R} :
is_unit a → is_unit (has_star.star a)
source
@[simp]
theorem is_unit_star {R : Type u} [monoid R] [star_semigroup R] {a : R} :
is_unit (has_star.star a) ↔ is_unit a
source
theorem ring.inverse_star {R : Type u} [semiring R] [star_ring R] (a : R) :
ring.inverse (has_star.star a) = has_star.star (ring.inverse a)
source
@[protected, instance]
def invertible.star {R : Type u_1} [monoid R] [star_semigroup R] (r : R) [invertible r] :
invertible (has_star.star r)
Equations
source
theorem star_inv_of {R : Type u_1} [monoid R] [star_semigroup R] (r : R) [invertible r] [invertible (has_star.star r)] :
has_star.star (⅟ r) = ⅟ (has_star.star r)
source
@[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
source
@[simp]
theorem mul_opposite.unop_star {R : Type u} [has_star R] (r : Rᵐᵒᵖ) :
mul_opposite.unop (has_star.star r) = has_star.star (mul_opposite.unop r)
source
@[simp]
theorem mul_opposite.op_star {R : Type u} [has_star R] (r : R) :
mul_opposite.op (has_star.star r) = has_star.star (mul_opposite.op r)
source
@[protected, instance]
def mul_opposite.has_involutive_star {R : Type u} [has_involutive_star R] :
has_involutive_star Rᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.star_semigroup {R : Type u} [monoid R] [star_semigroup R] :
star_semigroup Rᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.star_add_monoid {R : Type u} [add_monoid R] [star_add_monoid R] :
star_add_monoid Rᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.star_ring {R : Type u} [semiring R] [star_ring R] :
star_ring Rᵐᵒᵖ
Equations
source
@[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.