mathlib3 documentation

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 #

Typeclasses #

References #

Tags #

centroid

@[nolint]
@[class]
structure centroid_hom_class (F : Type u_3) (α : out_param (Type u_4)) [non_unital_non_assoc_semiring α] :
Type (max u_3 u_4)

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]
Equations

Centroid homomorphisms #

@[protected, instance]

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

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

Turn a centroid homomorphism into an additive monoid endomorphism.

Equations
@[protected]
def centroid_hom.copy {α : Type u_2} [non_unital_non_assoc_semiring α] (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} [non_unital_non_assoc_semiring α] (f : centroid_hom α) (f' : α α) (h : f' = f) :
(f.copy f' h) = f'
theorem centroid_hom.copy_eq {α : Type u_2} [non_unital_non_assoc_semiring α] (f : centroid_hom α) (f' : α α) (h : f' = f) :
f.copy f' h = f
@[protected, instance]
Equations
@[simp, norm_cast]
@[simp]
theorem centroid_hom.id_apply {α : Type u_2} [non_unital_non_assoc_semiring α] (a : α) :
@[simp, norm_cast]
theorem centroid_hom.coe_comp {α : Type u_2} [non_unital_non_assoc_semiring α] (g f : centroid_hom α) :
(g.comp f) = g f
@[simp]
theorem centroid_hom.comp_apply {α : Type u_2} [non_unital_non_assoc_semiring α] (g f : centroid_hom α) (a : α) :
(g.comp f) a = g (f a)
@[simp, norm_cast]
@[simp]
theorem centroid_hom.comp_assoc {α : Type u_2} [non_unital_non_assoc_semiring α] (h g f : centroid_hom α) :
(h.comp g).comp f = h.comp (g.comp f)
@[simp]
@[simp]
theorem centroid_hom.cancel_right {α : Type u_2} [non_unital_non_assoc_semiring α] {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} [non_unital_non_assoc_semiring α] {g f₁ f₂ : centroid_hom α} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
theorem centroid_hom.coe_add {α : Type u_2} [non_unital_non_assoc_semiring α] (f g : centroid_hom α) :
(f + g) = f + g
@[simp, norm_cast]
theorem centroid_hom.coe_mul {α : Type u_2} [non_unital_non_assoc_semiring α] (f g : centroid_hom α) :
(f * g) = f g
@[simp, norm_cast, nolint]
theorem centroid_hom.coe_nsmul {α : Type u_2} [non_unital_non_assoc_semiring α] (f : centroid_hom α) (n : ) :
(n f) = n f
@[simp]
theorem centroid_hom.zero_apply {α : Type u_2} [non_unital_non_assoc_semiring α] (a : α) :
0 a = 0
@[simp]
theorem centroid_hom.one_apply {α : Type u_2} [non_unital_non_assoc_semiring α] (a : α) :
1 a = a
@[simp]
theorem centroid_hom.add_apply {α : Type u_2} [non_unital_non_assoc_semiring α] (f g : centroid_hom α) (a : α) :
(f + g) a = f a + g a
@[simp]
theorem centroid_hom.mul_apply {α : Type u_2} [non_unital_non_assoc_semiring α] (f g : centroid_hom α) (a : α) :
(f * g) a = f (g a)
@[simp, nolint]
theorem centroid_hom.nsmul_apply {α : Type u_2} [non_unital_non_assoc_semiring α] (f : centroid_hom α) (n : ) (a : α) :
(n f) a = n f a
@[simp]
@[protected, instance]
Equations
@[simp, norm_cast]
theorem centroid_hom.nat_cast_apply {α : Type u_2} [non_unital_non_assoc_semiring α] (n : ) (m : α) :
n m = n m
@[simp]
@[simp]
@[simp]
theorem centroid_hom.to_End_pow {α : Type u_2} [non_unital_non_assoc_semiring α] (x : centroid_hom α) (n : ) :
(x ^ n).to_End = x.to_End ^ n
@[simp, norm_cast]
theorem centroid_hom.comp_mul_comm {α : Type u_2} [non_unital_non_assoc_semiring α] (T S : centroid_hom α) (a b : α) :
(T S) (a * b) = (S T) (a * b)
@[protected, instance]

Negation of centroid_homs as a centroid_hom.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp, norm_cast]
theorem centroid_hom.int_cast_apply {α : Type u_2} [non_unital_non_assoc_ring α] (z : ) (m : α) :
z m = z m
@[simp]
@[simp]
theorem centroid_hom.to_End_sub {α : Type u_2} [non_unital_non_assoc_ring α] (x y : centroid_hom α) :
(x - y).to_End = x.to_End - y.to_End
theorem centroid_hom.to_End_zsmul {α : Type u_2} [non_unital_non_assoc_ring α] (x : centroid_hom α) (n : ) :
(n x).to_End = n x.to_End
@[protected, instance]
Equations
@[simp, norm_cast]
@[simp, norm_cast]
theorem centroid_hom.coe_sub {α : Type u_2} [non_unital_non_assoc_ring α] (f g : centroid_hom α) :
(f - g) = f - g
@[simp]
theorem centroid_hom.neg_apply {α : Type u_2} [non_unital_non_assoc_ring α] (f : centroid_hom α) (a : α) :
(-f) a = -f a
@[simp]
theorem centroid_hom.sub_apply {α : Type u_2} [non_unital_non_assoc_ring α] (f g : centroid_hom α) (a : α) :
(f - g) a = f a - g a
@[simp, norm_cast]
@[protected, instance]
Equations