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_reducible]

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

Equations

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

@[instance_reducible]

instance StarSubsemiring.instPartialOrder {R : Type v} [NonAssocSemiring R] [Star R] : PartialOrder (StarSubsemiring R)

Equations

• StarSubsemiring.instPartialOrder = PartialOrder.ofSetLike (StarSubsemiring R)

def StarSubsemiring.ofClass {S : Type u_1} {R : Type u_2} [NonAssocSemiring R] [SetLike S R] [StarRing R] [SubsemiringClass S R] [StarMemClass S R] (s : S) : StarSubsemiring R

The actual StarSubsemiring obtained from an element of a StarSubsemiringClass.

Equations

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

@[simp]

theorem StarSubsemiring.coe_ofClass {S : Type u_1} {R : Type u_2} [NonAssocSemiring R] [SetLike S R] [StarRing R] [SubsemiringClass S R] [StarMemClass S R] (s : S) : ↑(ofClass s) = ↑s

@[instance 100]

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

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

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

@[instance_reducible]

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

Equations

• s.starRing = { toStar := StarMemClass.instStar s, star_involutive := ⋯, star_mul := ⋯, star_add := ⋯ }

@[instance_reducible]

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

theorem StarSubsemiring.ext_iff {R : Type v} [NonAssocSemiring R] [StarRing R] {S T : StarSubsemiring R} : S = T ↔ ∀ (x : R), x ∈ S ↔ x ∈ 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 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' := ⋯ }