Documentation

Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Bundled non-unital subsemirings #

We define bundled non-unital subsemirings and some standard constructions: CompleteLattice structure, subtype and inclusion ring homomorphisms, non-unital subsemiring map, comap and range (srange) of a NonUnitalRingHom etc.

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

  • add_mem : ∀ {s : S} {a b : R}, a sb sa + b s
  • zero_mem : ∀ (s : S), 0 s
  • mul_mem : ∀ {s : S} {a b : R}, a sb sa * b s
Instances
    theorem NonUnitalSubsemiringClass.mul_mem {S : Type u_1} {R : outParam (Type u)} :
    ∀ {inst : NonUnitalNonAssocSemiring R} {inst_1 : SetLike S R} [self : NonUnitalSubsemiringClass S R] {s : S} {a b : R}, a sb sa * b s
    @[instance 100]
    Equations
    • =

    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.

      • carrier : Set R
      • add_mem' : ∀ {a b : R}, a self.carrierb self.carriera + b self.carrier
      • zero_mem' : 0 self.carrier
      • mul_mem' : ∀ {a b : R}, a self.carrierb self.carriera * b self.carrier

        The product of two elements of a subsemigroup belongs to the subsemigroup.

      Instances For
        @[reducible]

        Reinterpret a NonUnitalSubsemiring as a Subsemigroup.

        Equations
        • self.toSubsemigroup = { carrier := self.carrier, mul_mem' := }
        Instances For
          Equations
          • NonUnitalSubsemiring.instSetLike = { coe := fun (s : NonUnitalSubsemiring R) => s.carrier, coe_injective' := }
          theorem NonUnitalSubsemiring.ext {R : Type u} [NonUnitalNonAssocSemiring R] {S : NonUnitalSubsemiring R} {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
            theorem NonUnitalSubsemiring.copy_eq {R : Type u} [NonUnitalNonAssocSemiring R] (S : NonUnitalSubsemiring R) (s : Set R) (hs : s = S) :
            S.copy s hs = S
            theorem NonUnitalSubsemiring.toSubsemigroup_mono {R : Type u} [NonUnitalNonAssocSemiring R] :
            Monotone NonUnitalSubsemiring.toSubsemigroup
            theorem NonUnitalSubsemiring.toAddSubmonoid_mono {R : Type u} [NonUnitalNonAssocSemiring R] :
            Monotone NonUnitalSubsemiring.toAddSubmonoid
            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
            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) :
              (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) :
              (NonUnitalSubsemiring.mk' s sg hg sa ha).toSubsemigroup = sg
              @[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) :
              (NonUnitalSubsemiring.mk' s sg hg sa ha).toAddSubmonoid = sa
              @[simp]
              theorem NonUnitalSubsemiring.coe_add {R : Type u} [NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R) (x : s) (y : s) :
              (x + y) = x + y
              @[simp]
              theorem NonUnitalSubsemiring.coe_mul {R : Type u} [NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R) (x : s) (y : s) :
              (x * y) = x * y

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

              @[simp]
              theorem NonUnitalSubsemiring.mem_toSubsemigroup {R : Type u} [NonUnitalNonAssocSemiring R] {s : NonUnitalSubsemiring R} {x : R} :
              x s.toSubsemigroup x s
              @[simp]
              @[simp]
              theorem NonUnitalSubsemiring.mem_toAddSubmonoid {R : Type u} [NonUnitalNonAssocSemiring R] {s : NonUnitalSubsemiring R} {x : R} :
              x s.toAddSubmonoid x s
              @[simp]

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

              Equations
              • NonUnitalSubsemiring.instTop = { top := let __src := ; let __src_1 := ; { carrier := __src.carrier, add_mem' := , zero_mem' := , mul_mem' := } }
              @[simp]
              @[simp]
              theorem NonUnitalSubsemiring.topEquiv_symm_apply_coe {R : Type u} [NonUnitalNonAssocSemiring R] (x : R) :
              (NonUnitalSubsemiring.topEquiv.symm x) = x
              @[simp]
              theorem NonUnitalSubsemiring.topEquiv_apply {R : Type u} [NonUnitalNonAssocSemiring R] (x : ) :
              NonUnitalSubsemiring.topEquiv x = x

              The ring equiv between the top element of NonUnitalSubsemiring R and R.

              Equations
              • NonUnitalSubsemiring.topEquiv = { toEquiv := Subsemigroup.topEquiv.toEquiv, map_mul' := , map_add' := }
              Instances For

                The preimage of a non-unital subsemiring along a non-unital ring homomorphism is a non-unital subsemiring.

                Equations
                Instances For

                  The image of a non-unital subsemiring along a ring homomorphism is a non-unital subsemiring.

                  Equations
                  Instances For
                    @[simp]
                    theorem NonUnitalSubsemiring.mem_map {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [FunLike F R S] [NonUnitalRingHomClass F R S] {f : F} {s : NonUnitalSubsemiring R} {y : S} :
                    y NonUnitalSubsemiring.map f s xs, f x = y

                    A non-unital subsemiring is isomorphic to its image under an injective function

                    Equations
                    • s.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑s) hf, map_mul' := , map_add' := }
                    Instances For
                      @[simp]
                      theorem NonUnitalSubsemiring.coe_equivMapOfInjective_apply {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [FunLike F R S] [NonUnitalRingHomClass F R S] (s : NonUnitalSubsemiring R) (f : F) (hf : Function.Injective f) (x : s) :
                      ((s.equivMapOfInjective f hf) x) = f x

                      The range of a non-unital ring homomorphism is a non-unital subsemiring. See note [range copy pattern].

                      Equations
                      Instances For
                        @[simp]
                        theorem NonUnitalRingHom.mem_srange {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [FunLike F R S] [NonUnitalRingHomClass F R S] {f : F} {y : S} :
                        y NonUnitalRingHom.srange f ∃ (x : R), f x = y

                        The range of a morphism of non-unital semirings is finite if the domain is a finite.

                        Equations
                        • =
                        Equations
                        • NonUnitalSubsemiring.instBot = { bot := { carrier := {0}, add_mem' := , zero_mem' := , mul_mem' := } }
                        Equations
                        • NonUnitalSubsemiring.instInhabited = { default := }

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

                        Equations
                        • One or more equations did not get rendered due to their size.
                        @[simp]
                        Equations
                        @[simp]
                        theorem NonUnitalSubsemiring.coe_sInf {R : Type u} [NonUnitalNonAssocSemiring R] (S : Set (NonUnitalSubsemiring R)) :
                        (sInf S) = sS, s
                        theorem NonUnitalSubsemiring.mem_sInf {R : Type u} [NonUnitalNonAssocSemiring R] {S : Set (NonUnitalSubsemiring R)} {x : R} :
                        x sInf S pS, x p
                        @[simp]
                        theorem NonUnitalSubsemiring.coe_iInf {R : Type u} [NonUnitalNonAssocSemiring R] {ι : Sort u_1} {S : ιNonUnitalSubsemiring R} :
                        (⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
                        theorem NonUnitalSubsemiring.mem_iInf {R : Type u} [NonUnitalNonAssocSemiring R] {ι : Sort u_1} {S : ιNonUnitalSubsemiring R} {x : R} :
                        x ⨅ (i : ι), S i ∀ (i : ι), x S i
                        @[simp]
                        theorem NonUnitalSubsemiring.sInf_toSubsemigroup {R : Type u} [NonUnitalNonAssocSemiring R] (s : Set (NonUnitalSubsemiring R)) :
                        (sInf s).toSubsemigroup = ts, t.toSubsemigroup
                        @[simp]
                        theorem NonUnitalSubsemiring.sInf_toAddSubmonoid {R : Type u} [NonUnitalNonAssocSemiring R] (s : Set (NonUnitalSubsemiring R)) :
                        (sInf s).toAddSubmonoid = ts, t.toAddSubmonoid

                        Non-unital subsemirings of a non-unital semiring form a complete lattice.

                        Equations

                        The center of a semiring R is the set of elements that commute and associate with everything in R

                        Equations
                        Instances For
                          theorem Set.mem_center_iff_addMonoidHom (R : Type u) [NonUnitalNonAssocSemiring R] (a : R) :
                          a Set.center R AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a AddMonoidHom.mul.compr₂ (AddMonoidHom.mulLeft a) = AddMonoidHom.mul.comp (AddMonoidHom.mulLeft a) AddMonoidHom.mul.comp (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulLeft a) AddMonoidHom.mul.compr₂ (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulRight a)

                          A point-free means of proving membership in the center, for a non-associative ring.

                          This can be helpful when working with types that have ext lemmas for R →+ R.

                          The centralizer of a set as non-unital subsemiring.

                          Equations
                          Instances For
                            @[simp]

                            The non-unital subsemiring generated by a set includes the set.

                            @[simp]

                            A non-unital subsemiring S includes closure s if and only if it includes s.

                            Subsemiring closure of a set is monotone in its argument: if s ⊆ t, then closure s ≤ closure t.

                            The additive closure of a non-unital subsemigroup is a non-unital subsemiring.

                            Equations
                            Instances For
                              theorem Subsemigroup.nonUnitalSubsemiringClosure_coe {R : Type u} [NonUnitalNonAssocSemiring R] (M : Subsemigroup R) :
                              M.nonUnitalSubsemiringClosure = (AddSubmonoid.closure M)
                              theorem Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid {R : Type u} [NonUnitalNonAssocSemiring R] (M : Subsemigroup R) :
                              M.nonUnitalSubsemiringClosure.toAddSubmonoid = AddSubmonoid.closure M

                              The NonUnitalSubsemiring generated by a multiplicative subsemigroup coincides with the NonUnitalSubsemiring.closure of the subsemigroup itself .

                              The elements of the non-unital subsemiring closure of M are exactly the elements of the additive closure of a multiplicative subsemigroup M.

                              theorem NonUnitalSubsemiring.closure_induction {R : Type u} [NonUnitalNonAssocSemiring R] {s : Set R} {p : RProp} {x : R} (h : x NonUnitalSubsemiring.closure s) (mem : xs, p x) (zero : p 0) (add : ∀ (x y : R), p xp yp (x + y)) (mul : ∀ (x y : R), p xp yp (x * y)) :
                              p x

                              An induction principle for closure membership. If p holds for 0, 1, and all elements of s, and is preserved under addition and multiplication, then p holds for all elements of the closure of s.

                              theorem NonUnitalSubsemiring.closure_induction₂ {R : Type u} [NonUnitalNonAssocSemiring R] {s : Set R} {p : RRProp} {x : R} {y : R} (hx : x NonUnitalSubsemiring.closure s) (hy : y NonUnitalSubsemiring.closure s) (Hs : xs, ys, p x y) (H0_left : ∀ (x : R), p 0 x) (H0_right : ∀ (x : R), p x 0) (Hadd_left : ∀ (x₁ x₂ y : R), p x₁ yp x₂ yp (x₁ + x₂) y) (Hadd_right : ∀ (x y₁ y₂ : R), p x y₁p x y₂p x (y₁ + y₂)) (Hmul_left : ∀ (x₁ x₂ y : R), p x₁ yp x₂ yp (x₁ * x₂) y) (Hmul_right : ∀ (x y₁ y₂ : R), p x y₁p x y₂p x (y₁ * y₂)) :
                              p x y

                              An induction principle for closure membership for predicates with two arguments.

                              def NonUnitalSubsemiring.gi (R : Type u) [NonUnitalNonAssocSemiring R] :
                              GaloisInsertion NonUnitalSubsemiring.closure SetLike.coe

                              closure forms a Galois insertion with the coercion to set.

                              Equations
                              Instances For

                                Closure of a non-unital subsemiring S equals S.

                                theorem NonUnitalSubsemiring.closure_iUnion {R : Type u} [NonUnitalNonAssocSemiring R] {ι : Sort u_2} (s : ιSet R) :
                                NonUnitalSubsemiring.closure (⋃ (i : ι), s i) = ⨆ (i : ι), NonUnitalSubsemiring.closure (s i)
                                theorem NonUnitalSubsemiring.map_iInf {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [FunLike F R S] [NonUnitalRingHomClass F R S] {ι : Sort u_2} [Nonempty ι] (f : F) (hf : Function.Injective f) (s : ιNonUnitalSubsemiring R) :

                                Given NonUnitalSubsemirings s, t of semirings R, S respectively, s.prod t is s × t as a non-unital subsemiring of R × S.

                                Equations
                                • s.prod t = { carrier := s ×ˢ t, add_mem' := , zero_mem' := , mul_mem' := }
                                Instances For
                                  theorem NonUnitalSubsemiring.prod_mono {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] ⦃s₁ : NonUnitalSubsemiring R ⦃s₂ : NonUnitalSubsemiring R (hs : s₁ s₂) ⦃t₁ : NonUnitalSubsemiring S ⦃t₂ : NonUnitalSubsemiring S (ht : t₁ t₂) :
                                  s₁.prod t₁ s₂.prod t₂

                                  Product of non-unital subsemirings is isomorphic to their product as semigroups.

                                  Equations
                                  • s.prodEquiv t = { toEquiv := Equiv.Set.prod s t, map_mul' := , map_add' := }
                                  Instances For
                                    theorem NonUnitalSubsemiring.mem_iSup_of_directed {R : Type u} [NonUnitalNonAssocSemiring R] {ι : Sort u_2} [hι : Nonempty ι] {S : ιNonUnitalSubsemiring R} (hS : Directed (fun (x1 x2 : NonUnitalSubsemiring R) => x1 x2) S) {x : R} :
                                    x ⨆ (i : ι), S i ∃ (i : ι), x S i
                                    theorem NonUnitalSubsemiring.coe_iSup_of_directed {R : Type u} [NonUnitalNonAssocSemiring R] {ι : Sort u_2} [hι : Nonempty ι] {S : ιNonUnitalSubsemiring R} (hS : Directed (fun (x1 x2 : NonUnitalSubsemiring R) => x1 x2) S) :
                                    (⨆ (i : ι), S i) = ⋃ (i : ι), (S i)
                                    theorem NonUnitalSubsemiring.mem_sSup_of_directedOn {R : Type u} [NonUnitalNonAssocSemiring R] {S : Set (NonUnitalSubsemiring R)} (Sne : S.Nonempty) (hS : DirectedOn (fun (x1 x2 : NonUnitalSubsemiring R) => x1 x2) S) {x : R} :
                                    x sSup S sS, x s
                                    theorem NonUnitalSubsemiring.coe_sSup_of_directedOn {R : Type u} [NonUnitalNonAssocSemiring R] {S : Set (NonUnitalSubsemiring R)} (Sne : S.Nonempty) (hS : DirectedOn (fun (x1 x2 : NonUnitalSubsemiring R) => x1 x2) S) :
                                    (sSup S) = sS, s
                                    theorem NonUnitalRingHom.eq_of_eqOn_stop {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] {F : Type u_1} [FunLike F R S] {f : F} {g : F} (h : Set.EqOn f g ) :
                                    f = g
                                    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
                                    Instances For

                                      Restriction of a non-unital ring homomorphism to its range interpreted as a non-unital subsemiring.

                                      This is the bundled version of Set.rangeFactorization.

                                      Equations
                                      Instances For
                                        @[simp]

                                        The range of a surjective non-unital ring homomorphism is the whole of the codomain.

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

                                        Equations
                                        Instances For
                                          theorem NonUnitalRingHom.eqOn_sclosure {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] {F : Type u_1} [FunLike F R S] [NonUnitalNonAssocSemiring S] [NonUnitalRingHomClass F R S] {f : F} {g : F} {s : Set R} (h : Set.EqOn (⇑f) (⇑g) s) :

                                          If two non-unital ring homomorphisms are equal on a set, then they are equal on its non-unital subsemiring closure.

                                          theorem NonUnitalRingHom.eq_of_eqOn_sdense {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] {F : Type u_1} [FunLike F R S] [NonUnitalNonAssocSemiring S] [NonUnitalRingHomClass F R S] {s : Set R} (hs : NonUnitalSubsemiring.closure s = ) {f : F} {g : F} (h : Set.EqOn (⇑f) (⇑g) s) :
                                          f = g

                                          The image under a ring homomorphism of the subsemiring generated by a set equals the subsemiring generated by the image of the set.

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

                                          Equations
                                          Instances For

                                            Makes the identity isomorphism from a proof two non-unital subsemirings of a multiplicative monoid are equal.

                                            Equations
                                            Instances For
                                              def RingEquiv.sofLeftInverse' {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [FunLike F R S] [NonUnitalRingHomClass F R S] {g : SR} {f : F} (h : Function.LeftInverse g f) :

                                              Restrict a non-unital ring homomorphism with a left inverse to a ring isomorphism to its NonUnitalRingHom.srange.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[simp]
                                                theorem RingEquiv.sofLeftInverse'_apply {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [FunLike F R S] [NonUnitalRingHomClass F R S] {g : SR} {f : F} (h : Function.LeftInverse g f) (x : R) :
                                                @[simp]
                                                theorem RingEquiv.sofLeftInverse'_symm_apply {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [FunLike F R S] [NonUnitalRingHomClass F R S] {g : SR} {f : F} (h : Function.LeftInverse g f) (x : (NonUnitalRingHom.srange f)) :
                                                (RingEquiv.sofLeftInverse' h).symm x = g x
                                                @[simp]
                                                theorem RingEquiv.nonUnitalSubsemiringMap_apply_coe {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) (s : NonUnitalSubsemiring R) (x : s.toAddSubmonoid) :
                                                ((e.nonUnitalSubsemiringMap s) x) = e x
                                                @[simp]
                                                theorem RingEquiv.nonUnitalSubsemiringMap_symm_apply_coe {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) (s : NonUnitalSubsemiring R) (y : (e.toAddEquiv '' s.toAddSubmonoid)) :
                                                ((e.nonUnitalSubsemiringMap s).symm y) = (↑e).symm y

                                                Given an equivalence e : R ≃+* S of non-unital semirings and a non-unital subsemiring s of R, non_unital_subsemiring_map e s is the induced equivalence between s and s.map e

                                                Equations
                                                • e.nonUnitalSubsemiringMap s = { toEquiv := (e.toAddEquiv.addSubmonoidMap s.toAddSubmonoid).toEquiv, map_mul' := , map_add' := }
                                                Instances For