# 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 DFunLike 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 #

• CentroidHomClass

## References #

• [Jacobson, Structure of Rings][Jacobson1956]
• [McCrimmon, A taste of Jordan algebras][mccrimmon2004]

## Tags #

centroid

structure CentroidHom (α : Type u_6) extends :
Type u_6

The type of centroid homomorphisms from α to α.

• toFun : αα
• map_zero' : (self.toAddMonoidHom).toFun 0 = 0
• map_mul_left' : ∀ (a b : α), (self.toAddMonoidHom).toFun (a * b) = a * (self.toAddMonoidHom).toFun b

Commutativity of centroid homomorphims with left multiplication.

• map_mul_right' : ∀ (a b : α), (self.toAddMonoidHom).toFun (a * b) = (self.toAddMonoidHom).toFun a * b

Commutativity of centroid homomorphims with right multiplication.

Instances For
theorem CentroidHom.map_mul_left' {α : Type u_6} (self : ) (a : α) (b : α) :

Commutativity of centroid homomorphims with left multiplication.

theorem CentroidHom.map_mul_right' {α : Type u_6} (self : ) (a : α) (b : α) :

Commutativity of centroid homomorphims with right multiplication.

class CentroidHomClass (F : Type u_6) (α : Type u_7) [FunLike F α α] extends :

CentroidHomClass F α states that F is a type of centroid homomorphisms.

You should extend this class when you extend CentroidHom.

• map_add : ∀ (f : F) (x y : α), f (x + y) = f x + f y
• map_zero : ∀ (f : F), f 0 = 0
• map_mul_left : ∀ (f : F) (a b : α), f (a * b) = a * f b

Commutativity of centroid homomorphims with left multiplication.

• map_mul_right : ∀ (f : F) (a b : α), f (a * b) = f a * b

Commutativity of centroid homomorphims with right multiplication.

Instances
theorem CentroidHomClass.map_mul_left {F : Type u_6} {α : Type u_7} [FunLike F α α] [self : ] (f : F) (a : α) (b : α) :
f (a * b) = a * f b

Commutativity of centroid homomorphims with left multiplication.

theorem CentroidHomClass.map_mul_right {F : Type u_6} {α : Type u_7} [FunLike F α α] [self : ] (f : F) (a : α) (b : α) :
f (a * b) = f a * b

Commutativity of centroid homomorphims with right multiplication.

instance instCoeTCCentroidHomOfCentroidHomClass {F : Type u_1} {α : Type u_5} [FunLike F α α] [] :
CoeTC F ()
Equations
• instCoeTCCentroidHomOfCentroidHomClass = { coe := fun (f : F) => let __src := f; { toFun := f, map_zero' := , map_add' := , map_mul_left' := , map_mul_right' := } }

### Centroid homomorphisms #

