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

ink

structure CentroidHom (α : Type u_1) [inst : NonUnitalNonAssocSemiring α] extends AddMonoidHom : 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 α.

ink

class CentroidHomClass (F : Type u_1) (α : outParam (Type u_2)) [inst : NonUnitalNonAssocSemiring α] extends AddMonoidHomClass : 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.

ink

instance instCoeTCCentroidHom {F : Type u_1} {α : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst : CentroidHomClass F α] : CoeTC F (CentroidHom α)

Equations

• One or more equations did not get rendered due to their size.

Centroid homomorphisms

ink

instance CentroidHom.instCentroidHomClassCentroidHom {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] : CentroidHomClass (CentroidHom α) α

Equations

• One or more equations did not get rendered due to their size.

ink

instance CentroidHom.instCoeFunCentroidHomForAll {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] : CoeFun (CentroidHom α) fun x => α → α

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

Equations

• CentroidHom.instCoeFunCentroidHomForAll = inferInstanceAs (CoeFun (CentroidHom α) fun x => α → α)

ink

theorem CentroidHom.ext {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] {f : CentroidHom α} {g : CentroidHom α} (h : ∀ (a : α), ↑f a = ↑g a) : f = g

ink

@[simp]

theorem CentroidHom.coe_toAddMonoidHom {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) : ↑↑f = ↑f

ink

@[simp]

theorem CentroidHom.toAddMonoidHom_eq_coe {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) : f.toAddMonoidHom = ↑f

ink

theorem CentroidHom.coe_toAddMonoidHom_injective {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] : Function.Injective AddMonoidHomClass.toAddMonoidHom

ink

def CentroidHom.toEnd {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) : AddMonoid.End α

Turn a centroid homomorphism into an additive monoid endomorphism.

Equations

• CentroidHom.toEnd f = ↑f

ink

theorem CentroidHom.toEnd_injective {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] : Function.Injective CentroidHom.toEnd

ink

