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.

  • 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

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.

    Instances For

      A non-unital subsemiring of a NonUnitalSemiring is a NonUnitalSemiring.

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

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

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

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

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

          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) :
            @[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 : { x // x s }) (y : { x // x s }) :
            ↑(x + y) = x + y
            @[simp]
            theorem NonUnitalSubsemiring.coe_mul {R : Type u} [NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R) (x : { x // x s }) (y : { x // x s }) :
            ↑(x * y) = x * y

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

            @[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.

            @[simp]
            @[simp]
            theorem NonUnitalSubsemiring.topEquiv_symm_apply_coe {R : Type u} [NonUnitalNonAssocSemiring R] (x : R) :
            ↑(↑(RingEquiv.symm NonUnitalSubsemiring.topEquiv) x) = x
            @[simp]
            theorem NonUnitalSubsemiring.topEquiv_apply {R : Type u} [NonUnitalNonAssocSemiring R] (x : { x // x }) :
            NonUnitalSubsemiring.topEquiv x = x

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

            Instances For

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

              Instances For

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

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

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

                  Instances For

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

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

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

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

                      @[simp]
                      @[simp]
                      theorem NonUnitalSubsemiring.coe_sInf {R : Type u} [NonUnitalNonAssocSemiring R] (S : Set (NonUnitalSubsemiring R)) :
                      ↑(sInf S) = ⋂ (s : NonUnitalSubsemiring R) (_ : s S), s
                      @[simp]
                      theorem NonUnitalSubsemiring.sInf_toAddSubmonoid {R : Type u} [NonUnitalNonAssocSemiring R] (s : Set (NonUnitalSubsemiring R)) :
                      (sInf s).toAddSubmonoid = ⨅ (t : NonUnitalSubsemiring R) (_ : t s), t.toAddSubmonoid

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

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

                      Instances For

                        The centralizer of a set as non-unital subsemiring.

                        Instances For
                          theorem NonUnitalSubsemiring.mem_centralizer_iff {R : Type u_1} [NonUnitalSemiring R] {s : Set R} {z : R} :
                          z NonUnitalSubsemiring.centralizer s ∀ (g : R), g sg * z = z * g
                          @[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.

                          Instances For

                            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) (Hs : (x : R) → x sp x) (H0 : p 0) (Hadd : (x y : R) → p xp yp (x + y)) (Hmul : (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 : (x : R) → x s(y : R) → y sp 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.

                            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)

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

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

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

                                Instances For
                                  theorem NonUnitalSubsemiring.mem_iSup_of_directed {R : Type u} [NonUnitalNonAssocSemiring R] {ι : Sort u_2} [hι : Nonempty ι] {S : ιNonUnitalSubsemiring R} (hS : Directed (fun x x_1 => x x_1) 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 x x_1 => x x_1) S) :
                                  ↑(⨆ (i : ι), S i) = ⋃ (i : ι), ↑(S i)
                                  theorem NonUnitalSubsemiring.mem_sSup_of_directedOn {R : Type u} [NonUnitalNonAssocSemiring R] {S : Set (NonUnitalSubsemiring R)} (Sne : Set.Nonempty S) (hS : DirectedOn (fun x x_1 => x x_1) S) {x : R} :
                                  x sSup S s, s S x s
                                  theorem NonUnitalSubsemiring.coe_sSup_of_directedOn {R : Type u} [NonUnitalNonAssocSemiring R] {S : Set (NonUnitalSubsemiring R)} (Sne : Set.Nonempty S) (hS : DirectedOn (fun x x_1 => x x_1) S) :
                                  ↑(sSup S) = ⋃ (s : NonUnitalSubsemiring R) (_ : s S), s
                                  def NonUnitalRingHom.codRestrict {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [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 →ₙ+* { x // x s }

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

                                  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.

                                    Instances For
                                      @[simp]
                                      @[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

                                      Instances For
                                        theorem NonUnitalRingHom.eqOn_sclosure {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [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_stop {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [NonUnitalRingHomClass F R S] {f : F} {g : F} (h : Set.EqOn f g ) :
                                        f = g
                                        theorem NonUnitalRingHom.eq_of_eqOn_sdense {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [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.

                                        Instances For

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

                                          Instances For
                                            def RingEquiv.sofLeftInverse' {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [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.

                                            Instances For
                                              @[simp]
                                              theorem RingEquiv.sofLeftInverse'_apply {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [NonUnitalRingHomClass F R S] {g : SR} {f : F} (h : Function.LeftInverse g f) (x : R) :
                                              ↑(↑(RingEquiv.sofLeftInverse' h) x) = f x
                                              @[simp]
                                              @[simp]
                                              theorem RingEquiv.nonUnitalSubsemiringMap_apply_coe {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) (s : NonUnitalSubsemiring R) :
                                              ∀ (a : s.toAddSubmonoid), ↑(↑(RingEquiv.nonUnitalSubsemiringMap e s) a) = e a
                                              @[simp]

                                              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

                                              Instances For