doc-next-gen

Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Module docstring

{"# Bundled non-unital subsemirings

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

NonUnitalSubsemiring.toSubsemigroup_strictMono theorem
: StrictMono (toSubsemigroup : NonUnitalSubsemiring R → Subsemigroup R)
Full source 
@[mono]
theorem toSubsemigroup_strictMono :
    StrictMono (toSubsemigroup : NonUnitalSubsemiring R → Subsemigroup R) := fun _ _ => id
Strict Monotonicity of Subsemigroup Projection from Non-unital Subsemirings
Informal description
The function that maps a non-unital subsemiring $S$ of a non-unital semiring $R$ to its underlying multiplicative subsemigroup is strictly monotone with respect to the partial orders induced by inclusion. That is, for any two non-unital subsemirings $S$ and $T$ of $R$, if $S \subsetneq T$, then the subsemigroup of $S$ is strictly contained in the subsemigroup of $T$.
NonUnitalSubsemiring.toSubsemigroup_mono theorem
: Monotone (toSubsemigroup : NonUnitalSubsemiring R → Subsemigroup R)
Full source 
@[mono]
theorem toSubsemigroup_mono : Monotone (toSubsemigroup : NonUnitalSubsemiring R → Subsemigroup R) :=
  toSubsemigroup_strictMono.monotone
Monotonicity of Subsemigroup Projection from Non-unital Subsemirings
Informal description
The function that maps a non-unital subsemiring $S$ of a non-unital semiring $R$ to its underlying multiplicative subsemigroup is monotone with respect to the partial orders induced by inclusion. That is, for any two non-unital subsemirings $S$ and $T$ of $R$, if $S \subseteq T$, then the subsemigroup of $S$ is contained in the subsemigroup of $T$.
NonUnitalSubsemiring.toAddSubmonoid_strictMono theorem
: StrictMono (toAddSubmonoid : NonUnitalSubsemiring R → AddSubmonoid R)
Full source 
@[mono]
theorem toAddSubmonoid_strictMono :
    StrictMono (toAddSubmonoid : NonUnitalSubsemiring R → AddSubmonoid R) := fun _ _ => id
Strict Monotonicity of the Additive Submonoid Map for Non-unital Subsemirings
Informal description
The function `toAddSubmonoid`, which maps a non-unital subsemiring of $R$ to its underlying additive submonoid, is strictly monotone. That is, for any two non-unital subsemirings $S$ and $T$ of $R$, if $S$ is strictly contained in $T$, then the additive submonoid of $S$ is strictly contained in the additive submonoid of $T$.
NonUnitalSubsemiring.toAddSubmonoid_mono theorem
: Monotone (toAddSubmonoid : NonUnitalSubsemiring R → AddSubmonoid R)
Full source 
@[mono]
theorem toAddSubmonoid_mono : Monotone (toAddSubmonoid : NonUnitalSubsemiring R → AddSubmonoid R) :=
  toAddSubmonoid_strictMono.monotone
Monotonicity of the Additive Submonoid Map for Non-unital Subsemirings
Informal description
The function that maps a non-unital subsemiring of $R$ to its underlying additive submonoid is monotone. That is, for any two non-unital subsemirings $S$ and $T$ of $R$, if $S \subseteq T$, then the additive submonoid of $S$ is contained in the additive submonoid of $T$.
NonUnitalSubsemiring.topEquiv definition
: (⊤ : NonUnitalSubsemiring R) ≃+* R
Full source 
/-- The ring equiv between the top element of `NonUnitalSubsemiring R` and `R`. -/
@[simps!]
def topEquiv : (⊤ : NonUnitalSubsemiring R) ≃+* R :=
  { Subsemigroup.topEquiv, AddSubmonoid.topEquiv with }
Ring equivalence between the top non-unital subsemiring and the semiring
Informal description
The ring equivalence between the top element of the lattice of non-unital subsemirings of $R$ (which is $R$ itself) and $R$. This equivalence preserves both the additive and multiplicative structures.
NonUnitalSubsemiring.comap definition
(f : F) (s : NonUnitalSubsemiring S) : NonUnitalSubsemiring R
Full source 
/-- The preimage of a non-unital subsemiring along a non-unital ring homomorphism is a
non-unital subsemiring. -/
def comap (f : F) (s : NonUnitalSubsemiring S) : NonUnitalSubsemiring R :=
  { s.toSubsemigroup.comap (f : MulHom R S), s.toAddSubmonoid.comap (f : R →+ S) with
    carrier := f ⁻¹' s }
Preimage of a non-unital subsemiring under a non-unital ring homomorphism
Informal description
Given a non-unital ring homomorphism \( f : R \to S \) and a non-unital subsemiring \( s \) of \( S \), the preimage \( f^{-1}(s) \) forms a non-unital subsemiring of \( R \). This subsemiring consists of all elements \( x \in R \) such that \( f(x) \in s \).
NonUnitalSubsemiring.coe_comap theorem
(s : NonUnitalSubsemiring S) (f : F) : (s.comap f : Set R) = f ⁻¹' s
Full source 
@[simp]
theorem coe_comap (s : NonUnitalSubsemiring S) (f : F) : (s.comap f : Set R) = f ⁻¹' s :=
  rfl
Preimage of Non-unital Subsemiring Under Homomorphism Equals Set Preimage
Informal description
For a non-unital subsemiring $s$ of a non-unital semiring $S$ and a non-unital ring homomorphism $f : R \to S$, the underlying set of the preimage subsemiring $s.\text{comap}\,f$ is equal to the preimage of $s$ under $f$, i.e., $(s.\text{comap}\,f : \text{Set}\,R) = f^{-1}(s)$.
NonUnitalSubsemiring.mem_comap theorem
{s : NonUnitalSubsemiring S} {f : F} {x : R} : x ∈ s.comap f ↔ f x ∈ s
Full source 
@[simp]
theorem mem_comap {s : NonUnitalSubsemiring S} {f : F} {x : R} : x ∈ s.comap fx ∈ s.comap f ↔ f x ∈ s :=
  Iff.rfl
Membership Criterion for Preimage of Non-unital Subsemiring
Informal description
Let $R$ and $S$ be non-unital non-associative semirings, $f : R \to S$ be a non-unital ring homomorphism, and $s$ be a non-unital subsemiring of $S$. For any $x \in R$, we have $x$ belongs to the preimage subsemiring $f^{-1}(s)$ if and only if $f(x)$ belongs to $s$.
NonUnitalSubsemiring.comap_comap theorem
(s : NonUnitalSubsemiring T) (g : G) (f : F) : ((s.comap g : NonUnitalSubsemiring S).comap f : NonUnitalSubsemiring R) = s.comap ((g : S →ₙ+* T).comp (f : R →ₙ+* S))
Full source 
theorem comap_comap (s : NonUnitalSubsemiring T) (g : G) (f : F) :
    ((s.comap g : NonUnitalSubsemiring S).comap f : NonUnitalSubsemiring R) =
      s.comap ((g : S →ₙ+* T).comp (f : R →ₙ+* S)) :=
  rfl
Preimage Composition for Non-Unital Subsemirings
Informal description
Let $R$, $S$, and $T$ be non-unital semirings, and let $f \colon R \to S$ and $g \colon S \to T$ be non-unital ring homomorphisms. For any non-unital subsemiring $s$ of $T$, the preimage of the preimage of $s$ under $g$ and $f$ is equal to the preimage of $s$ under the composition $g \circ f$. In other words, we have: \[ f^{-1}(g^{-1}(s)) = (g \circ f)^{-1}(s). \]
NonUnitalSubsemiring.map definition
(f : F) (s : NonUnitalSubsemiring R) : NonUnitalSubsemiring S
Full source 
/-- The image of a non-unital subsemiring along a ring homomorphism is a non-unital subsemiring. -/
def map (f : F) (s : NonUnitalSubsemiring R) : NonUnitalSubsemiring S :=
  { s.toSubsemigroup.map (f : R →ₙ* S), s.toAddSubmonoid.map (f : R →+ S) with carrier := f '' s }
Image of a non-unital subsemiring under a ring homomorphism
Informal description
Given a non-unital ring homomorphism $f \colon R \to S$ and a non-unital subsemiring $s$ of $R$, the image of $s$ under $f$ forms a non-unital subsemiring of $S$. More precisely, the image consists of all elements of the form $f(x)$ where $x \in s$, and this set is closed under addition, multiplication, and contains the additive identity of $S$.
NonUnitalSubsemiring.coe_map theorem
(f : F) (s : NonUnitalSubsemiring R) : (s.map f : Set S) = f '' s
Full source 
@[simp]
theorem coe_map (f : F) (s : NonUnitalSubsemiring R) : (s.map f : Set S) = f '' s :=
  rfl
Image of Non-unital Subsemiring Under Homomorphism Equals Function Image
Informal description
For any non-unital ring homomorphism $f \colon R \to S$ and any non-unital subsemiring $s$ of $R$, the underlying set of the image subsemiring $s.map(f)$ is equal to the image of the set $s$ under the function $f$, i.e., $s.map(f) = f(s)$.
NonUnitalSubsemiring.mem_map theorem
{f : F} {s : NonUnitalSubsemiring R} {y : S} : y ∈ s.map f ↔ ∃ x ∈ s, f x = y
Full source 
@[simp]
theorem mem_map {f : F} {s : NonUnitalSubsemiring R} {y : S} : y ∈ s.map fy ∈ s.map f ↔ ∃ x ∈ s, f x = y :=
  Iff.rfl
Characterization of Elements in the Image of a Non-unital Subsemiring under a Ring Homomorphism
Informal description
For a non-unital ring homomorphism $f \colon R \to S$, a non-unital subsemiring $s$ of $R$, and an element $y \in S$, we have $y \in f(s)$ if and only if there exists $x \in s$ such that $f(x) = y$.
NonUnitalSubsemiring.map_id theorem
: s.map (NonUnitalRingHom.id R) = s
Full source 
@[simp]
theorem map_id : s.map (NonUnitalRingHom.id R) = s :=
  SetLike.coe_injective <| Set.image_id _
Identity Map Preserves Non-unital Subsemiring
Informal description
For any non-unital subsemiring $s$ of a non-unital semiring $R$, the image of $s$ under the identity non-unital ring homomorphism $\mathrm{id}_R \colon R \to R$ is equal to $s$ itself, i.e., $\mathrm{id}_R(s) = s$.
NonUnitalSubsemiring.map_map theorem
(g : G) (f : F) : (s.map (f : R →ₙ+* S)).map (g : S →ₙ+* T) = s.map ((g : S →ₙ+* T).comp (f : R →ₙ+* S))
Full source 
theorem map_map (g : G) (f : F) :
    (s.map (f : R →ₙ+* S)).map (g : S →ₙ+* T) = s.map ((g : S →ₙ+* T).comp (f : R →ₙ+* S)) :=
  SetLike.coe_injective <| Set.image_image _ _ _
Composition of Images under Non-unital Ring Homomorphisms
Informal description
For any non-unital subsemiring $s$ of a non-unital semiring $R$, and non-unital ring homomorphisms $f \colon R \to S$ and $g \colon S \to T$, the image of the image of $s$ under $f$ under $g$ is equal to the image of $s$ under the composition $g \circ f$. In symbols: $$g(f(s)) = (g \circ f)(s).$$
NonUnitalSubsemiring.map_le_iff_le_comap theorem
{f : F} {s : NonUnitalSubsemiring R} {t : NonUnitalSubsemiring S} : s.map f ≤ t ↔ s ≤ t.comap f
Full source 
theorem map_le_iff_le_comap {f : F} {s : NonUnitalSubsemiring R} {t : NonUnitalSubsemiring S} :
    s.map f ≤ t ↔ s ≤ t.comap f :=
  Set.image_subset_iff
Image-Preimage Order Correspondence for Non-unital Subsemirings
Informal description
Let $R$ and $S$ be non-unital non-associative semirings, and let $f \colon R \to S$ be a non-unital ring homomorphism. For any non-unital subsemiring $s$ of $R$ and $t$ of $S$, the image $f(s)$ is contained in $t$ if and only if $s$ is contained in the preimage $f^{-1}(t)$. In symbols: \[ f(s) \leq t \leftrightarrow s \leq f^{-1}(t). \]
NonUnitalSubsemiring.gc_map_comap theorem
(f : F) : @GaloisConnection (NonUnitalSubsemiring R) (NonUnitalSubsemiring S) _ _ (map f) (comap f)
Full source 
theorem gc_map_comap (f : F) :
    @GaloisConnection (NonUnitalSubsemiring R) (NonUnitalSubsemiring S) _ _ (map f) (comap f) :=
  fun _ _ => map_le_iff_le_comap
Galois Connection Between Image and Preimage of Non-unital Subsemirings
Informal description
For any non-unital ring homomorphism $f \colon R \to S$, the pair of functions $(f[\cdot], f^{-1}[\cdot])$ forms a Galois connection between the complete lattices of non-unital subsemirings of $R$ and $S$. More precisely, for any non-unital subsemiring $s$ of $R$ and $t$ of $S$, we have: \[ f(s) \leq t \leftrightarrow s \leq f^{-1}(t). \]
NonUnitalSubsemiring.equivMapOfInjective definition
(f : F) (hf : Function.Injective (f : R → S)) : s ≃+* s.map f
Full source 
/-- A non-unital subsemiring is isomorphic to its image under an injective function -/
noncomputable def equivMapOfInjective (f : F) (hf : Function.Injective (f : R → S)) :
    s ≃+* s.map f :=
  { Equiv.Set.image f s hf with
    map_mul' := fun _ _ => Subtype.ext (map_mul f _ _)
    map_add' := fun _ _ => Subtype.ext (map_add f _ _) }
Isomorphism between a non-unital subsemiring and its image under an injective ring homomorphism
Informal description
Given an injective non-unital ring homomorphism \( f \colon R \to S \) and a non-unital subsemiring \( s \) of \( R \), there is an isomorphism of non-unital semirings between \( s \) and its image \( s.map f \) under \( f \). The isomorphism is given by: - The forward map sends each \( x \in s \) to \( f(x) \in s.map f \). - The inverse map sends each \( y \in s.map f \) to the unique \( x \in s \) such that \( f(x) = y \) (which exists and is unique by injectivity of \( f \)).
NonUnitalSubsemiring.coe_equivMapOfInjective_apply theorem
(f : F) (hf : Function.Injective f) (x : s) : (equivMapOfInjective s f hf x : S) = f x
Full source 
@[simp]
theorem coe_equivMapOfInjective_apply (f : F) (hf : Function.Injective f) (x : s) :
    (equivMapOfInjective s f hf x : S) = f x :=
  rfl
Image of Element under Isomorphism Induced by Injective Homomorphism
Informal description
Let $f \colon R \to S$ be an injective non-unital ring homomorphism, and let $s$ be a non-unital subsemiring of $R$. For any element $x \in s$, the image of $x$ under the isomorphism $\text{equivMapOfInjective}(s, f, hf)$ is equal to $f(x)$ in $S$.
NonUnitalRingHom.srange definition
: NonUnitalSubsemiring S
Full source 
/-- The range of a non-unital ring homomorphism is a non-unital subsemiring.
See note [range copy pattern]. -/
def srange : NonUnitalSubsemiring S :=
  ((⊤ : NonUnitalSubsemiring R).map (f : R →ₙ+* S)).copy (Set.range f) Set.image_univ.symm
Range of a non-unital ring homomorphism
Informal description
The range of a non-unital ring homomorphism $f \colon R \to S$ is the non-unital subsemiring of $S$ consisting of all elements of the form $f(x)$ for some $x \in R$. More precisely, it is the image of the top non-unital subsemiring of $R$ under $f$, which coincides with the set-theoretic range of $f$.
NonUnitalRingHom.coe_srange theorem
: (srange f : Set S) = Set.range f
Full source 
@[simp]
theorem coe_srange : (srange f : Set S) = Set.range f :=
  rfl
Range of Non-unital Ring Homomorphism as Set
Informal description
For a non-unital ring homomorphism $f \colon R \to S$, the underlying set of the range of $f$ (as a non-unital subsemiring of $S$) is equal to the set-theoretic range of $f$, i.e., $\{f(x) \mid x \in R\}$.
NonUnitalRingHom.mem_srange theorem
{f : F} {y : S} : y ∈ srange f ↔ ∃ x, f x = y
Full source 
@[simp]
theorem mem_srange {f : F} {y : S} : y ∈ srange fy ∈ srange f ↔ ∃ x, f x = y :=
  Iff.rfl
Characterization of Elements in the Range of a Non-Unital Ring Homomorphism
Informal description
For a non-unital ring homomorphism $f \colon R \to S$ and an element $y \in S$, $y$ belongs to the range of $f$ if and only if there exists an element $x \in R$ such that $f(x) = y$.
NonUnitalRingHom.srange_eq_map theorem
: srange f = (⊤ : NonUnitalSubsemiring R).map f
Full source 
theorem srange_eq_map : srange f = (⊤ : NonUnitalSubsemiring R).map f := by
  ext
  simp
Range of Non-Unital Ring Homomorphism as Image of Top Subsemiring
Informal description
The range of a non-unital ring homomorphism $f \colon R \to S$ is equal to the image of the top non-unital subsemiring of $R$ under $f$. In other words, $\text{srange}(f) = f(R)$ as non-unital subsemirings of $S$.
NonUnitalRingHom.mem_srange_self theorem
(f : F) (x : R) : f x ∈ srange f
Full source 
theorem mem_srange_self (f : F) (x : R) : f x ∈ srange f :=
  mem_srange.mpr ⟨x, rfl⟩
Image of Element under Non-Unital Ring Homomorphism is in its Range
Informal description
For any non-unital ring homomorphism $f \colon R \to S$ and any element $x \in R$, the image $f(x)$ belongs to the range of $f$.
NonUnitalRingHom.map_srange theorem
(g : S →ₙ+* T) (f : R →ₙ+* S) : map g (srange f) = srange (g.comp f)
Full source 
theorem map_srange (g : S →ₙ+* T) (f : R →ₙ+* S) : map g (srange f) = srange (g.comp f) := by
  simpa only [srange_eq_map] using (⊤ : NonUnitalSubsemiring R).map_map g f
Image of Range under Composition of Non-unital Ring Homomorphisms
Informal description
For any non-unital ring homomorphisms $f \colon R \to S$ and $g \colon S \to T$, the image of the range of $f$ under $g$ is equal to the range of the composition $g \circ f$. In symbols: $$g(\text{srange}(f)) = \text{srange}(g \circ f).$$
NonUnitalRingHom.finite_srange instance
[Finite R] (f : F) : Finite (srange f : NonUnitalSubsemiring S)
Full source 
/-- The range of a morphism of non-unital semirings is finite if the domain is a finite. -/
instance finite_srange [Finite R] (f : F) : Finite (srange f : NonUnitalSubsemiring S) :=
  (Set.finite_range f).to_subtype
Finiteness of the Range of a Non-unital Ring Homomorphism with Finite Domain
Informal description
For any non-unital ring homomorphism $f \colon R \to S$ where $R$ is finite, the range of $f$ is a finite non-unital subsemiring of $S$.
NonUnitalSubsemiring.instInfSet instance
: InfSet (NonUnitalSubsemiring R)
Full source 
instance : InfSet (NonUnitalSubsemiring R) :=
  ⟨fun s =>
    NonUnitalSubsemiring.mk' (⋂ t ∈ s, ↑t) (⨅ t ∈ s, NonUnitalSubsemiring.toSubsemigroup t)
      (by simp) (⨅ t ∈ s, NonUnitalSubsemiring.toAddSubmonoid t) (by simp)⟩
Complete Lattice Structure on Non-unital Subsemirings
Informal description
The collection of all non-unital subsemirings of a non-unital non-associative semiring $R$ forms a complete lattice with respect to inclusion, where the infimum of a family of subsemirings is given by their intersection.
NonUnitalSubsemiring.coe_sInf theorem
(S : Set (NonUnitalSubsemiring R)) : ((sInf S : NonUnitalSubsemiring R) : Set R) = ⋂ s ∈ S, ↑s
Full source 
@[simp, norm_cast]
theorem coe_sInf (S : Set (NonUnitalSubsemiring R)) :
    ((sInf S : NonUnitalSubsemiring R) : Set R) = ⋂ s ∈ S, ↑s :=
  rfl
Infimum of Non-unital Subsemirings as Intersection
Informal description
For any set $S$ of non-unital subsemirings of a non-unital non-associative semiring $R$, the underlying set of the infimum of $S$ is equal to the intersection of all the underlying sets of the subsemirings in $S$. That is, \[ \bigcap_{s \in S} s = \inf S. \]
NonUnitalSubsemiring.mem_sInf theorem
{S : Set (NonUnitalSubsemiring R)} {x : R} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
Full source 
theorem mem_sInf {S : Set (NonUnitalSubsemiring R)} {x : R} : x ∈ sInf Sx ∈ sInf S ↔ ∀ p ∈ S, x ∈ p :=
  Set.mem_iInter₂
Characterization of Membership in Infimum of Non-unital Subsemirings
Informal description
For any set $S$ of non-unital subsemirings of a non-unital non-associative semiring $R$ and any element $x \in R$, we have $x \in \bigwedge S$ if and only if $x$ belongs to every subsemiring $p \in S$. In symbols: $$x \in \bigwedge S \leftrightarrow \forall p \in S, x \in p$$
NonUnitalSubsemiring.coe_iInf theorem
{ι : Sort*} {S : ι → NonUnitalSubsemiring R} : (↑(⨅ i, S i) : Set R) = ⋂ i, S i
Full source 
@[simp, norm_cast]
theorem coe_iInf {ι : Sort*} {S : ι → NonUnitalSubsemiring R} :
    (↑(⨅ i, S i) : Set R) = ⋂ i, S i := by
  simp only [iInf, coe_sInf, Set.biInter_range]
Infimum of Non-unital Subsemirings as Intersection of Underlying Sets
Informal description
For any family of non-unital subsemirings $\{S_i\}_{i \in \iota}$ of a non-unital non-associative semiring $R$, the underlying set of their infimum $\bigsqcap_i S_i$ is equal to the intersection $\bigcap_i S_i$ of their underlying sets.
NonUnitalSubsemiring.mem_iInf theorem
{ι : Sort*} {S : ι → NonUnitalSubsemiring R} {x : R} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i
Full source 
theorem mem_iInf {ι : Sort*} {S : ι → NonUnitalSubsemiring R} {x : R} :
    (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by
  simp only [iInf, mem_sInf, Set.forall_mem_range]
Characterization of Membership in Infimum of Non-unital Subsemirings
Informal description
For any indexed family of non-unital subsemirings $\{S_i\}_{i \in \iota}$ of a non-unital non-associative semiring $R$ and any element $x \in R$, we have $x \in \bigsqcap_i S_i$ if and only if $x \in S_i$ for every $i \in \iota$.
NonUnitalSubsemiring.sInf_toSubsemigroup theorem
(s : Set (NonUnitalSubsemiring R)) : (sInf s).toSubsemigroup = ⨅ t ∈ s, NonUnitalSubsemiring.toSubsemigroup t
Full source 
@[simp]
theorem sInf_toSubsemigroup (s : Set (NonUnitalSubsemiring R)) :
    (sInf s).toSubsemigroup = ⨅ t ∈ s, NonUnitalSubsemiring.toSubsemigroup t :=
  mk'_toSubsemigroup _ _
Infimum of Non-Unital Subsemirings Preserves Subsemigroup Structure
Informal description
For any set $s$ of non-unital subsemirings of a non-unital non-associative semiring $R$, the subsemigroup component of the infimum of $s$ is equal to the infimum of the subsemigroup components of the elements of $s$. In other words, we have $$(\bigsqcap s).\text{toSubsemigroup} = \bigsqcap_{t \in s} t.\text{toSubsemigroup}.$$
NonUnitalSubsemiring.sInf_toAddSubmonoid theorem
(s : Set (NonUnitalSubsemiring R)) : (sInf s).toAddSubmonoid = ⨅ t ∈ s, NonUnitalSubsemiring.toAddSubmonoid t
Full source 
@[simp]
theorem sInf_toAddSubmonoid (s : Set (NonUnitalSubsemiring R)) :
    (sInf s).toAddSubmonoid = ⨅ t ∈ s, NonUnitalSubsemiring.toAddSubmonoid t :=
  mk'_toAddSubmonoid _ _
Infimum of Non-Unital Subsemirings Preserves Additive Submonoid Structure
Informal description
For any set $s$ of non-unital subsemirings of a non-unital non-associative semiring $R$, the additive submonoid component of the infimum of $s$ is equal to the infimum of the additive submonoid components of the subsemirings in $s$. In other words, $(\bigsqcap s).\text{toAddSubmonoid} = \bigsqcap_{t \in s} t.\text{toAddSubmonoid}$.
NonUnitalSubsemiring.instCompleteLattice instance
: CompleteLattice (NonUnitalSubsemiring R)
Full source 
/-- Non-unital subsemirings of a non-unital semiring form a complete lattice. -/
instance : CompleteLattice (NonUnitalSubsemiring R) :=
  { completeLatticeOfInf (NonUnitalSubsemiring R)
      fun _ => IsGLB.of_image SetLike.coe_subset_coe isGLB_biInf with
    bot := ⊥
    bot_le := fun s _ hx => (mem_bot.mp hx).symm ▸ zero_mem s
    top := ⊤
    le_top := fun _ _ _ => trivial
    inf := (· ⊓ ·)
    inf_le_left := fun _ _ _ => And.left
    inf_le_right := fun _ _ _ => And.right
    le_inf := fun _ _ _ h₁ h₂ _ hx => ⟨h₁ hx, h₂ hx⟩ }
Complete Lattice of Non-Unital Subsemirings
Informal description
The collection of all non-unital subsemirings of a non-unital semiring $R$ forms a complete lattice, where the partial order is given by inclusion, the infimum is given by intersection, and the supremum is given by the smallest subsemiring containing the union.
NonUnitalSubsemiring.center definition
: NonUnitalSubsemiring R
Full source 
/-- The center of a semiring `R` is the set of elements that commute and associate with everything
in `R` -/
def center : NonUnitalSubsemiring R :=
  { Subsemigroup.center R with
    zero_mem' := Set.zero_mem_center
    add_mem' := Set.add_mem_center }
Center of a non-unital semiring
Informal description
The center of a non-unital semiring $R$ is the subset of elements that commute and associate with all elements in $R$. It forms a non-unital subsemiring of $R$ that contains the additive identity and is closed under addition.
NonUnitalSubsemiring.coe_center theorem
: ↑(center R) = Set.center R
Full source 
theorem coe_center : ↑(center R) = Set.center R :=
  rfl
Underlying Set of Non-unital Semiring Center Equals Set Center
Informal description
The underlying set of the center of a non-unital semiring $R$ is equal to the center of $R$ as a set, i.e., $\overline{\text{center}(R)} = \text{Set.center}(R)$.
NonUnitalSubsemiring.center_toSubsemigroup theorem
: (center R).toSubsemigroup = Subsemigroup.center R
Full source 
@[simp]
theorem center_toSubsemigroup :
    (center R).toSubsemigroup = Subsemigroup.center R :=
  rfl
Subsemigroup Correspondence of Non-unital Semiring Center
Informal description
The subsemigroup associated with the center of a non-unital semiring $R$ is equal to the center of $R$ as a subsemigroup, i.e., $(\text{center}(R)).\text{toSubsemigroup} = \text{Subsemigroup.center}(R)$.
NonUnitalSubsemiring.center.instNonUnitalCommSemiring instance
: NonUnitalCommSemiring (center R)
Full source 
/-- The center is commutative and associative. -/
instance center.instNonUnitalCommSemiring : NonUnitalCommSemiring (center R) :=
  { Subsemigroup.center.commSemigroup,
    NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring (center R) with }
Non-unital Commutative Semiring Structure on the Center
Informal description
The center of a non-unital semiring $R$ forms a non-unital commutative semiring. That is, the subset of elements in $R$ that commute with all other elements under multiplication inherits a non-unital commutative semiring structure from $R$.
Set.mem_center_iff_addMonoidHom theorem
(a : R) : a ∈ Set.center R ↔ AddMonoidHom.mulLeft a = .mulRight a ∧ AddMonoidHom.compr₂ .mul (.mulLeft a) = .comp .mul (.mulLeft a) ∧ AddMonoidHom.comp .mul (.mulRight a) = .compl₂ .mul (.mulLeft a) ∧ AddMonoidHom.compr₂ .mul (.mulRight a) = .compl₂ .mul (.mulRight a)
Full source 
/-- 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`. -/
lemma _root_.Set.mem_center_iff_addMonoidHom (a : R) :
    a ∈ Set.center Ra ∈ Set.center R ↔
      AddMonoidHom.mulLeft a = .mulRight a ∧
      AddMonoidHom.compr₂ .mul (.mulLeft a) = .comp .mul (.mulLeft a) ∧
      AddMonoidHom.comp .mul (.mulRight a) = .compl₂ .mul (.mulLeft a) ∧
      AddMonoidHom.compr₂ .mul (.mulRight a) = .compl₂ .mul (.mulRight a) := by
  rw [Set.mem_center_iff, isMulCentral_iff]
  simp [DFunLike.ext_iff]
Characterization of Central Elements via Multiplication Maps in Non-unital Semirings
Informal description
An element $a$ of a non-unital semiring $R$ belongs to the center of $R$ if and only if the following conditions hold: 1. The left multiplication map by $a$ equals the right multiplication map by $a$, i.e., $\text{mulLeft}(a) = \text{mulRight}(a)$. 2. The composition of multiplication with left multiplication by $a$ equals the precomposition of multiplication with left multiplication by $a$, i.e., $\text{compr}_2(\text{mul}, \text{mulLeft}(a)) = \text{comp}(\text{mul}, \text{mulLeft}(a))$. 3. The precomposition of multiplication with right multiplication by $a$ equals the postcomposition of multiplication with left multiplication by $a$, i.e., $\text{comp}(\text{mul}, \text{mulRight}(a)) = \text{compl}_2(\text{mul}, \text{mulLeft}(a))$. 4. The composition of multiplication with right multiplication by $a$ equals the postcomposition of multiplication with right multiplication by $a$, i.e., $\text{compr}_2(\text{mul}, \text{mulRight}(a)) = \text{compl}_2(\text{mul}, \text{mulRight}(a))$.
NonUnitalSubsemiring.centerCongr definition
[NonUnitalNonAssocSemiring S] (e : R ≃+* S) : center R ≃+* center S
Full source 
/-- The center of isomorphic (not necessarily unital or associative) semirings are isomorphic. -/
@[simps!] def centerCongr [NonUnitalNonAssocSemiring S] (e : R ≃+* S) : centercenter R ≃+* center S where
  __ := Subsemigroup.centerCongr e
  map_add' _ _ := Subtype.ext <| by exact map_add e ..
Isomorphism of centers of non-unital semirings under semiring isomorphism
Informal description
Given two non-unital non-associative semirings $R$ and $S$, and a semiring isomorphism $e : R \simeq^* S$, the centers of $R$ and $S$ are isomorphic as non-unital semirings. Specifically, the isomorphism $e$ restricts to an isomorphism between $\text{center}(R)$ and $\text{center}(S)$, where $\text{center}(R)$ denotes the subset of $R$ consisting of elements that commute with all elements of $R$.
NonUnitalSubsemiring.centerToMulOpposite definition
: center R ≃+* center Rᵐᵒᵖ
Full source 
/-- The center of a (not necessarily unital or associative) semiring
is isomorphic to the center of its opposite. -/
@[simps!] def centerToMulOpposite : centercenter R ≃+* center Rᵐᵒᵖ where
  __ := Subsemigroup.centerToMulOpposite
  map_add' _ _ := rfl
Isomorphism between the center of a non-unital semiring and its opposite
Informal description
The center of a non-unital semiring $R$ is isomorphic as a non-unital semiring to the center of its multiplicative opposite $R^{\text{op}}$. This isomorphism preserves both the additive and multiplicative structures.
NonUnitalSubsemiring.mem_center_iff theorem
{R} [NonUnitalSemiring R] {z : R} : z ∈ center R ↔ ∀ g, g * z = z * g
Full source 
theorem mem_center_iff {R} [NonUnitalSemiring R] {z : R} : z ∈ center Rz ∈ center R ↔ ∀ g, g * z = z * g := by
  rw [← Semigroup.mem_center_iff]
  exact Iff.rfl
Characterization of Central Elements in a Non-unital Semiring: $z \in Z(R) \leftrightarrow \forall g, gz = zg$
Informal description
For any element $z$ in a non-unital semiring $R$, $z$ belongs to the center of $R$ if and only if $z$ commutes with every element $g$ in $R$, i.e., $g * z = z * g$ for all $g \in R$.
NonUnitalSubsemiring.decidableMemCenter instance
{R} [NonUnitalSemiring R] [DecidableEq R] [Fintype R] : DecidablePred (· ∈ center R)
Full source 
instance decidableMemCenter {R} [NonUnitalSemiring R] [DecidableEq R] [Fintype R] :
    DecidablePred (· ∈ center R) := fun _ => decidable_of_iff' _ mem_center_iff
Decidability of Center Membership in Finite Non-unital Semirings
Informal description
For any finite non-unital semiring $R$ with decidable equality, the predicate determining membership in the center of $R$ is decidable.
NonUnitalSubsemiring.center_eq_top theorem
(R) [NonUnitalCommSemiring R] : center R = ⊤
Full source 
@[simp]
theorem center_eq_top (R) [NonUnitalCommSemiring R] : center R = ⊤ :=
  SetLike.coe_injective (Set.center_eq_univ R)
Center Equals Whole Semiring in Non-Unital Commutative Semirings
Informal description
For any non-unital commutative semiring $R$, the center of $R$ is equal to the entire semiring, i.e., $\text{center}(R) = R$.
NonUnitalSubsemiring.centralizer definition
{R} [NonUnitalSemiring R] (s : Set R) : NonUnitalSubsemiring R
Full source 
/-- The centralizer of a set as non-unital subsemiring. -/
def centralizer {R} [NonUnitalSemiring R] (s : Set R) : NonUnitalSubsemiring R :=
  { Subsemigroup.centralizer s with
    carrier := s.centralizer
    zero_mem' := Set.zero_mem_centralizer
    add_mem' := Set.add_mem_centralizer }
Centralizer as a non-unital subsemiring
Informal description
Given a non-unital semiring \( R \) and a subset \( s \) of \( R \), the centralizer of \( s \) is the non-unital subsemiring consisting of all elements \( c \in R \) that commute with every element of \( s \), i.e., \( c * m = m * c \) for all \( m \in s \). This subsemiring contains the additive identity (zero) and is closed under addition and multiplication.
NonUnitalSubsemiring.coe_centralizer theorem
{R} [NonUnitalSemiring R] (s : Set R) : (centralizer s : Set R) = s.centralizer
Full source 
@[simp, norm_cast]
theorem coe_centralizer {R} [NonUnitalSemiring R] (s : Set R) :
    (centralizer s : Set R) = s.centralizer :=
  rfl
Equality of Non-unital Subsemiring Centralizer and Set Centralizer
Informal description
For any non-unital semiring $R$ and subset $s \subseteq R$, the underlying set of the centralizer non-unital subsemiring of $s$ is equal to the set-theoretic centralizer of $s$, i.e., $\{c \in R \mid \forall g \in s, g * c = c * g\}$.
NonUnitalSubsemiring.centralizer_toSubsemigroup theorem
{R} [NonUnitalSemiring R] (s : Set R) : (centralizer s).toSubsemigroup = Subsemigroup.centralizer s
Full source 
theorem centralizer_toSubsemigroup {R} [NonUnitalSemiring R] (s : Set R) :
    (centralizer s).toSubsemigroup = Subsemigroup.centralizer s :=
  rfl
Equality of Non-unital Subsemiring Centralizer and Subsemigroup Centralizer
Informal description
For any non-unital semiring $R$ and subset $s \subseteq R$, the underlying subsemigroup of the centralizer non-unital subsemiring of $s$ is equal to the subsemigroup centralizer of $s$.
NonUnitalSubsemiring.mem_centralizer_iff theorem
{R} [NonUnitalSemiring R] {s : Set R} {z : R} : z ∈ centralizer s ↔ ∀ g ∈ s, g * z = z * g
Full source 
theorem mem_centralizer_iff {R} [NonUnitalSemiring R] {s : Set R} {z : R} :
    z ∈ centralizer sz ∈ centralizer s ↔ ∀ g ∈ s, g * z = z * g :=
  Iff.rfl
Characterization of Centralizer Elements in Non-unital Semirings
Informal description
Let $R$ be a non-unital semiring and $s$ be a subset of $R$. An element $z \in R$ belongs to the centralizer of $s$ if and only if $z$ commutes with every element $g \in s$, i.e., $g * z = z * g$ for all $g \in s$.
NonUnitalSubsemiring.center_le_centralizer theorem
{R} [NonUnitalSemiring R] (s) : center R ≤ centralizer s
Full source 
theorem center_le_centralizer {R} [NonUnitalSemiring R] (s) : center R ≤ centralizer s :=
  s.center_subset_centralizer
Center is Contained in Centralizer for Non-Unital Semirings
Informal description
For any non-unital semiring $R$ and subset $s \subseteq R$, the center of $R$ is contained in the centralizer of $s$, i.e., $\text{center}(R) \subseteq \text{centralizer}(s)$.
NonUnitalSubsemiring.centralizer_le theorem
{R} [NonUnitalSemiring R] (s t : Set R) (h : s ⊆ t) : centralizer t ≤ centralizer s
Full source 
theorem centralizer_le {R} [NonUnitalSemiring R] (s t : Set R) (h : s ⊆ t) :
    centralizer t ≤ centralizer s :=
  Set.centralizer_subset h
Centralizer Antimonotonicity: $s \subseteq t$ implies $\text{centralizer}(t) \leq \text{centralizer}(s)$
Informal description
Let $R$ be a non-unital semiring and $s, t$ be subsets of $R$ such that $s \subseteq t$. Then the centralizer of $t$ is contained in the centralizer of $s$, i.e., $\text{centralizer}(t) \leq \text{centralizer}(s)$.
NonUnitalSubsemiring.centralizer_eq_top_iff_subset theorem
{R} [NonUnitalSemiring R] {s : Set R} : centralizer s = ⊤ ↔ s ⊆ center R
Full source 
@[simp]
theorem centralizer_eq_top_iff_subset {R} [NonUnitalSemiring R] {s : Set R} :
    centralizercentralizer s = ⊤ ↔ s ⊆ center R :=
  SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset
Centralizer Equals Entire Semiring iff Subset is Central
Informal description
For a non-unital semiring $R$ and a subset $s$ of $R$, the centralizer of $s$ is equal to the entire semiring $R$ if and only if $s$ is contained in the center of $R$. In other words, $\text{centralizer}(s) = R \leftrightarrow s \subseteq \text{center}(R)$.
NonUnitalSubsemiring.centralizer_univ theorem
{R} [NonUnitalSemiring R] : centralizer Set.univ = center R
Full source 
@[simp]
theorem centralizer_univ {R} [NonUnitalSemiring R] : centralizer Set.univ = center R :=
  SetLike.ext' (Set.centralizer_univ R)
Centralizer of Universal Set Equals Center in Non-unital Semiring
Informal description
For any non-unital semiring $R$, the centralizer of the universal set (i.e., the set of all elements in $R$) is equal to the center of $R$. In other words, the set of elements that commute with every element of $R$ is precisely the center of $R$.
NonUnitalSubsemiring.closure definition
(s : Set R) : NonUnitalSubsemiring R
Full source 
/-- The `NonUnitalSubsemiring` generated by a set. -/
def closure (s : Set R) : NonUnitalSubsemiring R :=
  sInf { S | s ⊆ S }
Non-unital subsemiring generated by a set
Informal description
Given a subset $s$ of a non-unital non-associative semiring $R$, the non-unital subsemiring generated by $s$ is the smallest non-unital subsemiring of $R$ containing $s$. It is defined as the intersection of all non-unital subsemirings of $R$ that contain $s$.
NonUnitalSubsemiring.mem_closure theorem
{x : R} {s : Set R} : x ∈ closure s ↔ ∀ S : NonUnitalSubsemiring R, s ⊆ S → x ∈ S
Full source 
theorem mem_closure {x : R} {s : Set R} :
    x ∈ closure sx ∈ closure s ↔ ∀ S : NonUnitalSubsemiring R, s ⊆ S → x ∈ S :=
  mem_sInf
Characterization of Membership in Non-unital Subsemiring Closure
Informal description
For any element $x$ in a non-unital non-associative semiring $R$ and any subset $s$ of $R$, $x$ belongs to the non-unital subsemiring generated by $s$ if and only if $x$ is contained in every non-unital subsemiring $S$ of $R$ that contains $s$. In symbols: $$x \in \text{closure}(s) \leftrightarrow \forall S \leq R, s \subseteq S \to x \in S$$
NonUnitalSubsemiring.subset_closure theorem
{s : Set R} : s ⊆ closure s
Full source 
/-- The non-unital subsemiring generated by a set includes the set. -/
@[simp, aesop safe 20 apply (rule_sets := [SetLike])]
theorem subset_closure {s : Set R} : s ⊆ closure s := fun _ hx => mem_closure.2 fun _ hS => hS hx
Subset Property of Non-unital Subsemiring Closure
Informal description
For any subset $s$ of a non-unital non-associative semiring $R$, the set $s$ is contained in the non-unital subsemiring generated by $s$, i.e., $s \subseteq \text{closure}(s)$.
NonUnitalSubsemiring.not_mem_of_not_mem_closure theorem
{s : Set R} {P : R} (hP : P ∉ closure s) : P ∉ s
Full source 
theorem not_mem_of_not_mem_closure {s : Set R} {P : R} (hP : P ∉ closure s) : P ∉ s := fun h =>
  hP (subset_closure h)
Non-membership in Subsemiring Closure Implies Non-membership in Original Set
Informal description
For any subset $s$ of a non-unital non-associative semiring $R$ and any element $P \in R$, if $P$ does not belong to the non-unital subsemiring generated by $s$, then $P$ does not belong to $s$. In other words, $P \notin \text{closure}(s)$ implies $P \notin s$.
NonUnitalSubsemiring.closure_le theorem
{s : Set R} {t : NonUnitalSubsemiring R} : closure s ≤ t ↔ s ⊆ t
Full source 
/-- A non-unital subsemiring `S` includes `closure s` if and only if it includes `s`. -/
@[simp]
theorem closure_le {s : Set R} {t : NonUnitalSubsemiring R} : closureclosure s ≤ t ↔ s ⊆ t :=
  ⟨Set.Subset.trans subset_closure, fun h => sInf_le h⟩
Characterization of Non-unital Subsemiring Closure: $\text{closure}(s) \leq t \leftrightarrow s \subseteq t$
Informal description
For any subset $s$ of a non-unital non-associative semiring $R$ and any non-unital subsemiring $t$ of $R$, the non-unital subsemiring generated by $s$ is contained in $t$ if and only if $s$ is a subset of $t$. In other words, $\text{closure}(s) \leq t \leftrightarrow s \subseteq t$.
NonUnitalSubsemiring.closure_mono theorem
⦃s t : Set R⦄ (h : s ⊆ t) : closure s ≤ closure t
Full source 
/-- Subsemiring closure of a set is monotone in its argument: if `s ⊆ t`,
then `closure s ≤ closure t`. -/
@[gcongr]
theorem closure_mono ⦃s t : Set R⦄ (h : s ⊆ t) : closure s ≤ closure t :=
  closure_le.2 <| Set.Subset.trans h subset_closure
Monotonicity of Non-unital Subsemiring Closure
Informal description
For any subsets $s$ and $t$ of a non-unital non-associative semiring $R$, if $s$ is a subset of $t$, then the non-unital subsemiring generated by $s$ is contained in the non-unital subsemiring generated by $t$, i.e., $\text{closure}(s) \leq \text{closure}(t)$.
NonUnitalSubsemiring.closure_eq_of_le theorem
{s : Set R} {t : NonUnitalSubsemiring R} (h₁ : s ⊆ t) (h₂ : t ≤ closure s) : closure s = t
Full source 
theorem closure_eq_of_le {s : Set R} {t : NonUnitalSubsemiring R} (h₁ : s ⊆ t)
    (h₂ : t ≤ closure s) : closure s = t :=
  le_antisymm (closure_le.2 h₁) h₂
Closure Equality Condition for Non-unital Subsemirings: $\text{closure}(s) = t$ given $s \subseteq t$ and $t \leq \text{closure}(s)$
Informal description
For any subset $s$ of a non-unital non-associative semiring $R$ and any non-unital subsemiring $t$ of $R$, if $s$ is contained in $t$ and $t$ is contained in the closure of $s$, then the closure of $s$ is equal to $t$. In other words, if $s \subseteq t$ and $t \leq \text{closure}(s)$, then $\text{closure}(s) = t$.
NonUnitalSubsemiring.closure_le_centralizer_centralizer theorem
{R : Type*} [NonUnitalSemiring R] (s : Set R) : closure s ≤ centralizer (centralizer s)
Full source 
lemma closure_le_centralizer_centralizer {R : Type*} [NonUnitalSemiring R] (s : Set R) :
    closure s ≤ centralizer (centralizer s) :=
  closure_le.mpr Set.subset_centralizer_centralizer
Subsemiring Closure is Contained in Double Centralizer
Informal description
For any subset $s$ of a non-unital semiring $R$, the non-unital subsemiring generated by $s$ is contained in the centralizer of the centralizer of $s$, i.e., \[ \text{closure}(s) \leq \text{centralizer}(\text{centralizer}(s)). \]
NonUnitalSubsemiring.closureNonUnitalCommSemiringOfComm abbrev
{R : Type*} [NonUnitalSemiring R] {s : Set R} (hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x) : NonUnitalCommSemiring (closure s)
Full source 
/-- If all the elements of a set `s` commute, then `closure s` is a non-unital commutative
semiring. -/
abbrev closureNonUnitalCommSemiringOfComm {R : Type*} [NonUnitalSemiring R] {s : Set R}
    (hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x) : NonUnitalCommSemiring (closure s) :=
  { NonUnitalSubsemiringClass.toNonUnitalSemiring (closure s)  with
    mul_comm := fun ⟨_, h₁⟩ ⟨_, h₂⟩ ↦
      have := closure_le_centralizer_centralizer s
      Subtype.ext <| Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂) }
Non-unital Commutative Semiring Structure on Closure of Commuting Set
Informal description
Let $R$ be a non-unital semiring and $s$ a subset of $R$ such that all elements of $s$ commute with each other (i.e., $x \cdot y = y \cdot x$ for all $x, y \in s$). Then the non-unital subsemiring generated by $s$, denoted $\text{closure}(s)$, forms a non-unital commutative semiring.
NonUnitalSubsemiring.mem_map_equiv theorem
{f : R ≃+* S} {K : NonUnitalSubsemiring R} {x : S} : x ∈ K.map (f : R →ₙ+* S) ↔ f.symm x ∈ K
Full source 
theorem mem_map_equiv {f : R ≃+* S} {K : NonUnitalSubsemiring R} {x : S} :
    x ∈ K.map (f : R →ₙ+* S)x ∈ K.map (f : R →ₙ+* S) ↔ f.symm x ∈ K := by
  convert @Set.mem_image_equiv _ _ (↑K) f.toEquiv x
Characterization of Image Membership via Ring Equivalence Inverse
Informal description
Let $R$ and $S$ be non-unital non-associative semirings, and let $f \colon R \simeq S$ be a ring equivalence. For any non-unital subsemiring $K$ of $R$ and any element $x \in S$, the element $x$ belongs to the image of $K$ under $f$ if and only if the inverse equivalence $f^{-1}$ maps $x$ back into $K$, i.e., \[ x \in f(K) \leftrightarrow f^{-1}(x) \in K. \]
NonUnitalSubsemiring.map_equiv_eq_comap_symm theorem
(f : R ≃+* S) (K : NonUnitalSubsemiring R) : K.map (f : R →ₙ+* S) = K.comap f.symm
Full source 
theorem map_equiv_eq_comap_symm (f : R ≃+* S) (K : NonUnitalSubsemiring R) :
    K.map (f : R →ₙ+* S) = K.comap f.symm :=
  SetLike.coe_injective (f.toEquiv.image_eq_preimage K)
Image-Preimage Duality for Non-unital Subsemirings under Ring Isomorphism
Informal description
Let $R$ and $S$ be non-unital semirings, and let $f \colon R \simeq S$ be a ring isomorphism. For any non-unital subsemiring $K$ of $R$, the image of $K$ under $f$ is equal to the preimage of $K$ under the inverse isomorphism $f^{-1}$. That is, \[ f(K) = f^{-1}^{-1}(K). \]
NonUnitalSubsemiring.comap_equiv_eq_map_symm theorem
(f : R ≃+* S) (K : NonUnitalSubsemiring S) : K.comap (f : R →ₙ+* S) = K.map f.symm
Full source 
theorem comap_equiv_eq_map_symm (f : R ≃+* S) (K : NonUnitalSubsemiring S) :
    K.comap (f : R →ₙ+* S) = K.map f.symm :=
  (map_equiv_eq_comap_symm f.symm K).symm
Preimage-Image Duality for Non-unital Subsemirings under Ring Isomorphism
Informal description
Let $R$ and $S$ be non-unital semirings, and let $f \colon R \simeq S$ be a ring isomorphism. For any non-unital subsemiring $K$ of $S$, the preimage of $K$ under $f$ is equal to the image of $K$ under the inverse isomorphism $f^{-1}$. That is, \[ f^{-1}(K) = f^{-1}(K). \]
Subsemigroup.nonUnitalSubsemiringClosure definition
(M : Subsemigroup R) : NonUnitalSubsemiring R
Full source 
/-- The additive closure of a non-unital subsemigroup is a non-unital subsemiring. -/
def nonUnitalSubsemiringClosure (M : Subsemigroup R) : NonUnitalSubsemiring R :=
  { AddSubmonoid.closure (M : Set R) with mul_mem' := MulMemClass.mul_mem_add_closure }
Non-unital subsemiring closure of a subsemigroup
Informal description
Given a multiplicative subsemigroup \( M \) of a non-unital semiring \( R \), the non-unital subsemiring closure of \( M \) is the smallest non-unital subsemiring of \( R \) containing \( M \). It is obtained by taking the additive closure of \( M \) (i.e., the smallest additive submonoid containing \( M \)) and ensuring it is closed under multiplication.
Subsemigroup.nonUnitalSubsemiringClosure_coe theorem
: (M.nonUnitalSubsemiringClosure : Set R) = AddSubmonoid.closure (M : Set R)
Full source 
theorem nonUnitalSubsemiringClosure_coe :
    (M.nonUnitalSubsemiringClosure : Set R) = AddSubmonoid.closure (M : Set R) :=
  rfl
Non-unital subsemiring closure equals additive closure of subsemigroup
Informal description
For a multiplicative subsemigroup $M$ of a non-unital semiring $R$, the underlying set of the non-unital subsemiring closure of $M$ is equal to the additive closure of $M$ as a subset of $R$. That is, \[ M.\text{nonUnitalSubsemiringClosure} = \text{AddSubmonoid.closure}(M). \]
Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid theorem
: M.nonUnitalSubsemiringClosure.toAddSubmonoid = AddSubmonoid.closure (M : Set R)
Full source 
theorem nonUnitalSubsemiringClosure_toAddSubmonoid :
    M.nonUnitalSubsemiringClosure.toAddSubmonoid = AddSubmonoid.closure (M : Set R) :=
  rfl
Additive Submonoid of Non-Unital Subsemiring Closure Equals Additive Closure of Subsemigroup
Informal description
For a multiplicative subsemigroup $M$ of a non-unital semiring $R$, the additive submonoid of the non-unital subsemiring closure of $M$ is equal to the additive closure of $M$ as a subset of $R$. That is, \[ \text{toAddSubmonoid}(M.\text{nonUnitalSubsemiringClosure}) = \text{AddSubmonoid.closure}(M). \]
Subsemigroup.nonUnitalSubsemiringClosure_eq_closure theorem
: M.nonUnitalSubsemiringClosure = NonUnitalSubsemiring.closure (M : Set R)
Full source 
/-- The `NonUnitalSubsemiring` generated by a multiplicative subsemigroup coincides with the
`NonUnitalSubsemiring.closure` of the subsemigroup itself . -/
theorem nonUnitalSubsemiringClosure_eq_closure :
    M.nonUnitalSubsemiringClosure = NonUnitalSubsemiring.closure (M : Set R) := by
  ext
  refine ⟨fun hx => ?_,
    fun hx => (NonUnitalSubsemiring.mem_closure.mp hx) M.nonUnitalSubsemiringClosure fun s sM => ?_⟩
  <;> rintro - ⟨H1, rfl⟩
  <;> rintro - ⟨H2, rfl⟩
  · exact AddSubmonoid.mem_closure.mp hx H1.toAddSubmonoid H2
  · exact H2 sM
Non-Unital Subsemiring Closure of Subsemigroup Equals Subsemiring Generated by Subsemigroup
Informal description
For any multiplicative subsemigroup $M$ of a non-unital semiring $R$, the non-unital subsemiring closure of $M$ is equal to the non-unital subsemiring generated by $M$ as a subset of $R$. That is, \[ M.\text{nonUnitalSubsemiringClosure} = \text{NonUnitalSubsemiring.closure}(M). \]
NonUnitalSubsemiring.closure_subsemigroup_closure theorem
(s : Set R) : closure ↑(Subsemigroup.closure s) = closure s
Full source 
@[simp]
theorem closure_subsemigroup_closure (s : Set R) : closure ↑(Subsemigroup.closure s) = closure s :=
  le_antisymm
    (closure_le.mpr fun _ hy =>
      (Subsemigroup.mem_closure.mp hy) (closure s).toSubsemigroup subset_closure)
    (closure_mono Subsemigroup.subset_closure)
Closure Equivalence: $\text{closure}(\text{Subsemigroup.closure}(s)) = \text{closure}(s)$
Informal description
For any subset $s$ of a non-unital non-associative semiring $R$, the non-unital subsemiring closure of the subsemigroup closure of $s$ is equal to the non-unital subsemiring closure of $s$. That is, \[ \text{closure}(\text{Subsemigroup.closure}(s)) = \text{closure}(s). \]
NonUnitalSubsemiring.coe_closure_eq theorem
(s : Set R) : (closure s : Set R) = AddSubmonoid.closure (Subsemigroup.closure s : Set R)
Full source 
/-- The elements of the non-unital subsemiring closure of `M` are exactly the elements of the
additive closure of a multiplicative subsemigroup `M`. -/
theorem coe_closure_eq (s : Set R) :
    (closure s : Set R) = AddSubmonoid.closure (Subsemigroup.closure s : Set R) := by
  simp [← Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid,
    Subsemigroup.nonUnitalSubsemiringClosure_eq_closure]
Non-unital Subsemiring Closure as Additive Closure of Multiplicative Closure
Informal description
For any subset $s$ of a non-unital non-associative semiring $R$, the underlying set of the non-unital subsemiring closure of $s$ is equal to the additive submonoid closure of the multiplicative subsemigroup closure of $s$. That is, \[ \text{closure}(s) = \text{AddSubmonoid.closure}(\text{Subsemigroup.closure}(s)). \]
NonUnitalSubsemiring.mem_closure_iff theorem
{s : Set R} {x} : x ∈ closure s ↔ x ∈ AddSubmonoid.closure (Subsemigroup.closure s : Set R)
Full source 
theorem mem_closure_iff {s : Set R} {x} :
    x ∈ closure sx ∈ closure s ↔ x ∈ AddSubmonoid.closure (Subsemigroup.closure s : Set R) :=
  Set.ext_iff.mp (coe_closure_eq s) x
Characterization of Non-unital Subsemiring Membership via Additive and Multiplicative Closures
Informal description
For any subset $s$ of a non-unital non-associative semiring $R$ and any element $x \in R$, $x$ belongs to the non-unital subsemiring generated by $s$ if and only if $x$ belongs to the additive submonoid generated by the multiplicative subsemigroup generated by $s$. That is, \[ x \in \text{closure}(s) \leftrightarrow x \in \text{AddSubmonoid.closure}(\text{Subsemigroup.closure}(s)). \]
NonUnitalSubsemiring.closure_addSubmonoid_closure theorem
{s : Set R} : closure ↑(AddSubmonoid.closure s) = closure s
Full source 
@[simp]
theorem closure_addSubmonoid_closure {s : Set R} :
    closure ↑(AddSubmonoid.closure s) = closure s := by
  ext x
  refine ⟨fun hx => ?_, fun hx => closure_mono AddSubmonoid.subset_closure hx⟩
  rintro - ⟨H, rfl⟩
  rintro - ⟨J, rfl⟩
  refine (AddSubmonoid.mem_closure.mp (mem_closure_iff.mp hx)) H.toAddSubmonoid fun y hy => ?_
  refine (Subsemigroup.mem_closure.mp hy) H.toSubsemigroup fun z hz => ?_
  exact (AddSubmonoid.mem_closure.mp hz) H.toAddSubmonoid fun w hw => J hw
Equality of Non-unital Subsemiring Closures via Additive Submonoid Closure
Informal description
For any subset $s$ of a non-unital non-associative semiring $R$, the non-unital subsemiring generated by the additive submonoid closure of $s$ is equal to the non-unital subsemiring generated by $s$ itself. That is, \[ \text{closure}(\text{AddSubmonoid.closure}(s)) = \text{closure}(s). \]
NonUnitalSubsemiring.closure_induction theorem
{s : Set R} {p : (x : R) → x ∈ closure s → Prop} (mem : ∀ (x) (hx : x ∈ s), p x (subset_closure hx)) (zero : p 0 (zero_mem _)) (add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (add_mem hx hy)) (mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy)) {x} (hx : x ∈ closure s) : p x hx
Full source 
/-- 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`. -/
@[elab_as_elim]
theorem closure_induction {s : Set R} {p : (x : R) → x ∈ closure s → Prop}
    (mem : ∀ (x) (hx : x ∈ s), p x (subset_closure hx)) (zero : p 0 (zero_mem _))
    (add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (add_mem hx hy))
    (mul : ∀ x y hx hy, p x hx → p y hy → p (x * y) (mul_mem hx hy))
    {x} (hx : x ∈ closure s) : p x hx :=
  let K : NonUnitalSubsemiring R :=
    { carrier := { x | ∃ hx, p x hx }
      mul_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, mul _ _ _ _ hpx hpy⟩
      add_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, add _ _ _ _ hpx hpy⟩
      zero_mem' := ⟨_, zero⟩ }
  closure_le (t := K) |>.mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id
Induction Principle for Non-unital Subsemiring Closure Membership
Informal description
Let $R$ be a non-unital non-associative semiring and $s$ a subset of $R$. Suppose $p$ is a predicate on elements of the non-unital subsemiring generated by $s$ (denoted $\text{closure}(s)$) such that: 1. $p(x)$ holds for all $x \in s$, 2. $p(0)$ holds, 3. For any $x, y \in \text{closure}(s)$, if $p(x)$ and $p(y)$ hold, then $p(x + y)$ holds, 4. For any $x, y \in \text{closure}(s)$, if $p(x)$ and $p(y)$ hold, then $p(x \cdot y)$ holds. Then $p(x)$ holds for all $x \in \text{closure}(s)$.
NonUnitalSubsemiring.closure_induction₂ theorem
{s : Set R} {p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop} (mem_mem : ∀ (x) (hx : x ∈ s) (y) (hy : y ∈ s), p x y (subset_closure hx) (subset_closure hy)) (zero_left : ∀ x hx, p 0 x (zero_mem _) hx) (zero_right : ∀ x hx, p x 0 hx (zero_mem _)) (add_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x + y) z (add_mem hx hy) hz) (add_right : ∀ x y z hx hy hz, p x y hx hy → p x z hx hz → p x (y + z) hx (add_mem hy hz)) (mul_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x * y) z (mul_mem hx hy) hz) (mul_right : ∀ x y z hx hy hz, p x y hx hy → p x z hx hz → p x (y * z) hx (mul_mem hy hz)) {x y : R} (hx : x ∈ closure s) (hy : y ∈ closure s) : p x y hx hy
Full source 
/-- An induction principle for closure membership for predicates with two arguments. -/
@[elab_as_elim]
theorem closure_induction₂ {s : Set R} {p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop}
    (mem_mem : ∀ (x) (hx : x ∈ s) (y) (hy : y ∈ s), p x y (subset_closure hx) (subset_closure hy))
    (zero_left : ∀ x hx, p 0 x (zero_mem _) hx) (zero_right : ∀ x hx, p x 0 hx (zero_mem _))
    (add_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x + y) z (add_mem hx hy) hz)
    (add_right : ∀ x y z hx hy hz, p x y hx hy → p x z hx hz → p x (y + z) hx (add_mem hy hz))
    (mul_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x * y) z (mul_mem hx hy) hz)
    (mul_right : ∀ x y z hx hy hz, p x y hx hy → p x z hx hz → p x (y * z) hx (mul_mem hy hz))
    {x y : R} (hx : x ∈ closure s) (hy : y ∈ closure s) :
    p x y hx hy := by
  induction hy using closure_induction with
  | mem z hz => induction hx using closure_induction with
    | mem _ h => exact mem_mem _ h _ hz
    | zero => exact zero_left _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
  | zero => exact zero_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
Two-Variable Induction Principle for Non-unital Subsemiring Closure Membership
Informal description
Let $R$ be a non-unital non-associative semiring and $s$ a subset of $R$. Suppose $p$ is a predicate on pairs of elements from the non-unital subsemiring generated by $s$ (denoted $\text{closure}(s)$) such that: 1. $p(x,y)$ holds for all $x, y \in s$, 2. $p(0,x)$ and $p(x,0)$ hold for all $x \in \text{closure}(s)$, 3. For any $x, y, z \in \text{closure}(s)$, if $p(x,z)$ and $p(y,z)$ hold, then $p(x+y,z)$ holds, 4. For any $x, y, z \in \text{closure}(s)$, if $p(x,y)$ and $p(x,z)$ hold, then $p(x,y+z)$ holds, 5. For any $x, y, z \in \text{closure}(s)$, if $p(x,z)$ and $p(y,z)$ hold, then $p(x \cdot y,z)$ holds, 6. For any $x, y, z \in \text{closure}(s)$, if $p(x,y)$ and $p(x,z)$ hold, then $p(x,y \cdot z)$ holds. Then $p(x,y)$ holds for all $x, y \in \text{closure}(s)$.
NonUnitalSubsemiring.gi definition
: GaloisInsertion (@closure R _) (↑)
Full source 
/-- `closure` forms a Galois insertion with the coercion to set. -/
protected def gi : GaloisInsertion (@closure R _) (↑) where
  choice s _ := closure s
  gc _ _ := closure_le
  le_l_u _ := subset_closure
  choice_eq _ _ := rfl
Galois insertion between subsets and non-unital subsemirings
Informal description
The pair of functions `(closure, (↑))` forms a Galois insertion between the power set of a non-unital non-associative semiring $R$ and the lattice of non-unital subsemirings of $R$. Here, `closure` is the function that takes a subset $s$ of $R$ to the smallest non-unital subsemiring containing $s$, and `(↑)` is the coercion function that takes a non-unital subsemiring to its underlying subset. This means: 1. For any subset $s$ of $R$ and any non-unital subsemiring $t$ of $R$, we have $\text{closure}(s) \leq t$ if and only if $s \subseteq t$. 2. The composition `(↑) ∘ closure` is the identity function on the lattice of non-unital subsemirings. 3. The function `closure` is a retraction of the coercion `(↑)`, and `(↑)` is a section of `closure`.
NonUnitalSubsemiring.closure_eq theorem
(s : NonUnitalSubsemiring R) : closure (s : Set R) = s
Full source 
/-- Closure of a non-unital subsemiring `S` equals `S`. -/
@[simp]
theorem closure_eq (s : NonUnitalSubsemiring R) : closure (s : Set R) = s :=
  (NonUnitalSubsemiring.gi R).l_u_eq s
Closure of a Non-Unital Subsemiring Equals Itself
Informal description
For any non-unital subsemiring $S$ of a non-unital non-associative semiring $R$, the closure of $S$ (viewed as a subset of $R$) is equal to $S$ itself.
NonUnitalSubsemiring.closure_empty theorem
: closure (∅ : Set R) = ⊥
Full source 
@[simp]
theorem closure_empty : closure (∅ : Set R) = ⊥ :=
  (NonUnitalSubsemiring.gi R).gc.l_bot
Empty Set Generates the Zero Subsemiring
Informal description
The non-unital subsemiring generated by the empty set in a non-unital semiring $R$ is the bottom element of the lattice of non-unital subsemirings of $R$, which is the subsemiring consisting of only the zero element $\{0\}$.
NonUnitalSubsemiring.closure_univ theorem
: closure (Set.univ : Set R) = ⊤
Full source 
@[simp]
theorem closure_univ : closure (Set.univ : Set R) = ⊤ :=
  @coe_top R _ ▸ closure_eq ⊤
Universal Set Generates the Whole Non-Unital Subsemiring
Informal description
The non-unital subsemiring generated by the universal set of a non-unital semiring $R$ is equal to the top element of the lattice of non-unital subsemirings of $R$, i.e., $\text{closure}(\text{Set.univ}) = \top$.
NonUnitalSubsemiring.closure_union theorem
(s t : Set R) : closure (s ∪ t) = closure s ⊔ closure t
Full source 
theorem closure_union (s t : Set R) : closure (s ∪ t) = closureclosure s ⊔ closure t :=
  (NonUnitalSubsemiring.gi R).gc.l_sup
Closure of Union Equals Supremum of Closures in Non-Unital Subsemirings
Informal description
For any two subsets $s$ and $t$ of a non-unital semiring $R$, the non-unital subsemiring generated by their union $s \cup t$ is equal to the supremum of the non-unital subsemirings generated by $s$ and $t$ individually, i.e., $\text{closure}(s \cup t) = \text{closure}(s) \sqcup \text{closure}(t)$.
NonUnitalSubsemiring.closure_iUnion theorem
{ι} (s : ι → Set R) : closure (⋃ i, s i) = ⨆ i, closure (s i)
Full source 
theorem closure_iUnion {ι} (s : ι → Set R) : closure (⋃ i, s i) = ⨆ i, closure (s i) :=
  (NonUnitalSubsemiring.gi R).gc.l_iSup
Closure of Union Equals Supremum of Closures in Non-unital Subsemirings
Informal description
For any indexed family of subsets $(s_i)_{i \in \iota}$ of a non-unital semiring $R$, the non-unital subsemiring generated by their union $\bigcup_i s_i$ is equal to the supremum of the non-unital subsemirings generated by each individual subset $s_i$. That is, \[ \text{closure}\left(\bigcup_{i \in \iota} s_i\right) = \bigsqcup_{i \in \iota} \text{closure}(s_i). \]
NonUnitalSubsemiring.closure_sUnion theorem
(s : Set (Set R)) : closure (⋃₀ s) = ⨆ t ∈ s, closure t
Full source 
theorem closure_sUnion (s : Set (Set R)) : closure (⋃₀ s) = ⨆ t ∈ s, closure t :=
  (NonUnitalSubsemiring.gi R).gc.l_sSup
Closure of Union of Subsets Equals Supremum of Closures in Non-Unital Subsemirings
Informal description
For any collection $s$ of subsets of a non-unital non-associative semiring $R$, the non-unital subsemiring generated by the union of all sets in $s$ is equal to the supremum of the non-unital subsemirings generated by each individual set in $s$. That is, \[ \text{closure}\left(\bigcup_{t \in s} t\right) = \bigsqcup_{t \in s} \text{closure}(t). \]
NonUnitalSubsemiring.map_sup theorem
(s t : NonUnitalSubsemiring R) (f : F) : (map f (s ⊔ t) : NonUnitalSubsemiring S) = map f s ⊔ map f t
Full source 
theorem map_sup (s t : NonUnitalSubsemiring R) (f : F) :
    (map f (s ⊔ t) : NonUnitalSubsemiring S) = mapmap f s ⊔ map f t :=
  @GaloisConnection.l_sup _ _ s t _ _ _ _ (gc_map_comap f)
Image of Supremum of Non-unital Subsemirings Equals Supremum of Images
Informal description
Let $R$ and $S$ be non-unital semirings, and let $f \colon R \to S$ be a non-unital ring homomorphism. For any two non-unital subsemirings $s$ and $t$ of $R$, the image of their supremum $s \sqcup t$ under $f$ equals the supremum of their images, i.e., \[ f(s \sqcup t) = f(s) \sqcup f(t). \]
NonUnitalSubsemiring.map_iSup theorem
{ι : Sort*} (f : F) (s : ι → NonUnitalSubsemiring R) : (map f (iSup s) : NonUnitalSubsemiring S) = ⨆ i, map f (s i)
Full source 
theorem map_iSup {ι : Sort*} (f : F) (s : ι → NonUnitalSubsemiring R) :
    (map f (iSup s) : NonUnitalSubsemiring S) = ⨆ i, map f (s i) :=
  @GaloisConnection.l_iSup _ _ _ _ _ _ _ (gc_map_comap f) s
Image of Supremum of Non-unital Subsemirings Equals Supremum of Images
Informal description
Let $R$ and $S$ be non-unital non-associative semirings, and let $f \colon R \to S$ be a non-unital ring homomorphism. For any family $\{S_i\}_{i \in \iota}$ of non-unital subsemirings of $R$, the image of the supremum $\bigsqcup_{i \in \iota} S_i$ under $f$ is equal to the supremum of the images $\bigsqcup_{i \in \iota} f(S_i)$. In other words, $f\left(\bigsqcup_{i \in \iota} S_i\right) = \bigsqcup_{i \in \iota} f(S_i)$.
NonUnitalSubsemiring.map_inf theorem
(s t : NonUnitalSubsemiring R) (f : F) (hf : Function.Injective f) : (map f (s ⊓ t) : NonUnitalSubsemiring S) = map f s ⊓ map f t
Full source 
theorem map_inf (s t : NonUnitalSubsemiring R) (f : F) (hf : Function.Injective f) :
    (map f (s ⊓ t) : NonUnitalSubsemiring S) = mapmap f s ⊓ map f t :=
  SetLike.coe_injective (Set.image_inter hf)
Image of Intersection of Non-unital Subsemirings under Injective Homomorphism Equals Intersection of Images
Informal description
Let $R$ and $S$ be non-unital non-associative semirings, and let $f \colon R \to S$ be an injective non-unital ring homomorphism. For any two non-unital subsemirings $s$ and $t$ of $R$, the image of their intersection $s \sqcap t$ under $f$ equals the intersection of their images, i.e., $f(s \sqcap t) = f(s) \sqcap f(t)$.
NonUnitalSubsemiring.map_iInf theorem
{ι : Sort*} [Nonempty ι] (f : F) (hf : Function.Injective f) (s : ι → NonUnitalSubsemiring R) : (map f (iInf s) : NonUnitalSubsemiring S) = ⨅ i, map f (s i)
Full source 
theorem map_iInf {ι : Sort*} [Nonempty ι] (f : F) (hf : Function.Injective f)
    (s : ι → NonUnitalSubsemiring R) :
    (map f (iInf s) : NonUnitalSubsemiring S) = ⨅ i, map f (s i) := by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coeSetLike.coe ∘ s)
Image of Infimum of Non-unital Subsemirings under Injective Homomorphism Equals Infimum of Images
Informal description
Let $R$ and $S$ be non-unital non-associative semirings, and let $f \colon R \to S$ be an injective non-unital ring homomorphism. For any nonempty index set $\iota$ and any family $\{S_i\}_{i \in \iota}$ of non-unital subsemirings of $R$, the image of the infimum $\bigsqcap_{i \in \iota} S_i$ under $f$ is equal to the infimum of the images $\bigsqcap_{i \in \iota} f(S_i)$. In other words, $f\left(\bigsqcap_{i \in \iota} S_i\right) = \bigsqcap_{i \in \iota} f(S_i)$.
NonUnitalSubsemiring.comap_inf theorem
(s t : NonUnitalSubsemiring S) (f : F) : (comap f (s ⊓ t) : NonUnitalSubsemiring R) = comap f s ⊓ comap f t
Full source 
theorem comap_inf (s t : NonUnitalSubsemiring S) (f : F) :
    (comap f (s ⊓ t) : NonUnitalSubsemiring R) = comapcomap f s ⊓ comap f t :=
  @GaloisConnection.u_inf _ _ s t _ _ _ _ (gc_map_comap f)
Preimage of Intersection of Non-unital Subsemirings Equals Intersection of Preimages
Informal description
For any non-unital ring homomorphism $f \colon R \to S$ and any two non-unital subsemirings $s, t$ of $S$, the preimage of their intersection $s \sqcap t$ under $f$ equals the intersection of their preimages, i.e., $f^{-1}(s \sqcap t) = f^{-1}(s) \sqcap f^{-1}(t)$.
NonUnitalSubsemiring.comap_iInf theorem
{ι : Sort*} (f : F) (s : ι → NonUnitalSubsemiring S) : (comap f (iInf s) : NonUnitalSubsemiring R) = ⨅ i, comap f (s i)
Full source 
theorem comap_iInf {ι : Sort*} (f : F) (s : ι → NonUnitalSubsemiring S) :
    (comap f (iInf s) : NonUnitalSubsemiring R) = ⨅ i, comap f (s i) :=
  @GaloisConnection.u_iInf _ _ _ _ _ _ _ (gc_map_comap f) s
Preimage of Infimum of Non-unital Subsemirings Equals Infimum of Preimages
Informal description
Let $R$ and $S$ be non-unital non-associative semirings, and let $f \colon R \to S$ be a non-unital ring homomorphism. For any family $\{s_i\}_{i \in \iota}$ of non-unital subsemirings of $S$, the preimage of their infimum under $f$ equals the infimum of their preimages: \[ f^{-1}\left(\bigsqcap_{i \in \iota} s_i\right) = \bigsqcap_{i \in \iota} f^{-1}(s_i). \]
NonUnitalSubsemiring.map_bot theorem
(f : F) : map f (⊥ : NonUnitalSubsemiring R) = (⊥ : NonUnitalSubsemiring S)
Full source 
@[simp]
theorem map_bot (f : F) : map f (⊥ : NonUnitalSubsemiring R) = (⊥ : NonUnitalSubsemiring S) :=
  (gc_map_comap f).l_bot
Image of Bottom Subsemiring is Bottom Subsemiring
Informal description
For any non-unital ring homomorphism $f \colon R \to S$, the image of the bottom non-unital subsemiring of $R$ (which is $\{0\}$) under $f$ is equal to the bottom non-unital subsemiring of $S$ (which is $\{0\}$). In other words, $f(\{0\}) = \{0\}$.
NonUnitalSubsemiring.comap_top theorem
(f : F) : comap f (⊤ : NonUnitalSubsemiring S) = (⊤ : NonUnitalSubsemiring R)
Full source 
@[simp]
theorem comap_top (f : F) : comap f (⊤ : NonUnitalSubsemiring S) = (⊤ : NonUnitalSubsemiring R) :=
  (gc_map_comap f).u_top
Preimage of Top Non-Unital Subsemiring is Top
Informal description
For any non-unital ring homomorphism $f \colon R \to S$, the preimage of the top non-unital subsemiring of $S$ (which is $S$ itself) under $f$ is the top non-unital subsemiring of $R$ (which is $R$ itself). In other words, $f^{-1}(S) = R$.
NonUnitalSubsemiring.prod definition
(s : NonUnitalSubsemiring R) (t : NonUnitalSubsemiring S) : NonUnitalSubsemiring (R × S)
Full source 
/-- Given `NonUnitalSubsemiring`s `s`, `t` of semirings `R`, `S` respectively, `s.prod t` is
`s × t` as a non-unital subsemiring of `R × S`. -/
def prod (s : NonUnitalSubsemiring R) (t : NonUnitalSubsemiring S) : NonUnitalSubsemiring (R × S) :=
  { s.toSubsemigroup.prod t.toSubsemigroup, s.toAddSubmonoid.prod t.toAddSubmonoid with
    carrier := (s : Set R) ×ˢ (t : Set S) }
Product of non-unital subsemirings
Informal description
Given non-unital subsemirings $s$ of $R$ and $t$ of $S$, the product $s \times t$ is a non-unital subsemiring of $R \times S$. It consists of all pairs $(r, s)$ where $r \in s$ and $s \in t$, and inherits the additive and multiplicative structures from $s$ and $t$.
NonUnitalSubsemiring.coe_prod theorem
(s : NonUnitalSubsemiring R) (t : NonUnitalSubsemiring S) : (s.prod t : Set (R × S)) = (s : Set R) ×ˢ (t : Set S)
Full source 
@[norm_cast]
theorem coe_prod (s : NonUnitalSubsemiring R) (t : NonUnitalSubsemiring S) :
    (s.prod t : Set (R × S)) = (s : Set R) ×ˢ (t : Set S) :=
  rfl
Underlying Set of Product Subsemiring is Cartesian Product
Informal description
For any non-unital subsemirings $s$ of $R$ and $t$ of $S$, the underlying set of their product $s \times t$ is equal to the Cartesian product of the underlying sets $s$ and $t$, i.e., $(s \times t) = s \timesˢ t$.
NonUnitalSubsemiring.mem_prod theorem
{s : NonUnitalSubsemiring R} {t : NonUnitalSubsemiring S} {p : R × S} : p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t
Full source 
theorem mem_prod {s : NonUnitalSubsemiring R} {t : NonUnitalSubsemiring S} {p : R × S} :
    p ∈ s.prod tp ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t :=
  Iff.rfl
Membership Criterion for Product of Non-unital Subsemirings
Informal description
For any non-unital subsemirings $s$ of $R$ and $t$ of $S$, and any pair $p = (p_1, p_2) \in R \times S$, the pair $p$ belongs to the product subsemiring $s \times t$ if and only if $p_1 \in s$ and $p_2 \in t$.
NonUnitalSubsemiring.prod_mono theorem
⦃s₁ s₂ : NonUnitalSubsemiring R⦄ (hs : s₁ ≤ s₂) ⦃t₁ t₂ : NonUnitalSubsemiring S⦄ (ht : t₁ ≤ t₂) : s₁.prod t₁ ≤ s₂.prod t₂
Full source 
@[mono]
theorem prod_mono ⦃s₁ s₂ : NonUnitalSubsemiring R⦄ (hs : s₁ ≤ s₂) ⦃t₁ t₂ : NonUnitalSubsemiring S⦄
    (ht : t₁ ≤ t₂) : s₁.prod t₁ ≤ s₂.prod t₂ :=
  Set.prod_mono hs ht
Monotonicity of Product of Non-unital Subsemirings with Respect to Inclusion
Informal description
For any non-unital subsemirings $s_1, s_2$ of $R$ and $t_1, t_2$ of $S$, if $s_1 \subseteq s_2$ and $t_1 \subseteq t_2$, then the product subsemiring $s_1 \times t_1$ is contained in $s_2 \times t_2$.
NonUnitalSubsemiring.prod_mono_right theorem
(s : NonUnitalSubsemiring R) : Monotone fun t : NonUnitalSubsemiring S => s.prod t
Full source 
theorem prod_mono_right (s : NonUnitalSubsemiring R) :
    Monotone fun t : NonUnitalSubsemiring S => s.prod t :=
  prod_mono (le_refl s)
Monotonicity of Product with Fixed First Factor in Non-unital Subsemirings
Informal description
For any non-unital subsemiring $s$ of a non-unital semiring $R$, the function that maps a non-unital subsemiring $t$ of $S$ to the product subsemiring $s \times t$ is monotone. That is, if $t_1 \subseteq t_2$ for subsemirings $t_1, t_2$ of $S$, then $s \times t_1 \subseteq s \times t_2$.
NonUnitalSubsemiring.prod_mono_left theorem
(t : NonUnitalSubsemiring S) : Monotone fun s : NonUnitalSubsemiring R => s.prod t
Full source 
theorem prod_mono_left (t : NonUnitalSubsemiring S) :
    Monotone fun s : NonUnitalSubsemiring R => s.prod t := fun _ _ hs => prod_mono hs (le_refl t)
Monotonicity of Left Factor in Product of Non-unital Subsemirings
Informal description
For any fixed non-unital subsemiring $t$ of a non-unital semiring $S$, the function that maps a non-unital subsemiring $s$ of $R$ to the product subsemiring $s \times t$ is monotone with respect to inclusion. That is, if $s_1 \subseteq s_2$ are non-unital subsemirings of $R$, then $s_1 \times t \subseteq s_2 \times t$.
NonUnitalSubsemiring.prod_top theorem
(s : NonUnitalSubsemiring R) : s.prod (⊤ : NonUnitalSubsemiring S) = s.comap (NonUnitalRingHom.fst R S)
Full source 
theorem prod_top (s : NonUnitalSubsemiring R) :
    s.prod (⊤ : NonUnitalSubsemiring S) = s.comap (NonUnitalRingHom.fst R S) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_fst]
