Documentation

Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Bundled non-unital subsemirings #

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

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

Instances
@[instance 75]

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

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

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

Equations
@[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
@[deprecated NonUnitalSubsemiringClass.coe_subtype (since := "2025-02-18")]

Alias of NonUnitalSubsemiringClass.coe_subtype.

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

The actual NonUnitalSubsemiring obtained from an element of a NonUnitalSubsemiringClass.

Equations
@[simp]
@[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 sy sx + y s) ∀ {x y : R}, x sy sx * y 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

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

Equations
  • S.copy s hs = { carrier := s, add_mem' := , zero_mem' := , mul_mem' := }
@[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) :

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

Equations
@[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) :
@[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) :
@[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.

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

Equations
Equations

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem NonUnitalSubsemiring.coe_inf {R : Type u} [NonUnitalNonAssocSemiring R] (p p' : NonUnitalSubsemiring R) :
(pp') = p p'
@[simp]
theorem NonUnitalSubsemiring.mem_inf {R : Type u} [NonUnitalNonAssocSemiring R] {p p' : NonUnitalSubsemiring R} {x : R} :
x pp' 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.

Equations

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

Equations

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

Equations