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.

We also define the class StarOrderedRing 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 StarOrderedRing could be defined for this case. Note that the current definition has the advantage of not requiring a topology.

class Star (R : Type u) :

A star operation (e.g. complex conjugate).
star : R → R

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

Instances

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

Closure under star.
star_mem : ∀ {s : S} {r : R}, r ∈ s → star r ∈ s

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

Instances

instance StarMemClass.star {R : Type u} {S : Type u} [inst : Star R] [inst : SetLike S R] [hS : StarMemClass S R] (s : S) :

Star { x // x ∈ s }

Equations

StarMemClass.star s = { star := fun r => { val := star ↑r, property := (_ : star ↑r ∈ s) } }

class InvolutiveStar (R : Type u) extends Star :

Involutive condition.
star_involutive : Function.Involutive star

Typeclass for a star operation with is involutive.

Instances

@[simp]

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

star (star r) = r

theorem star_injective {R : Type u} [inst : InvolutiveStar R] :

Function.Injective star

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

star as an equivalence when it is involutive.

Equations

Equiv.star = Function.Involutive.toPerm star (_ : Function.Involutive star)

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

s = star r

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

r = star s ↔ s = star r

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

star r = s ↔ star s = r

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

Condition that star is trivial
star_trivial : ∀ (r : R), star r = r

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

Instances

class StarSemigroup (R : Type u) [inst : Semigroup R] extends InvolutiveStar :

star skew-distributes over multiplication.
star_mul : ∀ (r s : R), star (r * s) = star s * star r

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

Instances

@[simp]

theorem star_mul' {R : Type u} [inst : CommSemigroup R] [inst : StarSemigroup R] (x : R) (y : R) :

star (x * y) = star x * star y

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

@[simp]

theorem starMulEquiv_apply {R : Type u} [inst : Semigroup R] [inst : StarSemigroup R] (x : R) :

↑starMulEquiv x = { unop := star x }

def starMulEquiv {R : Type u} [inst : Semigroup R] [inst : StarSemigroup R] :

R ≃* Rᵐᵒᵖ

star as a MulEquiv from R to Rᵐᵒᵖ

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem starMulAut_apply {R : Type u} [inst : CommSemigroup R] [inst : StarSemigroup R] :

∀ (a : R), ↑starMulAut a = star a

def starMulAut {R : Type u} [inst : CommSemigroup R] [inst : StarSemigroup R] :

star as a MulAut for commutative R.

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem star_one (R : Type u) [inst : Monoid R] [inst : StarSemigroup R] :

star 1 = 1

@[simp]

theorem star_pow {R : Type u} [inst : Monoid R] [inst : StarSemigroup R] (x : R) (n : ℕ) :

star (x ^ n) = star x ^ n

@[simp]

theorem star_inv {R : Type u} [inst : Group R] [inst : StarSemigroup R] (x : R) :

star x⁻¹ = (star x)⁻¹

@[simp]

theorem star_zpow {R : Type u} [inst : Group R] [inst : StarSemigroup R] (x : R) (z : ℤ) :

star (x ^ z) = star x ^ z

@[simp]

theorem star_div {R : Type u} [inst : CommGroup R] [inst : StarSemigroup R] (x : R) (y : R) :

star (x / y) = star x / star y

When multiplication is commutative, star preserves division.

def starSemigroupOfComm {R : Type u_1} [inst : CommMonoid R] :

StarSemigroup R

Any commutative monoid admits the trivial *-structure.

See note [reducible non-instances].

Equations

starSemigroupOfComm = StarSemigroup.mk (_ : ∀ (a b : R), a * b = b * a)

theorem star_id_of_comm {R : Type u_1} [inst : CommSemiring R] {x : R} :

star x = x

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

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

star commutes with addition
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 starAddEquiv_apply {R : Type u} [inst : AddMonoid R] [inst : StarAddMonoid R] :

∀ (a : R), ↑starAddEquiv a = star a

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

R ≃+ R

star as an AddEquiv

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem star_zero (R : Type u) [inst : AddMonoid R] [inst : StarAddMonoid R] :

star 0 = 0

@[simp]

theorem star_eq_zero {R : Type u} [inst : AddMonoid R] [inst : StarAddMonoid R] {x : R} :

star x = 0 ↔ x = 0

theorem star_ne_zero {R : Type u} [inst : AddMonoid R] [inst : StarAddMonoid R] {x : R} :

star x ≠ 0 ↔ x ≠ 0

@[simp]

theorem star_neg {R : Type u} [inst : AddGroup R] [inst : StarAddMonoid R] (r : R) :

star (-r) = -star r

@[simp]

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

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

@[simp]

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

star (n • x) = n • star x

@[simp]

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

star (n • x) = n • star x

class StarRing (R : Type u) [inst : NonUnitalSemiring R] extends StarSemigroup :

star commutes with addition
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

instance StarRing.toStarAddMonoid {R : Type u} [inst : NonUnitalSemiring R] [inst : StarRing R] :

StarAddMonoid R

Equations

StarRing.toStarAddMonoid = StarAddMonoid.mk (_ : ∀ (r s : R), star (r + s) = star r + star s)

@[simp]

theorem starRingEquiv_apply {R : Type u} [inst : NonUnitalSemiring R] [inst : StarRing R] (x : R) :

↑starRingEquiv x = { unop := star x }

def starRingEquiv {R : Type u} [inst : NonUnitalSemiring R] [inst : StarRing R] :

R ≃+* Rᵐᵒᵖ

star as an RingEquiv from R to Rᵐᵒᵖ

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem star_natCast {R : Type u} [inst : Semiring R] [inst : StarRing R] (n : ℕ) :

star ↑n = ↑n

@[simp]

theorem star_intCast {R : Type u} [inst : Ring R] [inst : StarRing R] (z : ℤ) :

star ↑z = ↑z

@[simp]

theorem star_ratCast {R : Type u} [inst : DivisionRing R] [inst : StarRing R] (r : ℚ) :

star ↑r = ↑r

@[simp]

theorem starRingAut_apply {R : Type u} [inst : CommSemiring R] [inst : StarRing R] :

∀ (a : R), ↑starRingAut a = star a

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

star as a ring automorphism, for commutative R.

Equations

One or more equations did not get rendered due to their size.

def starRingEnd (R : Type u) [inst : CommSemiring R] [inst : StarRing 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→ₗ⋆[R] F⋆[R] F for an R-conjugate-linear map (short for E →ₛₗ[starRingEnd R] F→ₛₗ[starRingEnd R] F) does not pretty-print if there is a coercion involved, as would be the case for (↑starRingAut : R →* R)↑starRingAut : R →* R)→* R).

