# Documentation

Mathlib.Algebra.Hom.Centroid

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

• CentroidHomClass

## References #

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

## Tags #

centroid

structure CentroidHom (α : Type u_1) [inst : ] extends :
Type u_1
• Commutativity of centroid homomorphims with left multiplication.

map_mul_left' : ∀ (a b : α), ZeroHom.toFun (toAddMonoidHom) (a * b) = a * ZeroHom.toFun (toAddMonoidHom) b
• Commutativity 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
class CentroidHomClass (F : Type u_1) (α : outParam (Type u_2)) [inst : ] extends :
Type (maxu_1u_2)
• Commutativity of centroid homomorphims with left multiplication.

map_mul_left : ∀ (f : F) (a b : α), f (a * b) = a * f b
• Commutativity of centroid homomorphims with right multiplication.

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

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

You should extend this class when you extend CentroidHom.

Instances
instance instCoeTCCentroidHom {F : Type u_1} {α : Type u_2} [inst : ] [inst : ] :
CoeTC F ()
Equations
• One or more equations did not get rendered due to their size.

### Centroid homomorphisms #

instance CentroidHom.instCentroidHomClassCentroidHom {α : Type u_1} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance CentroidHom.instCoeFunCentroidHomForAll {α : Type u_1} [inst : ] :
CoeFun () fun x => αα

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

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

Turn a centroid homomorphism into an additive monoid endomorphism.