Product of a Non-unital Subsemiring with the Whole Semiring Equals Preimage under First Projection
Informal description
For any non-unital subsemiring $s$ of a non-unital semiring $R$, the product subsemiring $s \times S$ is equal to the preimage of $s$ under the first projection homomorphism $\text{fst} : R \times S \to R$, where $S$ is the entire non-unital semiring considered as a subsemiring.
NonUnitalSubsemiring.top_prod theorem
(s : NonUnitalSubsemiring S) : (⊤ : NonUnitalSubsemiring R).prod s = s.comap (NonUnitalRingHom.snd R S)
Full source 
theorem top_prod (s : NonUnitalSubsemiring S) :
    (⊤ : NonUnitalSubsemiring R).prod s = s.comap (NonUnitalRingHom.snd R S) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_snd]
Product of Top Non-Unital Subsemiring with Another Equals Preimage Under Projection
Informal description
For any non-unital subsemiring $s$ of a non-unital semiring $S$, the product of the top non-unital subsemiring of $R$ (which is $R$ itself) with $s$ is equal to the preimage of $s$ under the second projection non-unital ring homomorphism from $R \times S$ to $S$. In other words, $(R \times s) = \text{comap}(\text{snd})(s)$, where $\text{snd} : R \times S \to S$ is the projection onto the second component.
NonUnitalSubsemiring.top_prod_top theorem
: (⊤ : NonUnitalSubsemiring R).prod (⊤ : NonUnitalSubsemiring S) = ⊤
Full source 
@[simp]
theorem top_prod_top : (⊤ : NonUnitalSubsemiring R).prod (⊤ : NonUnitalSubsemiring S) = ⊤ :=
  (top_prod _).trans <| comap_top _
