Star subrings

A *-subring is a subring of a *-ring which is closed under *.

structure StarSubsemiring (R : Type v) [NonAssocSemiring R] [Star R] extends Subsemiring R : Type v

A (unital) star subsemiring is a non-associative ring which is closed under the star operation.

• carrier : Set R
• mul_mem' : ∀ {a b : R}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• add_mem' : ∀ {a b : R}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• star_mem' : ∀ {a : R}, a ∈ self.carrier → star a ∈ self.carrier

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

instance StarSubsemiring.setLike {R : Type v} [NonAssocSemiring R] [StarRing R] : SetLike (StarSubsemiring R) R

Equations

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

instance StarSubsemiring.starMemClass {R : Type v} [NonAssocSemiring R] [StarRing R] : StarMemClass (StarSubsemiring R) R

Equations

• ⋯ = ⋯

instance StarSubsemiring.subsemiringClass {R : Type v} [NonAssocSemiring R] [StarRing R] : SubsemiringClass (StarSubsemiring R) R

Equations

• ⋯ = ⋯

instance StarSubsemiring.starRing {R : Type v} [NonAssocSemiring R] [StarRing R] (s : StarSubsemiring R) : StarRing ↥s

Equations

• s.starRing = StarRing.mk ⋯

instance StarSubsemiring.semiring {R : Type v} [NonAssocSemiring R] [StarRing R] (s : StarSubsemiring R) : NonAssocSemiring ↥s

Equations

• s.semiring = s.toNonAssocSemiring

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

theorem StarSubsemiring.ext {R : Type v} [NonAssocSemiring R] [StarRing R] {S T : StarSubsemiring R} (h : ∀ (x : R), x ∈ S ↔ x ∈ T) : S = T

@[simp]

theorem StarSubsemiring.coe_mk {R : Type v} [NonAssocSemiring R] [StarRing R] (S : Subsemiring R) (h : ∀ {a : R}, a ∈ S.carrier → star a ∈ S.carrier) : ↑{ toSubsemiring := S, star_mem' := h } = ↑S

@[simp]

theorem StarSubsemiring.mem_toSubsemiring {R : Type v} [NonAssocSemiring R] [StarRing R] {S : StarSubsemiring R} {x : R} : x ∈ S.toSubsemiring ↔ x ∈ S

@[simp]

theorem StarSubsemiring.coe_toSubsemiring {R : Type v} [NonAssocSemiring R] [StarRing R] (S : StarSubsemiring R) : ↑S.toSubsemiring = ↑S

theorem StarSubsemiring.toSubsemiring_injective {R : Type v} [NonAssocSemiring R] [StarRing R] : Function.Injective StarSubsemiring.toSubsemiring

theorem StarSubsemiring.toSubsemiring_inj {R : Type v} [NonAssocSemiring R] [StarRing R] {S U : StarSubsemiring R} : S.toSubsemiring = U.toSubsemiring ↔ S = U

theorem StarSubsemiring.toSubsemiring_le_iff {R : Type v} [NonAssocSemiring R] [StarRing R] {S₁ S₂ : StarSubsemiring R} : S₁.toSubsemiring ≤ S₂.toSubsemiring ↔ S₁ ≤ S₂

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

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

Equations

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

@[simp]

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

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

def StarSubsemiring.center (R : Type u_1) [NonAssocSemiring R] [StarRing R] : StarSubsemiring R

The center of a semiring R is the set of elements that commute and associate with everything in R

Equations

• StarSubsemiring.center R = { toSubsemiring := Subsemiring.center R, star_mem' := ⋯ }

def SubStarSemigroup.center (A : Type u_1) [Mul A] [StarMul A] : SubStarSemigroup A

The center of magma A is the set of elements that commute and associate with everything in A, here realized as a SubStarSemigroup.

Equations

• SubStarSemigroup.center A = { toSubsemigroup := Subsemigroup.center A, star_mem' := ⋯ }