Documentation

Mathlib.Algebra.Ring.CentroidHom

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 DFunLike 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_6) [NonUnitalNonAssocSemiring α] extends AddMonoidHom :

Type u_6

The type of centroid homomorphisms from α to α.

toFun : α → α
map_zero' : (↑self.toAddMonoidHom).toFun 0 = 0
map_add' : ∀ (x y : α), (↑self.toAddMonoidHom).toFun (x + y) = (↑self.toAddMonoidHom).toFun x + (↑self.toAddMonoidHom).toFun y
map_mul_left' : ∀ (a b : α), (↑self.toAddMonoidHom).toFun (a * b) = a * (↑self.toAddMonoidHom).toFun b
Commutativity of centroid homomorphims with left multiplication.
map_mul_right' : ∀ (a b : α), (↑self.toAddMonoidHom).toFun (a * b) = (↑self.toAddMonoidHom).toFun a * b
Commutativity of centroid homomorphims with right multiplication.

Instances For

theorem CentroidHom.map_mul_left' {α : Type u_6} [NonUnitalNonAssocSemiring α] (self : CentroidHom α) (a : α) (b : α) :

(↑self.toAddMonoidHom).toFun (a * b) = a * (↑self.toAddMonoidHom).toFun b

Commutativity of centroid homomorphims with left multiplication.

theorem CentroidHom.map_mul_right' {α : Type u_6} [NonUnitalNonAssocSemiring α] (self : CentroidHom α) (a : α) (b : α) :

(↑self.toAddMonoidHom).toFun (a * b) = (↑self.toAddMonoidHom).toFun a * b

Commutativity of centroid homomorphims with right multiplication.

class CentroidHomClass (F : Type u_6) (α : Type u_7) [NonUnitalNonAssocSemiring α] [FunLike F α α] extends AddMonoidHomClass :

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

You should extend this class when you extend CentroidHom.

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.

Instances

theorem CentroidHomClass.map_mul_left {F : Type u_6} {α : Type u_7} [NonUnitalNonAssocSemiring α] [FunLike F α α] [self : CentroidHomClass F α] (f : F) (a : α) (b : α) :

f (a * b) = a * f b

Commutativity of centroid homomorphims with left multiplication.

theorem CentroidHomClass.map_mul_right {F : Type u_6} {α : Type u_7} [NonUnitalNonAssocSemiring α] [FunLike F α α] [self : CentroidHomClass F α] (f : F) (a : α) (b : α) :

f (a * b) = f a * b

Commutativity of centroid homomorphims with right multiplication.

instance instCoeTCCentroidHomOfCentroidHomClass {F : Type u_1} {α : Type u_5} [NonUnitalNonAssocSemiring α] [FunLike F α α] [CentroidHomClass F α] :

CoeTC F (CentroidHom α)

Equations

instCoeTCCentroidHomOfCentroidHomClass = { coe := fun (f : F) => let __src := ↑f; { toFun := ⇑f, map_zero' := ⋯, map_add' := ⋯, map_mul_left' := ⋯, map_mul_right' := ⋯ } }

Centroid homomorphisms #

instance CentroidHom.instFunLike {α : Type u_5} [NonUnitalNonAssocSemiring α] :

FunLike (CentroidHom α) α α

Equations