Product of Top Non-Unital Subsemirings is Top
Informal description
The product of the top non-unital subsemiring of $R$ (which is $R$ itself) and the top non-unital subsemiring of $S$ (which is $S$ itself) is equal to the top non-unital subsemiring of $R \times S$ (which is $R \times S$ itself). In other words, $R \times S$ is the top element in the lattice of non-unital subsemirings of $R \times S$.
NonUnitalSubsemiring.prodEquiv definition
(s : NonUnitalSubsemiring R) (t : NonUnitalSubsemiring S) : s.prod t ≃+* s × t
Full source 
/-- Product of non-unital subsemirings is isomorphic to their product as semigroups. -/
def prodEquiv (s : NonUnitalSubsemiring R) (t : NonUnitalSubsemiring S) : s.prod t ≃+* s × t :=
  { Equiv.Set.prod (s : Set R) (t : Set S) with
    map_mul' := fun _ _ => rfl
    map_add' := fun _ _ => rfl }
Isomorphism between product of non-unital subsemirings and their direct product
Informal description
Given non-unital subsemirings $s$ of $R$ and $t$ of $S$, the product subsemiring $s \times t$ is isomorphic as a non-unital semiring to the direct product $s \times t$ of the underlying sets. The isomorphism preserves both the additive and multiplicative structures.
NonUnitalSubsemiring.mem_iSup_of_directed theorem
{ι} [hι : Nonempty ι] {S : ι → NonUnitalSubsemiring R} (hS : Directed (· ≤ ·) S) {x : R} : (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i
Full source 
theorem mem_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → NonUnitalSubsemiring R}
    (hS : Directed (· ≤ ·) S) {x : R} : (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i := by
  refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
  let U : NonUnitalSubsemiring R :=
    NonUnitalSubsemiring.mk' (⋃ i, (S i : Set R))
      (⨆ i, (S i).toSubsemigroup) (Subsemigroup.coe_iSup_of_directed hS)
      (⨆ i, (S i).toAddSubmonoid) (AddSubmonoid.coe_iSup_of_directed hS)
  -- Porting note `@this` doesn't work
  suffices H : ⨆ i, S i ≤ U by simpa [U] using @H x
  exact iSup_le fun i x hx => Set.mem_iUnion.2 ⟨i, hx⟩
Characterization of Membership in Directed Supremum of Non-Unital Subsemirings: $x \in \bigsqcup_i S_i \leftrightarrow \exists i, x \in S_i$
Informal description
Let $R$ be a non-unital semiring, $\iota$ a nonempty index set, and $(S_i)_{i \in \iota}$ a directed family of non-unital subsemirings of $R$ with respect to inclusion. For any element $x \in R$, we have $x \in \bigsqcup_{i \in \iota} S_i$ if and only if there exists an index $i \in \iota$ such that $x \in S_i$.
NonUnitalSubsemiring.coe_iSup_of_directed theorem
{ι} [hι : Nonempty ι] {S : ι → NonUnitalSubsemiring R} (hS : Directed (· ≤ ·) S) : ((⨆ i, S i : NonUnitalSubsemiring R) : Set R) = ⋃ i, S i
Full source 
theorem coe_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → NonUnitalSubsemiring R}
    (hS : Directed (· ≤ ·) S) : ((⨆ i, S i : NonUnitalSubsemiring R) : Set R) = ⋃ i, S i :=
  Set.ext fun x ↦ by simp [mem_iSup_of_directed hS]
Underlying Set of Directed Supremum of Non-Unital Subsemirings Equals Union of Underlying Sets
Informal description
Let $R$ be a non-unital semiring, $\iota$ a nonempty index set, and $(S_i)_{i \in \iota}$ a directed family of non-unital subsemirings of $R$ with respect to inclusion. Then the underlying set of the supremum $\bigsqcup_{i \in \iota} S_i$ is equal to the union $\bigcup_{i \in \iota} S_i$ of the underlying sets of the subsemirings $S_i$.
NonUnitalSubsemiring.mem_sSup_of_directedOn theorem
{S : Set (NonUnitalSubsemiring R)} (Sne : S.Nonempty) (hS : DirectedOn (· ≤ ·) S) {x : R} : x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
Full source 
theorem mem_sSup_of_directedOn {S : Set (NonUnitalSubsemiring R)} (Sne : S.Nonempty)
    (hS : DirectedOn (· ≤ ·) S) {x : R} : x ∈ sSup Sx ∈ sSup S ↔ ∃ s ∈ S, x ∈ s := by
  haveI : Nonempty S := Sne.to_subtype
  simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, Subtype.exists, exists_prop]
