# mathlib3documentation

algebra.hom.centroid

# Centroid homomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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" (centroid_hom) in keeping with add_monoid_hom etc.

We use the fun_like 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 #

• centroid_hom: Maps which preserve left and right multiplication.

## Typeclasses #

• centroid_hom_class

## Tags #

centroid

structure centroid_hom (α : Type u_3)  :
Type u_3

The type of centroid homomorphisms from α to α.

Instances for centroid_hom
@[nolint]
def centroid_hom.to_add_monoid_hom {α : Type u_3} (self : centroid_hom α) :
α →+ α
@[instance]
def centroid_hom_class.to_add_monoid_hom_class (F : Type u_3) (α : out_param (Type u_4)) [self : α] :
α
@[class]
structure centroid_hom_class (F : Type u_3) (α : out_param (Type u_4))  :
Type (max u_3 u_4)
• coe : F Π (a : α), (λ (_x : α), α) a
• coe_injective' :
• 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
• map_mul_right : (f : F) (a b : α), f (a * b) = f a * b

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

You should extend this class when you extend centroid_hom.

Instances of this typeclass
Instances of other typeclasses for centroid_hom_class
• centroid_hom_class.has_sizeof_inst
@[protected, instance]
def centroid_hom.has_coe_t {F : Type u_1} {α : Type u_2} [ α] :
Equations

### Centroid homomorphisms #