def CentroidHom.copy {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (f' : α → α) (h : f' = ↑f) : CentroidHom α

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.

ink

@[simp]

theorem CentroidHom.coe_copy {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (f' : α → α) (h : f' = ↑f) : ↑(CentroidHom.copy f f' h) = f'

ink

theorem CentroidHom.copy_eq {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (f' : α → α) (h : f' = ↑f) : CentroidHom.copy f f' h = f

ink

def CentroidHom.id (α : Type u_1) [inst : NonUnitalNonAssocSemiring α] : CentroidHom α

id as a CentroidHom.

Equations

• One or more equations did not get rendered due to their size.

ink

instance CentroidHom.instInhabitedCentroidHom (α : Type u_1) [inst : NonUnitalNonAssocSemiring α] : Inhabited (CentroidHom α)

Equations

• CentroidHom.instInhabitedCentroidHom α = { default := CentroidHom.id α }

ink

@[simp]

theorem CentroidHom.coe_id (α : Type u_1) [inst : NonUnitalNonAssocSemiring α] : ↑(CentroidHom.id α) = id

ink

@[simp]

theorem CentroidHom.toAddMonoidHom_id (α : Type u_1) [inst : NonUnitalNonAssocSemiring α] : ↑(CentroidHom.id α) = AddMonoidHom.id α

ink

@[simp]

theorem CentroidHom.id_apply {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (a : α) : ↑(CentroidHom.id α) a = a

ink

def CentroidHom.comp {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (g : CentroidHom α) (f : CentroidHom α) : CentroidHom α

Composition of CentroidHoms as a CentroidHom.

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem CentroidHom.coe_comp {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (g : CentroidHom α) (f : CentroidHom α) : ↑(CentroidHom.comp g f) = ↑g ∘ ↑f

ink

@[simp]

theorem CentroidHom.comp_apply {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (g : CentroidHom α) (f : CentroidHom α) (a : α) : ↑(CentroidHom.comp g f) a = ↑g (↑f a)

ink

@[simp]

theorem CentroidHom.coe_comp_addMonoidHom {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (g : CentroidHom α) (f : CentroidHom α) : ↑(CentroidHom.comp g f) = AddMonoidHom.comp ↑g ↑f

ink

@[simp]

theorem CentroidHom.comp_assoc {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (h : CentroidHom α) (g : CentroidHom α) (f : CentroidHom α) : CentroidHom.comp (CentroidHom.comp h g) f = CentroidHom.comp h (CentroidHom.comp g f)

ink

@[simp]

theorem CentroidHom.comp_id {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) : CentroidHom.comp f (CentroidHom.id α) = f

ink

@[simp]

theorem CentroidHom.id_comp {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) : CentroidHom.comp (CentroidHom.id α) f = f

ink

theorem CentroidHom.cancel_right {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] {g₁ : CentroidHom α} {g₂ : CentroidHom α} {f : CentroidHom α} (hf : Function.Surjective ↑f) : CentroidHom.comp g₁ f = CentroidHom.comp g₂ f ↔ g₁ = g₂

ink

theorem CentroidHom.cancel_left {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] {g : CentroidHom α} {f₁ : CentroidHom α} {f₂ : CentroidHom α} (hg : Function.Injective ↑g) : CentroidHom.comp g f₁ = CentroidHom.comp g f₂ ↔ f₁ = f₂

ink

instance CentroidHom.instZeroCentroidHom {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] : Zero (CentroidHom α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance CentroidHom.instOneCentroidHom {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] : One (CentroidHom α)

Equations

• CentroidHom.instOneCentroidHom = { one := CentroidHom.id α }

ink

instance CentroidHom.instAddCentroidHom {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] : Add (CentroidHom α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance CentroidHom.instMulCentroidHom {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] : Mul (CentroidHom α)

Equations

• CentroidHom.instMulCentroidHom = { mul := CentroidHom.comp }

ink

instance CentroidHom.hasNsmul {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] : SMul ℕ (CentroidHom α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance CentroidHom.hasNpowNat {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] : Pow (CentroidHom α) ℕ

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem CentroidHom.coe_zero {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] : ↑0 = 0

ink

@[simp]

theorem CentroidHom.coe_one {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] : ↑1 = id

ink

@[simp]

theorem CentroidHom.coe_add {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) : ↑(f + g) = ↑f + ↑g

ink

@[simp]

theorem CentroidHom.coe_mul {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) : ↑(f * g) = ↑f ∘ ↑g

ink

@[simp]

theorem CentroidHom.coe_nsmul {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (n : ℕ) : ↑(n • f) = n • ↑f

ink

@[simp]

theorem CentroidHom.zero_apply {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (a : α) : ↑0 a = 0

ink

@[simp]

theorem CentroidHom.one_apply {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (a : α) : ↑1 a = a

ink

@[simp]

theorem CentroidHom.add_apply {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) (a : α) : ↑(f + g) a = ↑f a + ↑g a

ink

@[simp]

theorem CentroidHom.mul_apply {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) (a : α) : ↑(f * g) a = ↑f (↑g a)

ink

@[simp]

theorem CentroidHom.nsmul_apply {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (n : ℕ) (a : α) : ↑(n • f) a = n • ↑f a

ink

@[simp]

theorem CentroidHom.toEnd_zero {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] : CentroidHom.toEnd 0 = 0

ink

@[simp]

theorem CentroidHom.toEnd_add {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (x : CentroidHom α) (y : CentroidHom α) : CentroidHom.toEnd (x + y) = CentroidHom.toEnd x + CentroidHom.toEnd y

ink

theorem CentroidHom.toEnd_nsmul {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (x : CentroidHom α) (n : ℕ) : CentroidHom.toEnd (n • x) = n • CentroidHom.toEnd x

ink

instance CentroidHom.instAddCommMonoidCentroidHom {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] : AddCommMonoid (CentroidHom α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance CentroidHom.instNatCastCentroidHom {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] : NatCast (CentroidHom α)

Equations

• CentroidHom.instNatCastCentroidHom = { natCast := fun n => n • 1 }

ink

@[simp]

theorem CentroidHom.coe_nat_cast {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (n : ℕ) : ↑↑n = ↑(n • CentroidHom.id α)

ink

theorem CentroidHom.nat_cast_apply {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (n : ℕ) (m : α) : ↑↑n m = n • m

ink

@[simp]

theorem CentroidHom.toEnd_one {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] : CentroidHom.toEnd 1 = 1

ink

@[simp]

theorem CentroidHom.toEnd_mul {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (x : CentroidHom α) (y : CentroidHom α) : CentroidHom.toEnd (x * y) = CentroidHom.toEnd x * CentroidHom.toEnd y

ink

@[simp]

theorem CentroidHom.toEnd_pow {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (x : CentroidHom α) (n : ℕ) : CentroidHom.toEnd (x ^ n) = CentroidHom.toEnd x ^ n

ink

@[simp]

theorem CentroidHom.toEnd_nat_cast {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (n : ℕ) : CentroidHom.toEnd ↑n = ↑n

ink

instance CentroidHom.instSemiringCentroidHom {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] : Semiring (CentroidHom α)

Equations

• One or more equations did not get rendered due to their size.

ink

theorem CentroidHom.comp_mul_comm {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (T : CentroidHom α) (S : CentroidHom α) (a : α) (b : α) : (↑T ∘ ↑S) (a * b) = (↑S ∘ ↑T) (a * b)

ink

instance CentroidHom.instNegCentroidHomToNonUnitalNonAssocSemiring {α : Type u_1} [inst : NonUnitalNonAssocRing α] : Neg (CentroidHom α)

Negation of CentroidHoms as a CentroidHom.

Equations

• One or more equations did not get rendered due to their size.

ink

instance CentroidHom.instSubCentroidHomToNonUnitalNonAssocSemiring {α : Type u_1} [inst : NonUnitalNonAssocRing α] : Sub (CentroidHom α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance CentroidHom.hasZsmul {α : Type u_1} [inst : NonUnitalNonAssocRing α] : SMul ℤ (CentroidHom α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance CentroidHom.instIntCastCentroidHomToNonUnitalNonAssocSemiring {α : Type u_1} [inst : NonUnitalNonAssocRing α] : IntCast (CentroidHom α)

Equations

• CentroidHom.instIntCastCentroidHomToNonUnitalNonAssocSemiring = { intCast := fun z => z • 1 }

ink

@[simp]

theorem CentroidHom.coe_int_cast {α : Type u_1} [inst : NonUnitalNonAssocRing α] (z : ℤ) : ↑↑z = ↑(z • CentroidHom.id α)

ink

theorem CentroidHom.int_cast_apply {α : Type u_1} [inst : NonUnitalNonAssocRing α] (z : ℤ) (m : α) : ↑↑z m = z • m

ink

@[simp]

theorem CentroidHom.toEnd_neg {α : Type u_1} [inst : NonUnitalNonAssocRing α] (x : CentroidHom α) : CentroidHom.toEnd (-x) = -CentroidHom.toEnd x

ink

@[simp]

theorem CentroidHom.toEnd_sub {α : Type u_1} [inst : NonUnitalNonAssocRing α] (x : CentroidHom α) (y : CentroidHom α) : CentroidHom.toEnd (x - y) = CentroidHom.toEnd x - CentroidHom.toEnd y

ink

theorem CentroidHom.toEnd_zsmul {α : Type u_1} [inst : NonUnitalNonAssocRing α] (x : CentroidHom α) (n : ℤ) : CentroidHom.toEnd (n • x) = n • CentroidHom.toEnd x

ink

instance CentroidHom.instAddCommGroupCentroidHomToNonUnitalNonAssocSemiring {α : Type u_1} [inst : NonUnitalNonAssocRing α] : AddCommGroup (CentroidHom α)

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem CentroidHom.coe_neg {α : Type u_1} [inst : NonUnitalNonAssocRing α] (f : CentroidHom α) : ↑(-f) = -↑f

ink

@[simp]

theorem CentroidHom.coe_sub {α : Type u_1} [inst : NonUnitalNonAssocRing α] (f : CentroidHom α) (g : CentroidHom α) : ↑(f - g) = ↑f - ↑g

ink

@[simp]

theorem CentroidHom.neg_apply {α : Type u_1} [inst : NonUnitalNonAssocRing α] (f : CentroidHom α) (a : α) : ↑(-f) a = -↑f a

ink

@[simp]

theorem CentroidHom.sub_apply {α : Type u_1} [inst : NonUnitalNonAssocRing α] (f : CentroidHom α) (g : CentroidHom α) (a : α) : ↑(f - g) a = ↑f a - ↑g a

ink

@[simp]

theorem CentroidHom.toEnd_int_cast {α : Type u_1} [inst : NonUnitalNonAssocRing α] (z : ℤ) : CentroidHom.toEnd ↑z = ↑z

ink

instance CentroidHom.instRingCentroidHomToNonUnitalNonAssocSemiring {α : Type u_1} [inst : NonUnitalNonAssocRing α] : Ring (CentroidHom α)

Equations

• One or more equations did not get rendered due to their size.

ink

def CentroidHom.commRing {α : Type u_1} [inst : NonUnitalRing α] (h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0) : CommRing (CentroidHom α)

A prime associative ring has commutative centroid.

Equations

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