Documentation

Mathlib.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] [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.

source
class Star (R : Type u) :
Type u

Notation typeclass (with no default notation!) for an algebraic structure with a star operation.

  • star : R → R

    A star operation (e.g. complex conjugate).

Instances
source
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.

Instances
source
instance StarMemClass.instStar {R : Type u} {S : Type w} [Star R] [SetLike S R] [hS : StarMemClass S R] (s : S) :
Star ↥s
Equations
source
@[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
source
class InvolutiveStar (R : Type u) extends Star :
Type u

Typeclass for a star operation with is involutive.

Instances
source
@[simp]
theorem star_star {R : Type u} [InvolutiveStar R] (r : R) :
star (star r) = r
source
theorem star_injective {R : Type u} [InvolutiveStar R] :
Function.Injective star
source
@[simp]
theorem star_inj {R : Type u} [InvolutiveStar R] {x : R} {y : R} :
star x = star y ↔ x = y
source
def Equiv.star {R : Type u} [InvolutiveStar R] :
Equiv.Perm R

star as an equivalence when it is involutive.

Equations
source
theorem eq_star_of_eq_star {R : Type u} [InvolutiveStar R] {r : R} {s : R} (h : r = star s) :
s = star r
source
theorem eq_star_iff_eq_star {R : Type u} [InvolutiveStar R] {r : R} {s : R} :
r = star s ↔ s = star r
source
theorem star_eq_iff_star_eq {R : Type u} [InvolutiveStar R] {r : R} {s : R} :
star r = s ↔ star s = r
source
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

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

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

Instances
source
theorem star_star_mul {R : Type u} [Mul R] [StarMul R] (x : R) (y : R) :
star (star x * y) = star y * x
source
theorem star_mul_star {R : Type u} [Mul R] [StarMul R] (x : R) (y : R) :
star (x * star y) = y * star x
source
@[simp]
theorem semiconjBy_star_star_star {R : Type u} [Mul R] [StarMul R] {x : R} {y : R} {z : R} :
SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z
source
theorem SemiconjBy.star_star_star {R : Type u} [Mul R] [StarMul R] {x : R} {y : R} {z : R} :
SemiconjBy x y z → SemiconjBy (star x) (star z) (star y)

Alias of the reverse direction of semiconjBy_star_star_star.

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

Alias of the reverse direction of commute_star_star.

source
theorem commute_star_comm {R : Type u} [Mul R] [StarMul R] {x : R} {y : R} :
Commute (star x) y ↔ Commute x (star y)
source
@[simp]
theorem star_mul' {R : Type u} [CommSemigroup R] [StarMul R] (x : R) (y : R) :
star (x * y) = star x * star y

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

source
@[simp]
theorem starMulEquiv_apply {R : Type u} [Mul R] [StarMul R] (x : R) :
starMulEquiv x = MulOpposite.op (star x)
source
def starMulEquiv {R : Type u} [Mul R] [StarMul R] :
R ≃* Rᵐᵒᵖ

star as a MulEquiv from R to Rᵐᵒᵖ

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem starMulAut_apply {R : Type u} [CommSemigroup R] [StarMul R] :
∀ (a : R), starMulAut a = star a
source
def starMulAut {R : Type u} [CommSemigroup R] [StarMul R] :
MulAut R

star as a MulAut for commutative R.

Equations
  • starMulAut = let __src := Function.Involutive.toPerm star ⋯; { toEquiv := { toFun := star, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }, map_mul' := ⋯ }
source
@[simp]
theorem star_one (R : Type u) [MulOneClass R] [StarMul R] :
star 1 = 1
source
@[simp]
theorem star_pow {R : Type u} [Monoid R] [StarMul R] (x : R) (n : ℕ) :
star (x ^ n) = star x ^ n
source
@[simp]
theorem star_inv {R : Type u} [Group R] [StarMul R] (x : R) :
star x⁻¹ = (star x)⁻¹
source
@[simp]
theorem star_zpow {R : Type u} [Group R] [StarMul R] (x : R) (z : ℤ) :
star (x ^ z) = star x ^ z
source
@[simp]
theorem star_div {R : Type u} [CommGroup R] [StarMul R] (x : R) (y : R) :
star (x / y) = star x / star y

When multiplication is commutative, star preserves division.

source
@[reducible]
def starMulOfComm {R : Type u_1} [CommMonoid R] :
StarMul R

Any commutative monoid admits the trivial *-structure.

See note [reducible non-instances].

Equations
source
theorem star_id_of_comm {R : Type u_1} [CommSemiring R] {x : R} :
star x = x

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

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

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

Instances
source
@[simp]
theorem starAddEquiv_apply {R : Type u} [AddMonoid R] [StarAddMonoid R] :
∀ (a : R), starAddEquiv a = star a
source
def starAddEquiv {R : Type u} [AddMonoid R] [StarAddMonoid R] :
R ≃+ R

star as an AddEquiv

Equations
  • starAddEquiv = let __src := Function.Involutive.toPerm star ⋯; { toEquiv := { toFun := star, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }, map_add' := ⋯ }
source
@[simp]
theorem star_zero (R : Type u) [AddMonoid R] [StarAddMonoid R] :
star 0 = 0
source
@[simp]
theorem star_eq_zero {R : Type u} [AddMonoid R] [StarAddMonoid R] {x : R} :
star x = 0 ↔ x = 0
source
theorem star_ne_zero {R : Type u} [AddMonoid R] [StarAddMonoid R] {x : R} :
star x ≠ 0 ↔ x ≠ 0
source
@[simp]
theorem star_neg {R : Type u} [AddGroup R] [StarAddMonoid R] (r : R) :
star (-r) = -star r
source
@[simp]
theorem star_sub {R : Type u} [AddGroup R] [StarAddMonoid R] (r : R) (s : R) :
star (r - s) = star r - star s
source
@[simp]
theorem star_nsmul {R : Type u} [AddMonoid R] [StarAddMonoid R] (x : R) (n : ℕ) :
star (n • x) = n • star x
source
@[simp]
theorem star_zsmul {R : Type u} [AddGroup R] [StarAddMonoid R] (x : R) (n : ℤ) :
star (n • x) = n • star x
source
class StarRing (R : Type u) [NonUnitalNonAssocSemiring R] extends StarMul :
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).

Instances
source
instance StarRing.toStarAddMonoid {R : Type u} [NonUnitalNonAssocSemiring R] [StarRing R] :
StarAddMonoid R
Equations
source
@[simp]
theorem starRingEquiv_apply {R : Type u} [NonUnitalNonAssocSemiring R] [StarRing R] (x : R) :
starRingEquiv x = MulOpposite.op (star x)
source
def starRingEquiv {R : Type u} [NonUnitalNonAssocSemiring R] [StarRing R] :
R ≃+* Rᵐᵒᵖ

star as a RingEquiv from R to Rᵐᵒᵖ

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem star_natCast {R : Type u} [NonAssocSemiring R] [StarRing R] (n : ℕ) :
star ↑n = ↑n
source
@[simp]
theorem star_ofNat {R : Type u} [NonAssocSemiring R] [StarRing R] (n : ℕ) [Nat.AtLeastTwo n] :
star (OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem star_intCast {R : Type u} [Ring R] [StarRing R] (z : ℤ) :
star ↑z = ↑z
source
@[simp]
theorem star_ratCast {R : Type u} [DivisionRing R] [StarRing R] (r : ℚ) :
star ↑r = ↑r
source
@[simp]
theorem starRingAut_apply {R : Type u} [CommSemiring R] [StarRing R] :
∀ (a : R), starRingAut a = star a
source
def starRingAut {R : Type u} [CommSemiring R] [StarRing R] :
RingAut R

star as a ring automorphism, for commutative R.

Equations
  • starRingAut = let __src := starAddEquiv; let __src_1 := starMulAut; { toEquiv := { toFun := star, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }, map_mul' := ⋯, map_add' := ⋯ }
source
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 locale 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).

Equations
Instances For
source
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 locale 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).

Equations
source
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.

source
theorem starRingEnd_self_apply {R : Type u} [CommSemiring R] [StarRing R] (x : R) :
(starRingEnd R) ((starRingEnd R) x) = x
source
instance RingHom.involutiveStar {R : Type u} [CommSemiring R] [StarRing R] {S : Type u_1} [NonAssocSemiring S] :
InvolutiveStar (S →+* R)
Equations
source
theorem RingHom.star_def {R : Type u} [CommSemiring R] [StarRing R] {S : Type u_1} [NonAssocSemiring S] (f : S →+* R) :
star f = RingHom.comp (starRingEnd R) f
source
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)
source
theorem Complex.conj_conj {R : Type u} [CommSemiring R] [StarRing R] (x : R) :
(starRingEnd R) ((starRingEnd R) x) = x

Alias of starRingEnd_self_apply.

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

Alias of starRingEnd_self_apply.

source
@[simp]
theorem conj_trivial {R : Type u} [CommSemiring R] [StarRing R] [TrivialStar R] (a : R) :
(starRingEnd R) a = a
source
@[simp]
theorem star_inv' {R : Type u} [DivisionSemiring R] [StarRing R] (x : R) :
star x⁻¹ = (star x)⁻¹
source
@[simp]
theorem star_zpow₀ {R : Type u} [DivisionSemiring R] [StarRing R] (x : R) (z : ℤ) :
star (x ^ z) = star x ^ z
source
@[simp]
theorem star_div' {R : Type u} [Semifield R] [StarRing R] (x : R) (y : R) :
star (x / y) = star x / star y

When multiplication is commutative, star preserves division.

source
@[simp]
theorem star_bit0 {R : Type u} [AddMonoid R] [StarAddMonoid R] (r : R) :
star (bit0 r) = bit0 (star r)
source
@[simp]
theorem star_bit1 {R : Type u} [Semiring R] [StarRing R] (r : R) :
star (bit1 r) = bit1 (star r)
source
@[reducible]
def starRingOfComm {R : Type u_1} [CommSemiring R] :
StarRing R

Any commutative semiring admits the trivial *-structure.

See note [reducible non-instances].

Equations
  • starRingOfComm = let __src := starMulOfComm; StarRing.mk ⋯
source
instance Nat.instStarRing :
StarRing ℕ
Equations
source
instance Int.instStarRing :
StarRing ℤ
Equations
source
instance Rat.instStarRing :
StarRing ℚ
Equations
source
instance NNRat.instStarRing :
StarRing NNRat
Equations
source
instance Nat.instTrivialStar :
TrivialStar ℕ
Equations
source
instance Int.instTrivialStar :
TrivialStar ℤ
Equations
source
instance Rat.instTrivialStar :
TrivialStar ℚ
Equations
source
instance NNRat.instTrivialStar :
TrivialStar NNRat
Equations
source
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 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] [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.

Instances
source
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.

Equations
  • ⋯ = ⋯
source
instance StarAddMonoid.toStarModuleNat {α : Type u_1} [AddCommMonoid α] [StarAddMonoid α] :
StarModule ℕ α
Equations
  • ⋯ = ⋯
source
instance RingHomInvPair.instRingHomInvPairToSemiringStarRingEnd {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 = ℂ).

Equations
  • ⋯ = ⋯
source
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

Instances #

source
instance Units.instStarMulUnitsInstMulUnits {R : Type u} [Monoid R] [StarMul R] :
StarMul Rˣ
Equations
source
@[simp]
theorem Units.coe_star {R : Type u} [Monoid R] [StarMul R] (u : Rˣ) :
↑(star u) = star ↑u
source
@[simp]
theorem Units.coe_star_inv {R : Type u} [Monoid R] [StarMul R] (u : Rˣ) :
↑(star u)⁻¹ = star ↑u⁻¹
source
instance Units.instStarModuleUnitsToStarToInvolutiveStarInstMulUnitsInstStarMulUnitsInstMulUnitsInstSMulUnits {R : Type u} [Monoid R] [StarMul R] {A : Type u_1} [Star A] [SMul R A] [StarModule R A] :
StarModule Rˣ A
Equations
  • ⋯ = ⋯
source
theorem IsUnit.star {R : Type u} [Monoid R] [StarMul R] {a : R} :
IsUnit a → IsUnit (star a)
source
@[simp]
theorem isUnit_star {R : Type u} [Monoid R] [StarMul R] {a : R} :
IsUnit (star a) ↔ IsUnit a
source
theorem Ring.inverse_star {R : Type u} [Semiring R] [StarRing R] (a : R) :
Ring.inverse (star a) = star (Ring.inverse a)
source
instance Invertible.star {R : Type u_1} [MulOneClass R] [StarMul R] (r : R) [Invertible r] :
Invertible (star r)
Equations
source
theorem star_invOf {R : Type u_1} [Monoid R] [StarMul R] (r : R) [Invertible r] [Invertible (star r)] :
star ⅟r = ⅟(star r)
source
instance MulOpposite.instStarMulOpposite {R : Type u} [Star R] :
Star Rᵐᵒᵖ

The opposite type carries the same star operation.

Equations
source
@[simp]
theorem MulOpposite.unop_star {R : Type u} [Star R] (r : Rᵐᵒᵖ) :
MulOpposite.unop (star r) = star (MulOpposite.unop r)
source
@[simp]
theorem MulOpposite.op_star {R : Type u} [Star R] (r : R) :
MulOpposite.op (star r) = star (MulOpposite.op r)
source
instance MulOpposite.instInvolutiveStarMulOpposite {R : Type u} [InvolutiveStar R] :
InvolutiveStar Rᵐᵒᵖ
Equations
source
instance MulOpposite.instStarMulMulOppositeMul {R : Type u} [Mul R] [StarMul R] :
StarMul Rᵐᵒᵖ
Equations
source
instance MulOpposite.instStarAddMonoidMulOppositeAddMonoid {R : Type u} [AddMonoid R] [StarAddMonoid R] :
StarAddMonoid Rᵐᵒᵖ
Equations
source
instance MulOpposite.instStarRingMulOppositeInstNonUnitalNonAssocSemiringToNonUnitalNonAssocSemiringToNonAssocSemiring {R : Type u} [Semiring R] [StarRing R] :
StarRing Rᵐᵒᵖ
Equations
  • MulOpposite.instStarRingMulOppositeInstNonUnitalNonAssocSemiringToNonUnitalNonAssocSemiringToNonAssocSemiring = StarRing.mk ⋯
source
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.

Equations
  • ⋯ = ⋯