Centroid homomorphisms on Star Rings

When a (nonunital, non-associative) semiring is equipped with an involutive automorphism the center of the centroid becomes a star ring in a natural way and the natural mapping of the centre of the semiring into the centre of the centroid becomes a *-homomorphism.

Tags

centroid

@[implicit_reducible]

instance CentroidHom.instStar {α : Type u_1} [NonUnitalNonAssocSemiring α] [StarRing α] : Star (CentroidHom α)

@[simp]

theorem CentroidHom.star_apply {α : Type u_1} [NonUnitalNonAssocSemiring α] [StarRing α] (f : CentroidHom α) (a : α) : (star f) a = star (f (star a))

@[implicit_reducible]

instance CentroidHom.instStarAddMonoid {α : Type u_1} [NonUnitalNonAssocSemiring α] [StarRing α] : StarAddMonoid (CentroidHom α)

@[implicit_reducible]

instance CentroidHom.instStarSubtypeMemSubsemiringCenter {α : Type u_1} [NonUnitalNonAssocSemiring α] [StarRing α] : Star ↥(Subsemiring.center (CentroidHom α))

@[implicit_reducible]

instance CentroidHom.instStarAddMonoidCenter {α : Type u_1} [NonUnitalNonAssocSemiring α] [StarRing α] : StarAddMonoid ↥(Subsemiring.center (CentroidHom α))

@[implicit_reducible]

instance CentroidHom.instStarRingSubtypeMemSubsemiringCenter {α : Type u_1} [NonUnitalNonAssocSemiring α] [StarRing α] : StarRing ↥(Subsemiring.center (CentroidHom α))

def CentroidHom.centerStarEmbedding {α : Type u_1} [NonUnitalNonAssocSemiring α] [StarRing α] : ↥(Subsemiring.center (CentroidHom α)) →⋆ₙ+* CentroidHom α

The canonical *-homomorphism embedding the center of CentroidHom α into CentroidHom α.

theorem CentroidHom.star_centerToCentroidCenter {α : Type u_1} [NonUnitalNonAssocSemiring α] [StarRing α] (z : ↥(NonUnitalStarSubsemiring.center α)) : star (centerToCentroidCenter z) = centerToCentroidCenter (star z)

def CentroidHom.starCenterToCentroidCenter {α : Type u_1} [NonUnitalNonAssocSemiring α] [StarRing α] : ↥(NonUnitalStarSubsemiring.center α) →⋆ₙ+* ↥(Subsemiring.center (CentroidHom α))

The canonical *-homomorphism from the center of a non-unital, non-associative *-semiring into the center of its centroid.

def CentroidHom.starCenterToCentroid {α : Type u_1} [NonUnitalNonAssocSemiring α] [StarRing α] : ↥(NonUnitalStarSubsemiring.center α) →⋆ₙ+* CentroidHom α

The canonical homomorphism from the center into the centroid

theorem CentroidHom.starCenterToCentroid_apply {α : Type u_1} [NonUnitalNonAssocSemiring α] [StarRing α] (z : ↥(NonUnitalStarSubsemiring.center α)) (a : α) : (starCenterToCentroid z) a = ↑z * a

@[reducible]

def CentroidHom.starRingOfCommCentroidHom {α : Type u_1} [NonUnitalNonAssocSemiring α] [StarRing α] (mul_comm : Std.Commutative fun (x1 x2 : CentroidHom α) => x1 * x2) : StarRing (CentroidHom α)

Let α be a star ring with commutative centroid. Then the centroid is a star ring.

def CentroidHom.starCenterIsoCentroid {α : Type u_1} [NonAssocSemiring α] [StarRing α] : ↥(StarSubsemiring.center α) ≃⋆+* CentroidHom α

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

@[simp]

theorem CentroidHom.starCenterIsoCentroid_apply {α : Type u_1} [NonAssocSemiring α] [StarRing α] (a : ↥(NonUnitalStarSubsemiring.center α)) : starCenterIsoCentroid a = starCenterToCentroid a

@[simp]

theorem CentroidHom.starCenterIsoCentroid_symm_apply_coe {α : Type u_1} [NonAssocSemiring α] [StarRing α] (T : CentroidHom α) : ↑(starCenterIsoCentroid.symm T) = T 1