Bundled non-unital subsemirings

We define bundled non-unital subsemirings and some standard constructions: subtype and inclusion ring homomorphisms.

theorem neg_mul_mem {R : Type u_1} {S : Type u_2} [Mul R] [HasDistribNeg R] [SetLike S R] [MulMemClass S R] {s : S} {x y : R} (hx : -x ∈ s) (hy : y ∈ s) : -(x * y) ∈ s

This lemma exists for aesop, as aesop simplifies -x * y to -(x * y) before applying unsafe rules like mul_mem, leading to a dead end in cases where neg_mem does not hold.

theorem mul_neg_mem {R : Type u_1} {S : Type u_2} [Mul R] [HasDistribNeg R] [SetLike S R] [MulMemClass S R] {s : S} {x y : R} (hx : x ∈ s) (hy : -y ∈ s) : -(x * y) ∈ s

This lemma exists for aesop, as aesop simplifies x * -y to -(x * y) before applying unsafe rules like mul_mem, leading to a dead end in cases where neg_mem does not hold.

class NonUnitalSubsemiringClass (S : Type u_1) (R : outParam (Type u)) [NonUnitalNonAssocSemiring R] [SetLike S R] extends AddSubmonoidClass S R : Prop

NonUnitalSubsemiringClass S R states that S is a type of subsets s ⊆ R that are both an additive submonoid and also a multiplicative subsemigroup.

• add_mem {s : S} {a b : R} : a ∈ s → b ∈ s → a + b ∈ s
• zero_mem (s : S) : 0 ∈ s
• mul_mem {s : S} {a b : R} : a ∈ s → b ∈ s → a * b ∈ s

@[instance 100]

instance NonUnitalSubsemiringClass.mulMemClass (S : Type u_1) (R : Type u) [NonUnitalNonAssocSemiring R] [SetLike S R] [h : NonUnitalSubsemiringClass S R] : MulMemClass S R

@[implicit_reducible, instance 75]

instance NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [SetLike S R] [NonUnitalSubsemiringClass S R] (s : S) : NonUnitalNonAssocSemiring ↥s

A non-unital subsemiring of a NonUnitalNonAssocSemiring inherits a NonUnitalNonAssocSemiring structure

@[implicit_reducible, instance 75]

instance NonUnitalSubsemiringClass.toNonUnitalNonAssocCommSemiring {S : Type v} (s : S) {R : Type u_1} [NonUnitalNonAssocCommSemiring R] [SetLike S R] [NonUnitalSubsemiringClass S R] : NonUnitalNonAssocCommSemiring ↥s

A non-unital subsemiring of a NonUnitalNonAssocCommSemiring inherits a NonUnitalNonAssocCommSemiring structure

