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] [StarRing 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 non-unital, non-associative, semirings, but of course we can prove star_neg : star (-r) = - star r when the underlying semiring is a ring.

class StarMemClass (S : Type u_1) (R : Type u_2) [Star R] [SetLike S R] : Prop

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

• star_mem {s : S} {r : R} : r ∈ s → star r ∈ s

  Closure under star.

instance StarMemClass.instStar {R : Type u} {S : Type w} [Star R] [SetLike S R] [hS : StarMemClass S R] (s : S) : Star ↥s

@[simp]

theorem StarMemClass.coe_star {R : Type u} {S : Type w} [Star R] [SetLike S R] [hS : StarMemClass S R] (s : S) (x : ↥s) : ↑(star x) = star ↑x

class InvolutiveStar (R : Type u) extends Star R : Type u

Typeclass for a star operation with is involutive.

• star : R → R
• star_involutive : Function.Involutive star

  Involutive condition.

@[simp]

theorem star_star {R : Type u} [InvolutiveStar R] (r : R) : star (star r) = r

theorem star_mem_iff {R : Type u} {S : Type u_1} [SetLike S R] [InvolutiveStar R] [StarMemClass S R] {s : S} {x : R} : star x ∈ s ↔ x ∈ s

theorem star_injective {R : Type u} [InvolutiveStar R] : Function.Injective star

theorem mem_of_star_mem {S : Type u_1} {R : Type u_2} [InvolutiveStar R] [SetLike S R] [StarMemClass S R] {s : S} {r : R} (hr : star r ∈ s) : r ∈ s

@[simp]

theorem star_inj {R : Type u} [InvolutiveStar R] {x y : R} : star x = star y ↔ x = y

def Equiv.star {R : Type u} [InvolutiveStar R] : Perm R

star as an equivalence when it is involutive.

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

theorem eq_star_iff_eq_star {R : Type u} [InvolutiveStar R] {r s : R} : r = star s ↔ s = star r

theorem star_eq_iff_star_eq {R : Type u} [InvolutiveStar R] {r s : R} : star r = s ↔ star s = r

class TrivialStar (R : Type u) [Star R] : Prop

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

• star_trivial (r : R) : star r = r

  Condition that star is trivial

class StarMul (R : Type u) [Mul R] extends InvolutiveStar R : Type u

A *-magma is a magma R with an involutive operation star such that star (r * s) = star s * star r.

• star : R → R
• star_involutive : Function.Involutive star
• star_mul (r s : R) : star (r * s) = star s * star r

  star skew-distributes over multiplication.

theorem star_star_mul {R : Type u} [Mul R] [StarMul R] (x y : R) : star (star x * y) = star y * x

theorem star_mul_star {R : Type u} [Mul R] [StarMul R] (x y : R) : star (x * star y) = y * star x

@[simp]

theorem semiconjBy_star_star_star {R : Type u} [Mul R] [StarMul R] {x y z : R} : SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z

theorem SemiconjBy.star_star_star {R : Type u} [Mul R] [StarMul R] {x y z : R} : SemiconjBy x y z → SemiconjBy (star x) (star z) (star y)

Alias of the reverse direction of semiconjBy_star_star_star.

@[simp]

theorem commute_star_star {R : Type u} [Mul R] [StarMul R] {x y : R} : Commute (star x) (star y) ↔ Commute x y

theorem Commute.star_star {R : Type u} [Mul R] [StarMul R] {x y : R} : Commute x y → Commute (star x) (star y)

Alias of the reverse direction of commute_star_star.

theorem commute_star_comm {R : Type u} [Mul R] [StarMul R] {x y : R} : Commute (star x) y ↔ Commute x (star y)

theorem Commute.star_right {R : Type u} [Mul R] [StarMul R] {x y : R} : Commute (star x) y → Commute x (star y)

Alias of the forward direction of commute_star_comm.

theorem Commute.star_left {R : Type u} [Mul R] [StarMul R] {x y : R} : Commute x (star y) → Commute (star x) y

Alias of the reverse direction of commute_star_comm.

@[simp]

theorem star_mul' {R : Type u} [CommMagma R] [StarMul R] (x y : R) : star (x * y) = star x * star y

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

def starMulEquiv {R : Type u} [Mul R] [StarMul R] : R ≃* Rᵐᵒᵖ

star as a MulEquiv from R to Rᵐᵒᵖ

@[simp]

theorem starMulEquiv_apply {R : Type u} [Mul R] [StarMul R] (x : R) : starMulEquiv x = MulOpposite.op (star x)

def starMulAut {R : Type u} [CommSemigroup R] [StarMul R] : MulAut R

star as a MulAut for commutative R.

@[simp]

theorem starMulAut_apply {R : Type u} [CommSemigroup R] [StarMul R] (a✝ : R) : starMulAut a✝ = star a✝

@[simp]

theorem star_one (R : Type u) [MulOneClass R] [StarMul R] : star 1 = 1

@[simp]

theorem Pi.star_mulSingle {ι : Type u_1} {R : ι → Type u_2} [DecidableEq ι] [(i : ι) → MulOneClass (R i)] [(i : ι) → StarMul (R i)] (i : ι) (r : R i) : star (mulSingle i r) = mulSingle i (star r)

@[simp]

theorem star_pow {R : Type u} [Monoid R] [StarMul R] (x : R) (n : ℕ) : star (x ^ n) = star x ^ n

@[simp]

theorem star_inv {R : Type u} [Group R] [StarMul R] (x : R) : star x⁻¹ = (star x)⁻¹

@[simp]

theorem star_zpow {R : Type u} [Group R] [StarMul R] (x : R) (z : ℤ) : star (x ^ z) = star x ^ z

@[simp]

theorem star_div {R : Type u} [CommGroup R] [StarMul R] (x y : R) : star (x / y) = star x / star y

When multiplication is commutative, star preserves division.

@[reducible, inline]

abbrev starMulOfComm {R : Type u_1} [CommMonoid R] : StarMul R

Any commutative monoid admits the trivial *-structure.

See note [reducible non-instances].

theorem star_id_of_comm {R : Type u_1} [CommMonoid R] {x : R} : star x = x

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

class StarAddMonoid (R : Type u) [AddMonoid R] extends InvolutiveStar R : Type u

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

• star : R → R
• star_involutive : Function.Involutive star
• star_add (r s : R) : star (r + s) = star r + star s

  star commutes with addition

def starAddEquiv {R : Type u} [AddMonoid R] [StarAddMonoid R] : R ≃+ R

star as an AddEquiv

@[simp]

theorem starAddEquiv_apply {R : Type u} [AddMonoid R] [StarAddMonoid R] (a✝ : R) : starAddEquiv a✝ = star a✝

@[simp]

theorem star_zero (R : Type u) [AddMonoid R] [StarAddMonoid R] : star 0 = 0

@[simp]

theorem Pi.star_single {ι : Type u_1} {R : ι → Type u_2} [DecidableEq ι] [(i : ι) → AddMonoid (R i)] [(i : ι) → StarAddMonoid (R i)] (i : ι) (r : R i) : star (single i r) = single i (star r)

@[simp]

theorem star_eq_zero {R : Type u} [AddMonoid R] [StarAddMonoid R] {x : R} : star x = 0 ↔ x = 0

theorem star_ne_zero {R : Type u} [AddMonoid R] [StarAddMonoid R] {x : R} : star x ≠ 0 ↔ x ≠ 0

@[simp]

theorem star_neg {R : Type u} [AddGroup R] [StarAddMonoid R] (r : R) : star (-r) = -star r

@[simp]

theorem star_sub {R : Type u} [AddGroup R] [StarAddMonoid R] (r s : R) : star (r - s) = star r - star s

@[simp]

theorem star_nsmul {R : Type u} [AddMonoid R] [StarAddMonoid R] (n : ℕ) (x : R) : star (n • x) = n • star x

@[simp]

theorem star_zsmul {R : Type u} [AddGroup R] [StarAddMonoid R] (n : ℤ) (x : R) : star (n • x) = n • star x

class StarRing (R : Type u) [NonUnitalNonAssocSemiring R] extends StarMul R : Type u

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

• star : R → R
• star_involutive : Function.Involutive star
• star_mul (r s : R) : star (r * s) = star s * star r
• star_add (r s : R) : star (r + s) = star r + star s

  star commutes with addition

@[instance 100]

instance StarRing.toStarAddMonoid {R : Type u} [NonUnitalNonAssocSemiring R] [StarRing R] : StarAddMonoid R

def starRingEquiv {R : Type u} [NonUnitalNonAssocSemiring R] [StarRing R] : R ≃+* Rᵐᵒᵖ

star as a RingEquiv from R to Rᵐᵒᵖ

@[simp]

theorem starRingEquiv_apply {R : Type u} [NonUnitalNonAssocSemiring R] [StarRing R] (x : R) : starRingEquiv x = MulOpposite.op (star x)

@[simp]

theorem star_natCast {R : Type u} [NonAssocSemiring R] [StarRing R] (n : ℕ) : star ↑n = ↑n

@[simp]

theorem star_ofNat {R : Type u} [NonAssocSemiring R] [StarRing R] (n : ℕ) [n.AtLeastTwo] : star (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem star_intCast {R : Type u} [NonAssocRing R] [StarRing R] (z : ℤ) : star ↑z = ↑z

def starRingAut {R : Type u} [CommSemiring R] [StarRing R] : RingAut R

star as a ring automorphism, for commutative R.

@[simp]

theorem starRingAut_apply {R : Type u} [CommSemiring R] [StarRing R] (a✝ : R) : starRingAut a✝ = star a✝

def starRingEnd (R : Type u) [CommSemiring R] [StarRing 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 scope ComplexConjugate.

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

def ComplexConjugate.termConj : Lean.ParserDescr

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

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

theorem starRingEnd_apply {R : Type u} [CommSemiring R] [StarRing R] (x : R) : (starRingEnd R) x = star x

This is not a simp lemma, since we usually want simp to keep starRingEnd 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.

theorem starRingEnd_self_apply {R : Type u} [CommSemiring R] [StarRing R] (x : R) : (starRingEnd R) ((starRingEnd R) x) = x

instance RingHom.involutiveStar {R : Type u} [CommSemiring R] [StarRing R] {S : Type u_1} [NonAssocSemiring S] : InvolutiveStar (S →+* R)

theorem RingHom.star_def {R : Type u} [CommSemiring R] [StarRing R] {S : Type u_1} [NonAssocSemiring S] (f : S →+* R) : star f = (starRingEnd R).comp f

theorem RingHom.star_apply {R : Type u} [CommSemiring R] [StarRing R] {S : Type u_1} [NonAssocSemiring S] (f : S →+* R) (s : S) : (star f) s = star (f s)

theorem Complex.conj_conj {R : Type u} [CommSemiring R] [StarRing R] (x : R) : (starRingEnd R) ((starRingEnd R) x) = x

Alias of starRingEnd_self_apply.

theorem RCLike.conj_conj {R : Type u} [CommSemiring R] [StarRing R] (x : R) : (starRingEnd R) ((starRingEnd R) x) = x

Alias of starRingEnd_self_apply.

@[simp]

theorem conj_trivial {R : Type u} [CommSemiring R] [StarRing R] [TrivialStar R] (a : R) : (starRingEnd R) a = a

@[simp]

theorem star_inv₀ {R : Type u} [GroupWithZero R] [StarMul R] (x : R) : star x⁻¹ = (star x)⁻¹

@[simp]

theorem star_zpow₀ {R : Type u} [GroupWithZero R] [StarMul R] (x : R) (z : ℤ) : star (x ^ z) = star x ^ z

@[simp]

theorem star_div₀ {R : Type u} [CommGroupWithZero R] [StarMul R] (x y : R) : star (x / y) = star x / star y

When multiplication is commutative, star preserves division.

@[reducible, inline]

abbrev starRingOfComm {R : Type u_1} [CommSemiring R] : StarRing R

Any commutative semiring admits the trivial *-structure.

See note [reducible non-instances].

instance Nat.instStarRing : StarRing ℕ

instance Int.instStarRing : StarRing ℤ

instance Nat.instTrivialStar : TrivialStar ℕ

instance Int.instTrivialStar : TrivialStar ℤ

class StarModule (R : Type u) (A : Type v) [Star R] [Star A] [SMul R A] : Prop

A star module A over a star ring R is a module which is a star additive 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] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A], and that the statement only requires [Star R] [Star A] [SMul R A].

If used as [CommRing R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A], this represents a star algebra.

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

  star commutes with scalar multiplication

instance StarMul.toStarModule {R : Type u} [CommMonoid R] [StarMul R] : StarModule R R

A commutative star monoid is a star module over itself via Monoid.toMulAction.

instance StarAddMonoid.toStarModuleNat {α : Type u_1} [AddCommMonoid α] [StarAddMonoid α] : StarModule ℕ α

instance StarAddMonoid.toStarModuleInt {α : Type u_1} [AddCommGroup α] [StarAddMonoid α] : StarModule ℤ α

instance RingHomInvPair.instStarRingEnd {R : Type u} [CommSemiring R] [StarRing R] : RingHomInvPair (starRingEnd R) (starRingEnd R)

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

class StarHomClass (F : Type u_1) (R : outParam (Type u_2)) (S : outParam (Type u_3)) [Star R] [Star S] [FunLike F R S] : Prop

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

• map_star (f : F) (r : R) : f (star r) = star (f r)

  the maps preserve star

Instances

instance Units.instStarMul {R : Type u} [Monoid R] [StarMul R] : StarMul Rˣ

@[simp]

theorem Units.coe_star {R : Type u} [Monoid R] [StarMul R] (u : Rˣ) : ↑(star u) = star ↑u

@[simp]

theorem Units.coe_star_inv {R : Type u} [Monoid R] [StarMul R] (u : Rˣ) : ↑(star u)⁻¹ = star ↑u⁻¹

instance Units.instStarModule {R : Type u} [Monoid R] [StarMul R] {A : Type u_1} [Star A] [SMul R A] [StarModule R A] : StarModule Rˣ A

theorem IsUnit.star {R : Type u} [Monoid R] [StarMul R] {a : R} : IsUnit a → IsUnit (star a)

@[simp]

theorem isUnit_star {R : Type u} [Monoid R] [StarMul R] {a : R} : IsUnit (star a) ↔ IsUnit a

theorem Ring.inverse_star {R : Type u} [Semiring R] [StarRing R] (a : R) : inverse (star a) = star (inverse a)

instance Invertible.star {R : Type u_1} [MulOneClass R] [StarMul R] (r : R) [Invertible r] : Invertible (star r)

theorem star_invOf {R : Type u_1} [Monoid R] [StarMul R] (r : R) [Invertible r] [Invertible (star r)] : star ⅟r = ⅟(star r)

theorem IsLeftRegular.star {R : Type u} [Mul R] [StarMul R] {x : R} (hx : IsLeftRegular x) : IsRightRegular (star x)

theorem IsRightRegular.star {R : Type u} [Mul R] [StarMul R] {x : R} (hx : IsRightRegular x) : IsLeftRegular (star x)

theorem IsRegular.star {R : Type u} [Mul R] [StarMul R] {x : R} (hx : IsRegular x) : IsRegular (star x)

@[simp]

theorem isRightRegular_star_iff {R : Type u} [Mul R] [StarMul R] {x : R} : IsRightRegular (star x) ↔ IsLeftRegular x

@[simp]

theorem isLeftRegular_star_iff {R : Type u} [Mul R] [StarMul R] {x : R} : IsLeftRegular (star x) ↔ IsRightRegular x

@[simp]

theorem isRegular_star_iff {R : Type u} [Mul R] [StarMul R] {x : R} : IsRegular (star x) ↔ IsRegular x

instance MulOpposite.instStar {R : Type u} [Star R] : Star Rᵐᵒᵖ

The opposite type carries the same star operation.

@[simp]

theorem MulOpposite.unop_star {R : Type u} [Star R] (r : Rᵐᵒᵖ) : unop (star r) = star (unop r)

@[simp]

theorem MulOpposite.op_star {R : Type u} [Star R] (r : R) : op (star r) = star (op r)

instance MulOpposite.instInvolutiveStar {R : Type u} [InvolutiveStar R] : InvolutiveStar Rᵐᵒᵖ

instance MulOpposite.instStarMul {R : Type u} [Mul R] [StarMul R] : StarMul Rᵐᵒᵖ

instance MulOpposite.instStarAddMonoid {R : Type u} [AddMonoid R] [StarAddMonoid R] : StarAddMonoid Rᵐᵒᵖ

instance MulOpposite.instStarRing {R : Type u} [NonUnitalSemiring R] [StarRing R] : StarRing Rᵐᵒᵖ

instance MulOpposite.instStarModule {R : Type u} {M : Type u_1} [Star R] [Star M] [SMul R M] [StarModule R M] : StarModule R Mᵐᵒᵖ

instance StarSemigroup.toOpposite_starModule {R : Type u} [CommMonoid R] [StarMul R] : StarModule Rᵐᵒᵖ R

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