Bundled subsemirings

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

class AddSubmonoidWithOneClass (S : Type u_1) (R : outParam (Type u_2)) [AddMonoidWithOne R] [SetLike S R] extends AddSubmonoidClass S R, OneMemClass S R : Prop

AddSubmonoidWithOneClass S R says S is a type of subsets s ≤ R that contain 0, 1, and are closed under (+)

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

@[simp]

theorem natCast_mem {S : Type u_1} {R : Type u_2} [AddMonoidWithOne R] [SetLike S R] (s : S) [AddSubmonoidWithOneClass S R] (n : ℕ) : ↑n ∈ s

@[simp]

theorem ofNat_mem {S : Type u_1} {R : Type u_2} [AddMonoidWithOne R] [SetLike S R] [AddSubmonoidWithOneClass S R] (s : S) (n : ℕ) [n.AtLeastTwo] : OfNat.ofNat n ∈ s

@[instance_reducible, instance 74]

instance AddSubmonoidWithOneClass.toAddMonoidWithOne {S : Type u_1} {R : Type u_2} [AddMonoidWithOne R] [SetLike S R] (s : S) [AddSubmonoidWithOneClass S R] : AddMonoidWithOne ↥s

Equations

• AddSubmonoidWithOneClass.toAddMonoidWithOne s = { natCast := fun (n : ℕ) => ⟨↑n, ⋯⟩, toAddMonoid := AddSubmonoidClass.toAddMonoid s, one := ⟨1, ⋯⟩, natCast_zero := ⋯, natCast_succ := ⋯ }

class SubsemiringClass (S : Type u_1) (R : outParam (Type u)) [NonAssocSemiring R] [SetLike S R] extends SubmonoidClass S R, AddSubmonoidClass S R : Prop

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

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

@[instance 100]

instance SubsemiringClass.addSubmonoidWithOneClass (S : Type u_1) (R : Type u) {x✝ : NonAssocSemiring R} [SetLike S R] [h : SubsemiringClass S R] : AddSubmonoidWithOneClass S R

@[instance 100]

instance SubsemiringClass.nonUnitalSubsemiringClass (S : Type u_1) (R : Type u) [NonAssocSemiring R] [SetLike S R] [SubsemiringClass S R] : NonUnitalSubsemiringClass S R

@[instance_reducible, instance 75]

instance SubsemiringClass.toNonAssocSemiring {R : Type u} {S : Type v} [NonAssocSemiring R] [SetLike S R] [hSR : SubsemiringClass S R] (s : S) : NonAssocSemiring ↥s

A subsemiring of a NonAssocSemiring inherits a NonAssocSemiring structure

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible, instance 75]

instance SubsemiringClass.toNonAssocCommSemiring {S : Type v} (s : S) {R : Type u_1} [NonAssocCommSemiring R] [SetLike S R] [SubsemiringClass S R] : NonAssocCommSemiring ↥s

A subsemiring of a NonAssocCommSemiring inherits a NonAssocCommSemiring structure

Equations

• SubsemiringClass.toNonAssocCommSemiring s = { toNonAssocSemiring := SubsemiringClass.toNonAssocSemiring s, mul_comm := ⋯ }

instance SubsemiringClass.nontrivial {R : Type u} {S : Type v} [NonAssocSemiring R] [SetLike S R] [hSR : SubsemiringClass S R] (s : S) [Nontrivial R] : Nontrivial ↥s

instance SubsemiringClass.noZeroDivisors {R : Type u} {S : Type v} [NonAssocSemiring R] [SetLike S R] [hSR : SubsemiringClass S R] (s : S) [NoZeroDivisors R] : NoZeroDivisors ↥s

def SubsemiringClass.subtype {R : Type u} {S : Type v} [NonAssocSemiring R] [SetLike S R] [hSR : SubsemiringClass S R] (s : S) : ↥s →+* R

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

Equations

• SubsemiringClass.subtype s = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

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

@[simp]

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

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

@[instance_reducible, instance 75]