Characterization of Membership in Directed Supremum of Non-Unital Subsemirings: $x \in \mathrm{sSup}(S) \leftrightarrow \exists s \in S, x \in s$
Informal description
Let $R$ be a non-unital semiring and $S$ a nonempty set of non-unital subsemirings of $R$ that is directed with respect to inclusion. For any element $x \in R$, we have $x \in \mathrm{sSup}(S)$ if and only if there exists a subsemiring $s \in S$ such that $x \in s$.
NonUnitalSubsemiring.coe_sSup_of_directedOn theorem
{S : Set (NonUnitalSubsemiring R)} (Sne : S.Nonempty) (hS : DirectedOn (· ≤ ·) S) : (↑(sSup S) : Set R) = ⋃ s ∈ S, ↑s
Full source 
theorem coe_sSup_of_directedOn {S : Set (NonUnitalSubsemiring R)} (Sne : S.Nonempty)
    (hS : DirectedOn (· ≤ ·) S) : (↑(sSup S) : Set R) = ⋃ s ∈ S, ↑s :=
  Set.ext fun x => by simp [mem_sSup_of_directedOn Sne hS]
Underlying Set of Directed Supremum of Non-Unital Subsemirings Equals Union of Underlying Sets
Informal description
Let $R$ be a non-unital semiring and $S$ a nonempty set of non-unital subsemirings of $R$ that is directed with respect to inclusion. Then the underlying set of the supremum $\mathrm{sSup}(S)$ is equal to the union $\bigcup_{s \in S} s$ of the underlying sets of the subsemirings in $S$.
NonUnitalRingHom.srangeRestrict definition
(f : F) : R →ₙ+* (srange f : NonUnitalSubsemiring S)
Full source 
/-- Restriction of a non-unital ring homomorphism to its range interpreted as a
non-unital subsemiring.