instance CentroidHom.instFunLike {α : Type u_5} :
FunLike () α α
Equations
• CentroidHom.instFunLike = { coe := fun (f : ) => (f.toAddMonoidHom).toFun, coe_injective' := }
Equations
• =
instance CentroidHom.instCoeFunForall {α : Type u_5} :
CoeFun () fun (x : ) => αα

Helper instance for when there's too many metavariables to apply DFunLike.CoeFun directly.

Equations
theorem CentroidHom.toFun_eq_coe {α : Type u_5} {f : } :
theorem CentroidHom.ext {α : Type u_5} {f : } {g : } (h : ∀ (a : α), f a = g a) :
f = g
@[simp]
theorem CentroidHom.coe_toAddMonoidHom {α : Type u_5} (f : ) :
f = f
@[simp]
theorem CentroidHom.toAddMonoidHom_eq_coe {α : Type u_5} (f : ) :
theorem CentroidHom.coe_toAddMonoidHom_injective {α : Type u_5} :
def CentroidHom.toEnd {α : Type u_5} (f : ) :

Turn a centroid homomorphism into an additive monoid endomorphism.

Equations
• f.toEnd = f
Instances For
theorem CentroidHom.toEnd_injective {α : Type u_5} :
Function.Injective CentroidHom.toEnd
def CentroidHom.copy {α : Type u_5} (f : ) (f' : αα) (h : f' = f) :

Copy of a CentroidHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations
• f.copy f' h = let __src := f.copy f' h; { toFun := f', map_zero' := , map_add' := , map_mul_left' := , map_mul_right' := }
Instances For
@[simp]
theorem CentroidHom.coe_copy {α : Type u_5} (f : ) (f' : αα) (h : f' = f) :
(f.copy f' h) = f'
theorem CentroidHom.copy_eq {α : Type u_5} (f : ) (f' : αα) (h : f' = f) :
f.copy f' h = f
def CentroidHom.id (α : Type u_5) :

id as a CentroidHom.

Equations
• = let __src := ; { toAddMonoidHom := __src, map_mul_left' := , map_mul_right' := }
Instances For
instance CentroidHom.instInhabited (α : Type u_5) :
Equations
• = { default := }
@[simp]
theorem CentroidHom.coe_id (α : Type u_5) :
() = id
@[simp]
theorem CentroidHom.toAddMonoidHom_id (α : Type u_5) :
@[simp]
theorem CentroidHom.id_apply {α : Type u_5} (a : α) :
() a = a
def CentroidHom.comp {α : Type u_5} (g : ) (f : ) :

Composition of CentroidHoms as a CentroidHom.

Equations
• g.comp f = let __src := g.comp f.toAddMonoidHom; { toAddMonoidHom := __src, map_mul_left' := , map_mul_right' := }
Instances For
@[simp]
theorem CentroidHom.coe_comp {α : Type u_5} (g : ) (f : ) :
(g.comp f) = g f
@[simp]
theorem CentroidHom.comp_apply {α : Type u_5} (g : ) (f : ) (a : α) :
(g.comp f) a = g (f a)
@[simp]
theorem CentroidHom.coe_comp_addMonoidHom {α : Type u_5} (g : ) (f : ) :
(g.comp f) = (g).comp f
@[simp]
theorem CentroidHom.comp_assoc {α : Type u_5} (h : ) (g : ) (f : ) :
(h.comp g).comp f = h.comp (g.comp f)
@[simp]
theorem CentroidHom.comp_id {α : Type u_5} (f : ) :
f.comp () = f
@[simp]
theorem CentroidHom.id_comp {α : Type u_5} (f : ) :
().comp f = f
@[simp]
theorem CentroidHom.cancel_right {α : Type u_5} {g₁ : } {g₂ : } {f : } (hf : ) :
g₁.comp f = g₂.comp f g₁ = g₂
@[simp]
theorem CentroidHom.cancel_left {α : Type u_5} {g : } {f₁ : } {f₂ : } (hg : ) :
g.comp f₁ = g.comp f₂ f₁ = f₂
instance CentroidHom.instZero {α : Type u_5} :
Zero ()
Equations
• CentroidHom.instZero = { zero := let __src := 0; { toAddMonoidHom := __src, map_mul_left' := , map_mul_right' := } }
instance CentroidHom.instOne {α : Type u_5} :
One ()
Equations
• CentroidHom.instOne = { one := }
instance CentroidHom.instAdd {α : Type u_5} :
Equations
• CentroidHom.instAdd = { add := fun (f g : ) => let __src := f + g; { toAddMonoidHom := __src, map_mul_left' := , map_mul_right' := } }
instance CentroidHom.instMul {α : Type u_5} :
Mul ()
Equations
• CentroidHom.instMul = { mul := CentroidHom.comp }
instance CentroidHom.instSMul {M : Type u_2} {α : Type u_5} [] [] [] [] :
SMul M ()
Equations
• CentroidHom.instSMul = { smul := fun (n : M) (f : ) => let __src := n f; { toAddMonoidHom := __src, map_mul_left' := , map_mul_right' := } }
instance CentroidHom.instIsScalarTower {M : Type u_2} {N : Type u_3} {α : Type u_5} [] [] [] [] [] [] [] [] [SMul M N] [] :
Equations
• =
instance CentroidHom.instSMulCommClass {M : Type u_2} {N : Type u_3} {α : Type u_5} [] [] [] [] [] [] [] [] [] :
Equations
• =
instance CentroidHom.instIsCentralScalar {M : Type u_2} {α : Type u_5} [] [] [] [] [] [] :
Equations
• =
instance CentroidHom.isScalarTowerRight {M : Type u_2} {α : Type u_5} [] [] [] [] :
Equations
• =
instance CentroidHom.hasNPowNat {α : Type u_5} :
Pow ()
Equations
• CentroidHom.hasNPowNat = { pow := fun (f : ) (n : ) => { toAddMonoidHom := f.toEnd ^ n, map_mul_left' := , map_mul_right' := } }
@[simp]
theorem CentroidHom.coe_zero {α : Type u_5} :
0 = 0
@[simp]
theorem CentroidHom.coe_one {α : Type u_5} :
1 = id
@[simp]
theorem CentroidHom.coe_add {α : Type u_5} (f : ) (g : ) :
(f + g) = f + g
@[simp]
theorem CentroidHom.coe_mul {α : Type u_5} (f : ) (g : ) :
(f * g) = f g
@[simp]
theorem CentroidHom.coe_smul {M : Type u_2} {α : Type u_5} [] [] [] [] (n : M) (f : ) :
(n f) = n f
@[simp]
theorem CentroidHom.zero_apply {α : Type u_5} (a : α) :
0 a = 0
@[simp]
theorem CentroidHom.one_apply {α : Type u_5} (a : α) :
1 a = a
@[simp]
theorem CentroidHom.add_apply {α : Type u_5} (f : ) (g : ) (a : α) :
(f + g) a = f a + g a
@[simp]
theorem CentroidHom.mul_apply {α : Type u_5} (f : ) (g : ) (a : α) :
(f * g) a = f (g a)
@[simp]
theorem CentroidHom.smul_apply {M : Type u_2} {α : Type u_5} [] [] [] [] (n : M) (f : ) (a : α) :
(n f) a = n f a
@[simp]
theorem CentroidHom.toEnd_zero {α : Type u_5} :
@[simp]
theorem CentroidHom.toEnd_add {α : Type u_5} (x : ) (y : ) :
(x + y).toEnd = x.toEnd + y.toEnd
theorem CentroidHom.toEnd_smul {M : Type u_2} {α : Type u_5} [] [] [] [] (m : M) (x : ) :
(m x).toEnd = m x.toEnd
instance CentroidHom.instAddCommMonoid {α : Type u_5} :
Equations
instance CentroidHom.instNatCast {α : Type u_5} :
Equations
• CentroidHom.instNatCast = { natCast := fun (n : ) => n 1 }
@[simp]
theorem CentroidHom.coe_natCast {α : Type u_5} (n : ) :
n = n ()
theorem CentroidHom.natCast_apply {α : Type u_5} (n : ) (m : α) :
n m = n m
@[simp]
theorem CentroidHom.toEnd_one {α : Type u_5} :
@[simp]
theorem CentroidHom.toEnd_mul {α : Type u_5} (x : ) (y : ) :
(x * y).toEnd = x.toEnd * y.toEnd
@[simp]
theorem CentroidHom.toEnd_pow {α : Type u_5} (x : ) (n : ) :
(x ^ n).toEnd = x.toEnd ^ n
@[simp]
theorem CentroidHom.toEnd_natCast {α : Type u_5} (n : ) :
(n).toEnd = n
instance CentroidHom.instSemiring {α : Type u_5} :
Equations
@[simp]
theorem CentroidHom.toEndRingHom_apply (α : Type u_5) (f : ) :
= f.toEnd

CentroidHom.toEnd as a RingHom.

Equations
• = { toFun := CentroidHom.toEnd, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
theorem CentroidHom.comp_mul_comm {α : Type u_5} (T : ) (S : ) (a : α) (b : α) :
(T S) (a * b) = (S T) (a * b)
instance CentroidHom.instDistribMulAction {M : Type u_2} {α : Type u_5} [] [] [] [] :
Equations
instance CentroidHom.instModule {R : Type u_4} {α : Type u_5} [] [Module R α] [] [] :
Module R ()
Equations

The following instances show that α is a non-unital and non-associative algebra over CentroidHom α.

instance CentroidHom.applyModule {α : Type u_5} :
Module () α

The tautological action by CentroidHom α on α.

This generalizes Function.End.applyMulAction.

Equations
• CentroidHom.applyModule =
@[simp]
theorem CentroidHom.smul_def {α : Type u_5} (T : ) (a : α) :
T a = T a
instance CentroidHom.instSMulCommClass_1 {α : Type u_5} :
SMulCommClass () α α
Equations
• =
instance CentroidHom.instSMulCommClass_2 {α : Type u_5} :
SMulCommClass α () α
Equations
• =
instance CentroidHom.instIsScalarTower_1 {α : Type u_5} :
IsScalarTower () α α
Equations
• =

Let α be an algebra over R, such that the canonical ring homomorphism of R into CentroidHom α lies in the center of CentroidHom α. Then CentroidHom α is an algebra over R

@[simp]
theorem Module.toCentroidHom_apply_toFun {α : Type u_5} {R : Type u_6} [] [Module R α] [] [] (x : R) (a : α) :
(Module.toCentroidHom x) a = x a
def Module.toCentroidHom {α : Type u_5} {R : Type u_6} [] [Module R α] [] [] :

The natural ring homomorphism from R into CentroidHom α.

This is a stronger version of Module.toAddMonoidEnd.

Equations
• Module.toCentroidHom = RingHom.smulOneHom
Instances For
theorem CentroidHom.centroid_eq_centralizer_mulLeftRight {α : Type u_5} :

The canonical homomorphism from the center into the centroid

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CentroidHom.centerToCentroid_apply {α : Type u_5} (z : ) (a : α) :
(CentroidHom.centerToCentroid z) a = z * a
theorem NonUnitalNonAssocSemiring.mem_center_iff {α : Type u_5} (a : α) :
theorem NonUnitalNonAssocCommSemiring.mem_center_iff {α : Type u_5} (a : α) :

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
instance CentroidHom.instNeg {α : Type u_5} :
Neg ()

Negation of CentroidHoms as a CentroidHom.

Equations
• CentroidHom.instNeg = { neg := fun (f : ) => let __src := -f; { toAddMonoidHom := __src, map_mul_left' := , map_mul_right' := } }
instance CentroidHom.instSub {α : Type u_5} :
Sub ()
Equations
• CentroidHom.instSub = { sub := fun (f g : ) => let __src := f - g; { toAddMonoidHom := __src, map_mul_left' := , map_mul_right' := } }
instance CentroidHom.instIntCast {α : Type u_5} :
Equations
• CentroidHom.instIntCast = { intCast := fun (z : ) => z 1 }
@[simp]
theorem CentroidHom.coe_intCast {α : Type u_5} (z : ) :
z = z ()
theorem CentroidHom.intCast_apply {α : Type u_5} (z : ) (m : α) :
z m = z m
@[simp]
theorem CentroidHom.toEnd_neg {α : Type u_5} (x : ) :
(-x).toEnd = -x.toEnd
@[simp]
theorem CentroidHom.toEnd_sub {α : Type u_5} (x : ) (y : ) :
(x - y).toEnd = x.toEnd - y.toEnd
instance CentroidHom.instAddCommGroup {α : Type u_5} :
Equations
@[simp]
theorem CentroidHom.coe_neg {α : Type u_5} (f : ) :
(-f) = -f
@[simp]
theorem CentroidHom.coe_sub {α : Type u_5} (f : ) (g : ) :
(f - g) = f - g
@[simp]
theorem CentroidHom.neg_apply {α : Type u_5} (f : ) (a : α) :
(-f) a = -f a
@[simp]
theorem CentroidHom.sub_apply {α : Type u_5} (f : ) (g : ) (a : α) :
(f - g) a = f a - g a
@[simp]
theorem CentroidHom.toEnd_intCast {α : Type u_5} (z : ) :
(z).toEnd = z
instance CentroidHom.instRing {α : Type u_5} :
Ring ()
Equations
@[reducible, inline]
abbrev CentroidHom.commRing {α : Type u_5} [] (h : ∀ (a b : α), (∀ (r : α), a * r * b = 0)a = 0 b = 0) :

A prime associative ring has commutative centroid.

Equations
• = let __src := CentroidHom.instRing;
Instances For