instance SubsemiringClass.toSemiring {S : Type v} (s : S) {R : Type u_1} [Semiring R] [SetLike S R] [SubsemiringClass S R] : Semiring ↥s

A subsemiring of a Semiring is a Semiring.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance SubsemiringClass.toCommSemiring {S : Type v} (s : S) {R : Type u_1} [CommSemiring R] [SetLike S R] [SubsemiringClass S R] : CommSemiring ↥s

A subsemiring of a CommSemiring is a CommSemiring.

Equations

• SubsemiringClass.toCommSemiring s = { toSemiring := SubsemiringClass.toSemiring s, mul_comm := ⋯ }

structure Subsemiring (R : Type u) [NonAssocSemiring R] extends Submonoid R, AddSubmonoid R : Type u

A subsemiring of a semiring R is a subset s that is both a multiplicative and an additive submonoid.

• 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

@[instance_reducible]

instance Subsemiring.instSetLike {R : Type u} [NonAssocSemiring R] : SetLike (Subsemiring R) R

Equations

• Subsemiring.instSetLike = { coe := fun (s : Subsemiring R) => s.carrier, coe_injective := ⋯ }

@[instance_reducible]

instance Subsemiring.instPartialOrder {R : Type u} [NonAssocSemiring R] : PartialOrder (Subsemiring R)

Equations

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

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

The actual Subsemiring obtained from an element of a SubsemiringClass.

Equations

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

@[simp]

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

@[instance 100]

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

instance Subsemiring.instSubsemiringClass {R : Type u} [NonAssocSemiring R] : SubsemiringClass (Subsemiring R) R

@[reducible]

def Subsemiring.toNonUnitalSubsemiring {R : Type u} [NonAssocSemiring R] (S : Subsemiring R) : NonUnitalSubsemiring R

Turn a Subsemiring into a NonUnitalSubsemiring by forgetting that it contains 1.

Equations

• S.toNonUnitalSubsemiring = { carrier := S.carrier, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯ }

@[simp]

theorem Subsemiring.mem_toSubmonoid {R : Type u} [NonAssocSemiring R] {s : Subsemiring R} {x : R} : x ∈ s.toSubmonoid ↔ x ∈ s

@[simp]

theorem Subsemiring.mem_toNonUnitalSubsemiring {R : Type u} [NonAssocSemiring R] {S : Subsemiring R} {x : R} : x ∈ S.toNonUnitalSubsemiring ↔ x ∈ S

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

@[simp]

theorem Subsemiring.coe_toNonUnitalSubsemiring {R : Type u} [NonAssocSemiring R] (S : Subsemiring R) : ↑S.toNonUnitalSubsemiring = ↑S

@[simp]

theorem Subsemiring.mem_mk {R : Type u} [NonAssocSemiring R] {toSubmonoid : Submonoid R} (add_mem : ∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier) (zero_mem : 0 ∈ toSubmonoid.carrier) {x : R} : x ∈ { toSubmonoid := toSubmonoid, add_mem' := add_mem, zero_mem' := zero_mem } ↔ x ∈ toSubmonoid

@[simp]

theorem Subsemiring.coe_set_mk {R : Type u} [NonAssocSemiring R] {toSubmonoid : Submonoid R} (add_mem : ∀ {a b : R}, a ∈ toSubmonoid.carrier → b ∈ toSubmonoid.carrier → a + b ∈ toSubmonoid.carrier) (zero_mem : 0 ∈ toSubmonoid.carrier) : ↑{ toSubmonoid := toSubmonoid, add_mem' := add_mem, zero_mem' := zero_mem } = ↑toSubmonoid

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

Two subsemirings are equal if they have the same elements.

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

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

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

Equations

• S.copy s hs = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

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

@[simp]

theorem Subsemiring.copy_toSubmonoid {R : Type u} [NonAssocSemiring R] (S : Subsemiring R) (s : Set R) (hs : s = ↑S) : (S.copy s hs).toSubmonoid = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯ }

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