Equations

starRingEnd R = ↑starRingAut

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→ₗ⋆[R] F⋆[R] F for an R-conjugate-linear map (short for E →ₛₗ[starRingEnd R] F→ₛₗ[starRingEnd R] F) does not pretty-print if there is a coercion involved, as would be the case for (↑starRingAut : R →* R)↑starRingAut : R →* R)→* R).

Equations

ComplexConjugate.termConj = Lean.ParserDescr.node `ComplexConjugate.termConj 1024 (Lean.ParserDescr.symbol "conj")

theorem starRingEnd_apply {R : Type u} [inst : CommSemiring R] [inst : 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} [inst : CommSemiring R] [inst : StarRing R] (x : R) :

↑(starRingEnd R) (↑(starRingEnd R) x) = x

instance RingHom.involutiveStar {R : Type u} {S : Type u_1} [inst : NonAssocSemiring S] [inst : CommSemiring R] [inst : StarRing R] :

InvolutiveStar (S →+* R)

Equations

RingHom.involutiveStar = InvolutiveStar.mk (_ : ∀ (x : S →+* R), star (star x) = x)

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

star f = RingHom.comp (starRingEnd R) f

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

↑(star f) s = star (↑f s)

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

↑(starRingEnd R) (↑(starRingEnd R) x) = x

Alias of starRingEnd_self_apply.

theorem IsROrC.conj_conj {R : Type u} [inst : CommSemiring R] [inst : StarRing R] (x : R) :

↑(starRingEnd R) (↑(starRingEnd R) x) = x

Alias of starRingEnd_self_apply.

@[simp]

theorem star_inv' {R : Type u} [inst : DivisionRing R] [inst : StarRing R] (x : R) :

star x⁻¹ = (star x)⁻¹

@[simp]

theorem star_zpow₀ {R : Type u} [inst : DivisionRing R] [inst : StarRing R] (x : R) (z : ℤ) :

star (x ^ z) = star x ^ z

@[simp]

theorem star_div' {R : Type u} [inst : Field R] [inst : StarRing R] (x : R) (y : R) :

star (x / y) = star x / star y

When multiplication is commutative, star preserves division.

@[simp]

theorem star_bit0 {R : Type u} [inst : AddMonoid R] [inst : StarAddMonoid R] (r : R) :

star (bit0 r) = bit0 (star r)

@[simp]

theorem star_bit1 {R : Type u} [inst : Semiring R] [inst : StarRing R] (r : R) :

star (bit1 r) = bit1 (star r)

def starRingOfComm {R : Type u_1} [inst : CommSemiring R] :

Any commutative semiring admits the trivial *-structure.

See note [reducible non-instances].

Equations

starRingOfComm = let src := starSemigroupOfComm; StarRing.mk (_ : ∀ (x x_1 : R), star (x + x_1) = star (x + x_1))

class StarOrderedRing (R : Type u) [inst : NonUnitalSemiring R] [inst : PartialOrder R] extends StarRing :

addition commutes with ≤≤
add_le_add_left : ∀ (a b : R), a ≤ b → ∀ (c : R), c + a ≤ c + b
characterization of non-negativity
nonneg_iff : ∀ (r : R), 0 ≤ r ↔ ∃ s, r = star s * s

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

Instances

instance StarOrderedRing.instOrderedAddCommGroup {R : Type u} [inst : NonUnitalRing R] [inst : PartialOrder R] [inst : StarOrderedRing R] :

OrderedAddCommGroup R

Equations

One or more equations did not get rendered due to their size.

theorem star_mul_self_nonneg {R : Type u} [inst : NonUnitalSemiring R] [inst : PartialOrder R] [inst : StarOrderedRing R] {r : R} :

0 ≤ star r * r

theorem star_mul_self_nonneg' {R : Type u} [inst : NonUnitalSemiring R] [inst : PartialOrder R] [inst : StarOrderedRing R] {r : R} :

0 ≤ r * star r

theorem conjugate_nonneg {R : Type u} [inst : NonUnitalSemiring R] [inst : PartialOrder R] [inst : StarOrderedRing R] {a : R} (ha : 0 ≤ a) (c : R) :

0 ≤ star c * a * c

theorem conjugate_nonneg' {R : Type u} [inst : NonUnitalSemiring R] [inst : PartialOrder R] [inst : StarOrderedRing R] {a : R} (ha : 0 ≤ a) (c : R) :

0 ≤ c * a * star c

theorem conjugate_le_conjugate {R : Type u} [inst : NonUnitalRing R] [inst : PartialOrder R] [inst : StarOrderedRing R] {a : R} {b : R} (hab : a ≤ b) (c : R) :

star c * a * c ≤ star c * b * c

theorem conjugate_le_conjugate' {R : Type u} [inst : NonUnitalRing R] [inst : PartialOrder R] [inst : StarOrderedRing R] {a : R} {b : R} (hab : a ≤ b) (c : R) :

c * a * star c ≤ c * b * star c

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

star commutes with scalar multiplication
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] [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

instance StarSemigroup.to_starModule {R : Type u} [inst : CommMonoid R] [inst : StarSemigroup R] :

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

Equations

@StarSemigroup.to_starModule = @StarSemigroup.to_starModule.proof_1

instance RingHomInvPair.instRingHomInvPairToSemiringStarRingEnd {R : Type u} [inst : CommSemiring R] [inst : 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

@RingHomInvPair.instRingHomInvPairToSemiringStarRingEnd = @RingHomInvPair.instRingHomInvPairToSemiringStarRingEnd.proof_1

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

Type (max(maxu_1u_2)u_3)

the maps preserve star
map_star : ∀ (f : F) (r : R), ↑f (star r) = star (↑f r)

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

Instances

Instances #

instance Units.instStarSemigroupUnitsToSemigroupToMonoidToDivInvMonoidInstGroupUnits {R : Type u} [inst : Monoid R] [inst : StarSemigroup R] :

StarSemigroup Rˣ

Equations

Units.instStarSemigroupUnitsToSemigroupToMonoidToDivInvMonoidInstGroupUnits = StarSemigroup.mk (_ : ∀ (x x_1 : Rˣ), star (x * x_1) = star x_1 * star x)

@[simp]

theorem Units.coe_star {R : Type u} [inst : Monoid R] [inst : StarSemigroup R] (u : Rˣ) :

↑(star u) = star ↑u

@[simp]

theorem Units.coe_star_inv {R : Type u} [inst : Monoid R] [inst : StarSemigroup R] (u : Rˣ) :

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

instance Units.instStarModuleUnitsToStarToInvolutiveStarToSemigroupToMonoidToDivInvMonoidInstGroupUnitsInstStarSemigroupUnitsToSemigroupToMonoidToDivInvMonoidInstGroupUnitsInstSMulUnits {R : Type u} [inst : Monoid R] [inst : StarSemigroup R] {A : Type u_1} [inst : Star A] [inst : SMul R A] [inst : StarModule R A] :

StarModule Rˣ A

Equations

One or more equations did not get rendered due to their size.

theorem IsUnit.star {R : Type u} [inst : Monoid R] [inst : StarSemigroup R] {a : R} :

IsUnit a → IsUnit (star a)

@[simp]

theorem isUnit_star {R : Type u} [inst : Monoid R] [inst : StarSemigroup R] {a : R} :

IsUnit (star a) ↔ IsUnit a

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

Ring.inverse (star a) = star (Ring.inverse a)

instance Invertible.star {R : Type u_1} [inst : Monoid R] [inst : StarSemigroup R] (r : R) [inst : Invertible r] :

Invertible (star r)

Equations

Invertible.star r = { invOf := star ⅟r, invOf_mul_self := (_ : star ⅟r * star r = 1), mul_invOf_self := (_ : star r * star ⅟r = 1) }

theorem star_invOf {R : Type u_1} [inst : Monoid R] [inst : StarSemigroup R] (r : R) [inst : Invertible r] [inst : Invertible (star r)] :

star ⅟r = ⅟(star r)

instance MulOpposite.instStarMulOpposite {R : Type u} [inst : Star R] :

Star Rᵐᵒᵖ

The opposite type carries the same star operation.

Equations

MulOpposite.instStarMulOpposite = { star := fun r => { unop := star r.unop } }

@[simp]

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

(star r).unop = star r.unop

@[simp]

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

{ unop := star r } = star { unop := r }

instance MulOpposite.instInvolutiveStarMulOpposite {R : Type u} [inst : InvolutiveStar R] :

InvolutiveStar Rᵐᵒᵖ

Equations

MulOpposite.instInvolutiveStarMulOpposite = InvolutiveStar.mk (_ : ∀ (r : Rᵐᵒᵖ), star (star r) = r)

instance MulOpposite.instStarSemigroupMulOppositeInstSemigroupMulOppositeToSemigroup {R : Type u} [inst : Monoid R] [inst : StarSemigroup R] :

StarSemigroup Rᵐᵒᵖ

Equations

MulOpposite.instStarSemigroupMulOppositeInstSemigroupMulOppositeToSemigroup = StarSemigroup.mk (_ : ∀ (x y : Rᵐᵒᵖ), star (x * y) = star y * star x)

instance MulOpposite.instStarAddMonoidMulOppositeInstAddMonoidMulOpposite {R : Type u} [inst : AddMonoid R] [inst : StarAddMonoid R] :

StarAddMonoid Rᵐᵒᵖ

Equations

MulOpposite.instStarAddMonoidMulOppositeInstAddMonoidMulOpposite = StarAddMonoid.mk (_ : ∀ (x y : Rᵐᵒᵖ), star (x + y) = star x + star y)

instance MulOpposite.instStarRingMulOppositeInstNonUnitalSemiringMulOppositeToNonUnitalSemiring {R : Type u} [inst : Semiring R] [inst : StarRing R] :

StarRing Rᵐᵒᵖ

Equations

MulOpposite.instStarRingMulOppositeInstNonUnitalSemiringMulOppositeToNonUnitalSemiring = StarRing.mk (_ : ∀ (x y : Rᵐᵒᵖ), star (x + y) = star x + star y)

instance StarSemigroup.toOpposite_starModule {R : Type u} [inst : CommMonoid R] [inst : StarSemigroup R] :

StarModule Rᵐᵒᵖ R

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

Equations

@StarSemigroup.toOpposite_starModule = @StarSemigroup.toOpposite_starModule.proof_1