Non-unital Star Subsemirings

In this file we define NonUnitalStarSubsemirings and the usual operations on them.

Implementation

This file is heavily inspired by Mathlib.Algebra.Star.NonUnitalSubalgebra.

structure SubStarSemigroup (M : Type v) [Mul M] [Star M] extends Subsemigroup : Type v

A sub star semigroup is a subset of a magma which is closed under the star

• carrier : Set M
• mul_mem' : ∀ {a b : M}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• star_mem' : ∀ {a : M}, a ∈ self.carrier → star a ∈ self.carrier

  The carrier of a StarSubset is closed under the star operation.

theorem SubStarSemigroup.star_mem' {M : Type v} [Mul M] [Star M] (self : SubStarSemigroup M) {a : M} (_ha : a ∈ self.carrier) : star a ∈ self.carrier

The carrier of a StarSubset is closed under the star operation.

structure NonUnitalStarSubsemiring (R : Type v) [NonUnitalNonAssocSemiring R] [Star R] extends NonUnitalSubsemiring , AddSubmonoid , Subsemigroup , AddSubsemigroup : Type v

A non-unital star subsemiring is a non-unital subsemiring which also is closed under the star operation.

theorem NonUnitalStarSubsemiring.star_mem' {R : Type v} [NonUnitalNonAssocSemiring R] [Star R] (self : NonUnitalStarSubsemiring R) {a : R} (_ha : a ∈ self.carrier) : star a ∈ self.carrier

The carrier of a NonUnitalStarSubsemiring is closed under the star operation.

instance NonUnitalStarSubsemiring.instSetLike {R : Type v} [NonUnitalNonAssocSemiring R] [StarRing R] : SetLike (NonUnitalStarSubsemiring R) R

Equations

• NonUnitalStarSubsemiring.instSetLike = { coe := fun {s : NonUnitalStarSubsemiring R} => s.carrier, coe_injective' := ⋯ }

instance NonUnitalStarSubsemiring.instNonUnitalSubsemiringClass {R : Type v} [NonUnitalNonAssocSemiring R] [StarRing R] : NonUnitalSubsemiringClass (NonUnitalStarSubsemiring R) R

Equations

• ⋯ = ⋯

instance NonUnitalStarSubsemiring.instStarMemClass {R : Type v} [NonUnitalNonAssocSemiring R] [StarRing R] : StarMemClass (NonUnitalStarSubsemiring R) R

Equations

• ⋯ = ⋯

theorem NonUnitalStarSubsemiring.mem_carrier {R : Type v} [NonUnitalNonAssocSemiring R] [StarRing R] {s : NonUnitalStarSubsemiring R} {x : R} : x ∈ s.carrier ↔ x ∈ s

def NonUnitalStarSubsemiring.copy {R : Type v} [NonUnitalNonAssocSemiring R] [StarRing R] (S : NonUnitalStarSubsemiring R) (s : Set R) (hs : s = ↑S) : NonUnitalStarSubsemiring R

Copy of a non-unital star subsemiring with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations

• S.copy s hs = { toNonUnitalSubsemiring := S.copy s hs, star_mem' := ⋯ }

@[simp]

theorem NonUnitalStarSubsemiring.coe_copy {R : Type v} [NonUnitalNonAssocSemiring R] [StarRing R] (S : NonUnitalStarSubsemiring R) (s : Set R) (hs : s = ↑S) : ↑(S.copy s hs) = s

theorem NonUnitalStarSubsemiring.copy_eq {R : Type v} [NonUnitalNonAssocSemiring R] [StarRing R] (S : NonUnitalStarSubsemiring R) (s : Set R) (hs : s = ↑S) : S.copy s hs = S

def NonUnitalStarSubsemiring.center (R : Type u_1) [NonUnitalNonAssocSemiring R] [StarRing R] : NonUnitalStarSubsemiring R

The center of a non-unital non-associative semiring R is the set of elements that commute and associate with everything in R, here realized as non-unital star subsemiring.

Equations

• NonUnitalStarSubsemiring.center R = { toNonUnitalSubsemiring := NonUnitalSubsemiring.center R, star_mem' := ⋯ }