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
The type of centroid homomorphisms from α
to α
.
- 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.
Instances For
CentroidHomClass F α
states that F
is a type of centroid homomorphisms.
You should extend this class when you extend CentroidHom
.
- 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.
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 : CentroidHom α) => α → α)
Turn a centroid homomorphism into an additive monoid endomorphism.
Equations
- CentroidHom.toEnd f = ↑f
Instances For
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.
Instances For
id
as a CentroidHom
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
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
- (_ : IsScalarTower M N (CentroidHom α)) = (_ : IsScalarTower M N (CentroidHom α))
Equations
- (_ : SMulCommClass M N (CentroidHom α)) = (_ : SMulCommClass M N (CentroidHom α))
Equations
- (_ : IsCentralScalar M (CentroidHom α)) = (_ : IsCentralScalar M (CentroidHom α))
Equations
- (_ : IsScalarTower M (CentroidHom α) (CentroidHom α)) = (_ : IsScalarTower M (CentroidHom α) (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.
CentroidHom.toEnd
as a RingHom
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
The canonical homomorphism from the center into the centroid
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical isomorphism from the center of a (non-associative) semiring onto its centroid.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
A prime associative ring has commutative centroid.
Equations
- CentroidHom.commRing h = let src := CentroidHom.instRing; CommRing.mk (_ : ∀ (f g : CentroidHom α), f * g = g * f)