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
    Instances For

      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.

      Instances For
        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' := }
        Instances For
          @[simp]
          theorem NonUnitalSubsemiring.coe_copy {R : Type u} [NonUnitalNonAssocSemiring R] (S : NonUnitalSubsemiring R) (s : Set R) (hs : s = S) :
          (S.copy s hs) = 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
          Instances For
            @[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) :
            @[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} :

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

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

            Equations
            Instances For

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

              Equations
              Instances For

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

                Equations
                Instances For