This is the bundled version of `Set.rangeFactorization`. -/
def srangeRestrict (f : F) : R →ₙ+* (srange f : NonUnitalSubsemiring S) :=
  codRestrict f (srange f) (mem_srange_self f)
Range restriction of a non-unital ring homomorphism
Informal description
Given a non-unital ring homomorphism $f \colon R \to S$, the function `srangeRestrict` restricts the codomain of $f$ to its range, yielding a homomorphism $R \to \text{srange}(f)$, where $\text{srange}(f)$ is the non-unital subsemiring of $S$ consisting of all elements of the form $f(x)$ for some $x \in R$.
NonUnitalRingHom.coe_srangeRestrict theorem
(f : F) (x : R) : (srangeRestrict f x : S) = f x
Full source 
@[simp]
theorem coe_srangeRestrict (f : F) (x : R) : (srangeRestrict f x : S) = f x :=
  rfl
Commutativity of Range-Restricted Homomorphism Evaluation
Informal description
For any non-unital ring homomorphism $f \colon R \to S$ and any element $x \in R$, the image of $x$ under the range-restricted homomorphism $\text{srangeRestrict}(f) \colon R \to \text{srange}(f)$ is equal to $f(x)$ when viewed as an element of $S$. In other words, the following diagram commutes: $$ \text{srangeRestrict}(f)(x) = f(x) \text{ in } S. $$
NonUnitalRingHom.srangeRestrict_surjective theorem
(f : F) : Function.Surjective (srangeRestrict f : R → (srange f : NonUnitalSubsemiring S))
Full source 
theorem srangeRestrict_surjective (f : F) :
    Function.Surjective (srangeRestrict f : R → (srange f : NonUnitalSubsemiring S)) :=
  fun ⟨_, hy⟩ =>
  let ⟨x, hx⟩ := mem_srange.mp hy
  ⟨x, Subtype.ext hx⟩