CentroidHom.instFunLike = { coe := fun (f : CentroidHom α) => (↑f.toAddMonoidHom).toFun, coe_injective' := ⋯ }

instance CentroidHom.instCentroidHomClass {α : Type u_5} [NonUnitalNonAssocSemiring α] :

CentroidHomClass (CentroidHom α) α

Equations

⋯ = ⋯

instance CentroidHom.instCoeFunForall {α : Type u_5} [NonUnitalNonAssocSemiring α] :

CoeFun (CentroidHom α) fun (x : CentroidHom α) => α → α

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

Equations

CentroidHom.instCoeFunForall = inferInstanceAs (CoeFun (CentroidHom α) fun (x : CentroidHom α) => α → α)

theorem CentroidHom.toFun_eq_coe {α : Type u_5} [NonUnitalNonAssocSemiring α] {f : CentroidHom α} :

(↑f.toAddMonoidHom).toFun = ⇑f

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

f = g

@[simp]

theorem CentroidHom.coe_toAddMonoidHom {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) :

⇑↑f = ⇑f

@[simp]

theorem CentroidHom.toAddMonoidHom_eq_coe {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) :

f.toAddMonoidHom = ↑f

theorem CentroidHom.coe_toAddMonoidHom_injective {α : Type u_5} [NonUnitalNonAssocSemiring α] :

Function.Injective AddMonoidHomClass.toAddMonoidHom

def CentroidHom.toEnd {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) :

AddMonoid.End α

Turn a centroid homomorphism into an additive monoid endomorphism.

Equations

f.toEnd = ↑f

Instances For

theorem CentroidHom.toEnd_injective {α : Type u_5} [NonUnitalNonAssocSemiring α] :

Function.Injective CentroidHom.toEnd

def CentroidHom.copy {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (f' : α → α) (h : f' = ⇑f) :

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

Equations

f.copy f' h = let __src := f.copy f' h; { toFun := f', map_zero' := ⋯, map_add' := ⋯, map_mul_left' := ⋯, map_mul_right' := ⋯ }

Instances For

@[simp]

theorem CentroidHom.coe_copy {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (f' : α → α) (h : f' = ⇑f) :

⇑(f.copy f' h) = f'

theorem CentroidHom.copy_eq {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (f' : α → α) (h : f' = ⇑f) :

f.copy f' h = f

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

id as a CentroidHom.

Equations

CentroidHom.id α = let __src := AddMonoidHom.id α; { toAddMonoidHom := __src, map_mul_left' := ⋯, map_mul_right' := ⋯ }

Instances For

instance CentroidHom.instInhabited (α : Type u_5) [NonUnitalNonAssocSemiring α] :

Inhabited (CentroidHom α)

Equations

CentroidHom.instInhabited α = { default := CentroidHom.id α }

@[simp]

theorem CentroidHom.coe_id (α : Type u_5) [NonUnitalNonAssocSemiring α] :

⇑(CentroidHom.id α) = id

@[simp]

theorem CentroidHom.toAddMonoidHom_id (α : Type u_5) [NonUnitalNonAssocSemiring α] :

↑(CentroidHom.id α) = AddMonoidHom.id α

@[simp]

theorem CentroidHom.id_apply {α : Type u_5} [NonUnitalNonAssocSemiring α] (a : α) :

(CentroidHom.id α) a = a

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

Composition of CentroidHoms as a CentroidHom.

Equations

g.comp f = let __src := g.comp f.toAddMonoidHom; { toAddMonoidHom := __src, map_mul_left' := ⋯, map_mul_right' := ⋯ }

Instances For

@[simp]

theorem CentroidHom.coe_comp {α : Type u_5} [NonUnitalNonAssocSemiring α] (g : CentroidHom α) (f : CentroidHom α) :

⇑(g.comp f) = ⇑g ∘ ⇑f

@[simp]

theorem CentroidHom.comp_apply {α : Type u_5} [NonUnitalNonAssocSemiring α] (g : CentroidHom α) (f : CentroidHom α) (a : α) :

(g.comp f) a = g (f a)

@[simp]

theorem CentroidHom.coe_comp_addMonoidHom {α : Type u_5} [NonUnitalNonAssocSemiring α] (g : CentroidHom α) (f : CentroidHom α) :

↑(g.comp f) = (↑g).comp ↑f

@[simp]

theorem CentroidHom.comp_assoc {α : Type u_5} [NonUnitalNonAssocSemiring α] (h : CentroidHom α) (g : CentroidHom α) (f : CentroidHom α) :

(h.comp g).comp f = h.comp (g.comp f)

@[simp]

theorem CentroidHom.comp_id {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) :

f.comp (CentroidHom.id α) = f

@[simp]

theorem CentroidHom.id_comp {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) :

(CentroidHom.id α).comp f = f

@[simp]

theorem CentroidHom.cancel_right {α : Type u_5} [NonUnitalNonAssocSemiring α] {g₁ : CentroidHom α} {g₂ : CentroidHom α} {f : CentroidHom α} (hf : Function.Surjective ⇑f) :

g₁.comp f = g₂.comp f ↔ g₁ = g₂

@[simp]

theorem CentroidHom.cancel_left {α : Type u_5} [NonUnitalNonAssocSemiring α] {g : CentroidHom α} {f₁ : CentroidHom α} {f₂ : CentroidHom α} (hg : Function.Injective ⇑g) :

g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

instance CentroidHom.instZero {α : Type u_5} [NonUnitalNonAssocSemiring α] :

Zero (CentroidHom α)

Equations

CentroidHom.instZero = { zero := let __src := 0; { toAddMonoidHom := __src, map_mul_left' := ⋯, map_mul_right' := ⋯ } }

instance CentroidHom.instOne {α : Type u_5} [NonUnitalNonAssocSemiring α] :

One (CentroidHom α)

Equations

CentroidHom.instOne = { one := CentroidHom.id α }

instance CentroidHom.instAdd {α : Type u_5} [NonUnitalNonAssocSemiring α] :

Add (CentroidHom α)

Equations

CentroidHom.instAdd = { add := fun (f g : CentroidHom α) => let __src := ↑f + ↑g; { toAddMonoidHom := __src, map_mul_left' := ⋯, map_mul_right' := ⋯ } }

instance CentroidHom.instMul {α : Type u_5} [NonUnitalNonAssocSemiring α] :

Mul (CentroidHom α)

Equations

CentroidHom.instMul = { mul := CentroidHom.comp }

instance CentroidHom.instSMul {M : Type u_2} {α : Type u_5} [NonUnitalNonAssocSemiring α] [Monoid M] [DistribMulAction M α] [SMulCommClass M α α] [IsScalarTower M α α] :

SMul M (CentroidHom α)

Equations

CentroidHom.instSMul = { smul := fun (n : M) (f : CentroidHom α) => let __src := n • ↑f; { toAddMonoidHom := __src, map_mul_left' := ⋯, map_mul_right' := ⋯ } }

instance CentroidHom.instIsScalarTower {M : Type u_2} {N : Type u_3} {α : Type u_5} [NonUnitalNonAssocSemiring α] [Monoid M] [Monoid N] [DistribMulAction M α] [SMulCommClass M α α] [IsScalarTower M α α] [DistribMulAction N α] [SMulCommClass N α α] [IsScalarTower N α α] [SMul M N] [IsScalarTower M N α] :

IsScalarTower M N (CentroidHom α)

Equations

⋯ = ⋯

instance CentroidHom.instSMulCommClass {M : Type u_2} {N : Type u_3} {α : Type u_5} [NonUnitalNonAssocSemiring α] [Monoid M] [Monoid N] [DistribMulAction M α] [SMulCommClass M α α] [IsScalarTower M α α] [DistribMulAction N α] [SMulCommClass N α α] [IsScalarTower N α α] [SMulCommClass M N α] :

SMulCommClass M N (CentroidHom α)

Equations

⋯ = ⋯

instance CentroidHom.instIsCentralScalar {M : Type u_2} {α : Type u_5} [NonUnitalNonAssocSemiring α] [Monoid M] [DistribMulAction M α] [SMulCommClass M α α] [IsScalarTower M α α] [DistribMulAction Mᵐᵒᵖ α] [IsCentralScalar M α] :

IsCentralScalar M (CentroidHom α)

Equations

⋯ = ⋯

instance CentroidHom.isScalarTowerRight {M : Type u_2} {α : Type u_5} [NonUnitalNonAssocSemiring α] [Monoid M] [DistribMulAction M α] [SMulCommClass M α α] [IsScalarTower M α α] :

IsScalarTower M (CentroidHom α) (CentroidHom α)

Equations

⋯ = ⋯

instance CentroidHom.hasNPowNat {α : Type u_5} [NonUnitalNonAssocSemiring α] :

Pow (CentroidHom α) ℕ

Equations

CentroidHom.hasNPowNat = { pow := fun (f : CentroidHom α) (n : ℕ) => { toAddMonoidHom := f.toEnd ^ n, map_mul_left' := ⋯, map_mul_right' := ⋯ } }

@[simp]

theorem CentroidHom.coe_zero {α : Type u_5} [NonUnitalNonAssocSemiring α] :

⇑0 = 0

@[simp]

theorem CentroidHom.coe_one {α : Type u_5} [NonUnitalNonAssocSemiring α] :

⇑1 = id

@[simp]

theorem CentroidHom.coe_add {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) :

⇑(f + g) = ⇑f + ⇑g

@[simp]

theorem CentroidHom.coe_mul {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) :

⇑(f * g) = ⇑f ∘ ⇑g

@[simp]

theorem CentroidHom.coe_smul {M : Type u_2} {α : Type u_5} [NonUnitalNonAssocSemiring α] [Monoid M] [DistribMulAction M α] [SMulCommClass M α α] [IsScalarTower M α α] (n : M) (f : CentroidHom α) :

⇑(n • f) = n • ⇑f

@[simp]

theorem CentroidHom.zero_apply {α : Type u_5} [NonUnitalNonAssocSemiring α] (a : α) :

0 a = 0

@[simp]

theorem CentroidHom.one_apply {α : Type u_5} [NonUnitalNonAssocSemiring α] (a : α) :

1 a = a

@[simp]

theorem CentroidHom.add_apply {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) (a : α) :

(f + g) a = f a + g a

@[simp]

theorem CentroidHom.mul_apply {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) (a : α) :

(f * g) a = f (g a)

@[simp]

theorem CentroidHom.smul_apply {M : Type u_2} {α : Type u_5} [NonUnitalNonAssocSemiring α] [Monoid M] [DistribMulAction M α] [SMulCommClass M α α] [IsScalarTower M α α] (n : M) (f : CentroidHom α) (a : α) :

(n • f) a = n • f a

@[simp]

theorem CentroidHom.toEnd_zero {α : Type u_5} [NonUnitalNonAssocSemiring α] :

CentroidHom.toEnd 0 = 0

@[simp]

theorem CentroidHom.toEnd_add {α : Type u_5} [NonUnitalNonAssocSemiring α] (x : CentroidHom α) (y : CentroidHom α) :

(x + y).toEnd = x.toEnd + y.toEnd

theorem CentroidHom.toEnd_smul {M : Type u_2} {α : Type u_5} [NonUnitalNonAssocSemiring α] [Monoid M] [DistribMulAction M α] [SMulCommClass M α α] [IsScalarTower M α α] (m : M) (x : CentroidHom α) :

(m • x).toEnd = m • x.toEnd

instance CentroidHom.instAddCommMonoid {α : Type u_5} [NonUnitalNonAssocSemiring α] :

AddCommMonoid (CentroidHom α)

Equations

CentroidHom.instAddCommMonoid = Function.Injective.addCommMonoid AddMonoidHomClass.toAddMonoidHom ⋯ ⋯ ⋯ ⋯

instance CentroidHom.instNatCast {α : Type u_5} [NonUnitalNonAssocSemiring α] :

NatCast (CentroidHom α)

Equations

CentroidHom.instNatCast = { natCast := fun (n : ℕ) => n • 1 }

@[simp]

theorem CentroidHom.coe_natCast {α : Type u_5} [NonUnitalNonAssocSemiring α] (n : ℕ) :

⇑↑n = n • ⇑(CentroidHom.id α)

@[deprecated CentroidHom.coe_natCast]

theorem CentroidHom.coe_nat_cast {α : Type u_5} [NonUnitalNonAssocSemiring α] (n : ℕ) :

⇑↑n = n • ⇑(CentroidHom.id α)

Alias of CentroidHom.coe_natCast.

theorem CentroidHom.natCast_apply {α : Type u_5} [NonUnitalNonAssocSemiring α] (n : ℕ) (m : α) :

↑n m = n • m

@[deprecated CentroidHom.natCast_apply]

theorem CentroidHom.nat_cast_apply {α : Type u_5} [NonUnitalNonAssocSemiring α] (n : ℕ) (m : α) :

↑n m = n • m

Alias of CentroidHom.natCast_apply.

@[simp]

theorem CentroidHom.toEnd_one {α : Type u_5} [NonUnitalNonAssocSemiring α] :

CentroidHom.toEnd 1 = 1

@[simp]

theorem CentroidHom.toEnd_mul {α : Type u_5} [NonUnitalNonAssocSemiring α] (x : CentroidHom α) (y : CentroidHom α) :

(x * y).toEnd = x.toEnd * y.toEnd

@[simp]

theorem CentroidHom.toEnd_pow {α : Type u_5} [NonUnitalNonAssocSemiring α] (x : CentroidHom α) (n : ℕ) :

(x ^ n).toEnd = x.toEnd ^ n

@[simp]

theorem CentroidHom.toEnd_natCast {α : Type u_5} [NonUnitalNonAssocSemiring α] (n : ℕ) :

(↑n).toEnd = ↑n

@[deprecated CentroidHom.toEnd_natCast]

theorem CentroidHom.toEnd_nat_cast {α : Type u_5} [NonUnitalNonAssocSemiring α] (n : ℕ) :

(↑n).toEnd = ↑n

Alias of CentroidHom.toEnd_natCast.

instance CentroidHom.instSemiring {α : Type u_5} [NonUnitalNonAssocSemiring α] :

Semiring (CentroidHom α)

Equations

CentroidHom.instSemiring = Function.Injective.semiring CentroidHom.toEnd ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem CentroidHom.toEndRingHom_apply (α : Type u_5) [NonUnitalNonAssocSemiring α] (f : CentroidHom α) :

(CentroidHom.toEndRingHom α) f = f.toEnd

def CentroidHom.toEndRingHom (α : Type u_5) [NonUnitalNonAssocSemiring α] :

CentroidHom α →+* AddMonoid.End α

CentroidHom.toEnd as a RingHom.

Equations

CentroidHom.toEndRingHom α = { toFun := CentroidHom.toEnd, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Instances For

theorem CentroidHom.comp_mul_comm {α : Type u_5} [NonUnitalNonAssocSemiring α] (T : CentroidHom α) (S : CentroidHom α) (a : α) (b : α) :

(⇑T ∘ ⇑S) (a * b) = (⇑S ∘ ⇑T) (a * b)

instance CentroidHom.instDistribMulAction {M : Type u_2} {α : Type u_5} [NonUnitalNonAssocSemiring α] [Monoid M] [DistribMulAction M α] [SMulCommClass M α α] [IsScalarTower M α α] :

DistribMulAction M (CentroidHom α)

Equations

CentroidHom.instDistribMulAction = Function.Injective.distribMulAction (CentroidHom.toEndRingHom α).toAddMonoidHom ⋯ ⋯

instance CentroidHom.instModule {R : Type u_4} {α : Type u_5} [NonUnitalNonAssocSemiring α] [Semiring R] [Module R α] [SMulCommClass R α α] [IsScalarTower R α α] :

Module R (CentroidHom α)

Equations

CentroidHom.instModule = Function.Injective.module R (CentroidHom.toEndRingHom α).toAddMonoidHom ⋯ ⋯

The following instances show that α is a non-unital and non-associative algebra over CentroidHom α.

instance CentroidHom.applyModule {α : Type u_5} [NonUnitalNonAssocSemiring α] :

Module (CentroidHom α) α

The tautological action by CentroidHom α on α.

This generalizes Function.End.applyMulAction.

Equations

CentroidHom.applyModule = Module.mk ⋯ ⋯

@[simp]

theorem CentroidHom.smul_def {α : Type u_5} [NonUnitalNonAssocSemiring α] (T : CentroidHom α) (a : α) :

T • a = T a

instance CentroidHom.instSMulCommClass_1 {α : Type u_5} [NonUnitalNonAssocSemiring α] :

SMulCommClass (CentroidHom α) α α

Equations

⋯ = ⋯

instance CentroidHom.instSMulCommClass_2 {α : Type u_5} [NonUnitalNonAssocSemiring α] :

SMulCommClass α (CentroidHom α) α

Equations

⋯ = ⋯

instance CentroidHom.instIsScalarTower_1 {α : Type u_5} [NonUnitalNonAssocSemiring α] :

IsScalarTower (CentroidHom α) α α

Equations

⋯ = ⋯

Let α be an algebra over R, such that the canonical ring homomorphism of R into CentroidHom α lies in the center of CentroidHom α. Then CentroidHom α is an algebra over R

@[simp]

theorem Module.toCentroidHom_apply_toFun {α : Type u_5} [NonUnitalNonAssocSemiring α] {R : Type u_6} [CommSemiring R] [Module R α] [SMulCommClass R α α] [IsScalarTower R α α] (x : R) (a : α) :

(Module.toCentroidHom x) a = x • a

def Module.toCentroidHom {α : Type u_5} [NonUnitalNonAssocSemiring α] {R : Type u_6} [CommSemiring R] [Module R α] [SMulCommClass R α α] [IsScalarTower R α α] :

R →+* CentroidHom α

The natural ring homomorphism from R into CentroidHom α.

This is a stronger version of Module.toAddMonoidEnd.

Equations

Module.toCentroidHom = RingHom.smulOneHom

Instances For

theorem CentroidHom.centroid_eq_centralizer_mulLeftRight {α : Type u_5} [NonUnitalNonAssocSemiring α] :

(CentroidHom.toEndRingHom α).rangeS = Subsemiring.centralizer (Set.range ⇑AddMonoid.End.mulLeft ∪ Set.range ⇑AddMonoid.End.mulRight)

def CentroidHom.centerToCentroid {α : Type u_5} [NonUnitalNonAssocSemiring α] :

↥(NonUnitalSubsemiring.center α) →ₙ+* CentroidHom α

The canonical homomorphism from the center into the centroid

Equations

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

Instances For

theorem CentroidHom.centerToCentroid_apply {α : Type u_5} [NonUnitalNonAssocSemiring α] (z : ↥(NonUnitalSubsemiring.center α)) (a : α) :

(CentroidHom.centerToCentroid z) a = ↑z * a

theorem NonUnitalNonAssocSemiring.mem_center_iff {α : Type u_5} [NonUnitalNonAssocSemiring α] (a : α) :

a ∈ NonUnitalSubsemiring.center α ↔ AddMonoid.End.mulRight a = AddMonoid.End.mulLeft a ∧ AddMonoid.End.mulLeft a ∈ (CentroidHom.toEndRingHom α).rangeS

theorem NonUnitalNonAssocCommSemiring.mem_center_iff {α : Type u_5} [NonUnitalNonAssocCommSemiring α] (a : α) :

a ∈ NonUnitalSubsemiring.center α ↔ ∀ (b : α), Commute (AddMonoid.End.mulLeft b) (AddMonoid.End.mulLeft a)

def CentroidHom.centerIsoCentroid {α : Type u_5} [NonAssocSemiring α] :

↥(Subsemiring.center α) ≃+* CentroidHom α

The canonical isomorphism from the center of a (non-associative) semiring onto its centroid.

Equations

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

Instances For

instance CentroidHom.instNeg {α : Type u_5} [NonUnitalNonAssocRing α] :

Neg (CentroidHom α)

Negation of CentroidHoms as a CentroidHom.

Equations

CentroidHom.instNeg = { neg := fun (f : CentroidHom α) => let __src := -↑f; { toAddMonoidHom := __src, map_mul_left' := ⋯, map_mul_right' := ⋯ } }

instance CentroidHom.instSub {α : Type u_5} [NonUnitalNonAssocRing α] :

Sub (CentroidHom α)

Equations

CentroidHom.instSub = { sub := fun (f g : CentroidHom α) => let __src := ↑f - ↑g; { toAddMonoidHom := __src, map_mul_left' := ⋯, map_mul_right' := ⋯ } }

instance CentroidHom.instIntCast {α : Type u_5} [NonUnitalNonAssocRing α] :

IntCast (CentroidHom α)

Equations

CentroidHom.instIntCast = { intCast := fun (z : ℤ) => z • 1 }

@[simp]

theorem CentroidHom.coe_intCast {α : Type u_5} [NonUnitalNonAssocRing α] (z : ℤ) :

⇑↑z = z • ⇑(CentroidHom.id α)

@[deprecated CentroidHom.coe_intCast]

theorem CentroidHom.coe_int_cast {α : Type u_5} [NonUnitalNonAssocRing α] (z : ℤ) :

⇑↑z = z • ⇑(CentroidHom.id α)

Alias of CentroidHom.coe_intCast.

theorem CentroidHom.intCast_apply {α : Type u_5} [NonUnitalNonAssocRing α] (z : ℤ) (m : α) :

↑z m = z • m

@[deprecated CentroidHom.intCast_apply]

theorem CentroidHom.int_cast_apply {α : Type u_5} [NonUnitalNonAssocRing α] (z : ℤ) (m : α) :

↑z m = z • m

Alias of CentroidHom.intCast_apply.

@[simp]

theorem CentroidHom.toEnd_neg {α : Type u_5} [NonUnitalNonAssocRing α] (x : CentroidHom α) :

(-x).toEnd = -x.toEnd

@[simp]

theorem CentroidHom.toEnd_sub {α : Type u_5} [NonUnitalNonAssocRing α] (x : CentroidHom α) (y : CentroidHom α) :

(x - y).toEnd = x.toEnd - y.toEnd

instance CentroidHom.instAddCommGroup {α : Type u_5} [NonUnitalNonAssocRing α] :

AddCommGroup (CentroidHom α)

Equations

CentroidHom.instAddCommGroup = Function.Injective.addCommGroup CentroidHom.toEnd ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem CentroidHom.coe_neg {α : Type u_5} [NonUnitalNonAssocRing α] (f : CentroidHom α) :

⇑(-f) = -⇑f

@[simp]

theorem CentroidHom.coe_sub {α : Type u_5} [NonUnitalNonAssocRing α] (f : CentroidHom α) (g : CentroidHom α) :

⇑(f - g) = ⇑f - ⇑g

@[simp]

theorem CentroidHom.neg_apply {α : Type u_5} [NonUnitalNonAssocRing α] (f : CentroidHom α) (a : α) :

(-f) a = -f a

@[simp]

theorem CentroidHom.sub_apply {α : Type u_5} [NonUnitalNonAssocRing α] (f : CentroidHom α) (g : CentroidHom α) (a : α) :

(f - g) a = f a - g a

@[simp]

theorem CentroidHom.toEnd_intCast {α : Type u_5} [NonUnitalNonAssocRing α] (z : ℤ) :

(↑z).toEnd = ↑z

@[deprecated CentroidHom.toEnd_intCast]

theorem CentroidHom.toEnd_int_cast {α : Type u_5} [NonUnitalNonAssocRing α] (z : ℤ) :

(↑z).toEnd = ↑z

Alias of CentroidHom.toEnd_intCast.

instance CentroidHom.instRing {α : Type u_5} [NonUnitalNonAssocRing α] :

Ring (CentroidHom α)

Equations

CentroidHom.instRing = Function.Injective.ring CentroidHom.toEnd ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev CentroidHom.commRing {α : Type u_5} [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.instRing; CommRing.mk ⋯

Instances For