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
- toFun : α → α
- map_zero' : ZeroHom.toFun (↑s.toAddMonoidHom) 0 = 0
- map_add' : ∀ (x y : α), ZeroHom.toFun (↑s.toAddMonoidHom) (x + y) = ZeroHom.toFun (↑s.toAddMonoidHom) x + ZeroHom.toFun (↑s.toAddMonoidHom) y
- map_mul_left' : ∀ (a b : α), ZeroHom.toFun (↑s.toAddMonoidHom) (a * b) = a * ZeroHom.toFun (↑s.toAddMonoidHom) b
Commutativity of centroid homomorphims with left multiplication.
- map_mul_right' : ∀ (a b : α), ZeroHom.toFun (↑s.toAddMonoidHom) (a * b) = ZeroHom.toFun (↑s.toAddMonoidHom) a * b
Commutativity of centroid homomorphims with right multiplication.
The type of centroid homomorphisms from α
to α
.
Instances For
- coe : F → α → α
- coe_injective' : Function.Injective FunLike.coe
- map_zero : ∀ (f : F), ↑f 0 = 0
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
Centroid homomorphisms #
Helper instance for when there's too many metavariables to apply FunLike.CoeFun
directly.
Turn a centroid homomorphism into an additive monoid endomorphism.
Instances For
Copy of a CentroidHom
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Instances For
id
as a CentroidHom
.
Instances For
Composition of CentroidHom
s as a CentroidHom
.
Instances For
Negation of CentroidHom
s as a CentroidHom
.
A prime associative ring has commutative centroid.