theorem Subsemiring.toSubmonoid_injective {R : Type u} [NonAssocSemiring R] : Function.Injective toSubmonoid

theorem Subsemiring.toAddSubmonoid_injective {R : Type u} [NonAssocSemiring R] : Function.Injective toAddSubmonoid

theorem Subsemiring.toNonUnitalSubsemiring_injective {R : Type u} [NonAssocSemiring R] : Function.Injective toNonUnitalSubsemiring

theorem Subsemiring.toNonUnitalSubsemiring_inj {R : Type u} [NonAssocSemiring R] {S₁ S₂ : Subsemiring R} : S₁.toNonUnitalSubsemiring = S₂.toNonUnitalSubsemiring ↔ S₁ = S₂

theorem Subsemiring.one_mem_toNonUnitalSubsemiring {R : Type u} [NonAssocSemiring R] (S : Subsemiring R) : 1 ∈ S.toNonUnitalSubsemiring

def Subsemiring.mk' {R : Type u} [NonAssocSemiring R] (s : Set R) (sm : Submonoid R) (hm : ↑sm = s) (sa : AddSubmonoid R) (ha : ↑sa = s) : Subsemiring R

Construct a Subsemiring R from a set s, a submonoid sm, and an additive submonoid sa such that x ∈ s ↔ x ∈ sm ↔ x ∈ sa.

Equations

• Subsemiring.mk' s sm hm sa ha = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem Subsemiring.coe_mk' {R : Type u} [NonAssocSemiring R] (s : Set R) (sm : Submonoid R) (hm : ↑sm = s) (sa : AddSubmonoid R) (ha : ↑sa = s) : ↑(Subsemiring.mk' s sm hm sa ha) = s

@[simp]

theorem Subsemiring.mem_mk' {R : Type u} [NonAssocSemiring R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubmonoid R} (ha : ↑sa = s) {x : R} : x ∈ Subsemiring.mk' s sm hm sa ha ↔ x ∈ s

@[simp]

theorem Subsemiring.mk'_toSubmonoid {R : Type u} [NonAssocSemiring R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubmonoid R} (ha : ↑sa = s) : (Subsemiring.mk' s sm hm sa ha).toSubmonoid = sm

@[simp]

theorem Subsemiring.mk'_toAddSubmonoid {R : Type u} [NonAssocSemiring R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubmonoid R} (ha : ↑sa = s) : (Subsemiring.mk' s sm hm sa ha).toAddSubmonoid = sa

theorem Subsemiring.one_mem {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) : 1 ∈ s

A subsemiring contains the semiring's 1.

theorem Subsemiring.zero_mem {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) : 0 ∈ s

A subsemiring contains the semiring's 0.

theorem Subsemiring.mul_mem {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) {x y : R} : x ∈ s → y ∈ s → x * y ∈ s

A subsemiring is closed under multiplication.

theorem Subsemiring.add_mem {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) {x y : R} : x ∈ s → y ∈ s → x + y ∈ s

A subsemiring is closed under addition.

@[instance_reducible]

instance Subsemiring.toNonAssocSemiring {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) : NonAssocSemiring ↥s

A subsemiring of a NonAssocSemiring inherits a NonAssocSemiring structure

Equations

• s.toNonAssocSemiring = SubsemiringClass.toNonAssocSemiring s

@[simp]

theorem Subsemiring.coe_one {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) : ↑1 = 1

@[simp]

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

@[simp]

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

@[simp]

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

instance Subsemiring.nontrivial {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) [Nontrivial R] : Nontrivial ↥s

theorem Subsemiring.pow_mem {R : Type u_1} [Semiring R] (s : Subsemiring R) {x : R} (hx : x ∈ s) (n : ℕ) : x ^ n ∈ s

instance Subsemiring.noZeroDivisors {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) [NoZeroDivisors R] : NoZeroDivisors ↥s

@[instance_reducible]

