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

    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.

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

    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.

    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) :
    ↑(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.

    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