Surjectivity of the Range-Restricted Non-Unital Ring Homomorphism
Informal description
For any non-unital ring homomorphism $f \colon R \to S$, the restricted homomorphism $\text{srangeRestrict}(f) \colon R \to \text{srange}(f)$ is surjective, where $\text{srange}(f)$ denotes the range of $f$ as a non-unital subsemiring of $S$.
NonUnitalRingHom.srange_eq_top_iff_surjective theorem
{f : F} : srange f = (⊤ : NonUnitalSubsemiring S) ↔ Function.Surjective (f : R → S)
Full source 
theorem srange_eq_top_iff_surjective {f : F} :
    srangesrange f = (⊤ : NonUnitalSubsemiring S) ↔ Function.Surjective (f : R → S) :=
  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_srange, coe_top]) Set.range_eq_univ
Range Equals Entire Codomain iff Non-Unital Ring Homomorphism is Surjective
Informal description
For a non-unital ring homomorphism $f \colon R \to S$, the range of $f$ (as a non-unital subsemiring of $S$) equals the entire semiring $S$ if and only if $f$ is surjective. In other words: $$ \text{range}(f) = S \leftrightarrow f \text{ is surjective} $$
NonUnitalRingHom.srange_eq_top_of_surjective theorem
(f : F) (hf : Function.Surjective (f : R → S)) : srange f = (⊤ : NonUnitalSubsemiring S)
Full source 
/-- The range of a surjective non-unital ring homomorphism is the whole of the codomain. -/
@[simp]
theorem srange_eq_top_of_surjective (f : F) (hf : Function.Surjective (f : R → S)) :
    srange f = (⊤ : NonUnitalSubsemiring S) :=
  srange_eq_top_iff_surjective.2 hf
