Documentation

Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Bundled non-unital subsemirings #

We define the CompleteLattice structure, and non-unital subsemiring map, comap and range (srange) of a NonUnitalRingHom etc.

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

Equations
    Instances For

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

      Equations
        Instances For
          @[simp]
          theorem NonUnitalSubsemiring.coe_comap {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [FunLike F R S] [NonUnitalRingHomClass F R S] (s : NonUnitalSubsemiring S) (f : F) :
          (comap f s) = f ⁻¹' s
          @[simp]
          theorem NonUnitalSubsemiring.mem_comap {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [FunLike F R S] [NonUnitalRingHomClass F R S] {s : NonUnitalSubsemiring S} {f : F} {x : R} :
          x comap f s f x s
          theorem NonUnitalSubsemiring.comap_comap {R : Type u} {S : Type v} {T : Type w} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] {F : Type u_1} {G : Type u_2} [FunLike F R S] [NonUnitalRingHomClass F R S] [FunLike G S T] [NonUnitalRingHomClass G S T] (s : NonUnitalSubsemiring T) (g : G) (f : F) :
          comap f (comap g s) = comap ((↑g).comp f) s

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

          Equations
            Instances For
              @[simp]
              theorem NonUnitalSubsemiring.coe_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) :
              (map f s) = f '' s
              @[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 map f s xs, f x = y
              theorem NonUnitalSubsemiring.map_map {R : Type u} {S : Type v} {T : Type w} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] {F : Type u_1} {G : Type u_2} [FunLike F R S] [NonUnitalRingHomClass F R S] [FunLike G S T] [NonUnitalRingHomClass G S T] (s : NonUnitalSubsemiring R) (g : G) (f : F) :
              map (↑g) (map (↑f) s) = map ((↑g).comp f) s
              noncomputable def NonUnitalSubsemiring.equivMapOfInjective {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) :
              s ≃+* (map f s)

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

              Equations
                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.coe_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) :
                      (srange f) = Set.range f
                      @[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 srange f ∃ (x : R), f x = y

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

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

                      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

                            The center is commutative and associative.

                            Equations

                              The center of isomorphic (not necessarily unital or associative) semirings are isomorphic.

                              Equations
                                Instances For

                                  The center of a (not necessarily unital or associative) semiring is isomorphic to the center of its opposite.

                                  Equations
                                    Instances For
                                      theorem NonUnitalSubsemiring.mem_center_iff {R : Type u_1} [NonUnitalSemiring R] {z : R} :
                                      z center R ∀ (g : R), g * z = z * g

                                      The centralizer of a set as non-unital subsemiring.

                                      Equations
                                        Instances For
                                          theorem NonUnitalSubsemiring.mem_centralizer_iff {R : Type u_1} [NonUnitalSemiring R] {s : Set R} {z : R} :
                                          z centralizer s gs, g * z = z * g

                                          The NonUnitalSubsemiring generated by a set.

                                          Equations
                                            Instances For
                                              theorem NonUnitalSubsemiring.mem_closure {R : Type u} [NonUnitalNonAssocSemiring R] {x : R} {s : Set R} :
                                              x closure s ∀ (S : NonUnitalSubsemiring R), s Sx S
                                              @[simp]

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

                                              theorem NonUnitalSubsemiring.notMem_of_notMem_closure {R : Type u} [NonUnitalNonAssocSemiring R] {s : Set R} {P : R} (hP : Pclosure s) :
                                              Ps
                                              @[deprecated NonUnitalSubsemiring.notMem_of_notMem_closure (since := "2025-05-23")]
                                              theorem NonUnitalSubsemiring.not_mem_of_not_mem_closure {R : Type u} [NonUnitalNonAssocSemiring R] {s : Set R} {P : R} (hP : Pclosure s) :
                                              Ps

                                              Alias of NonUnitalSubsemiring.notMem_of_notMem_closure.

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

                                              theorem NonUnitalSubsemiring.closure_eq_of_le {R : Type u} [NonUnitalNonAssocSemiring R] {s : Set R} {t : NonUnitalSubsemiring R} (h₁ : s t) (h₂ : t closure s) :
                                              @[reducible, inline]
                                              abbrev NonUnitalSubsemiring.closureNonUnitalCommSemiringOfComm {R : Type u_1} [NonUnitalSemiring R] {s : Set R} (hcomm : xs, ys, x * y = y * x) :

                                              If all the elements of a set s commute, then closure s is a non-unital commutative semiring.

                                              Equations
                                                Instances For

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

                                                  Equations
                                                    Instances For

                                                      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 : (x : R) → x closure sProp} (mem : ∀ (x : R) (hx : x s), p x ) (zero : p 0 ) (add : ∀ (x y : R) (hx : x closure s) (hy : y closure s), p x hxp y hyp (x + y) ) (mul : ∀ (x y : R) (hx : x closure s) (hy : y closure s), p x hxp y hyp (x * y) ) {x : R} (hx : x closure s) :
                                                      p x hx

                                                      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 : (x y : R) → x closure sy closure sProp} (mem_mem : ∀ (x : R) (hx : x s) (y : R) (hy : y s), p x y ) (zero_left : ∀ (x : R) (hx : x closure s), p 0 x hx) (zero_right : ∀ (x : R) (hx : x closure s), p x 0 hx ) (add_left : ∀ (x y z : R) (hx : x closure s) (hy : y closure s) (hz : z closure s), p x z hx hzp y z hy hzp (x + y) z hz) (add_right : ∀ (x y z : R) (hx : x closure s) (hy : y closure s) (hz : z closure s), p x y hx hyp x z hx hzp x (y + z) hx ) (mul_left : ∀ (x y z : R) (hx : x closure s) (hy : y closure s) (hz : z closure s), p x z hx hzp y z hy hzp (x * y) z hz) (mul_right : ∀ (x y z : R) (hx : x closure s) (hy : y closure s) (hz : z closure s), p x y hx hyp x z hx hzp x (y * z) hx ) {x y : R} (hx : x closure s) (hy : y closure s) :
                                                      p x y hx hy

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

                                                      closure forms a Galois insertion with the coercion to set.

                                                      Equations
                                                        Instances For
                                                          @[simp]

                                                          Closure of a non-unital subsemiring S equals S.

                                                          theorem NonUnitalSubsemiring.closure_iUnion {R : Type u} [NonUnitalNonAssocSemiring R] {ι : Sort u_2} (s : ιSet R) :
                                                          closure (⋃ (i : ι), s i) = ⨆ (i : ι), closure (s i)
                                                          theorem NonUnitalSubsemiring.map_sup {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [FunLike F R S] [NonUnitalRingHomClass F R S] (s t : NonUnitalSubsemiring R) (f : F) :
                                                          map f (st) = map f smap f t
                                                          theorem NonUnitalSubsemiring.map_iSup {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} (f : F) (s : ιNonUnitalSubsemiring R) :
                                                          map f (iSup s) = ⨆ (i : ι), map f (s i)
                                                          theorem NonUnitalSubsemiring.map_inf {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [FunLike F R S] [NonUnitalRingHomClass F R S] (s t : NonUnitalSubsemiring R) (f : F) (hf : Function.Injective f) :
                                                          map f (st) = map f smap f t
                                                          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) :
                                                          map f (iInf s) = ⨅ (i : ι), map f (s i)
                                                          theorem NonUnitalSubsemiring.comap_inf {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [FunLike F R S] [NonUnitalRingHomClass F R S] (s t : NonUnitalSubsemiring S) (f : F) :
                                                          comap f (st) = comap f scomap f t
                                                          theorem NonUnitalSubsemiring.comap_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} (f : F) (s : ιNonUnitalSubsemiring S) :
                                                          comap f (iInf s) = ⨅ (i : ι), comap f (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.

                                                          Equations
                                                            Instances For
                                                              theorem NonUnitalSubsemiring.prod_mono {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] s₁ s₂ : NonUnitalSubsemiring R (hs : s₁ s₂) t₁ 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
                                                                Instances For
                                                                  theorem NonUnitalSubsemiring.mem_iSup_of_directed {R : Type u} [NonUnitalNonAssocSemiring R] {ι : Sort u_2} [ : 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} [ : 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 g : F} (h : Set.EqOn f g ) :
                                                                  f = g

                                                                  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]
                                                                      theorem NonUnitalRingHom.coe_srangeRestrict {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] {F : Type u_1} [FunLike F R S] [NonUnitalNonAssocSemiring S] [NonUnitalRingHomClass F R S] (f : F) (x : R) :
                                                                      ((srangeRestrict f) x) = f x
                                                                      @[deprecated NonUnitalRingHom.srange_eq_top_iff_surjective (since := "2024-11-11")]

                                                                      Alias of NonUnitalRingHom.srange_eq_top_iff_surjective.

                                                                      @[simp]

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

                                                                      @[deprecated NonUnitalRingHom.srange_eq_top_of_surjective (since := "2024-11-11")]

                                                                      Alias of NonUnitalRingHom.srange_eq_top_of_surjective.


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

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

                                                                      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
                                                                            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) :
                                                                              ((sofLeftInverse' h) x) = f x
                                                                              @[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)) :
                                                                              (sofLeftInverse' h).symm x = g x

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