@[protected, instance]
Equations
@[protected, instance]
def centroid_hom.has_coe_to_fun {α : Type u_2}  :
(λ (_x : , α α)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[simp]
theorem centroid_hom.to_fun_eq_coe {α : Type u_2} {f : centroid_hom α} :
@[ext]
theorem centroid_hom.ext {α : Type u_2} {f g : centroid_hom α} (h : (a : α), f a = g a) :
f = g
@[simp, norm_cast]
theorem centroid_hom.coe_to_add_monoid_hom {α : Type u_2} (f : centroid_hom α) :
@[simp]
def centroid_hom.to_End {α : Type u_2} (f : centroid_hom α) :

Turn a centroid homomorphism into an additive monoid endomorphism.

Equations
@[protected]
def centroid_hom.copy {α : Type u_2} (f : centroid_hom α) (f' : α α) (h : f' = f) :

Copy of a centroid_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem centroid_hom.coe_copy {α : Type u_2} (f : centroid_hom α) (f' : α α) (h : f' = f) :
(f.copy f' h) = f'
theorem centroid_hom.copy_eq {α : Type u_2} (f : centroid_hom α) (f' : α α) (h : f' = f) :
f.copy f' h = f
@[protected]
def centroid_hom.id (α : Type u_2)  :

id as a centroid_hom.

Equations
@[protected, instance]
def centroid_hom.inhabited (α : Type u_2)  :
Equations
@[simp, norm_cast]
theorem centroid_hom.coe_id (α : Type u_2)  :
@[simp, norm_cast]
@[simp]
theorem centroid_hom.id_apply {α : Type u_2} (a : α) :
a = a
def centroid_hom.comp {α : Type u_2} (g f : centroid_hom α) :

Composition of centroid_homs as a centroid_hom.

Equations
@[simp, norm_cast]
theorem centroid_hom.coe_comp {α : Type u_2} (g f : centroid_hom α) :
(g.comp f) = g f
@[simp]
theorem centroid_hom.comp_apply {α : Type u_2} (g f : centroid_hom α) (a : α) :
(g.comp f) a = g (f a)
@[simp, norm_cast]
theorem centroid_hom.coe_comp_add_monoid_hom {α : Type u_2} (g f : centroid_hom α) :
(g.comp f) = g.comp f
@[simp]
theorem centroid_hom.comp_assoc {α : Type u_2} (h g f : centroid_hom α) :
(h.comp g).comp f = h.comp (g.comp f)
@[simp]
theorem centroid_hom.comp_id {α : Type u_2} (f : centroid_hom α) :
f.comp = f
@[simp]
theorem centroid_hom.id_comp {α : Type u_2} (f : centroid_hom α) :
.comp f = f
theorem centroid_hom.cancel_right {α : Type u_2} {g₁ g₂ f : centroid_hom α} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem centroid_hom.cancel_left {α : Type u_2} {g f₁ f₂ : centroid_hom α} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
@[protected, instance]
def centroid_hom.has_zero {α : Type u_2}  :
Equations
@[protected, instance]
def centroid_hom.has_one {α : Type u_2}  :
Equations
@[protected, instance]
def centroid_hom.has_add {α : Type u_2}  :
Equations
@[protected, instance]
def centroid_hom.has_mul {α : Type u_2}  :
Equations
@[protected, instance]
def centroid_hom.has_nsmul {α : Type u_2}  :
Equations
@[protected, instance]
def centroid_hom.has_npow_nat {α : Type u_2}  :
Equations
@[simp, norm_cast]
theorem centroid_hom.coe_zero {α : Type u_2}  :
0 = 0
@[simp, norm_cast]
theorem centroid_hom.coe_one {α : Type u_2}  :
@[simp, norm_cast]
theorem centroid_hom.coe_add {α : Type u_2} (f g : centroid_hom α) :
(f + g) = f + g
@[simp, norm_cast]
theorem centroid_hom.coe_mul {α : Type u_2} (f g : centroid_hom α) :
(f * g) = f g
@[simp, norm_cast, nolint]
theorem centroid_hom.coe_nsmul {α : Type u_2} (f : centroid_hom α) (n : ) :
(n f) = n f
@[simp]
theorem centroid_hom.zero_apply {α : Type u_2} (a : α) :
0 a = 0
@[simp]
theorem centroid_hom.one_apply {α : Type u_2} (a : α) :
1 a = a
@[simp]
theorem centroid_hom.add_apply {α : Type u_2} (f g : centroid_hom α) (a : α) :
(f + g) a = f a + g a
@[simp]
theorem centroid_hom.mul_apply {α : Type u_2} (f g : centroid_hom α) (a : α) :
(f * g) a = f (g a)
@[simp, nolint]
theorem centroid_hom.nsmul_apply {α : Type u_2} (f : centroid_hom α) (n : ) (a : α) :
(n f) a = n f a
@[simp]
theorem centroid_hom.to_End_zero {α : Type u_2}  :
0.to_End = 0
@[simp]
theorem centroid_hom.to_End_add {α : Type u_2} (x y : centroid_hom α) :
(x + y).to_End = x.to_End + y.to_End
theorem centroid_hom.to_End_nsmul {α : Type u_2} (x : centroid_hom α) (n : ) :
(n x).to_End = n x.to_End
@[protected, instance]
def centroid_hom.add_comm_monoid {α : Type u_2}  :
Equations
@[protected, instance]
def centroid_hom.has_nat_cast {α : Type u_2}  :
Equations
@[simp, norm_cast]
theorem centroid_hom.coe_nat_cast {α : Type u_2} (n : ) :
theorem centroid_hom.nat_cast_apply {α : Type u_2} (n : ) (m : α) :
n m = n m
@[simp]
theorem centroid_hom.to_End_one {α : Type u_2}  :
1.to_End = 1
@[simp]
theorem centroid_hom.to_End_mul {α : Type u_2} (x y : centroid_hom α) :
(x * y).to_End = x.to_End * y.to_End
@[simp]
theorem centroid_hom.to_End_pow {α : Type u_2} (x : centroid_hom α) (n : ) :
(x ^ n).to_End = x.to_End ^ n
@[simp, norm_cast]
theorem centroid_hom.to_End_nat_cast {α : Type u_2} (n : ) :
@[protected, instance]
def centroid_hom.semiring {α : Type u_2}  :
Equations
theorem centroid_hom.comp_mul_comm {α : Type u_2} (T S : centroid_hom α) (a b : α) :
(T S) (a * b) = (S T) (a * b)
@[protected, instance]
def centroid_hom.has_neg {α : Type u_2}  :

Negation of centroid_homs as a centroid_hom.

Equations
@[protected, instance]
def centroid_hom.has_sub {α : Type u_2}  :
Equations
@[protected, instance]
def centroid_hom.has_zsmul {α : Type u_2}  :
Equations
@[protected, instance]
def centroid_hom.has_int_cast {α : Type u_2}  :
Equations
@[simp, norm_cast]
theorem centroid_hom.coe_int_cast {α : Type u_2} (z : ) :
theorem centroid_hom.int_cast_apply {α : Type u_2} (z : ) (m : α) :
z m = z m
@[simp]
theorem centroid_hom.to_End_neg {α : Type u_2} (x : centroid_hom α) :
@[simp]
theorem centroid_hom.to_End_sub {α : Type u_2} (x y : centroid_hom α) :
(x - y).to_End = x.to_End - y.to_End
theorem centroid_hom.to_End_zsmul {α : Type u_2} (x : centroid_hom α) (n : ) :
(n x).to_End = n x.to_End
@[protected, instance]
def centroid_hom.add_comm_group {α : Type u_2}  :
Equations
@[simp, norm_cast]
theorem centroid_hom.coe_neg {α : Type u_2} (f : centroid_hom α) :
@[simp, norm_cast]
theorem centroid_hom.coe_sub {α : Type u_2} (f g : centroid_hom α) :
(f - g) = f - g
@[simp]
theorem centroid_hom.neg_apply {α : Type u_2} (f : centroid_hom α) (a : α) :
(-f) a = -f a
@[simp]
theorem centroid_hom.sub_apply {α : Type u_2} (f g : centroid_hom α) (a : α) :
(f - g) a = f a - g a
@[simp, norm_cast]
theorem centroid_hom.to_End_int_cast {α : Type u_2} (z : ) :
@[protected, instance]
def centroid_hom.ring {α : Type u_2}  :
Equations
@[reducible]
def centroid_hom.comm_ring {α : Type u_2} (h : (a b : α), ( (r : α), a * r * b = 0) a = 0 b = 0) :

A prime associative ring has commutative centroid.

Equations