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 , ZeroHom , AddHom :

Type u_6

The type of centroid homomorphisms from α to α.

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) (α : outParam (Type u_7)) [NonUnitalNonAssocSemiring α] [FunLike F α α] extends AddMonoidHomClass , AddHomClass , ZeroHomClass :

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

You should extend this class when you extend CentroidHom.

Instances

theorem CentroidHomClass.map_mul_left {F : Type u_6} {α : outParam (Type u_7)} :

∀ {inst : NonUnitalNonAssocSemiring α} {inst_1 : 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} {α : outParam (Type u_7)} :

∀ {inst : NonUnitalNonAssocSemiring α} {inst_1 : 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

⋯ = ⋯

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 = { 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 α = { toAddMonoidHom := AddMonoidHom.id α, 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 = { toAddMonoidHom := g.comp f.toAddMonoidHom, 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 ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

@[simp]

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

(CentroidHom.toEndRingHom α) f = f.toEnd

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

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

@[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

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.centerToCentroidCenter {α : Type u_5} [NonUnitalNonAssocSemiring α] :

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

The canonical homomorphism from the center into the center of the centroid

Equations

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

Instances For

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

FunLike (↥(Subsemiring.center (CentroidHom α))) α α

Equations

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

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

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

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

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

The canonical homomorphism from the center into the centroid

Equations

CentroidHom.centerToCentroid = (SubsemiringClass.subtype (Subsemiring.center (CentroidHom α))).toNonUnitalRingHom.comp CentroidHom.centerToCentroidCenter

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

CentroidHom.centerIsoCentroid = { toFun := CentroidHom.centerToCentroid.toFun, invFun := fun (T : CentroidHom α) => ⟨T 1, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

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 = CommRing.mk ⋯

Instances For