instance NonUnitalSubsemiringClass.noZeroDivisors {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [SetLike S R] [NonUnitalSubsemiringClass S R] (s : S) [NoZeroDivisors R] : NoZeroDivisors ↥s

def NonUnitalSubsemiringClass.subtype {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [SetLike S R] [NonUnitalSubsemiringClass S R] (s : S) : ↥s →ₙ+* R

The natural non-unital ring hom from a non-unital subsemiring of a non-unital semiring R to R.

@[simp]

theorem NonUnitalSubsemiringClass.subtype_apply {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [SetLike S R] [NonUnitalSubsemiringClass S R] {s : S} (x : ↥s) : (subtype s) x = ↑x

theorem NonUnitalSubsemiringClass.subtype_injective {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [SetLike S R] [NonUnitalSubsemiringClass S R] (s : S) : Function.Injective ⇑(subtype s)

@[simp]

theorem NonUnitalSubsemiringClass.coe_subtype {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [SetLike S R] [NonUnitalSubsemiringClass S R] (s : S) : ⇑(subtype s) = Subtype.val

@[implicit_reducible]

instance NonUnitalSubsemiringClass.toNonUnitalSemiring {S : Type v} (s : S) {R : Type u_1} [NonUnitalSemiring R] [SetLike S R] [NonUnitalSubsemiringClass S R] : NonUnitalSemiring ↥s

A non-unital subsemiring of a NonUnitalSemiring is a NonUnitalSemiring.

@[implicit_reducible]

instance NonUnitalSubsemiringClass.toNonUnitalCommSemiring {S : Type v} (s : S) {R : Type u_1} [NonUnitalCommSemiring R] [SetLike S R] [NonUnitalSubsemiringClass S R] : NonUnitalCommSemiring ↥s

A non-unital subsemiring of a NonUnitalCommSemiring is a NonUnitalCommSemiring.

Note: currently, there are no ordered versions of non-unital rings.

structure NonUnitalSubsemiring (R : Type u) [NonUnitalNonAssocSemiring R] extends AddSubmonoid R, Subsemigroup R : Type u

A non-unital subsemiring of a non-unital semiring R is a subset s that is both an additive submonoid and a semigroup.

• 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

theorem NonUnitalSubsemiring.toAddSubmonoid_injective {R : Type u} [NonUnitalNonAssocSemiring R] : Function.Injective toAddSubmonoid

@[simp]

theorem NonUnitalSubsemiring.toAddSubmonoid_inj {R : Type u} [NonUnitalNonAssocSemiring R] {s t : NonUnitalSubsemiring R} : s.toAddSubmonoid = t.toAddSubmonoid ↔ s = t

@[implicit_reducible]

instance NonUnitalSubsemiring.instSetLike {R : Type u} [NonUnitalNonAssocSemiring R] : SetLike (NonUnitalSubsemiring R) R

theorem NonUnitalSubsemiring.toSubsemigroup_injective {R : Type u} [NonUnitalNonAssocSemiring R] : Function.Injective toSubsemigroup

@[implicit_reducible]

instance NonUnitalSubsemiring.instPartialOrder {R : Type u} [NonUnitalNonAssocSemiring R] : PartialOrder (NonUnitalSubsemiring R)

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

The actual NonUnitalSubsemiring obtained from an element of a NonUnitalSubsemiringClass.

@[simp]

theorem NonUnitalSubsemiring.ofClass_carrier {S : Type u_1} {R : Type u_2} [NonUnitalNonAssocSemiring R] [SetLike S R] [NonUnitalSubsemiringClass S R] (s : S) : ↑(ofClass s) = ↑s

@[instance 100]

instance NonUnitalSubsemiring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMul {R : Type u} [NonUnitalNonAssocSemiring R] : CanLift (Set R) (NonUnitalSubsemiring 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

instance NonUnitalSubsemiring.instNonUnitalSubsemiringClass {R : Type u} [NonUnitalNonAssocSemiring R] : NonUnitalSubsemiringClass (NonUnitalSubsemiring R) R

theorem NonUnitalSubsemiring.mem_carrier {R : Type u} [NonUnitalNonAssocSemiring R] {s : NonUnitalSubsemiring R} {x : R} : x ∈ s.carrier ↔ x ∈ s

theorem NonUnitalSubsemiring.ext {R : Type u} [NonUnitalNonAssocSemiring R] {S T : NonUnitalSubsemiring R} (h : ∀ (x : R), x ∈ S ↔ x ∈ T) : S = T

Two non-unital subsemirings are equal if they have the same elements.

theorem NonUnitalSubsemiring.ext_iff {R : Type u} [NonUnitalNonAssocSemiring R] {S T : NonUnitalSubsemiring R} : S = T ↔ ∀ (x : R), x ∈ S ↔ x ∈ T

def NonUnitalSubsemiring.copy {R : Type u} [NonUnitalNonAssocSemiring R] (S : NonUnitalSubsemiring R) (s : Set R) (hs : s = ↑S) : NonUnitalSubsemiring R

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

@[simp]

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

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

def NonUnitalSubsemiring.mk' {R : Type u} [NonUnitalNonAssocSemiring R] (s : Set R) (sg : Subsemigroup R) (hg : ↑sg = s) (sa : AddSubmonoid R) (ha : ↑sa = s) : NonUnitalSubsemiring R

Construct a NonUnitalSubsemiring R from a set s, a subsemigroup sg, and an additive submonoid sa such that x ∈ s ↔ x ∈ sg ↔ x ∈ sa.

@[simp]

theorem NonUnitalSubsemiring.coe_mk' {R : Type u} [NonUnitalNonAssocSemiring R] {s : Set R} {sg : Subsemigroup R} (hg : ↑sg = s) {sa : AddSubmonoid R} (ha : ↑sa = s) : ↑(NonUnitalSubsemiring.mk' s sg hg sa ha) = s

@[simp]

theorem NonUnitalSubsemiring.mem_mk' {R : Type u} [NonUnitalNonAssocSemiring R] {s : Set R} {sg : Subsemigroup R} (hg : ↑sg = s) {sa : AddSubmonoid R} (ha : ↑sa = s) {x : R} : x ∈ NonUnitalSubsemiring.mk' s sg hg sa ha ↔ x ∈ s

@[simp]

theorem NonUnitalSubsemiring.mk'_toSubsemigroup {R : Type u} [NonUnitalNonAssocSemiring R] {s : Set R} {sg : Subsemigroup R} (hg : ↑sg = s) {sa : AddSubmonoid R} (ha : ↑sa = s) : (NonUnitalSubsemiring.mk' s sg hg sa ha).toSubsemigroup = sg

@[simp]

theorem NonUnitalSubsemiring.mk'_toAddSubmonoid {R : Type u} [NonUnitalNonAssocSemiring R] {s : Set R} {sg : Subsemigroup R} (hg : ↑sg = s) {sa : AddSubmonoid R} (ha : ↑sa = s) : (NonUnitalSubsemiring.mk' s sg hg sa ha).toAddSubmonoid = sa

@[simp]

theorem NonUnitalSubsemiring.coe_zero {R : Type u} [NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R) : ↑0 = 0

@[simp]

theorem NonUnitalSubsemiring.coe_add {R : Type u} [NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R) (x y : ↥s) : ↑(x + y) = ↑x + ↑y

@[simp]

theorem NonUnitalSubsemiring.coe_mul {R : Type u} [NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R) (x y : ↥s) : ↑(x * y) = ↑x * ↑y

Note: currently, there are no ordered versions of non-unital rings.

@[simp]

theorem NonUnitalSubsemiring.mem_toSubsemigroup {R : Type u} [NonUnitalNonAssocSemiring R] {s : NonUnitalSubsemiring R} {x : R} : x ∈ s.toSubsemigroup ↔ x ∈ s

@[simp]

theorem NonUnitalSubsemiring.coe_toSubsemigroup {R : Type u} [NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R) : ↑s.toSubsemigroup = ↑s

@[simp]

theorem NonUnitalSubsemiring.mem_toAddSubmonoid {R : Type u} [NonUnitalNonAssocSemiring R] {s : NonUnitalSubsemiring R} {x : R} : x ∈ s.toAddSubmonoid ↔ x ∈ s

@[simp]

theorem NonUnitalSubsemiring.coe_toAddSubmonoid {R : Type u} [NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R) : ↑s.toAddSubmonoid = ↑s

@[implicit_reducible]

instance NonUnitalSubsemiring.instTop {R : Type u} [NonUnitalNonAssocSemiring R] : Top (NonUnitalSubsemiring R)

The non-unital subsemiring R of the non-unital semiring R.

@[simp]

theorem NonUnitalSubsemiring.mem_top {R : Type u} [NonUnitalNonAssocSemiring R] (x : R) : x ∈ ⊤

@[simp]

theorem NonUnitalSubsemiring.coe_top {R : Type u} [NonUnitalNonAssocSemiring R] : ↑⊤ = Set.univ

@[simp]

theorem NonUnitalSubsemiring.toAddSubmonoid_top {R : Type u} [NonUnitalNonAssocSemiring R] : ⊤.toAddSubmonoid = ⊤

@[simp]

theorem NonUnitalSubsemiring.toAddSubmonoid_eq_top {R : Type u} [NonUnitalNonAssocSemiring R] {S : NonUnitalSubsemiring R} : S.toAddSubmonoid = ⊤ ↔ S = ⊤

@[implicit_reducible]

instance NonUnitalSubsemiring.instBot {R : Type u} [NonUnitalNonAssocSemiring R] : Bot (NonUnitalSubsemiring R)

@[implicit_reducible]

instance NonUnitalSubsemiring.instInhabited {R : Type u} [NonUnitalNonAssocSemiring R] : Inhabited (NonUnitalSubsemiring R)

theorem NonUnitalSubsemiring.coe_bot {R : Type u} [NonUnitalNonAssocSemiring R] : ↑⊥ = {0}

theorem NonUnitalSubsemiring.mem_bot {R : Type u} [NonUnitalNonAssocSemiring R] {x : R} : x ∈ ⊥ ↔ x = 0

@[implicit_reducible]

instance NonUnitalSubsemiring.instMin {R : Type u} [NonUnitalNonAssocSemiring R] : Min (NonUnitalSubsemiring R)

The inf of two non-unital subsemirings is their intersection.

@[simp]

theorem NonUnitalSubsemiring.coe_inf {R : Type u} [NonUnitalNonAssocSemiring R] (p p' : NonUnitalSubsemiring R) : ↑(p ⊓ p') = ↑p ∩ ↑p'

@[simp]

theorem NonUnitalSubsemiring.mem_inf {R : Type u} [NonUnitalNonAssocSemiring R] {p p' : NonUnitalSubsemiring R} {x : R} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

def NonUnitalRingHom.codRestrict {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] {F : Type u_1} [FunLike F R S] [NonUnitalNonAssocSemiring S] [NonUnitalRingHomClass F R S] {S' : Type u_2} [SetLike S' S] [NonUnitalSubsemiringClass S' S] (f : F) (s : S') (h : ∀ (x : R), f x ∈ s) : R →ₙ+* ↥s

Restriction of a non-unital ring homomorphism to a non-unital subsemiring of the codomain.

def NonUnitalRingHom.eqSlocus {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] {F : Type u_1} [FunLike F R S] [NonUnitalNonAssocSemiring S] [NonUnitalRingHomClass F R S] (f g : F) : NonUnitalSubsemiring R

The non-unital subsemiring of elements x : R such that f x = g x

def NonUnitalSubsemiring.inclusion {R : Type u} [NonUnitalNonAssocSemiring R] {S T : NonUnitalSubsemiring R} (h : S ≤ T) : ↥S →ₙ+* ↥T

The non-unital ring homomorphism associated to an inclusion of non-unital subsemirings.