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.lean.

structure SubStarSemigroup (M : Type v) [Mul M] [Star M] extends Subsemigroup M : 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} (_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 R : Type v

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

• carrier : Set R
• add_mem' {a b : R} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• mul_mem' {a b : R} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• star_mem' {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] [Star R] : SetLike (NonUnitalStarSubsemiring R) R

Equations

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

def NonUnitalStarSubsemiring.ofClass {S : Type u_1} {R : Type u_2} [NonUnitalNonAssocSemiring R] [StarRing R] [SetLike S R] [NonUnitalSubsemiringClass S R] [StarMemClass S R] (s : S) : NonUnitalStarSubsemiring R

The actual NonUnitalStarSubsemiring obtained from an element of a type satisfying NonUnitalSubsemiringClass and StarMemClass.

Equations

• NonUnitalStarSubsemiring.ofClass s = { carrier := ↑s, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, star_mem' := ⋯ }

@[simp]

theorem NonUnitalStarSubsemiring.coe_ofClass {S : Type u_1} {R : Type u_2} [NonUnitalNonAssocSemiring R] [StarRing R] [SetLike S R] [NonUnitalSubsemiringClass S R] [StarMemClass S R] (s : S) : ↑(ofClass s) = ↑s

@[instance 100]

instance NonUnitalStarSubsemiring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallStar {R : Type v} [NonUnitalNonAssocSemiring R] [StarRing R] : CanLift (Set R) (NonUnitalStarSubsemiring R) SetLike.coe fun (s : Set R) => 0 ∈ s ∧ (∀ {x y : R}, x ∈ s → y ∈ s → x + y ∈ s) ∧ (∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x : R}, x ∈ s → star x ∈ s

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

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

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' := ⋯ }