# 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_3) extends :
Type u_3
• toFun : αα
• map_zero' : ZeroHom.toFun (s.toAddMonoidHom) 0 = 0
• 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
class CentroidHomClass (F : Type u_3) (α : outParam (Type u_4)) extends :
Type (max u_3 u_4)
• coe : Fαα
• coe_injective' : Function.Injective FunLike.coe
• 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.

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} [] :
CoeTC F ()

### Centroid homomorphisms #

instance CentroidHom.instCoeFunCentroidHomForAll {α : Type u_2} :
CoeFun () fun x => αα

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

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

Turn a centroid homomorphism into an additive monoid endomorphism.

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

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

Instances For
@[simp]
theorem CentroidHom.coe_copy {α : Type u_2} (f : ) (f' : αα) (h : f' = f) :
↑(CentroidHom.copy f f' h) = f'
theorem CentroidHom.copy_eq {α : Type u_2} (f : ) (f' : αα) (h : f' = f) :
def CentroidHom.id (α : Type u_2) :

id as a CentroidHom.

Instances For
@[simp]
theorem CentroidHom.coe_id (α : Type u_2) :
↑() = id
@[simp]
theorem CentroidHom.toAddMonoidHom_id (α : Type u_2) :
@[simp]
theorem CentroidHom.id_apply {α : Type u_2} (a : α) :
↑() a = a
def CentroidHom.comp {α : Type u_2} (g : ) (f : ) :

Composition of CentroidHoms as a CentroidHom.

Instances For
@[simp]
theorem CentroidHom.coe_comp {α : Type u_2} (g : ) (f : ) :
↑() = g f
@[simp]
theorem CentroidHom.comp_apply {α : Type u_2} (g : ) (f : ) (a : α) :
↑() a = g (f a)
@[simp]
theorem CentroidHom.coe_comp_addMonoidHom {α : Type u_2} (g : ) (f : ) :
↑() =
@[simp]
theorem CentroidHom.comp_assoc {α : Type u_2} (h : ) (g : ) (f : ) :
=
@[simp]
theorem CentroidHom.comp_id {α : Type u_2} (f : ) :
= f
@[simp]
theorem CentroidHom.id_comp {α : Type u_2} (f : ) :
= f
@[simp]
theorem CentroidHom.cancel_right {α : Type u_2} {g₁ : } {g₂ : } {f : } (hf : ) :
= g₁ = g₂
@[simp]
theorem CentroidHom.cancel_left {α : Type u_2} {g : } {f₁ : } {f₂ : } (hg : ) :
= f₁ = f₂
instance CentroidHom.hasNsmul {α : Type u_2} :
instance CentroidHom.hasNpowNat {α : Type u_2} :
Pow ()
@[simp]
theorem CentroidHom.coe_zero {α : Type u_2} :
0 = 0
@[simp]
theorem CentroidHom.coe_one {α : Type u_2} :
1 = id
@[simp]
theorem CentroidHom.coe_add {α : Type u_2} (f : ) (g : ) :
↑(f + g) = f + g
@[simp]
theorem CentroidHom.coe_mul {α : Type u_2} (f : ) (g : ) :
↑(f * g) = f g
@[simp]
theorem CentroidHom.coe_nsmul {α : Type u_2} (f : ) (n : ) :
↑(n f) = n f
@[simp]
theorem CentroidHom.zero_apply {α : Type u_2} (a : α) :
0 a = 0
@[simp]
theorem CentroidHom.one_apply {α : Type u_2} (a : α) :
1 a = a
@[simp]
theorem CentroidHom.add_apply {α : Type u_2} (f : ) (g : ) (a : α) :
↑(f + g) a = f a + g a
@[simp]
theorem CentroidHom.mul_apply {α : Type u_2} (f : ) (g : ) (a : α) :
↑(f * g) a = f (g a)
@[simp]
theorem CentroidHom.nsmul_apply {α : Type u_2} (f : ) (n : ) (a : α) :
↑(n f) a = n f a
@[simp]
theorem CentroidHom.toEnd_zero {α : Type u_2} :
@[simp]
theorem CentroidHom.toEnd_add {α : Type u_2} (x : ) (y : ) :
theorem CentroidHom.toEnd_nsmul {α : Type u_2} (x : ) (n : ) :
@[simp]
theorem CentroidHom.coe_nat_cast {α : Type u_2} (n : ) :
n = ↑()
theorem CentroidHom.nat_cast_apply {α : Type u_2} (n : ) (m : α) :
n m = n m
@[simp]
theorem CentroidHom.toEnd_one {α : Type u_2} :
@[simp]
theorem CentroidHom.toEnd_mul {α : Type u_2} (x : ) (y : ) :
@[simp]
theorem CentroidHom.toEnd_pow {α : Type u_2} (x : ) (n : ) :
@[simp]
theorem CentroidHom.toEnd_nat_cast {α : Type u_2} (n : ) :
= n
theorem CentroidHom.comp_mul_comm {α : Type u_2} (T : ) (S : ) (a : α) (b : α) :
(T S) (a * b) = (S T) (a * b)

Negation of CentroidHoms as a CentroidHom.

instance CentroidHom.hasZsmul {α : Type u_2} :
@[simp]
theorem CentroidHom.coe_int_cast {α : Type u_2} (z : ) :
z = ↑()
theorem CentroidHom.int_cast_apply {α : Type u_2} (z : ) (m : α) :
z m = z m
@[simp]
theorem CentroidHom.toEnd_neg {α : Type u_2} (x : ) :
@[simp]
theorem CentroidHom.toEnd_sub {α : Type u_2} (x : ) (y : ) :
theorem CentroidHom.toEnd_zsmul {α : Type u_2} (x : ) (n : ) :
@[simp]
theorem CentroidHom.coe_neg {α : Type u_2} (f : ) :
↑(-f) = -f
@[simp]
theorem CentroidHom.coe_sub {α : Type u_2} (f : ) (g : ) :
↑(f - g) = f - g
@[simp]
theorem CentroidHom.neg_apply {α : Type u_2} (f : ) (a : α) :
↑(-f) a = -f a
@[simp]
theorem CentroidHom.sub_apply {α : Type u_2} (f : ) (g : ) (a : α) :
↑(f - g) a = f a - g a
@[simp]
theorem CentroidHom.toEnd_int_cast {α : Type u_2} (z : ) :
= z
instance CentroidHom.instRing {α : Type u_2} :
Ring ()
@[reducible]
def CentroidHom.commRing {α : Type u_2} [] (h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 b = 0) :

A prime associative ring has commutative centroid.

Instances For