Centroid homomorphisms on Star Rings

When a (non unital, non-associative) semi-ring 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 semi-ring into the centre of the centroid becomes a *-homomorphism.

Tags

centroid

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

Equations

• CentroidHom.instStar = { star := fun (f : CentroidHom α) => { toFun := fun (a : α) => star (f (star a)), map_zero' := ⋯, map_add' := ⋯, map_mul_left' := ⋯, map_mul_right' := ⋯ } }

@[simp]

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

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

Equations

• CentroidHom.instStarAddMonoid = StarAddMonoid.mk ⋯

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

Equations

• CentroidHom.instStarSubtypeMemSubsemiringCenter = { star := fun (f : ↥(Subsemiring.center (CentroidHom α))) => ⟨star ↑f, ⋯⟩ }

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

Equations

• CentroidHom.instStarAddMonoidCenter = StarAddMonoid.mk ⋯

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

Equations

• CentroidHom.instStarRingSubtypeMemSubsemiringCenter = StarRing.mk ⋯

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

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

Equations

• CentroidHom.centerStarEmbedding = { toNonUnitalRingHom := (SubsemiringClass.subtype (Subsemiring.center (CentroidHom α))).toNonUnitalRingHom, map_star' := ⋯ }

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.

Equations

• CentroidHom.starCenterToCentroidCenter = { toNonUnitalRingHom := CentroidHom.centerToCentroidCenter, map_star' := ⋯ }

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

The canonical homomorphism from the center into the centroid

Equations

• CentroidHom.starCenterToCentroid = CentroidHom.centerStarEmbedding.comp CentroidHom.starCenterToCentroidCenter

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.

Equations

• CentroidHom.starRingOfCommCentroidHom mul_comm = StarRing.mk ⋯

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.

Equations

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

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