Equations
theorem CentroidHom.toEnd_injective {α : Type u_1} [inst : ] :
Function.Injective CentroidHom.toEnd
def CentroidHom.copy {α : Type u_1} [inst : ] (f : ) (f' : αα) (h : 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.
@[simp]
theorem CentroidHom.coe_copy {α : Type u_1} [inst : ] (f : ) (f' : αα) (h : f' = f) :
↑(CentroidHom.copy f f' h) = f'
theorem CentroidHom.copy_eq {α : Type u_1} [inst : ] (f : ) (f' : αα) (h : f' = f) :
def CentroidHom.id (α : Type u_1) [inst : ] :

id as a CentroidHom.

Equations
• One or more equations did not get rendered due to their size.
instance CentroidHom.instInhabitedCentroidHom (α : Type u_1) [inst : ] :
Equations
• = { default := }
@[simp]
theorem CentroidHom.coe_id (α : Type u_1) [inst : ] :
↑() = id
@[simp]
theorem CentroidHom.toAddMonoidHom_id (α : Type u_1) [inst : ] :
@[simp]
theorem CentroidHom.id_apply {α : Type u_1} [inst : ] (a : α) :
↑() a = a
def CentroidHom.comp {α : Type u_1} [inst : ] (g : ) (f : ) :

Composition of CentroidHoms as a CentroidHom.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem CentroidHom.coe_comp {α : Type u_1} [inst : ] (g : ) (f : ) :
↑() = g f
@[simp]
theorem CentroidHom.comp_apply {α : Type u_1} [inst : ] (g : ) (f : ) (a : α) :
↑() a = g (f a)
@[simp]
theorem CentroidHom.coe_comp_addMonoidHom {α : Type u_1} [inst : ] (g : ) (f : ) :
↑() =
@[simp]
theorem CentroidHom.comp_assoc {α : Type u_1} [inst : ] (h : ) (g : ) (f : ) :
=
@[simp]
theorem CentroidHom.comp_id {α : Type u_1} [inst : ] (f : ) :
= f
@[simp]
theorem CentroidHom.id_comp {α : Type u_1} [inst : ] (f : ) :
= f
theorem CentroidHom.cancel_right {α : Type u_1} [inst : ] {g₁ : } {g₂ : } {f : } (hf : ) :
= g₁ = g₂
theorem CentroidHom.cancel_left {α : Type u_1} [inst : ] {g : } {f₁ : } {f₂ : } (hg : ) :
= f₁ = f₂
instance CentroidHom.instZeroCentroidHom {α : Type u_1} [inst : ] :
Zero ()
Equations
• One or more equations did not get rendered due to their size.
instance CentroidHom.instOneCentroidHom {α : Type u_1} [inst : ] :
One ()
Equations
• CentroidHom.instOneCentroidHom = { one := }
instance CentroidHom.instAddCentroidHom {α : Type u_1} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance CentroidHom.instMulCentroidHom {α : Type u_1} [inst : ] :
Mul ()
Equations
• CentroidHom.instMulCentroidHom = { mul := CentroidHom.comp }
instance CentroidHom.hasNsmul {α : Type u_1} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance CentroidHom.hasNpowNat {α : Type u_1} [inst : ] :
Pow ()
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem CentroidHom.coe_zero {α : Type u_1} [inst : ] :
0 = 0
@[simp]
theorem CentroidHom.coe_one {α : Type u_1} [inst : ] :
1 = id
@[simp]
theorem CentroidHom.coe_add {α : Type u_1} [inst : ] (f : ) (g : ) :
↑(f + g) = f + g
@[simp]
theorem CentroidHom.coe_mul {α : Type u_1} [inst : ] (f : ) (g : ) :
↑(f * g) = f g
@[simp]
theorem CentroidHom.coe_nsmul {α : Type u_1} [inst : ] (f : ) (n : ) :
↑(n f) = n f
@[simp]
theorem CentroidHom.zero_apply {α : Type u_1} [inst : ] (a : α) :
0 a = 0
@[simp]
theorem CentroidHom.one_apply {α : Type u_1} [inst : ] (a : α) :
1 a = a
@[simp]
theorem CentroidHom.add_apply {α : Type u_1} [inst : ] (f : ) (g : ) (a : α) :
↑(f + g) a = f a + g a
@[simp]
theorem CentroidHom.mul_apply {α : Type u_1} [inst : ] (f : ) (g : ) (a : α) :
↑(f * g) a = f (g a)
@[simp]
theorem CentroidHom.nsmul_apply {α : Type u_1} [inst : ] (f : ) (n : ) (a : α) :
↑(n f) a = n f a
@[simp]
theorem CentroidHom.toEnd_zero {α : Type u_1} [inst : ] :
@[simp]
theorem CentroidHom.toEnd_add {α : Type u_1} [inst : ] (x : ) (y : ) :
theorem CentroidHom.toEnd_nsmul {α : Type u_1} [inst : ] (x : ) (n : ) :
instance CentroidHom.instAddCommMonoidCentroidHom {α : Type u_1} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance CentroidHom.instNatCastCentroidHom {α : Type u_1} [inst : ] :
Equations
• CentroidHom.instNatCastCentroidHom = { natCast := fun n => n 1 }
@[simp]
theorem CentroidHom.coe_nat_cast {α : Type u_1} [inst : ] (n : ) :
n = ↑()
theorem CentroidHom.nat_cast_apply {α : Type u_1} [inst : ] (n : ) (m : α) :
n m = n m
@[simp]
theorem CentroidHom.toEnd_one {α : Type u_1} [inst : ] :
@[simp]
theorem CentroidHom.toEnd_mul {α : Type u_1} [inst : ] (x : ) (y : ) :
@[simp]
theorem CentroidHom.toEnd_pow {α : Type u_1} [inst : ] (x : ) (n : ) :
@[simp]
theorem CentroidHom.toEnd_nat_cast {α : Type u_1} [inst : ] (n : ) :
= n
instance CentroidHom.instSemiringCentroidHom {α : Type u_1} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
theorem CentroidHom.comp_mul_comm {α : Type u_1} [inst : ] (T : ) (S : ) (a : α) (b : α) :
(T S) (a * b) = (S T) (a * b)

Negation of CentroidHoms 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.
instance CentroidHom.hasZsmul {α : Type u_1} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
Equations
• CentroidHom.instIntCastCentroidHomToNonUnitalNonAssocSemiring = { intCast := fun z => z 1 }
@[simp]
theorem CentroidHom.coe_int_cast {α : Type u_1} [inst : ] (z : ) :
z = ↑()
theorem CentroidHom.int_cast_apply {α : Type u_1} [inst : ] (z : ) (m : α) :
z m = z m
@[simp]
theorem CentroidHom.toEnd_neg {α : Type u_1} [inst : ] (x : ) :
@[simp]
theorem CentroidHom.toEnd_sub {α : Type u_1} [inst : ] (x : ) (y : ) :
theorem CentroidHom.toEnd_zsmul {α : Type u_1} [inst : ] (x : ) (n : ) :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem CentroidHom.coe_neg {α : Type u_1} [inst : ] (f : ) :
↑(-f) = -f
@[simp]
theorem CentroidHom.coe_sub {α : Type u_1} [inst : ] (f : ) (g : ) :
↑(f - g) = f - g
@[simp]
theorem CentroidHom.neg_apply {α : Type u_1} [inst : ] (f : ) (a : α) :
↑(-f) a = -f a
@[simp]
theorem CentroidHom.sub_apply {α : Type u_1} [inst : ] (f : ) (g : ) (a : α) :
↑(f - g) a = f a - g a
@[simp]
theorem CentroidHom.toEnd_int_cast {α : Type u_1} [inst : ] (z : ) :
= z
Equations
• One or more equations did not get rendered due to their size.
def CentroidHom.commRing {α : Type u_1} [inst : ] (h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 b = 0) :

A prime associative ring has commutative centroid.

Equations
• = let src := CentroidHom.instRingCentroidHomToNonUnitalNonAssocSemiring; CommRing.mk (_ : ∀ (f g : ), f * g = g * f)