Centroid homomorphisms #
Let A
be a (non unital, non associative) algebra. The centroid of A
is the set of linear maps
T
on A
such that T
commutes with left and right multiplication, that is to say, for all a
and b
in A
,
$$
T(ab) = (Ta)b, T(ab) = a(Tb).
$$
In mathlib we call elements of the centroid "centroid homomorphisms" (CentroidHom
) in keeping
with AddMonoidHom
etc.
We use the FunLike
design, so each type of morphisms has a companion typeclass which is meant to
be satisfied by itself and all stricter types.
Types of morphisms #
CentroidHom
: Maps which preserve left and right multiplication.
Typeclasses #
References #
- [Jacobson, Structure of Rings][Jacobson1956]
- [McCrimmon, A taste of Jordan algebras][mccrimmon2004]
Tags #
centroid
Commutativity of centroid homomorphims with left multiplication.
map_mul_left' : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom) (a * b) = a * ZeroHom.toFun (↑toAddMonoidHom) bCommutativity of centroid homomorphims with right multiplication.
map_mul_right' : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom) (a * b) = ZeroHom.toFun (↑toAddMonoidHom) a * b
The type of centroid homomorphisms from α
to α
.
Instances For
Commutativity of centroid homomorphims with left multiplication.
Commutativity of centroid homomorphims with right multiplication.
CentroidHomClass F α
states that F
is a type of centroid homomorphisms.
You should extend this class when you extend CentroidHom
.
Instances
Equations
- One or more equations did not get rendered due to their size.
Centroid homomorphisms #
Equations
- One or more equations did not get rendered due to their size.
Helper instance for when there's too many metavariables to apply FunLike.CoeFun
directly.
Equations
- CentroidHom.instCoeFunCentroidHomForAll = inferInstanceAs (CoeFun (CentroidHom α) fun x => α → α)
Turn a centroid homomorphism into an additive monoid endomorphism.
Equations
- CentroidHom.toEnd f = ↑f
Copy of a CentroidHom
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Equations
- One or more equations did not get rendered due to their size.
id
as a CentroidHom
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- CentroidHom.instInhabitedCentroidHom α = { default := CentroidHom.id α }
Composition of CentroidHom
s as a CentroidHom
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- CentroidHom.instOneCentroidHom = { one := CentroidHom.id α }
Equations
- One or more equations did not get rendered due to their size.
Equations
- CentroidHom.instMulCentroidHom = { mul := CentroidHom.comp }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Negation of CentroidHom
s as a CentroidHom
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
A prime associative ring has commutative centroid.
Equations
- CentroidHom.commRing h = let src := CentroidHom.instRingCentroidHomToNonUnitalNonAssocSemiring; CommRing.mk (_ : ∀ (f g : CentroidHom α), f * g = g * f)