Range of Surjective Non-Unital Ring Homomorphism is Entire Codomain
Informal description
Let $f \colon R \to S$ be a surjective non-unital ring homomorphism. Then the range of $f$ is equal to the entire codomain $S$, i.e., $\text{range}(f) = S$.
NonUnitalRingHom.eqOn_sclosure theorem
{f g : F} {s : Set R} (h : Set.EqOn (f : R → S) (g : R → S) s) : Set.EqOn f g (closure s)
Full source 
/-- If two non-unital ring homomorphisms are equal on a set, then they are equal on its
non-unital subsemiring closure. -/
theorem eqOn_sclosure {f g : F} {s : Set R} (h : Set.EqOn (f : R → S) (g : R → S) s) :
    Set.EqOn f g (closure s) :=
  show closure s ≤ eqSlocus f g from closure_le.2 h
Agreement of Non-Unital Ring Homomorphisms on Generated Subsemiring
Informal description
Let $R$ and $S$ be non-unital non-associative semirings, and let $f, g \colon R \to S$ be non-unital ring homomorphisms. If $f$ and $g$ agree on a subset $s \subseteq R$, then they also agree on the non-unital subsemiring generated by $s$.
NonUnitalRingHom.sclosure_preimage_le theorem
(f : F) (s : Set S) : closure ((f : R → S) ⁻¹' s) ≤ (closure s).comap f
Full source 
theorem sclosure_preimage_le (f : F) (s : Set S) :
    closure ((f : R → S) ⁻¹' s) ≤ (closure s).comap f :=
  closure_le.2 fun _ hx => SetLike.mem_coe.2 <| mem_comap.2 <| subset_closure hx
Inclusion of Generated Subsemirings for Preimages under Non-unital Ring Homomorphisms
Informal description
Let $R$ and $S$ be non-unital non-associative semirings, and let $f : R \to S$ be a non-unital ring homomorphism. For any subset $s \subseteq S$, the non-unital subsemiring generated by the preimage $f^{-1}(s)$ is contained in the preimage of the non-unital subsemiring generated by $s$. In other words, $\text{closure}(f^{-1}(s)) \leq f^{-1}(\text{closure}(s))$.
NonUnitalRingHom.map_sclosure theorem
(f : F) (s : Set R) : (closure s).map f = closure ((f : R → S) '' s)
Full source 
/-- The image under a ring homomorphism of the subsemiring generated by a set equals
the subsemiring generated by the image of the set. -/
theorem map_sclosure (f : F) (s : Set R) : (closure s).map f = closure ((f : R → S) '' s) :=
  Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) (NonUnitalSubsemiring.gi S).gc
    (NonUnitalSubsemiring.gi R).gc fun _ ↦ rfl
Image of Generated Non-unital Subsemiring Equals Generated Image
Informal description
Let $R$ and $S$ be non-unital non-associative semirings, and let $f : R \to S$ be a non-unital ring homomorphism. For any subset $s \subseteq R$, the image under $f$ of the non-unital subsemiring generated by $s$ equals the non-unital subsemiring generated by the image $f(s)$. In other words: \[ f(\text{closure}(s)) = \text{closure}(f(s)). \]
NonUnitalSubsemiring.srange_subtype theorem
(s : NonUnitalSubsemiring R) : NonUnitalRingHom.srange (subtype s) = s
Full source 
@[simp]
theorem srange_subtype (s : NonUnitalSubsemiring R) : NonUnitalRingHom.srange (subtype s) = s :=
  SetLike.coe_injective <| (coe_srange _).trans Subtype.range_coe
Range of Inclusion Homomorphism Equals Subsemiring
Informal description
For any non-unital subsemiring $s$ of a non-unital semiring $R$, the range of the inclusion homomorphism from $s$ to $R$ is equal to $s$ itself. That is, $\text{srange}(\text{subtype } s) = s$.
NonUnitalSubsemiring.range_fst theorem
: NonUnitalRingHom.srange (fst R S) = ⊤
Full source 
@[simp]
theorem range_fst : NonUnitalRingHom.srange (fst R S) = ⊤ :=
  NonUnitalRingHom.srange_eq_top_of_surjective (fst R S) Prod.fst_surjective
First Projection Homomorphism Has Full Range in Product Semiring
Informal description
For any non-unital semirings $R$ and $S$, the range of the first projection homomorphism $\operatorname{fst} \colon R \times S \to R$ is equal to the entire semiring $R$, i.e., $\text{srange}(\operatorname{fst}) = R$.
NonUnitalSubsemiring.range_snd theorem
: NonUnitalRingHom.srange (snd R S) = ⊤
Full source 
@[simp]
theorem range_snd : NonUnitalRingHom.srange (snd R S) = ⊤ :=
  NonUnitalRingHom.srange_eq_top_of_surjective (snd R S) <| Prod.snd_surjective
Range of Second Projection Homomorphism is Entire Codomain
Informal description
The range of the second projection homomorphism $\operatorname{snd} \colon R \times S \to S$ is equal to the entire non-unital subsemiring $S$, i.e., $\text{srange}(\operatorname{snd}) = S$.
RingEquiv.nonUnitalSubsemiringCongr definition
(h : s = t) : s ≃+* t
Full source 
/-- Makes the identity isomorphism from a proof two non-unital subsemirings of a multiplicative
monoid are equal. -/
def nonUnitalSubsemiringCongr (h : s = t) : s ≃+* t :=
  { Equiv.setCongr <| congr_arg _ h with
    map_mul' := fun _ _ => rfl
    map_add' := fun _ _ => rfl }
Ring isomorphism between equal non-unital subsemirings
Informal description
Given two non-unital subsemirings $s$ and $t$ of a non-unital semiring $R$ that are equal ($s = t$), the identity map induces a ring isomorphism between $s$ and $t$. This isomorphism preserves both the additive and multiplicative structures of the subsemirings.
RingEquiv.sofLeftInverse' definition
{g : S → R} {f : F} (h : Function.LeftInverse g f) : R ≃+* srange f
Full source 
/-- Restrict a non-unital ring homomorphism with a left inverse to a ring isomorphism to its
`NonUnitalRingHom.srange`. -/
def sofLeftInverse' {g : S → R} {f : F} (h : Function.LeftInverse g f) : R ≃+* srange f :=
  { srangeRestrict f with
    toFun := srangeRestrict f
    invFun := fun x => g (subtype (srange f) x)
    left_inv := h
    right_inv := fun x =>
      Subtype.ext <|
        let ⟨x', hx'⟩ := NonUnitalRingHom.mem_srange.mp x.prop
        show f (g x) = x by rw [← hx', h x'] }
Ring isomorphism from a ring to the range of a homomorphism with left inverse
Informal description
Given a non-unital ring homomorphism $f \colon R \to S$ with a left inverse $g \colon S \to R$ (i.e., $g \circ f = \text{id}_R$), the function `sofLeftInverse'` constructs a ring isomorphism between $R$ and the range $\text{srange}(f)$ of $f$. The isomorphism maps $x \in R$ to $f(x) \in \text{srange}(f)$, and its inverse maps $y \in \text{srange}(f)$ to $g(y) \in R$.
RingEquiv.sofLeftInverse'_apply theorem
{g : S → R} {f : F} (h : Function.LeftInverse g f) (x : R) : ↑(sofLeftInverse' h x) = f x
Full source 
@[simp]
theorem sofLeftInverse'_apply {g : S → R} {f : F} (h : Function.LeftInverse g f) (x : R) :
    ↑(sofLeftInverse' h x) = f x :=
  rfl
Image under Ring Isomorphism to Range Equals Original Homomorphism Evaluation
Informal description
Given a non-unital ring homomorphism $f \colon R \to S$ with a left inverse $g \colon S \to R$ (i.e., $g \circ f = \text{id}_R$), and any element $x \in R$, the image of $x$ under the ring isomorphism $\text{sofLeftInverse'}\ h$ is equal to $f(x)$ when viewed as an element of $S$.
RingEquiv.sofLeftInverse'_symm_apply theorem
{g : S → R} {f : F} (h : Function.LeftInverse g f) (x : srange f) : (sofLeftInverse' h).symm x = g x
Full source 
@[simp]
theorem sofLeftInverse'_symm_apply {g : S → R} {f : F} (h : Function.LeftInverse g f)
    (x : srange f) : (sofLeftInverse' h).symm x = g x :=
  rfl
Inverse of Ring Isomorphism to Range of Homomorphism with Left Inverse
Informal description
Given a non-unital ring homomorphism $f \colon R \to S$ with a left inverse $g \colon S \to R$ (i.e., $g \circ f = \text{id}_R$), the inverse of the ring isomorphism $\text{sofLeftInverse'}\ h$ maps any element $x$ in the range $\text{srange}(f)$ to $g(x) \in R$.
RingEquiv.nonUnitalSubsemiringMap definition
(e : R ≃+* S) (s : NonUnitalSubsemiring R) : s ≃+* NonUnitalSubsemiring.map e.toNonUnitalRingHom s
Full source 
/-- 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` -/
@[simps!]
def nonUnitalSubsemiringMap (e : R ≃+* S) (s : NonUnitalSubsemiring R) :
    s ≃+* NonUnitalSubsemiring.map e.toNonUnitalRingHom s :=
  { e.toAddEquiv.addSubmonoidMap s.toAddSubmonoid,
    e.toMulEquiv.subsemigroupMap s.toSubsemigroup with }
Equivalence of non-unital subsemirings under isomorphism
Informal description
Given a non-unital semiring equivalence (isomorphism) $e \colon R \simeq+* S$ and a non-unital subsemiring $s$ of $R$, the function `nonUnitalSubsemiringMap` constructs an equivalence between $s$ and its image under $e$ in $S$. More precisely, this equivalence maps the subsemiring $s$ to the subsemiring $\{e(x) \mid x \in s\}$ in $S$, preserving both the additive and multiplicative structures.