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 ofStarOrderedRing
could be defined for this case. Note that the current definition has the advantage of not requiring a topology.
Equations
- StarMemClass.star s = { star := fun r => { val := star ↑r, property := (_ : star ↑r ∈ s) } }
Involutive condition.
star_involutive : Function.Involutive star
Typeclass for a star operation with is involutive.
Instances
star
as an equivalence when it is involutive.
Equations
- Equiv.star = Function.Involutive.toPerm star (_ : Function.Involutive star)
Any commutative monoid admits the trivial *
-structure.
See note [reducible non-instances].
Equations
- starSemigroupOfComm = StarSemigroup.mk (_ : ∀ (a b : R), a * b = b * a)
Note that since starSemigroupOfComm
is reducible, simp
can already prove this.
Equations
- One or more equations did not get rendered due to their size.
star
as a ring automorphism, for commutative R
.
Equations
- One or more equations did not get rendered due to their size.
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
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")
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
.
Alias of starRingEnd_self_apply
.
Alias of starRingEnd_self_apply
.
Any commutative semiring admits the trivial *
-structure.
See note [reducible non-instances].
addition commutes with
≤≤
characterization of non-negativity
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
Equations
- One or more equations did not get rendered due to their size.
star
commutes with scalar multiplication
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
A commutative star monoid is a star module over itself via Monoid.toMulAction
.
Instance needed to define star-linear maps over a commutative star ring (ex: conjugate-linear maps when R = ℂ).
Instances #
Equations
- One or more equations did not get rendered due to their size.
A commutative star monoid is a star module over its opposite via
Monoid.toOppositeMulAction
.