Documentation

Mathlib.Algebra.Ring.Subsemiring.Defs

Bundled subsemirings #

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

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

Instances
    theorem natCast_mem {S : Type u_1} {R : Type u_2} [AddMonoidWithOne R] [SetLike S R] (s : S) [AddSubmonoidWithOneClass S R] (n : ) :
    n s
    theorem ofNat_mem {S : Type u_1} {R : Type u_2} [AddMonoidWithOne R] [SetLike S R] [AddSubmonoidWithOneClass S R] (s : S) (n : ) [n.AtLeastTwo] :
    @[instance 74]
    Equations
      class SubsemiringClass (S : Type u_1) (R : outParam (Type u)) [NonAssocSemiring R] [SetLike S R] extends SubmonoidClass S R, AddSubmonoidClass S R :

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

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

        A subsemiring of a NonAssocSemiring inherits a NonAssocSemiring structure

        Equations
          instance SubsemiringClass.nontrivial {R : Type u} {S : Type v} [NonAssocSemiring R] [SetLike S R] [hSR : SubsemiringClass S R] (s : S) [Nontrivial R] :
          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
            Instances For
              @[simp]
              theorem SubsemiringClass.coe_subtype {R : Type u} {S : Type v} [NonAssocSemiring R] [SetLike S R] [hSR : SubsemiringClass S R] (s : S) :
              @[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
              @[instance 75]
              instance SubsemiringClass.toSemiring {S : Type v} (s : S) {R : Type u_1} [Semiring R] [SetLike S R] [SubsemiringClass S R] :

              A subsemiring of a Semiring is a Semiring.

              Equations
                @[simp]
                theorem SubsemiringClass.coe_pow {S : Type v} (s : S) {R : Type u_1} [Monoid R] [SetLike S R] [SubmonoidClass S R] (x : s) (n : ) :
                ↑(x ^ n) = x ^ n
                instance SubsemiringClass.toCommSemiring {S : Type v} (s : S) {R : Type u_1} [CommSemiring R] [SetLike S R] [SubsemiringClass S R] :

                A subsemiring of a CommSemiring is a CommSemiring.

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

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

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

                    The actual Subsemiring obtained from an element of a SubsemiringClass.

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

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

                        Equations
                          Instances For
                            @[simp]
                            theorem Subsemiring.mem_toSubmonoid {R : Type u} [NonAssocSemiring R] {s : Subsemiring R} {x : R} :
                            theorem Subsemiring.mem_carrier {R : Type u} [NonAssocSemiring R] {s : Subsemiring R} {x : R} :
                            x s.carrier x s
                            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) :

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

                            Equations
                              Instances For
                                @[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' := }
                                @[simp]
                                theorem Subsemiring.coe_copy {R : Type u} [NonAssocSemiring R] (S : Subsemiring R) (s : Set R) (hs : s = S) :
                                (S.copy s hs) = s
                                theorem Subsemiring.copy_eq {R : Type u} [NonAssocSemiring R] (S : Subsemiring R) (s : Set R) (hs : s = S) :
                                S.copy s hs = S
                                def Subsemiring.mk' {R : Type u} [NonAssocSemiring R] (s : Set R) (sm : Submonoid R) (hm : sm = s) (sa : AddSubmonoid R) (ha : sa = s) :

                                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
                                  Instances For
                                    @[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 sy sx * y s

                                    A subsemiring is closed under multiplication.

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

                                    A subsemiring is closed under addition.

                                    A subsemiring of a NonAssocSemiring inherits a NonAssocSemiring structure

                                    Equations
                                      @[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
                                      theorem Subsemiring.pow_mem {R : Type u_1} [Semiring R] (s : Subsemiring R) {x : R} (hx : x s) (n : ) :
                                      x ^ n s
                                      instance Subsemiring.toSemiring {R : Type u_1} [Semiring R] (s : Subsemiring R) :

                                      A subsemiring of a Semiring is a Semiring.

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

                                        A subsemiring of a CommSemiring is a CommSemiring.

                                        Equations

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

                                          Equations
                                            Instances For
                                              @[simp]
                                              theorem Subsemiring.subtype_apply {R : Type u} [NonAssocSemiring R] {s : Subsemiring R} (x : s) :
                                              s.subtype x = x
                                              theorem Subsemiring.nsmul_mem {R : Type u} [NonAssocSemiring R] (s : Subsemiring R) {x : R} (hx : x s) (n : ) :
                                              n x s
                                              @[simp]

                                              The subsemiring R of the semiring R.

                                              Equations
                                                @[simp]
                                                theorem Subsemiring.mem_top {R : Type u} [NonAssocSemiring R] (x : R) :

                                                The inf of two subsemirings is their intersection.

                                                Equations
                                                  @[simp]
                                                  theorem Subsemiring.coe_inf {R : Type u} [NonAssocSemiring R] (p p' : Subsemiring R) :
                                                  (pp') = p p'
                                                  @[simp]
                                                  theorem Subsemiring.mem_inf {R : Type u} [NonAssocSemiring R] {p p' : Subsemiring R} {x : R} :
                                                  x pp' 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
                                                    Instances For
                                                      @[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) :

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

                                                      Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem RingHom.eqLocusS_same {R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) :

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

                                                          Equations
                                                            Instances For