instance Subsemiring.toSemiring {R : Type u_1} [Semiring R] (s : Subsemiring R) : Semiring ↥s

A subsemiring of a Semiring is a Semiring.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Subsemiring.coe_pow {R : Type u_1} [Semiring R] (s : Subsemiring R) (x : ↥s) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

@[instance_reducible]

instance Subsemiring.toCommSemiring {R : Type u_1} [CommSemiring R] (s : Subsemiring R) : CommSemiring ↥s

A subsemiring of a CommSemiring is a CommSemiring.

Equations

• s.toCommSemiring = { toSemiring := s.toSemiring, mul_comm := ⋯ }

def Subsemiring.subtype {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) : ↥s →+* R

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

Equations

• s.subtype = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Subsemiring.subtype_apply {R : Type u} [NonAssocSemiring R] {s : Subsemiring R} (x : ↥s) : s.subtype x = ↑x

theorem Subsemiring.subtype_injective {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) : Function.Injective ⇑s.subtype

@[simp]

theorem Subsemiring.coe_subtype {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) : ⇑s.subtype = Subtype.val

theorem Subsemiring.nsmul_mem {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) {x : R} (hx : x ∈ s) (n : ℕ) : n • x ∈ s

@[simp]

theorem Subsemiring.coe_toSubmonoid {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) : ↑s.toSubmonoid = ↑s

@[simp]

theorem Subsemiring.coe_carrier_toSubmonoid {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) : s.carrier = ↑s

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

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

@[instance_reducible]

instance Subsemiring.instTop {R : Type u} [NonAssocSemiring R] : Top (Subsemiring R)

The subsemiring R of the semiring R.

Equations

• Subsemiring.instTop = { top := let __src := ⊤; have __src_1 := ⊤; { toSubmonoid := __src, add_mem' := ⋯, zero_mem' := ⋯ } }

@[simp]

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

@[simp]

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

@[instance_reducible]

instance Subsemiring.instMin {R : Type u} [NonAssocSemiring R] : Min (Subsemiring R)

The inf of two subsemirings is their intersection.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

def RingHom.domRestrict {R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S] {σR : Type u_1} [SetLike σR R] [SubsemiringClass σR R] (f : R →+* S) (s : σR) : ↥s →+* S

Restriction of a ring homomorphism to a subsemiring of the domain.

Equations

• f.domRestrict s = f.comp (SubsemiringClass.subtype s)

@[simp]

theorem RingHom.restrict_apply {R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S] {σR : Type u_1} [SetLike σR R] [SubsemiringClass σR R] (f : R →+* S) {s : σR} (x : ↥s) : (f.domRestrict s) x = f ↑x

def RingHom.eqLocusS {R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S] (f g : R →+* S) : Subsemiring R

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

Equations

• f.eqLocusS g = { carrier := {x : R | f x = g x}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }

@[simp]

theorem RingHom.mem_eqLocusS {R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S] {f g : R →+* S} {x : R} : x ∈ f.eqLocusS g ↔ f x = g x

@[simp]

theorem RingHom.eqLocusS_same {R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) : f.eqLocusS f = ⊤

def NonUnitalSubsemiring.toSubsemiring {R : Type u} [NonAssocSemiring R] (S : NonUnitalSubsemiring R) (h1 : 1 ∈ S) : Subsemiring R

Turn a non-unital subsemiring containing 1 into a subsemiring.

Equations

• S.toSubsemiring h1 = { carrier := S.carrier, mul_mem' := ⋯, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ }

theorem Subsemiring.toNonUnitalSubsemiring_toSubsemiring {R : Type u} [NonAssocSemiring R] (S : Subsemiring R) : S.toNonUnitalSubsemiring.toSubsemiring ⋯ = S

theorem NonUnitalSubsemiring.toSubsemiring_toNonUnitalSubsemiring {R : Type u} [NonAssocSemiring R] (S : NonUnitalSubsemiring R) (h1 : 1 ∈ S) : (S.toSubsemiring h1).toNonUnitalSubsemiring = S