Mathlib.Algebra.Ring.Subsemiring.Basic

SubsemiringClass.instCharZero instance

[CharZero R] : CharZero s

Full source

instance instCharZero [CharZero R] : CharZero s :=
  ⟨Function.Injective.of_comp (f := Subtype.val) (g := Nat.cast (R := s)) Nat.cast_injective⟩

Subsemirings Inherit Characteristic Zero

Informal description

For any subsemiring $s$ of a semiring $R$ with characteristic zero, $s$ also has characteristic zero.

Subsemiring.toSubmonoid_strictMono theorem

: StrictMono (toSubmonoid : Subsemiring R → Submonoid R)

Full source

@[mono]
theorem toSubmonoid_strictMono : StrictMono (toSubmonoid : Subsemiring R → Submonoid R) :=
  fun _ _ => id

Strict Monotonicity of Subsemiring to Submonoid Map

Informal description

The function that maps a subsemiring $S$ of a semiring $R$ to its underlying multiplicative submonoid is strictly monotone. That is, for any two subsemirings $S_1, S_2$ of $R$, if $S_1 < S_2$ in the partial order of subsemirings, then the multiplicative submonoid of $S_1$ is strictly contained in the multiplicative submonoid of $S_2$.

Subsemiring.toSubmonoid_mono theorem

: Monotone (toSubmonoid : Subsemiring R → Submonoid R)

Full source

@[mono]
theorem toSubmonoid_mono : Monotone (toSubmonoid : Subsemiring R → Submonoid R) :=
  toSubmonoid_strictMono.monotone

Monotonicity of Subsemiring to Submonoid Map

Informal description

The function that maps a subsemiring $S$ of a semiring $R$ to its underlying multiplicative submonoid is monotone. That is, for any two subsemirings $S_1, S_2$ of $R$, if $S_1 \leq S_2$ in the partial order of subsemirings, then the multiplicative submonoid of $S_1$ is contained in the multiplicative submonoid of $S_2$.

Subsemiring.toAddSubmonoid_strictMono theorem

: StrictMono (toAddSubmonoid : Subsemiring R → AddSubmonoid R)

Full source

@[mono]
theorem toAddSubmonoid_strictMono : StrictMono (toAddSubmonoid : Subsemiring R → AddSubmonoid R) :=
  fun _ _ => id

Strict Monotonicity of Subsemiring to Additive Submonoid Map

Informal description

The function that maps a subsemiring $S$ of a semiring $R$ to its underlying additive submonoid is strictly monotone. That is, for any two subsemirings $S_1, S_2$ of $R$, if $S_1 < S_2$ in the partial order of subsemirings, then the additive submonoid of $S_1$ is strictly contained in the additive submonoid of $S_2$.

Subsemiring.toAddSubmonoid_mono theorem

: Monotone (toAddSubmonoid : Subsemiring R → AddSubmonoid R)

Full source

@[mono]
theorem toAddSubmonoid_mono : Monotone (toAddSubmonoid : Subsemiring R → AddSubmonoid R) :=
  toAddSubmonoid_strictMono.monotone

Monotonicity of Subsemiring to Additive Submonoid Map

Informal description

The function that maps a subsemiring $S$ of a semiring $R$ to its underlying additive submonoid is monotone. That is, for any two subsemirings $S_1, S_2$ of $R$, if $S_1 \leq S_2$ in the partial order of subsemirings, then the additive submonoid of $S_1$ is contained in the additive submonoid of $S_2$.

Subsemiring.list_prod_mem theorem

{R : Type*} [Semiring R] (s : Subsemiring R) {l : List R} : (∀ x ∈ l, x ∈ s) → l.prod ∈ s

Full source

/-- Product of a list of elements in a `Subsemiring` is in the `Subsemiring`. -/
nonrec theorem list_prod_mem {R : Type*} [Semiring R] (s : Subsemiring R) {l : List R} :
    (∀ x ∈ l, x ∈ s) → l.prod ∈ s :=
  list_prod_mem

Product of List Elements in Subsemiring Belongs to Subsemiring

Informal description

Let $R$ be a semiring and $s$ a subsemiring of $R$. For any list $l$ of elements in $R$, if every element $x \in l$ belongs to $s$, then the product of all elements in $l$ (computed in $R$) also belongs to $s$.

Subsemiring.list_sum_mem theorem

{l : List R} : (∀ x ∈ l, x ∈ s) → l.sum ∈ s

Full source

/-- Sum of a list of elements in a `Subsemiring` is in the `Subsemiring`. -/
protected theorem list_sum_mem {l : List R} : (∀ x ∈ l, x ∈ s) → l.sum ∈ s :=
  list_sum_mem

Sum of List Elements in Subsemiring

Informal description

Let $R$ be a non-associative semiring and $s$ be a subsemiring of $R$. For any list $l$ of elements of $R$, if every element $x \in l$ belongs to $s$, then the sum of all elements in $l$ also belongs to $s$.

Subsemiring.multiset_prod_mem theorem

{R} [CommSemiring R] (s : Subsemiring R) (m : Multiset R) : (∀ a ∈ m, a ∈ s) → m.prod ∈ s

Full source

/-- Product of a multiset of elements in a `Subsemiring` of a `CommSemiring`
    is in the `Subsemiring`. -/
protected theorem multiset_prod_mem {R} [CommSemiring R] (s : Subsemiring R) (m : Multiset R) :
    (∀ a ∈ m, a ∈ s) → m.prod ∈ s :=
  multiset_prod_mem m

Product of Multiset in Subsemiring is in Subsemiring

Informal description

Let $R$ be a commutative semiring and $s$ a subsemiring of $R$. For any multiset $m$ of elements in $R$, if every element $a \in m$ belongs to $s$, then the product of all elements in $m$ (computed in $R$) also belongs to $s$.

Subsemiring.multiset_sum_mem theorem

(m : Multiset R) : (∀ a ∈ m, a ∈ s) → m.sum ∈ s

Full source

/-- Sum of a multiset of elements in a `Subsemiring` of a `NonAssocSemiring` is
in the `Subsemiring`. -/
protected theorem multiset_sum_mem (m : Multiset R) : (∀ a ∈ m, a ∈ s) → m.sum ∈ s :=
  multiset_sum_mem m

Sum of Multiset Elements in Subsemiring

Informal description

Let $R$ be a non-associative semiring and $s$ be a subsemiring of $R$. For any multiset $m$ of elements of $R$, if every element $a \in m$ belongs to $s$, then the sum of all elements in $m$ also belongs to $s$.

Subsemiring.prod_mem theorem

 {R : Type*} [CommSemiring R] (s : Subsemiring R) {ι : Type*} {t : Finset ι} {f : ι → R} (h : ∀ c ∈ t, f c ∈ s) :
  (∏ i ∈ t, f i) ∈ s

Full source

/-- Product of elements of a subsemiring of a `CommSemiring` indexed by a `Finset` is in the
`Subsemiring`. -/
protected theorem prod_mem {R : Type*} [CommSemiring R] (s : Subsemiring R) {ι : Type*}
    {t : Finset ι} {f : ι → R} (h : ∀ c ∈ t, f c ∈ s) : (∏ i ∈ t, f i) ∈ s :=
  prod_mem h

Product of Subsemiring Elements over a Finite Set Belongs to Subsemiring

Informal description

Let $R$ be a commutative semiring and $S$ a subsemiring of $R$. For any finite index set $t$ and function $f : \iota \to R$, if $f(c) \in S$ for every $c \in t$, then the product $\prod_{i \in t} f(i)$ belongs to $S$.

Subsemiring.sum_mem theorem

(s : Subsemiring R) {ι : Type*} {t : Finset ι} {f : ι → R} (h : ∀ c ∈ t, f c ∈ s) : (∑ i ∈ t, f i) ∈ s

Full source

/-- Sum of elements in a `Subsemiring` of a `NonAssocSemiring` indexed by a `Finset`
is in the `Subsemiring`. -/
protected theorem sum_mem (s : Subsemiring R) {ι : Type*} {t : Finset ι} {f : ι → R}
    (h : ∀ c ∈ t, f c ∈ s) : (∑ i ∈ t, f i) ∈ s :=
  sum_mem h

Sum of Elements in a Subsemiring Belongs to the Subsemiring

Informal description

Let $R$ be a non-associative semiring and $s$ be a subsemiring of $R$. For any finite index set $t$ (represented as a `Finset`) and function $f : t \to R$, if every element $f(c)$ belongs to $s$ for all $c \in t$, then the sum $\sum_{i \in t} f(i)$ also belongs to $s$.

Subsemiring.topEquiv definition

: (⊤ : Subsemiring R) ≃+* R

Full source

/-- The ring equiv between the top element of `Subsemiring R` and `R`. -/
@[simps]
def topEquiv : (⊤ : Subsemiring R) ≃+* R where
  toFun r := r
  invFun r := ⟨r, Subsemiring.mem_top r⟩
  left_inv _ := rfl
  right_inv _ := rfl
  map_mul' := (⊤ : Subsemiring R).coe_mul
  map_add' := (⊤ : Subsemiring R).coe_add

Ring isomorphism between the top subsemiring and the semiring

Informal description

The ring isomorphism between the top element of the lattice of subsemirings of $R$ (which is $R$ itself) and $R$. It is defined by the identity map on $R$, with its inverse being the inclusion of $R$ into the top subsemiring. The isomorphism preserves both the multiplicative and additive structures of $R$.

Subsemiring.comap definition

(f : R →+* S) (s : Subsemiring S) : Subsemiring R

Full source

/-- The preimage of a subsemiring along a ring homomorphism is a subsemiring. -/
@[simps coe toSubmonoid]
def comap (f : R →+* S) (s : Subsemiring S) : Subsemiring R :=
  { s.toSubmonoid.comap (f : R →* S), s.toAddSubmonoid.comap (f : R →+ S) with carrier := f ⁻¹' s }

Preimage of a subsemiring under a ring homomorphism

Informal description

Given a ring homomorphism $f \colon R \to S$ and a subsemiring $s$ of $S$, the preimage $f^{-1}(s)$ forms a subsemiring of $R$. This subsemiring consists of all elements $x \in R$ such that $f(x) \in s$.

Subsemiring.mem_comap theorem

{s : Subsemiring S} {f : R →+* S} {x : R} : x ∈ s.comap f ↔ f x ∈ s

Full source

@[simp]
theorem mem_comap {s : Subsemiring S} {f : R →+* S} {x : R} : x ∈ s.comap fx ∈ s.comap f ↔ f x ∈ s :=
  Iff.rfl

Membership Criterion for Preimage of Subsemiring under Ring Homomorphism

Informal description

For any subsemiring $s$ of $S$, any ring homomorphism $f \colon R \to S$, and any element $x \in R$, we have $x \in \text{comap}(f, s)$ if and only if $f(x) \in s$.

Subsemiring.comap_comap theorem

(s : Subsemiring T) (g : S →+* T) (f : R →+* S) : (s.comap g).comap f = s.comap (g.comp f)

Full source

theorem comap_comap (s : Subsemiring T) (g : S →+* T) (f : R →+* S) :
    (s.comap g).comap f = s.comap (g.comp f) :=
  rfl

Double Preimage of Subsemiring Equals Preimage of Composition

Informal description

For any subsemiring $s$ of $T$ and ring homomorphisms $g \colon S \to T$ and $f \colon R \to S$, the preimage of the preimage of $s$ under $g$ and then under $f$ is equal to the preimage of $s$ under the composition $g \circ f$. In other words: $$(g^{-1}(s))^{-1}(f) = (g \circ f)^{-1}(s)$$

Subsemiring.map definition

(f : R →+* S) (s : Subsemiring R) : Subsemiring S

Full source

/-- The image of a subsemiring along a ring homomorphism is a subsemiring. -/
@[simps coe toSubmonoid]
def map (f : R →+* S) (s : Subsemiring R) : Subsemiring S :=
  { s.toSubmonoid.map (f : R →* S), s.toAddSubmonoid.map (f : R →+ S) with carrier := f '' s }

Image of a subsemiring under a ring homomorphism

Informal description

Given a ring homomorphism $f \colon R \to S$ and a subsemiring $s$ of $R$, the image of $s$ under $f$ is the subsemiring of $S$ consisting of all elements of the form $f(x)$ for $x \in s$. More formally, $\text{map}(f, s)$ is the subsemiring of $S$ whose underlying set is the image $f(s) = \{f(x) \mid x \in s\}$.

Subsemiring.mem_map theorem

{f : R →+* S} {s : Subsemiring R} {y : S} : y ∈ s.map f ↔ ∃ x ∈ s, f x = y

Full source

@[simp]
lemma mem_map {f : R →+* S} {s : Subsemiring 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 Subsemiring under a Ring Homomorphism

Informal description

For any ring homomorphism $f \colon R \to S$, subsemiring $s$ of $R$, and element $y \in S$, the element $y$ belongs to the image subsemiring $s.map(f)$ if and only if there exists an element $x \in s$ such that $f(x) = y$.

Subsemiring.map_id theorem

: s.map (RingHom.id R) = s

Full source

@[simp]
theorem map_id : s.map (RingHom.id R) = s :=
  SetLike.coe_injective <| Set.image_id _

Identity Ring Homomorphism Preserves Subsemiring

Informal description

For any subsemiring $s$ of a semiring $R$, the image of $s$ under the identity ring homomorphism $\mathrm{id}_R$ is equal to $s$ itself, i.e., $\mathrm{id}_R(s) = s$.

Subsemiring.map_map theorem

(g : S →+* T) (f : R →+* S) : (s.map f).map g = s.map (g.comp f)

Full source

theorem map_map (g : S →+* T) (f : R →+* S) : (s.map f).map g = s.map (g.comp f) :=
  SetLike.coe_injective <| Set.image_image _ _ _

Image of Subsemiring under Composition of Ring Homomorphisms Equals Image under Composed Homomorphism

Informal description

For ring homomorphisms $f \colon R \to S$ and $g \colon S \to T$ between non-associative semirings, and a subsemiring $s$ of $R$, 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).$$

Subsemiring.map_le_iff_le_comap theorem

{f : R →+* S} {s : Subsemiring R} {t : Subsemiring S} : s.map f ≤ t ↔ s ≤ t.comap f

Full source

theorem map_le_iff_le_comap {f : R →+* S} {s : Subsemiring R} {t : Subsemiring S} :
    s.map f ≤ t ↔ s ≤ t.comap f :=
  Set.image_subset_iff

Image-Preimage Order Correspondence for Subsemirings

Informal description

Let $f \colon R \to S$ be a ring homomorphism between non-associative semirings, and let $s$ be a subsemiring of $R$ and $t$ a subsemiring of $S$. Then the image of $s$ under $f$ is contained in $t$ if and only if $s$ is contained in the preimage of $t$ under $f$. In symbols: \[ f(s) \subseteq t \leftrightarrow s \subseteq f^{-1}(t). \]

Subsemiring.gc_map_comap theorem

(f : R →+* S) : GaloisConnection (map f) (comap f)

Full source

theorem gc_map_comap (f : R →+* S) : GaloisConnection (map f) (comap f) := fun _ _ =>
  map_le_iff_le_comap

Galois Connection Between Subsemiring Image and Preimage

Informal description

For any ring homomorphism $f \colon R \to S$ between non-associative semirings, the pair of functions $(f_*, f^*)$ forms a Galois connection between the complete lattices of subsemirings of $R$ and $S$, where: - $f_*(s) = f(s)$ is the image of a subsemiring $s \subseteq R$ under $f$ - $f^*(t) = f^{-1}(t)$ is the preimage of a subsemiring $t \subseteq S$ under $f$ This means that for any subsemirings $s \subseteq R$ and $t \subseteq S$, we have the equivalence: \[ f(s) \subseteq t \iff s \subseteq f^{-1}(t). \]

Subsemiring.equivMapOfInjective definition

(f : R →+* S) (hf : Function.Injective f) : s ≃+* s.map f

Full source

/-- A subsemiring is isomorphic to its image under an injective function -/
noncomputable def equivMapOfInjective (f : R →+* S) (hf : Function.Injective f) : s ≃+* s.map f :=
  { Equiv.Set.image f s hf with
    map_mul' := fun _ _ => Subtype.ext (f.map_mul _ _)
    map_add' := fun _ _ => Subtype.ext (f.map_add _ _) }

Isomorphism between a subsemiring and its image under an injective ring homomorphism

Informal description

Given an injective ring homomorphism $ f \colon R \to S $ and a subsemiring $ s $ of $ R $, there exists a ring isomorphism between $ s $ and its image $ f(s) $ under $ f $. More precisely, the isomorphism is given by: - The forward map sends each $ x \in s $ to $ f(x) \in f(s) $. - The inverse map sends each $ y \in f(s) $ to the unique $ x \in s $ such that $ f(x) = y $ (which exists and is unique by injectivity of $ f $). - The map preserves both the multiplicative and additive structures of the subsemiring.

Subsemiring.coe_equivMapOfInjective_apply theorem

(f : R →+* S) (hf : Function.Injective f) (x : s) : (equivMapOfInjective s f hf x : S) = f x

Full source

@[simp]
theorem coe_equivMapOfInjective_apply (f : R →+* S) (hf : Function.Injective f) (x : s) :
    (equivMapOfInjective s f hf x : S) = f x :=
  rfl

Image of Subsemiring Element under Injective Homomorphism Equals Direct Application

Informal description

Let $R$ and $S$ be non-associative semirings, $f : R \to S$ be an injective ring homomorphism, and $s$ be a subsemiring of $R$. For any element $x \in s$, the image of $x$ under the isomorphism $\text{equivMapOfInjective}(s, f, hf)$ (which maps $s$ to its image under $f$) equals $f(x)$ when viewed as an element of $S$.

RingHom.rangeS definition

: Subsemiring S

Full source

/-- The range of a ring homomorphism is a subsemiring. See Note [range copy pattern]. -/
@[simps! coe toSubmonoid]
def rangeS : Subsemiring S :=
  ((⊤ : Subsemiring R).map f).copy (Set.range f) Set.image_univ.symm

Range of a ring homomorphism as a subsemiring

Informal description

The range of a ring homomorphism $f \colon R \to S$ is the subsemiring of $S$ consisting of all elements of the form $f(x)$ for some $x \in R$. More formally, $\text{rangeS}(f)$ is the subsemiring of $S$ whose underlying set is $\{f(x) \mid x \in R\}$.

RingHom.mem_rangeS theorem

{f : R →+* S} {y : S} : y ∈ f.rangeS ↔ ∃ x, f x = y

Full source

@[simp]
theorem mem_rangeS {f : R →+* S} {y : S} : y ∈ f.rangeSy ∈ f.rangeS ↔ ∃ x, f x = y :=
  Iff.rfl

Characterization of Elements in the Range of a Ring Homomorphism

Informal description

For a ring homomorphism $f \colon R \to S$ and an element $y \in S$, we have $y \in \text{rangeS}(f)$ if and only if there exists $x \in R$ such that $f(x) = y$.

RingHom.rangeS_eq_map theorem

(f : R →+* S) : f.rangeS = (⊤ : Subsemiring R).map f

Full source

theorem rangeS_eq_map (f : R →+* S) : f.rangeS = (⊤ : Subsemiring R).map f := by
  ext
  simp

Range of Ring Homomorphism as Image of Top Subsemiring

Informal description

For any ring homomorphism $f \colon R \to S$ between non-associative semirings, the range of $f$ as a subsemiring of $S$ is equal to the image of the top subsemiring of $R$ under $f$. That is, $\text{rangeS}(f) = f(\top)$, where $\top$ denotes the entire semiring $R$ viewed as a subsemiring of itself.

RingHom.mem_rangeS_self theorem

(f : R →+* S) (x : R) : f x ∈ f.rangeS

Full source

theorem mem_rangeS_self (f : R →+* S) (x : R) : f x ∈ f.rangeS :=
  mem_rangeS.mpr ⟨x, rfl⟩

Image of Element under Ring Homomorphism is in Range

Informal description

For any ring homomorphism $f \colon R \to S$ between non-associative semirings and any element $x \in R$, the image $f(x)$ belongs to the range of $f$ (as a subsemiring of $S$).

RingHom.map_rangeS theorem

: f.rangeS.map g = (g.comp f).rangeS

Full source

theorem map_rangeS : f.rangeS.map g = (g.comp f).rangeS := by
  simpa only [rangeS_eq_map] using (⊤ : Subsemiring R).map_map g f

Image of Range under Composition of Ring Homomorphisms

Informal description

For ring homomorphisms $f \colon R \to S$ and $g \colon S \to T$ between non-associative semirings, the image of the range of $f$ under $g$ is equal to the range of the composition $g \circ f$. In symbols: $$g(f.\text{rangeS}) = (g \circ f).\text{rangeS}.$$

RingHom.fintypeRangeS instance

[Fintype R] [DecidableEq S] (f : R →+* S) : Fintype (rangeS f)

Full source

/-- The range of a morphism of semirings is a fintype, if the domain is a fintype.
Note: this instance can form a diamond with `Subtype.fintype` in the
  presence of `Fintype S`. -/
instance fintypeRangeS [Fintype R] [DecidableEq S] (f : R →+* S) : Fintype (rangeS f) :=
  Set.fintypeRange f

Finiteness of the Range of a Ring Homomorphism from a Finite Domain

Informal description

For any ring homomorphism $f \colon R \to S$ between non-associative semirings, if $R$ is finite and $S$ has decidable equality, then the range of $f$ (as a subsemiring of $S$) is finite.

Subsemiring.instBot instance

: Bot (Subsemiring R)

Full source

instance : Bot (Subsemiring R) :=
  ⟨(Nat.castRingHom R).rangeS⟩

Bottom Element in the Lattice of Subsemirings

Informal description

For any non-associative semiring $R$, the subsemirings of $R$ form a complete lattice with a bottom element. The bottom element is the subsemiring generated by the image of the canonical ring homomorphism from the natural numbers to $R$.

Subsemiring.instInhabited instance

: Inhabited (Subsemiring R)

Full source

instance : Inhabited (Subsemiring R) :=
  ⟨⊥⟩

Nonempty Collection of Subsemirings

Informal description

For any non-associative semiring $R$, the collection of subsemirings of $R$ is nonempty.

Subsemiring.coe_bot theorem

: ((⊥ : Subsemiring R) : Set R) = Set.range ((↑) : ℕ → R)

Full source

theorem coe_bot : ((⊥ : Subsemiring R) : Set R) = Set.range ((↑) : ℕ → R) :=
  (Nat.castRingHom R).coe_rangeS

Characterization of the Bottom Subsemiring as the Image of Natural Numbers

Informal description

The underlying set of the bottom subsemiring of a non-associative semiring $R$ is equal to the range of the canonical embedding of the natural numbers into $R$. In other words, $(\bot : \text{Subsemiring } R) = \{n \cdot 1_R \mid n \in \mathbb{N}\}$ where $1_R$ is the multiplicative identity in $R$.

Subsemiring.mem_bot theorem

{x : R} : x ∈ (⊥ : Subsemiring R) ↔ ∃ n : ℕ, ↑n = x

Full source

theorem mem_bot {x : R} : x ∈ (⊥ : Subsemiring R)x ∈ (⊥ : Subsemiring R) ↔ ∃ n : ℕ, ↑n = x :=
  RingHom.mem_rangeS

Characterization of Elements in the Bottom Subsemiring via Natural Number Embedding

Informal description

For any element $x$ in a non-associative semiring $R$, $x$ belongs to the bottom subsemiring $\bot$ of $R$ if and only if there exists a natural number $n$ such that the canonical image of $n$ in $R$ equals $x$.

Subsemiring.instInfSet instance

: InfSet (Subsemiring R)

Full source

instance : InfSet (Subsemiring R) :=
  ⟨fun s =>
    Subsemiring.mk' (⋂ t ∈ s, ↑t) (⨅ t ∈ s, Subsemiring.toSubmonoid t) (by simp)
      (⨅ t ∈ s, Subsemiring.toAddSubmonoid t)
      (by simp)⟩

Complete Lattice Structure on Subsemirings

Informal description

The collection of subsemirings of a semiring $R$ forms a complete lattice with respect to inclusion, where the infimum of a family of subsemirings is given by their intersection.

Subsemiring.coe_sInf theorem

(S : Set (Subsemiring R)) : ((sInf S : Subsemiring R) : Set R) = ⋂ s ∈ S, ↑s

Full source

@[simp, norm_cast]
theorem coe_sInf (S : Set (Subsemiring R)) : ((sInf S : Subsemiring R) : Set R) = ⋂ s ∈ S, ↑s :=
  rfl

Infimum of Subsemirings as Intersection

Informal description

For any collection $S$ of subsemirings of a semiring $R$, the underlying set of the infimum of $S$ (as a subsemiring) is equal to the intersection of all the underlying sets of the subsemirings in $S$. That is, $$ \bigcap_{s \in S} s = \text{sInf}(S) $$ where $\text{sInf}(S)$ denotes the infimum of $S$ in the lattice of subsemirings of $R$.

Subsemiring.mem_sInf theorem

{S : Set (Subsemiring R)} {x : R} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Full source

theorem mem_sInf {S : Set (Subsemiring R)} {x : R} : x ∈ sInf Sx ∈ sInf S ↔ ∀ p ∈ S, x ∈ p :=
  Set.mem_iInter₂

Characterization of Membership in Infimum of Subsemirings

Informal description

For any set $S$ of subsemirings of a semiring $R$ and any element $x \in R$, $x$ belongs to the infimum of $S$ if and only if $x$ belongs to every subsemiring in $S$.

Subsemiring.coe_iInf theorem

{ι : Sort*} {S : ι → Subsemiring R} : (↑(⨅ i, S i) : Set R) = ⋂ i, S i

Full source

@[simp, norm_cast]
theorem coe_iInf {ι : Sort*} {S : ι → Subsemiring R} : (↑(⨅ i, S i) : Set R) = ⋂ i, S i := by
  simp only [iInf, coe_sInf, Set.biInter_range]

Infimum of Subsemirings as Intersection of Underlying Sets

Informal description

For any family of subsemirings $\{S_i\}_{i \in \iota}$ of a semiring $R$, the underlying set of their infimum (greatest lower bound) as subsemirings is equal to the intersection of their underlying sets. In symbols: \[ \left(\bigsqcap_{i \in \iota} S_i\right) = \bigcap_{i \in \iota} S_i. \]

Subsemiring.mem_iInf theorem

{ι : Sort*} {S : ι → Subsemiring R} {x : R} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i

Full source

theorem mem_iInf {ι : Sort*} {S : ι → Subsemiring 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 Subsemirings

Informal description

For any family of subsemirings $\{S_i\}_{i \in \iota}$ of a 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$.

Subsemiring.sInf_toSubmonoid theorem

(s : Set (Subsemiring R)) : (sInf s).toSubmonoid = ⨅ t ∈ s, Subsemiring.toSubmonoid t

Full source

@[simp]
theorem sInf_toSubmonoid (s : Set (Subsemiring R)) :
    (sInf s).toSubmonoid = ⨅ t ∈ s, Subsemiring.toSubmonoid t :=
  mk'_toSubmonoid _ _

Infimum of Subsemirings Preserves Underlying Submonoid Structure

Informal description

For any set $s$ of subsemirings of a semiring $R$, the underlying submonoid of the infimum of $s$ is equal to the infimum of the underlying submonoids of all subsemirings in $s$. In other words, $$(\bigsqcap s).\text{toSubmonoid} = \bigsqcap_{t \in s} t.\text{toSubmonoid}.$$

Subsemiring.sInf_toAddSubmonoid theorem

(s : Set (Subsemiring R)) : (sInf s).toAddSubmonoid = ⨅ t ∈ s, Subsemiring.toAddSubmonoid t

Full source

@[simp]
theorem sInf_toAddSubmonoid (s : Set (Subsemiring R)) :
    (sInf s).toAddSubmonoid = ⨅ t ∈ s, Subsemiring.toAddSubmonoid t :=
  mk'_toAddSubmonoid _ _

Infimum of Subsemirings Preserves Additive Submonoid Structure

Informal description

For any set $s$ of subsemirings of a semiring $R$, the underlying additive submonoid of the infimum of $s$ is equal to the infimum of the underlying additive submonoids of all subsemirings in $s$. In symbols: $$(\bigsqcap s).\text{toAddSubmonoid} = \bigsqcap_{t \in s} t.\text{toAddSubmonoid}$$

Subsemiring.instCompleteLattice instance

: CompleteLattice (Subsemiring R)

Full source

/-- Subsemirings of a semiring form a complete lattice. -/
instance : CompleteLattice (Subsemiring R) :=
  { completeLatticeOfInf (Subsemiring R) fun _ =>
      IsGLB.of_image
        (fun {s t : Subsemiring R} => show (s : Set R) ⊆ t(s : Set R) ⊆ t ↔ s ≤ t from SetLike.coe_subset_coe)
        isGLB_biInf with
    bot := ⊥
    bot_le := fun s _ hx =>
      let ⟨n, hn⟩ := mem_bot.1 hx
      hn ▸ natCast_mem s n
    top := ⊤
    le_top := fun _ _ _ => mem_top _
    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 Structure on Subsemirings

Informal description

The collection of all subsemirings of a semiring $R$ forms a complete lattice with respect to inclusion, where the infimum of a family of subsemirings is their intersection and the supremum is the smallest subsemiring containing all of them.

Subsemiring.center definition

: Subsemiring R

Full source

/-- The center of a non-associative semiring `R` is the set of elements that commute and associate
with everything in `R` -/
@[simps coe toSubmonoid]
def center : Subsemiring R :=
  { NonUnitalSubsemiring.center R with
    one_mem' := Set.one_mem_center }

Center of a semiring

Informal description

The center of a semiring $R$ is the subsemiring consisting of all elements that commute with every element of $R$ (i.e., $z \in R$ such that $z \cdot r = r \cdot z$ for all $r \in R$), and contains the multiplicative identity $1$.

Subsemiring.center.commSemiring' abbrev

: CommSemiring (center R)

Full source

/-- The center is commutative and associative.

This is not an instance as it forms a non-defeq diamond with
`NonUnitalSubringClass.toNonUnitalRing` in the `npow` field. -/
abbrev center.commSemiring' : CommSemiring (center R) :=
  { Submonoid.center.commMonoid', (center R).toNonAssocSemiring with }

Commutative Semiring Structure on the Center of a Semiring

Informal description

The center of a semiring $R$, denoted $\text{center}(R)$, forms a commutative semiring under the same operations as $R$.

Subsemiring.centerCongr definition

[NonAssocSemiring S] (e : R ≃+* S) : center R ≃+* center S

Full source

/-- The center of isomorphic (not necessarily associative) semirings are isomorphic. -/
@[simps!] def centerCongr [NonAssocSemiring S] (e : R ≃+* S) : centercenter R ≃+* center S :=
  NonUnitalSubsemiring.centerCongr e

Isomorphism of centers of semirings under semiring isomorphism

Informal description

Given two non-associative semirings $R$ and $S$, and a semiring isomorphism $e : R \simeq^* S$, the centers of $R$ and $S$ are isomorphic as semirings. Specifically, the isomorphism $e$ restricts to an isomorphism between $\text{center}(R)$ and $\text{center}(S)$, where $\text{center}(R)$ denotes the subsemiring of $R$ consisting of elements that commute with all elements of $R$.

Subsemiring.centerToMulOpposite definition

: center R ≃+* center Rᵐᵒᵖ

Full source

/-- The center of a (not necessarily associative) semiring
is isomorphic to the center of its opposite. -/
@[simps!] def centerToMulOpposite : centercenter R ≃+* center Rᵐᵒᵖ :=
  NonUnitalSubsemiring.centerToMulOpposite

Isomorphism between the center of a semiring and its opposite

Informal description

The center of a semiring $R$ is isomorphic as a semiring to the center of its multiplicative opposite $R^{\text{op}}$. This isomorphism preserves both the additive and multiplicative structures.

Subsemiring.center.commSemiring instance

{R} [Semiring R] : CommSemiring (center R)

Full source

/-- The center is commutative. -/
instance center.commSemiring {R} [Semiring R] : CommSemiring (center R) :=
  { Submonoid.center.commMonoid, (center R).toSemiring with }

Commutative Semiring Structure on the Center of a Semiring

Informal description

For any semiring $R$, the center of $R$ (the subsemiring consisting of all elements that commute with every element of $R$) forms a commutative semiring under the same operations as $R$.

Subsemiring.mem_center_iff theorem

{R} [Semiring R] {z : R} : z ∈ center R ↔ ∀ g, g * z = z * g

Full source

theorem mem_center_iff {R} [Semiring R] {z : R} : z ∈ center Rz ∈ center R ↔ ∀ g, g * z = z * g :=
  Subsemigroup.mem_center_iff

Characterization of Central Elements in a Semiring

Informal description

For any element $z$ in a semiring $R$, $z$ belongs to the center of $R$ if and only if $z$ commutes with every element $g \in R$, i.e., $g \cdot z = z \cdot g$ for all $g \in R$.

Subsemiring.decidableMemCenter instance

{R} [Semiring R] [DecidableEq R] [Fintype R] : DecidablePred (· ∈ center R)

Full source

instance decidableMemCenter {R} [Semiring R] [DecidableEq R] [Fintype R] :
    DecidablePred (· ∈ center R) := fun _ => decidable_of_iff' _ mem_center_iff

Decidability of Membership in the Center of a Finite Semiring

Informal description

For any finite semiring $R$ with decidable equality, the membership in the center of $R$ is decidable. That is, given an element $z \in R$, there is an algorithm to determine whether $z$ commutes with every element of $R$.

Subsemiring.center_eq_top theorem

(R) [CommSemiring R] : center R = ⊤

Full source

@[simp]
theorem center_eq_top (R) [CommSemiring R] : center R = ⊤ :=
  SetLike.coe_injective (Set.center_eq_univ R)

Center of Commutative Semiring is Entire Semiring

Informal description

For a commutative semiring $R$, the center of $R$ is equal to the entire semiring, i.e., $\text{center}(R) = \top$.

Subsemiring.centralizer definition

{R} [Semiring R] (s : Set R) : Subsemiring R

Full source

/-- The centralizer of a set as subsemiring. -/
def centralizer {R} [Semiring R] (s : Set R) : Subsemiring R :=
  { Submonoid.centralizer s with
    carrier := s.centralizer
    zero_mem' := Set.zero_mem_centralizer
    add_mem' := Set.add_mem_centralizer }

Centralizer subsemiring of a set in a semiring

Informal description

The centralizer of a subset $ s $ in a semiring $ R $ is the subsemiring consisting of all elements $ r \in R $ that commute with every element of $ s $, i.e., $ r * x = x * r $ for all $ x \in s $. It inherits the additive and multiplicative structure from $ R $ and contains the zero element.

Subsemiring.coe_centralizer theorem

{R} [Semiring R] (s : Set R) : (centralizer s : Set R) = s.centralizer

Full source

@[simp, norm_cast]
theorem coe_centralizer {R} [Semiring R] (s : Set R) : (centralizer s : Set R) = s.centralizer :=
  rfl

Equality of Centralizer Subsemiring and Set Centralizer in a Semiring

Informal description

For any semiring $R$ and any subset $s$ of $R$, the underlying set of the centralizer subsemiring of $s$ is equal to the centralizer of $s$ as a set, i.e., $(\text{centralizer}\ s : \text{Set}\ R) = s.\text{centralizer}$.

Subsemiring.centralizer_toSubmonoid theorem

{R} [Semiring R] (s : Set R) : (centralizer s).toSubmonoid = Submonoid.centralizer s

Full source

theorem centralizer_toSubmonoid {R} [Semiring R] (s : Set R) :
    (centralizer s).toSubmonoid = Submonoid.centralizer s :=
  rfl

Equality of Centralizer Submonoid and Subsemiring-to-Submonoid

Informal description

For any semiring $R$ and subset $s \subseteq R$, the underlying submonoid of the centralizer subsemiring of $s$ is equal to the centralizer submonoid of $s$.

Subsemiring.mem_centralizer_iff theorem

{R} [Semiring R] {s : Set R} {z : R} : z ∈ centralizer s ↔ ∀ g ∈ s, g * z = z * g

Full source

theorem mem_centralizer_iff {R} [Semiring R] {s : Set R} {z : R} :
    z ∈ centralizer sz ∈ centralizer s ↔ ∀ g ∈ s, g * z = z * g :=
  Iff.rfl

Characterization of Centralizer Subsemiring Membership via Commutation

Informal description

Let $R$ be a semiring and $s$ be a subset of $R$. An element $z \in R$ belongs to the centralizer subsemiring 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$.

Subsemiring.center_le_centralizer theorem

{R} [Semiring R] (s) : center R ≤ centralizer s

Full source

theorem center_le_centralizer {R} [Semiring R] (s) : center R ≤ centralizer s :=
  s.center_subset_centralizer

Center is Contained in Centralizer of Any Subset in a Semiring

Informal description

For any semiring $R$ and subset $s \subseteq R$, the center of $R$ is contained in the centralizer of $s$, i.e., $\text{center}(R) \leq \text{centralizer}(s)$.

Subsemiring.centralizer_le theorem

{R} [Semiring R] (s t : Set R) (h : s ⊆ t) : centralizer t ≤ centralizer s

Full source

theorem centralizer_le {R} [Semiring R] (s t : Set R) (h : s ⊆ t) : centralizer t ≤ centralizer s :=
  Set.centralizer_subset h

Antimonotonicity of Centralizer Subsemirings: $s \subseteq t$ implies $\text{centralizer}(t) \leq \text{centralizer}(s)$

Informal description

Let $R$ be a semiring and $s, t$ be subsets of $R$. If $s \subseteq t$, then the centralizer subsemiring of $t$ is contained in the centralizer subsemiring of $s$, i.e., $\text{centralizer}(t) \leq \text{centralizer}(s)$.

Subsemiring.centralizer_eq_top_iff_subset theorem

{R} [Semiring R] {s : Set R} : centralizer s = ⊤ ↔ s ⊆ center R

Full source

@[simp]
theorem centralizer_eq_top_iff_subset {R} [Semiring 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 semiring $R$ and a subset $s \subseteq R$, the centralizer subsemiring of $s$ is equal to the entire semiring $R$ if and only if $s$ is contained in the center of $R$.

Subsemiring.centralizer_univ theorem

{R} [Semiring R] : centralizer Set.univ = center R

Full source

@[simp]
theorem centralizer_univ {R} [Semiring R] : centralizer Set.univ = center R :=
  SetLike.ext' (Set.centralizer_univ R)

Centralizer of Universal Set Equals Center in Semirings

Informal description

For any 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 subsemiring of elements that commute with every element of $R$ is precisely the center of $R$.

Subsemiring.le_centralizer_centralizer theorem

{R} [Semiring R] {s : Subsemiring R} : s ≤ centralizer (centralizer (s : Set R))

Full source

lemma le_centralizer_centralizer {R} [Semiring R] {s : Subsemiring R} :
    s ≤ centralizer (centralizer (s : Set R)) :=
  Set.subset_centralizer_centralizer

Subsemiring Inclusion in Double Centralizer

Informal description

For any subsemiring $s$ of a semiring $R$, $s$ is contained in the centralizer of its centralizer, i.e., $s \subseteq \text{centralizer}(\text{centralizer}(s))$.

Subsemiring.centralizer_centralizer_centralizer theorem

{R} [Semiring R] {s : Set R} : centralizer s.centralizer.centralizer = centralizer s

Full source

@[simp]
lemma centralizer_centralizer_centralizer {R} [Semiring R] {s : Set R} :
    centralizer s.centralizer.centralizer = centralizer s := by
  apply SetLike.coe_injective
  simp only [coe_centralizer, Set.centralizer_centralizer_centralizer]

Triple Centralizer Identity in Semirings: $\text{centralizer}^3(s) = \text{centralizer}(s)$

Informal description

For any subset $s$ of a semiring $R$, the triple centralizer of $s$ equals the centralizer of $s$, i.e., $\text{centralizer}(\text{centralizer}(\text{centralizer}(s))) = \text{centralizer}(s)$.

Subsemiring.closure definition

(s : Set R) : Subsemiring R

Full source

/-- The `Subsemiring` generated by a set. -/
def closure (s : Set R) : Subsemiring R :=
  sInf { S | s ⊆ S }

Subsemiring generated by a set

Informal description

Given a subset $s$ of a semiring $R$, the subsemiring $\text{closure}(s)$ is the smallest subsemiring of $R$ containing $s$, defined as the infimum of all subsemirings that contain $s$.

Subsemiring.mem_closure theorem

{x : R} {s : Set R} : x ∈ closure s ↔ ∀ S : Subsemiring R, s ⊆ S → x ∈ S

Full source

theorem mem_closure {x : R} {s : Set R} : x ∈ closure sx ∈ closure s ↔ ∀ S : Subsemiring R, s ⊆ S → x ∈ S :=
  mem_sInf

Characterization of Membership in Subsemiring Closure

Informal description

For any element $x$ in a semiring $R$ and any subset $s \subseteq R$, $x$ belongs to the subsemiring generated by $s$ if and only if $x$ is contained in every subsemiring of $R$ that contains $s$. In other words: $$x \in \text{closure}(s) \iff \forall S \leq R \text{ (subsemiring)}, s \subseteq S \implies x \in S.$$

Subsemiring.subset_closure theorem

{s : Set R} : s ⊆ closure s

Full source

/-- The 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 Subsemiring Closure

Informal description

For any subset $s$ of a semiring $R$, the set $s$ is contained in the subsemiring generated by $s$, i.e., $s \subseteq \text{closure}(s)$.

Subsemiring.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 semiring $R$ and any element $P \in R$, if $P$ does not belong to the subsemiring generated by $s$, then $P$ does not belong to $s$. In other words: $$P \notin \text{closure}(s) \implies P \notin s.$$

Subsemiring.closure_le theorem

{s : Set R} {t : Subsemiring R} : closure s ≤ t ↔ s ⊆ t

Full source

/-- A subsemiring `S` includes `closure s` if and only if it includes `s`. -/
@[simp]
theorem closure_le {s : Set R} {t : Subsemiring R} : closureclosure s ≤ t ↔ s ⊆ t :=
  ⟨Set.Subset.trans subset_closure, fun h => sInf_le h⟩

Subsemiring Closure Containment Criterion: $\text{closure}(s) \leq t \leftrightarrow s \subseteq t$

Informal description

For any subset $s$ of a semiring $R$ and any subsemiring $t$ of $R$, the 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.$$

Subsemiring.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 Subsemiring Closure: $s \subseteq t \Rightarrow \text{closure}(s) \leq \text{closure}(t)$

Informal description

For any two subsets $s$ and $t$ of a non-associative semiring $R$, if $s$ is contained in $t$ ($s \subseteq t$), then the subsemiring generated by $s$ is contained in the subsemiring generated by $t$ ($\text{closure}(s) \leq \text{closure}(t)$).

Subsemiring.closure_eq_of_le theorem

{s : Set R} {t : Subsemiring R} (h₁ : s ⊆ t) (h₂ : t ≤ closure s) : closure s = t

Full source

theorem closure_eq_of_le {s : Set R} {t : Subsemiring R} (h₁ : s ⊆ t) (h₂ : t ≤ closure s) :
    closure s = t :=
  le_antisymm (closure_le.2 h₁) h₂

Subsemiring Generation Criterion: $\text{closure}(s) = t$ when $s \subseteq t \leq \text{closure}(s)$

Informal description

For any subset $s$ of a non-associative semiring $R$ and any subsemiring $t$ of $R$, if $s \subseteq t$ and $t$ is contained in the subsemiring generated by $s$, then the subsemiring generated by $s$ is equal to $t$. In other words: \[ s \subseteq t \land t \leq \text{closure}(s) \implies \text{closure}(s) = t. \]

Subsemiring.mem_map_equiv theorem

{f : R ≃+* S} {K : Subsemiring R} {x : S} : x ∈ K.map (f : R →+* S) ↔ f.symm x ∈ K

Full source

theorem mem_map_equiv {f : R ≃+* S} {K : Subsemiring 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 using 1

Characterization of Image Membership via Ring Isomorphism Inverse

Informal description

Let $R$ and $S$ be non-associative semirings, and let $f : R \simeq+* S$ be a ring isomorphism between them. For any subsemiring $K$ of $R$ and any element $x \in S$, we have that $x$ belongs to the image of $K$ under $f$ if and only if the inverse isomorphism $f^{-1}$ maps $x$ back into $K$. In symbols: \[ x \in f(K) \leftrightarrow f^{-1}(x) \in K. \]

Subsemiring.map_equiv_eq_comap_symm theorem

(f : R ≃+* S) (K : Subsemiring R) : K.map (f : R →+* S) = K.comap f.symm

Full source

theorem map_equiv_eq_comap_symm (f : R ≃+* S) (K : Subsemiring R) :
    K.map (f : R →+* S) = K.comap f.symm :=
  SetLike.coe_injective (f.toEquiv.image_eq_preimage K)

Image-Preimage Duality for Subsemirings under Ring Isomorphism

Informal description

For any ring isomorphism $f \colon R \simeq+* S$ and any 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). \]

Subsemiring.comap_equiv_eq_map_symm theorem

(f : R ≃+* S) (K : Subsemiring S) : K.comap (f : R →+* S) = K.map f.symm

Full source

theorem comap_equiv_eq_map_symm (f : R ≃+* S) (K : Subsemiring S) :
    K.comap (f : R →+* S) = K.map f.symm :=
  (map_equiv_eq_comap_symm f.symm K).symm

Preimage-Image Duality for Subsemirings under Ring Isomorphism

Informal description

For any ring isomorphism $f \colon R \simeq+* S$ and any 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). \]

Submonoid.subsemiringClosure definition

(M : Submonoid R) : Subsemiring R

Full source

/-- The additive closure of a submonoid is a subsemiring. -/
def subsemiringClosure (M : Submonoid R) : Subsemiring R :=
  { AddSubmonoid.closure (M : Set R) with
    one_mem' := AddSubmonoid.mem_closure.mpr fun _ hy => hy M.one_mem
    mul_mem' := MulMemClass.mul_mem_add_closure }

Subsemiring closure of a submonoid

Informal description

Given a submonoid $M$ of a semiring $R$, the subsemiring closure of $M$ is the smallest subsemiring of $R$ containing $M$. It is constructed as the additive closure of the underlying set of $M$, ensuring it contains the multiplicative identity and is closed under multiplication.

Submonoid.subsemiringClosure_coe theorem

: (M.subsemiringClosure : Set R) = AddSubmonoid.closure (M : Set R)

Full source

theorem subsemiringClosure_coe :
    (M.subsemiringClosure : Set R) = AddSubmonoid.closure (M : Set R) :=
  rfl

Subsemiring Closure as Additive Closure of Submonoid

Informal description

For a submonoid $M$ of a semiring $R$, the underlying set of the subsemiring closure of $M$ is equal to the additive closure of the underlying set of $M$. In other words, $(M.\text{subsemiringClosure} : \text{Set } R) = \text{AddSubmonoid.closure}(M : \text{Set } R)$.

Submonoid.subsemiringClosure_mem theorem

{x : R} : x ∈ M.subsemiringClosure ↔ x ∈ AddSubmonoid.closure (M : Set R)

Full source

theorem subsemiringClosure_mem {x : R} :
    x ∈ M.subsemiringClosurex ∈ M.subsemiringClosure ↔ x ∈ AddSubmonoid.closure (M : Set R) :=
  Iff.rfl

Membership Criterion for Subsemiring Closure of a Submonoid

Informal description

For any element $x$ in a semiring $R$, $x$ belongs to the subsemiring closure of a submonoid $M$ if and only if $x$ belongs to the additive closure of $M$ as a subset of $R$.

Submonoid.subsemiringClosure_toAddSubmonoid theorem

: M.subsemiringClosure.toAddSubmonoid = AddSubmonoid.closure (M : Set R)

Full source

theorem subsemiringClosure_toAddSubmonoid :
    M.subsemiringClosure.toAddSubmonoid = AddSubmonoid.closure (M : Set R) :=
  rfl

Additive Submonoid of Subsemiring Closure Equals Additive Closure of Submonoid

Informal description

For a submonoid $M$ of a semiring $R$, the additive submonoid associated with the subsemiring closure of $M$ is equal to the additive closure of $M$ as a subset of $R$. That is, the underlying additive submonoid of $M.\text{subsemiringClosure}$ is $\text{AddSubmonoid.closure}(M)$.

Submonoid.subsemiringClosure_toNonUnitalSubsemiring theorem

(M : Submonoid R) : M.subsemiringClosure.toNonUnitalSubsemiring = .closure M

Full source

@[simp] lemma subsemiringClosure_toNonUnitalSubsemiring (M : Submonoid R) :
    M.subsemiringClosure.toNonUnitalSubsemiring = .closure M := by
  refine Eq.symm (NonUnitalSubsemiring.closure_eq_of_le ?_ fun _ hx ↦ ?_)
  · simp [Submonoid.subsemiringClosure_coe]
  · simp only [Subsemiring.mem_toNonUnitalSubsemiring, subsemiringClosure_mem] at hx
    induction hx using AddSubmonoid.closure_induction <;> aesop

Non-unital subsemiring structure of subsemiring closure equals non-unital subsemiring generated by submonoid

Informal description

For any submonoid $M$ of a semiring $R$, the underlying non-unital subsemiring of the subsemiring closure of $M$ is equal to the non-unital subsemiring generated by $M$.

Submonoid.subsemiringClosure_eq_closure theorem

: M.subsemiringClosure = Subsemiring.closure (M : Set R)

Full source

/-- The `Subsemiring` generated by a multiplicative submonoid coincides with the
`Subsemiring.closure` of the submonoid itself . -/
theorem subsemiringClosure_eq_closure : M.subsemiringClosure = Subsemiring.closure (M : Set R) := by
  ext
  refine
    ⟨fun hx => ?_, fun hx =>
      (Subsemiring.mem_closure.mp hx) M.subsemiringClosure fun s sM => ?_⟩
  <;> rintro - ⟨H1, rfl⟩
  <;> rintro - ⟨H2, rfl⟩
  · exact AddSubmonoid.mem_closure.mp hx H1.toAddSubmonoid H2
  · exact H2 sM

Subsemiring Closure of Submonoid Equals Subsemiring Generated by Submonoid

Informal description

For any submonoid $M$ of a semiring $R$, the subsemiring closure of $M$ is equal to the subsemiring generated by $M$ as a subset of $R$. That is, $M.\text{subsemiringClosure} = \text{Subsemiring.closure}(M)$.

Subsemiring.closure_submonoid_closure theorem

(s : Set R) : closure ↑(Submonoid.closure s) = closure s

Full source

@[simp]
theorem closure_submonoid_closure (s : Set R) : closure ↑(Submonoid.closure s) = closure s :=
  le_antisymm
    (closure_le.mpr fun _ hy =>
      (Submonoid.mem_closure.mp hy) (closure s).toSubmonoid subset_closure)
    (closure_mono Submonoid.subset_closure)

Subsemiring Closure of Submonoid Closure Equals Subsemiring Closure

Informal description

For any subset $s$ of a non-associative semiring $R$, the subsemiring generated by the submonoid closure of $s$ is equal to the subsemiring generated by $s$ itself. In symbols: $$\text{closure}(\text{Submonoid.closure}(s)) = \text{closure}(s).$$

Subsemiring.coe_closure_eq theorem

(s : Set R) : (closure s : Set R) = AddSubmonoid.closure (Submonoid.closure s : Set R)

Full source

/-- The elements of the subsemiring closure of `M` are exactly the elements of the additive closure
of a multiplicative submonoid `M`. -/
theorem coe_closure_eq (s : Set R) :
    (closure s : Set R) = AddSubmonoid.closure (Submonoid.closure s : Set R) := by
  simp [← Submonoid.subsemiringClosure_toAddSubmonoid, Submonoid.subsemiringClosure_eq_closure]

Subsemiring Closure as Additive Closure of Submonoid Closure

Informal description

For any subset $s$ of a non-associative semiring $R$, the underlying set of the subsemiring generated by $s$ is equal to the additive closure of the submonoid generated by $s$. In symbols: $$(\text{closure}(s) : \text{Set } R) = \text{AddSubmonoid.closure}(\text{Submonoid.closure}(s) : \text{Set } R).$$

Subsemiring.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 (Submonoid.mem_closure.mp hy) H.toSubmonoid fun z hz => ?_
  exact (AddSubmonoid.mem_closure.mp hz) H.toAddSubmonoid fun w hw => J hw

Subsemiring Closure of Additive Submonoid Closure Equals Subsemiring Closure

Informal description

For any subset $s$ of a non-associative semiring $R$, the subsemiring generated by the additive submonoid closure of $s$ is equal to the subsemiring generated by $s$ itself. In symbols: $$\text{closure}(\text{AddSubmonoid.closure}(s)) = \text{closure}(s).$$

Subsemiring.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 _)) (one : p 1 (one_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 _)) (one : p 1 (one_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 : Subsemiring R :=
    { carrier := { x | ∃ hx, p x hx }
      mul_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, mul _ _ _ _ hpx hpy⟩
      add_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, add _ _ _ _ hpx hpy⟩
      one_mem' := ⟨_, one⟩
      zero_mem' := ⟨_, zero⟩ }
  closure_le (t := K) |>.mpr (fun y hy ↦ ⟨subset_closure hy, mem y hy⟩) hx |>.elim fun _ ↦ id

Induction Principle for Subsemiring Membership

Informal description

Let $R$ be a non-associative semiring and $s$ a subset of $R$. For any predicate $p : R \to \mathrm{Prop}$ satisfying: 1. $p(x)$ holds for all $x \in s$, 2. $p(0)$ holds, 3. $p(1)$ holds, 4. For any $x, y \in R$, if $p(x)$ and $p(y)$ hold, then $p(x + y)$ holds, 5. For any $x, y \in R$, if $p(x)$ and $p(y)$ hold, then $p(x \cdot y)$ holds, then $p(x)$ holds for every $x$ in the subsemiring generated by $s$.

Subsemiring.closure_induction₂ theorem

 {s : Set R} {p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop}
  (mem_mem : ∀ (x) (y) (hx : x ∈ s) (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 _))
  (one_left : ∀ x hx, p 1 x (one_mem _) hx) (one_right : ∀ x hx, p x 1 hx (one_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) (y) (hx : x ∈ s) (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 _))
    (one_left : ∀ x hx, p 1 x (one_mem _) hx) (one_right : ∀ x hx, p x 1 hx (one_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 _ _
    | one => exact one_left _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
  | zero => exact zero_right x hx
  | one => exact one_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂

Double Induction Principle for Subsemiring Membership

Informal description

Let $R$ be a non-associative semiring and $s$ a subset of $R$. For any predicate $p : R \times R \to \mathrm{Prop}$ satisfying: 1. $p(x,y)$ holds for all $x, y \in s$, 2. $p(0,x)$ holds for all $x \in \text{closure}(s)$, 3. $p(x,0)$ holds for all $x \in \text{closure}(s)$, 4. $p(1,x)$ holds for all $x \in \text{closure}(s)$, 5. $p(x,1)$ holds for all $x \in \text{closure}(s)$, 6. For any $x, y, z \in \text{closure}(s)$, if $p(x,z)$ and $p(y,z)$ hold, then $p(x+y,z)$ holds, 7. For any $x, y, z \in \text{closure}(s)$, if $p(x,y)$ and $p(x,z)$ hold, then $p(x,y+z)$ holds, 8. 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, 9. 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 every $x, y \in \text{closure}(s)$.

Subsemiring.mem_closure_iff_exists_list theorem

 {R} [Semiring R] {s : Set R} {x} :
  x ∈ closure s ↔ ∃ L : List (List R), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (L.map List.prod).sum = x

Full source

theorem mem_closure_iff_exists_list {R} [Semiring R] {s : Set R} {x} :
    x ∈ closure sx ∈ closure s ↔ ∃ L : List (List R), (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (L.map List.prod).sum = x := by
  constructor
  · intro hx
    rw [mem_closure_iff] at hx
    induction hx using AddSubmonoid.closure_induction with
    | mem x hx =>
      suffices ∃ t : List R, (∀ y ∈ t, y ∈ s) ∧ t.prod = x from
        let ⟨t, ht1, ht2⟩ := this
        ⟨[t], List.forall_mem_singleton.2 ht1, by
          rw [List.map_singleton, List.sum_singleton, ht2]⟩
      induction hx using Submonoid.closure_induction with
      | mem x hx => exact ⟨[x], List.forall_mem_singleton.2 hx, List.prod_singleton⟩
      | one => exact ⟨[], List.forall_mem_nil _, rfl⟩
      | mul x y _ _ ht hu =>
        obtain ⟨⟨t, ht1, ht2⟩, ⟨u, hu1, hu2⟩⟩ := And.intro ht hu
        exact ⟨t ++ u, List.forall_mem_append.2 ⟨ht1, hu1⟩, by rw [List.prod_append, ht2, hu2]⟩
    | one => exact ⟨[], List.forall_mem_nil _, rfl⟩
    | mul x y _ _ hL hM =>
      obtain ⟨⟨L, HL1, HL2⟩, ⟨M, HM1, HM2⟩⟩ := And.intro hL hM
      exact ⟨L ++ M, List.forall_mem_append.2 ⟨HL1, HM1⟩, by
        rw [List.map_append, List.sum_append, HL2, HM2]⟩
  · rintro ⟨L, HL1, rfl⟩
    exact
      list_sum_mem fun r hr =>
        let ⟨t, ht1, ht2⟩ := List.mem_map.1 hr
        ht2 ▸ list_prod_mem _ fun y hy => subset_closure <| HL1 t ht1 y hy

Characterization of Subsemiring Membership via Sums of Products

Informal description

Let $R$ be a semiring and $s$ a subset of $R$. An element $x \in R$ belongs to the subsemiring generated by $s$ if and only if there exists a list of lists $L$ such that: 1. Every element in every sublist of $L$ belongs to $s$, and 2. The sum of the products of the sublists in $L$ equals $x$. In other words, $x \in \text{closure}(s)$ if and only if $x$ can be expressed as a finite sum of finite products of elements from $s$.

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

Informal description

The pair of functions `(closure, (↑))` forms a Galois insertion between the power set of a semiring $R$ and its lattice of subsemirings. Here: - `closure : \mathcal{P}(R) → \text{Subsemiring}(R)` is the function that takes a subset $s ⊆ R$ to the smallest subsemiring containing $s$ - `(↑) : \text{Subsemiring}(R) → \mathcal{P}(R)` is the coercion that maps a subsemiring to its underlying set This means: 1. For any subset $s ⊆ R$ and subsemiring $t$, we have $\text{closure}(s) ≤ t ↔ s ⊆ t$ (Galois connection property) 2. For any subsemiring $t$, we have $t ⊆ \text{closure}(t)$ (section property) 3. The composition satisfies $\text{closure} ∘ (↑) = \text{id}$ on subsemirings

Subsemiring.closure_eq theorem

(s : Subsemiring R) : closure (s : Set R) = s

Full source

/-- Closure of a subsemiring `S` equals `S`. -/
@[simp]
theorem closure_eq (s : Subsemiring R) : closure (s : Set R) = s :=
  (Subsemiring.gi R).l_u_eq s

Closure of a Subsemiring Equals Itself

Informal description

For any subsemiring $S$ of a semiring $R$, the closure of $S$ (viewed as a subset of $R$) equals $S$ itself, i.e., $\text{closure}(S) = S$.

Subsemiring.closure_empty theorem

: closure (∅ : Set R) = ⊥

Full source

@[simp]
theorem closure_empty : closure (∅ : Set R) = ⊥ :=
  (Subsemiring.gi R).gc.l_bot

Empty Set Generates Bottom Subsemiring

Informal description

The subsemiring generated by the empty set in a non-associative semiring $R$ is equal to the bottom element of the lattice of subsemirings of $R$.

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

Informal description

For any non-associative semiring $R$, the subsemiring generated by the universal set (the set of all elements of $R$) is equal to the top element of the lattice of subsemirings of $R$, i.e., $\text{closure}(\text{univ}) = \top$.

Subsemiring.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 :=
  (Subsemiring.gi R).gc.l_sup

Subsemiring Generation of Union Equals Supremum of Generations

Informal description

For any two subsets $s$ and $t$ of a semiring $R$, the subsemiring generated by their union $s \cup t$ is equal to the supremum of the subsemirings generated by $s$ and $t$ individually, i.e., \[ \text{closure}(s \cup t) = \text{closure}(s) \sqcup \text{closure}(t). \]

Subsemiring.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) :=
  (Subsemiring.gi R).gc.l_iSup

Subsemiring Closure of Union Equals Supremum of Closures

Informal description

For any indexed family of subsets $(s_i)_{i \in \iota}$ of a non-associative semiring $R$, the subsemiring generated by their union $\bigcup_i s_i$ is equal to the supremum of the subsemirings generated by each individual subset $s_i$.

Subsemiring.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 :=
  (Subsemiring.gi R).gc.l_sSup

Subsemiring Closure Preserves Set Union: $\text{closure}(\bigcup₀ s) = \bigsqcup_{t \in s} \text{closure}(t)$

Informal description

For any family of subsets $s$ of a non-associative semiring $R$, the subsemiring generated by the union of all sets in $s$ is equal to the supremum of the 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). \]

Subsemiring.closure_singleton_natCast theorem

(n : ℕ) : closure {(n : R)} = ⊥

Full source

@[simp]
theorem closure_singleton_natCast (n : ℕ) : closure {(n : R)} = ⊥ :=
  bot_unique <| closure_le.2 <| Set.singleton_subset_iff.mpr <| natCast_mem _ _

Subsemiring Generated by Singleton Natural Number is Bottom Element

Informal description

For any natural number $n$ and any non-associative semiring $R$, the subsemiring generated by the singleton set $\{n\}$ (where $n$ is viewed as an element of $R$ via the canonical map from $\mathbb{N}$ to $R$) is equal to the bottom element $\bot$ of the complete lattice of subsemirings of $R$.

Subsemiring.closure_singleton_zero theorem

: closure {(0 : R)} = ⊥

Full source

@[simp]
theorem closure_singleton_zero : closure {(0 : R)} = ⊥ := mod_cast closure_singleton_natCast 0

Subsemiring Generated by Zero is Bottom Element

Informal description

For any non-associative semiring $R$, the subsemiring generated by the singleton set $\{0\}$ is equal to the bottom element $\bot$ of the complete lattice of subsemirings of $R$.

Subsemiring.closure_singleton_one theorem

: closure {(1 : R)} = ⊥

Full source

@[simp]
theorem closure_singleton_one : closure {(1 : R)} = ⊥ := mod_cast closure_singleton_natCast 1

Subsemiring Generated by $\{1\}$ is Bottom Element

Informal description

For any non-associative semiring $R$, the subsemiring generated by the singleton set $\{1\}$ (where $1$ is the multiplicative identity of $R$) is equal to the bottom element $\bot$ of the complete lattice of subsemirings of $R$.

Subsemiring.closure_insert_natCast theorem

(n : ℕ) (s : Set R) : closure (insert (n : R) s) = closure s

Full source

@[simp]
theorem closure_insert_natCast (n : ℕ) (s : Set R) : closure (insert (n : R) s) = closure s := by
  rw [Set.insert_eq, closure_union]
  simp

Subsemiring Generation Unaffected by Insertion of Natural Number Elements: $\text{closure}(\text{insert}(n, s)) = \text{closure}(s)$

Informal description

For any natural number $n$ and any subset $s$ of a non-associative semiring $R$, the subsemiring generated by the insertion of $n$ (viewed as an element of $R$) into $s$ is equal to the subsemiring generated by $s$ alone, i.e., \[ \text{closure}(\text{insert}(n, s)) = \text{closure}(s). \]

Subsemiring.closure_insert_zero theorem

(s : Set R) : closure (insert 0 s) = closure s

Full source

@[simp]
theorem closure_insert_zero (s : Set R) : closure (insert 0 s) = closure s :=
  mod_cast closure_insert_natCast 0 s

Subsemiring Generation Unaffected by Insertion of Zero: $\text{closure}(\text{insert}(0, s)) = \text{closure}(s)$

Informal description

For any subset $s$ of a non-associative semiring $R$, the subsemiring generated by inserting the zero element into $s$ is equal to the subsemiring generated by $s$ alone, i.e., \[ \text{closure}(\text{insert}(0, s)) = \text{closure}(s). \]

Subsemiring.closure_insert_one theorem

(s : Set R) : closure (insert 1 s) = closure s

Full source

@[simp]
theorem closure_insert_one (s : Set R) : closure (insert 1 s) = closure s :=
  mod_cast closure_insert_natCast 1 s

Subsemiring Generation Unaffected by Insertion of One: $\text{closure}(\text{insert}(1, s)) = \text{closure}(s)$

Informal description

For any subset $s$ of a non-associative semiring $R$, the subsemiring generated by inserting the multiplicative identity $1$ into $s$ is equal to the subsemiring generated by $s$ alone, i.e., \[ \text{closure}(\text{insert}(1, s)) = \text{closure}(s). \]

Subsemiring.map_sup theorem

(s t : Subsemiring R) (f : R →+* S) : (s ⊔ t).map f = s.map f ⊔ t.map f

Full source

theorem map_sup (s t : Subsemiring R) (f : R →+* S) : (s ⊔ t).map f = s.map f ⊔ t.map f :=
  (gc_map_comap f).l_sup

Image of Subsemiring Supremum under Ring Homomorphism Equals Supremum of Images

Informal description

Let $R$ and $S$ be non-associative semirings, $f \colon R \to S$ a ring homomorphism, and $s, t$ subsemirings of $R$. Then the image of the supremum $s \sqcup t$ under $f$ equals the supremum of the images of $s$ and $t$ under $f$: \[ f(s \sqcup t) = f(s) \sqcup f(t). \]

Subsemiring.map_iSup theorem

{ι : Sort*} (f : R →+* S) (s : ι → Subsemiring R) : (iSup s).map f = ⨆ i, (s i).map f

Full source

theorem map_iSup {ι : Sort*} (f : R →+* S) (s : ι → Subsemiring R) :
    (iSup s).map f = ⨆ i, (s i).map f :=
  (gc_map_comap f).l_iSup

Image of Supremum of Subsemirings Equals Supremum of Images under Ring Homomorphism

Informal description

Let $R$ and $S$ be non-associative semirings, and let $f \colon R \to S$ be a ring homomorphism. For any family of subsemirings $\{s_i\}_{i \in \iota}$ of $R$, the image of their supremum under $f$ equals the supremum of their images: \[ f\left(\bigsqcup_{i \in \iota} s_i\right) = \bigsqcup_{i \in \iota} f(s_i). \]

Subsemiring.map_inf theorem

(s t : Subsemiring R) (f : R →+* S) (hf : Function.Injective f) : (s ⊓ t).map f = s.map f ⊓ t.map f

Full source

theorem map_inf (s t : Subsemiring R) (f : R →+* S) (hf : Function.Injective f) :
    (s ⊓ t).map f = s.map f ⊓ t.map f := SetLike.coe_injective (Set.image_inter hf)

Image of Intersection of Subsemirings under Injective Ring Homomorphism Equals Intersection of Images

Informal description

Let $R$ and $S$ be non-associative semirings, $f \colon R \to S$ an injective ring homomorphism, and $s, t$ subsemirings of $R$. Then the image of the intersection $s \cap t$ under $f$ equals the intersection of the images of $s$ and $t$ under $f$: \[ f(s \cap t) = f(s) \cap f(t). \]

Subsemiring.map_iInf theorem

 {ι : Sort*} [Nonempty ι] (f : R →+* S) (hf : Function.Injective f) (s : ι → Subsemiring R) :
  (iInf s).map f = ⨅ i, (s i).map f

Full source

theorem map_iInf {ι : Sort*} [Nonempty ι] (f : R →+* S) (hf : Function.Injective f)
    (s : ι → Subsemiring R) : (iInf s).map f = ⨅ i, (s i).map f := by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coeSetLike.coe ∘ s)

Image of Infimum of Subsemirings under Injective Ring Homomorphism Equals Infimum of Images

Informal description

Let $R$ and $S$ be non-associative semirings, $\iota$ a nonempty index set, and $f \colon R \to S$ an injective ring homomorphism. For any family of subsemirings $\{S_i\}_{i \in \iota}$ of $R$, the image of their infimum under $f$ equals the infimum of their images: \[ f\left(\bigsqcap_{i \in \iota} S_i\right) = \bigsqcap_{i \in \iota} f(S_i). \]

Subsemiring.comap_inf theorem

(s t : Subsemiring S) (f : R →+* S) : (s ⊓ t).comap f = s.comap f ⊓ t.comap f

Full source

theorem comap_inf (s t : Subsemiring S) (f : R →+* S) : (s ⊓ t).comap f = s.comap f ⊓ t.comap f :=
  (gc_map_comap f).u_inf

Preimage of Subsemiring Intersection Equals Intersection of Preimages

Informal description

Let $R$ and $S$ be non-associative semirings, $f \colon R \to S$ a ring homomorphism, and $s, t$ subsemirings of $S$. Then the preimage of the intersection $s \cap t$ under $f$ equals the intersection of the preimages of $s$ and $t$ under $f$: \[ f^{-1}(s \cap t) = f^{-1}(s) \cap f^{-1}(t). \]

Subsemiring.comap_iInf theorem

{ι : Sort*} (f : R →+* S) (s : ι → Subsemiring S) : (iInf s).comap f = ⨅ i, (s i).comap f

Full source

theorem comap_iInf {ι : Sort*} (f : R →+* S) (s : ι → Subsemiring S) :
    (iInf s).comap f = ⨅ i, (s i).comap f :=
  (gc_map_comap f).u_iInf

Preimage of Infimum of Subsemirings Equals Infimum of Preimages

Informal description

Let $R$ and $S$ be non-associative semirings, $\iota$ an index set, and $f \colon R \to S$ a ring homomorphism. For any family of subsemirings $\{S_i\}_{i \in \iota}$ 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). \]

Subsemiring.map_bot theorem

(f : R →+* S) : (⊥ : Subsemiring R).map f = ⊥

Full source

@[simp]
theorem map_bot (f : R →+* S) : (⊥ : Subsemiring R).map f = ⊥ :=
  (gc_map_comap f).l_bot

Image of Bottom Subsemiring is Bottom

Informal description

For any ring homomorphism $f \colon R \to S$ between non-associative semirings, the image of the bottom subsemiring of $R$ under $f$ is equal to the bottom subsemiring of $S$. That is, $f(\bot_R) = \bot_S$.

Subsemiring.comap_top theorem

(f : R →+* S) : (⊤ : Subsemiring S).comap f = ⊤

Full source

@[simp]
theorem comap_top (f : R →+* S) : (⊤ : Subsemiring S).comap f = ⊤ :=
  (gc_map_comap f).u_top

Preimage of Top Subsemiring is Top

Informal description

For any ring homomorphism $f \colon R \to S$ between non-associative semirings, the preimage of the top subsemiring of $S$ under $f$ is equal to the top subsemiring of $R$. That is, $f^{-1}(S) = R$.

Subsemiring.prod definition

(s : Subsemiring R) (t : Subsemiring S) : Subsemiring (R × S)

Full source

/-- Given `Subsemiring`s `s`, `t` of semirings `R`, `S` respectively, `s.prod t` is `s × t`
as a subsemiring of `R × S`. -/
def prod (s : Subsemiring R) (t : Subsemiring S) : Subsemiring (R × S) :=
  { s.toSubmonoid.prod t.toSubmonoid, s.toAddSubmonoid.prod t.toAddSubmonoid with
    carrier := s ×ˢ t }

Product of subsemirings

Informal description

Given subsemirings $s$ of a semiring $R$ and $t$ of a semiring $S$, the product subsemiring $s \times t$ is defined as the subsemiring of $R \times S$ consisting of all pairs $(r, s)$ where $r \in s$ and $s \in t$. This subsemiring is constructed by taking the product of the underlying submonoids and additive submonoids of $s$ and $t$.

Subsemiring.coe_prod theorem

(s : Subsemiring R) (t : Subsemiring S) : (s.prod t : Set (R × S)) = (s : Set R) ×ˢ (t : Set S)

Full source

@[norm_cast]
theorem coe_prod (s : Subsemiring R) (t : Subsemiring 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 subsemirings $s$ of a semiring $R$ and $t$ of a semiring $S$, the underlying set of the product subsemiring $s \times t$ is equal to the Cartesian product of the underlying sets of $s$ and $t$, i.e., $(s \times t) = s \timesˢ t$ as subsets of $R \times S$.

Subsemiring.mem_prod theorem

{s : Subsemiring R} {t : Subsemiring S} {p : R × S} : p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t

Full source

theorem mem_prod {s : Subsemiring R} {t : Subsemiring S} {p : R × S} :
    p ∈ s.prod tp ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t :=
  Iff.rfl

Membership in Product of Subsemirings

Informal description

For any subsemirings $s$ of a semiring $R$ and $t$ of a semiring $S$, and any element $p = (r, s) \in R \times S$, we have $p \in s \times t$ if and only if $r \in s$ and $s \in t$.

Subsemiring.prod_mono theorem

 ⦃s₁ s₂ : Subsemiring R⦄ (hs : s₁ ≤ s₂) ⦃t₁ t₂ : Subsemiring S⦄ (ht : t₁ ≤ t₂) : s₁.prod t₁ ≤ s₂.prod t₂

Full source

@[gcongr, mono]
theorem prod_mono ⦃s₁ s₂ : Subsemiring R⦄ (hs : s₁ ≤ s₂) ⦃t₁ t₂ : Subsemiring S⦄ (ht : t₁ ≤ t₂) :
    s₁.prod t₁ ≤ s₂.prod t₂ :=
  Set.prod_mono hs ht

Monotonicity of Product Subsemirings with Respect to Inclusion

Informal description

For any subsemirings $s_1, s_2$ of a semiring $R$ and $t_1, t_2$ of a semiring $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$.

Subsemiring.prod_mono_right theorem

(s : Subsemiring R) : Monotone fun t : Subsemiring S => s.prod t

Full source

theorem prod_mono_right (s : Subsemiring R) : Monotone fun t : Subsemiring S => s.prod t :=
  prod_mono (le_refl s)

Monotonicity of Product Subsemirings in the Right Factor

Informal description

For any subsemiring $s$ of a non-associative semiring $R$, the function that maps a subsemiring $t$ of a non-associative semiring $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$.

Subsemiring.prod_mono_left theorem

(t : Subsemiring S) : Monotone fun s : Subsemiring R => s.prod t

Full source

theorem prod_mono_left (t : Subsemiring S) : Monotone fun s : Subsemiring R => s.prod t :=
  fun _ _ hs => prod_mono hs (le_refl t)

Monotonicity of Left Factor in Product Subsemirings

Informal description

For any subsemiring $t$ of a semiring $S$, the function that maps a 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 subsemirings of $R$, then $s_1 \times t \subseteq s_2 \times t$.

Subsemiring.prod_top theorem

(s : Subsemiring R) : s.prod (⊤ : Subsemiring S) = s.comap (RingHom.fst R S)

Full source

theorem prod_top (s : Subsemiring R) : s.prod (⊤ : Subsemiring S) = s.comap (RingHom.fst R S) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_fst]

Product of a Subsemiring with Top Subsemiring Equals Preimage under First Projection

Informal description

For any subsemiring $s$ of a non-associative semiring $R$, the product subsemiring $s \times S$ (where $S$ is the top subsemiring of another non-associative semiring $S$) is equal to the preimage of $s$ under the first projection ring homomorphism from $R \times S$ to $R$.

Subsemiring.top_prod theorem

(s : Subsemiring S) : (⊤ : Subsemiring R).prod s = s.comap (RingHom.snd R S)

Full source

theorem top_prod (s : Subsemiring S) : (⊤ : Subsemiring R).prod s = s.comap (RingHom.snd R S) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_snd]

Product of Top Subsemiring with $s$ Equals Preimage under Second Projection

Informal description

For any subsemiring $s$ of a semiring $S$, the product of the top subsemiring of $R$ with $s$ is equal to the preimage of $s$ under the second projection homomorphism $\text{snd} \colon R \times S \to S$.

Subsemiring.top_prod_top theorem

: (⊤ : Subsemiring R).prod (⊤ : Subsemiring S) = ⊤

Full source

@[simp]
theorem top_prod_top : (⊤ : Subsemiring R).prod (⊤ : Subsemiring S) = ⊤ :=
  (top_prod _).trans <| comap_top _

Product of Top Subsemirings is Top Subsemiring of Product

Informal description

For any non-associative semirings $R$ and $S$, the product of the top subsemiring of $R$ and the top subsemiring of $S$ is equal to the top subsemiring of $R \times S$.

Subsemiring.prodEquiv definition

(s : Subsemiring R) (t : Subsemiring S) : s.prod t ≃+* s × t

Full source

/-- Product of subsemirings is isomorphic to their product as monoids. -/
def prodEquiv (s : Subsemiring R) (t : Subsemiring 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 subsemiring and product of subsemirings

Informal description

Given subsemirings $ s $ of a semiring $ R $ and $ t $ of a semiring $ S $, the product subsemiring $ s \times t $ is isomorphic (as a semiring) to the direct product of the subsemirings $ s $ and $ t $. The isomorphism is given by the canonical bijection between the product set $ s \times t $ and the product type $ s \times t $, which preserves both the multiplicative and additive structures.

Subsemiring.mem_iSup_of_directed theorem

 {ι} [hι : Nonempty ι] {S : ι → Subsemiring R} (hS : Directed (· ≤ ·) S) {x : R} : (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i

Full source

theorem mem_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → Subsemiring 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 : Subsemiring R :=
    Subsemiring.mk' (⋃ i, (S i : Set R))
      (⨆ i, (S i).toSubmonoid) (Submonoid.coe_iSup_of_directed hS)
      (⨆ i, (S i).toAddSubmonoid) (AddSubmonoid.coe_iSup_of_directed hS)
  suffices ⨆ i, S i ≤ U by simpa [U] using @this x
  exact iSup_le fun i x hx ↦ Set.mem_iUnion.2 ⟨i, hx⟩

Characterization of Membership in Directed Supremum of Subsemirings: $x \in \bigsqcup_i S_i \leftrightarrow \exists i, x \in S_i$

Informal description

Let $R$ be a non-associative semiring, $\iota$ a nonempty index set, and $(S_i)_{i \in \iota}$ a directed family of 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$.

Subsemiring.coe_iSup_of_directed theorem

 {ι} [hι : Nonempty ι] {S : ι → Subsemiring R} (hS : Directed (· ≤ ·) S) :
  ((⨆ i, S i : Subsemiring R) : Set R) = ⋃ i, S i

Full source

theorem coe_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → Subsemiring R}
    (hS : Directed (· ≤ ·) S) : ((⨆ i, S i : Subsemiring R) : Set R) = ⋃ i, S i :=
  Set.ext fun x ↦ by simp [mem_iSup_of_directed hS]

Supremum of Directed Family of Subsemirings Equals Union of Their Underlying Sets

Informal description

Let $R$ be a non-associative semiring, $\iota$ a nonempty index set, and $(S_i)_{i \in \iota}$ a directed family of subsemirings of $R$ with respect to inclusion. Then the underlying set of the supremum of the subsemirings $S_i$ is equal to the union of the underlying sets of the $S_i$, i.e., \[ \big(\bigsqcup_{i \in \iota} S_i\big) = \bigcup_{i \in \iota} S_i. \]

Subsemiring.mem_sSup_of_directedOn theorem

 {S : Set (Subsemiring 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 (Subsemiring 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, SetCoe.exists, Subtype.coe_mk,
    exists_prop]

Characterization of Membership in Directed Supremum of Subsemirings: $x \in \bigsqcup S \leftrightarrow \exists s \in S, x \in s$

Informal description

Let $R$ be a non-associative semiring and $S$ a nonempty set of 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$.

Subsemiring.coe_sSup_of_directedOn theorem

 {S : Set (Subsemiring R)} (Sne : S.Nonempty) (hS : DirectedOn (· ≤ ·) S) : (↑(sSup S) : Set R) = ⋃ s ∈ S, ↑s

Full source

theorem coe_sSup_of_directedOn {S : Set (Subsemiring 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]

Supremum of Directed Family of Subsemirings Equals Union of Their Carrier Sets

Informal description

Let $R$ be a non-associative semiring and $S$ a nonempty set of subsemirings of $R$ that is directed with respect to inclusion. Then the underlying set of the supremum of $S$ is equal to the union of the underlying sets of the subsemirings in $S$, i.e., \[ \big(\bigsqcup S\big) = \bigcup_{s \in S} s. \]

RingHom.codRestrict definition

(f : R →+* S) (s : σS) (h : ∀ x, f x ∈ s) : R →+* s

Full source

/-- Restriction of a ring homomorphism to a subsemiring of the codomain. -/
def codRestrict (f : R →+* S) (s : σS) (h : ∀ x, f x ∈ s) : R →+* s :=
  { (f : R →* S).codRestrict s h, (f : R →+ S).codRestrict s h with toFun := fun n => ⟨f n, h n⟩ }

Restriction of a ring homomorphism to a subsemiring of the codomain

Informal description

Given a ring homomorphism $ f \colon R \to S $ and a subsemiring $ s $ of $ S $ such that $ f(x) \in s $ for all $ x \in R $, the function `RingHom.codRestrict` restricts the codomain of $ f $ to $ s $, yielding a ring homomorphism $ R \to s $. This is defined by mapping each $ x \in R $ to $ \langle f(x), h(x) \rangle $, where $ h $ is the proof that $ f(x) \in s $, and preserving both the additive and multiplicative structures (including zero and one).

RingHom.codRestrict_apply theorem

(f : R →+* S) (s : σS) (h : ∀ x, f x ∈ s) (x : R) : (f.codRestrict s h x : S) = f x

Full source

@[simp]
theorem codRestrict_apply (f : R →+* S) (s : σS) (h : ∀ x, f x ∈ s) (x : R) :
    (f.codRestrict s h x : S) = f x :=
  rfl

Codomain Restriction of Ring Homomorphism Preserves Images

Informal description

Let $f \colon R \to S$ be a ring homomorphism, $s$ a subsemiring of $S$, and $h$ a proof that $f(x) \in s$ for all $x \in R$. Then for any $x \in R$, the image of $x$ under the codomain-restricted homomorphism $f.\text{codRestrict}\, s\, h$ (viewed as an element of $S$) equals $f(x)$. In other words, $(f.\text{codRestrict}\, s\, h)(x) = f(x)$ as elements of $S$.

RingHom.restrict definition

(f : R →+* S) (s' : σR) (s : σS) (h : ∀ x ∈ s', f x ∈ s) : s' →+* s

Full source

/-- The ring homomorphism from the preimage of `s` to `s`. -/
def restrict (f : R →+* S) (s' : σR) (s : σS) (h : ∀ x ∈ s', f x ∈ s) : s' →+* s :=
  (f.domRestrict s').codRestrict s fun x => h x x.2

Restriction of a ring homomorphism to subsemirings of domain and codomain

Informal description

Given a ring homomorphism $ f \colon R \to S $, a subsemiring $ s' $ of $ R $, and a subsemiring $ s $ of $ S $ such that $ f(x) \in s $ for all $ x \in s' $, the function `RingHom.restrict` restricts both the domain and codomain of $ f $, yielding a ring homomorphism $ s' \to s $. This is defined by first restricting the domain to $ s' $ and then restricting the codomain to $ s $, while preserving both the additive and multiplicative structures (including zero and one).

RingHom.coe_restrict_apply theorem

(f : R →+* S) (s' : σR) (s : σS) (h : ∀ x ∈ s', f x ∈ s) (x : s') : (f.restrict s' s h x : S) = f x

Full source

@[simp]
theorem coe_restrict_apply (f : R →+* S) (s' : σR) (s : σS) (h : ∀ x ∈ s', f x ∈ s) (x : s') :
    (f.restrict s' s h x : S) = f x :=
  rfl

Restricted Ring Homomorphism Preserves Images

Informal description

Let $f \colon R \to S$ be a ring homomorphism between non-associative semirings, $s'$ a subsemiring of $R$, and $s$ a subsemiring of $S$ such that $f(x) \in s$ for all $x \in s'$. Then for any $x \in s'$, the image of $x$ under the restricted homomorphism $f|_{s'}^{s}$ (viewed as an element of $S$) equals $f(x)$. In other words, $(f|_{s'}^{s})(x) = f(x)$ as elements of $S$.

RingHom.comp_restrict theorem

 (f : R →+* S) (s' : σR) (s : σS) (h : ∀ x ∈ s', f x ∈ s) :
  (SubsemiringClass.subtype s).comp (f.restrict s' s h) = f.comp (SubsemiringClass.subtype s')

Full source

@[simp]
theorem comp_restrict (f : R →+* S) (s' : σR) (s : σS) (h : ∀ x ∈ s', f x ∈ s) :
    (SubsemiringClass.subtype s).comp (f.restrict s' s h) = f.comp (SubsemiringClass.subtype s') :=
  rfl

Commutativity of Restriction and Composition for Ring Homomorphisms

Informal description

Let $R$ and $S$ be non-associative semirings, and let $f \colon R \to S$ be a ring homomorphism. Given subsemirings $s' \subseteq R$ and $s \subseteq S$ such that $f(x) \in s$ for all $x \in s'$, the composition of the inclusion map $s \hookrightarrow S$ with the restricted homomorphism $f|_{s'} \colon s' \to s$ equals the composition of $f$ with the inclusion map $s' \hookrightarrow R$. That is, the following diagram commutes: \[ \begin{CD} s' @>{f|_{s'}}>> s \\ @VVV @VVV \\ R @>{f}>> S \end{CD} \] where the vertical maps are the inclusion homomorphisms.

RingHom.rangeSRestrict definition

(f : R →+* S) : R →+* f.rangeS

Full source

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

This is the bundled version of `Set.rangeFactorization`. -/
def rangeSRestrict (f : R →+* S) : R →+* f.rangeS :=
  f.codRestrict (R := R) (S := S) (σS := Subsemiring S) f.rangeS f.mem_rangeS_self

Restriction of a ring homomorphism to its range subsemiring

Informal description

Given a ring homomorphism $ f \colon R \to S $ between non-associative semirings, the function `RingHom.rangeSRestrict` restricts the codomain of $ f $ to its range $ f.\text{rangeS} $ (which is a subsemiring of $ S $), yielding a ring homomorphism $ R \to f.\text{rangeS} $. This is defined by mapping each $ x \in R $ to $ \langle f(x), h(x) \rangle $, where $ h $ is the proof that $ f(x) \in f.\text{rangeS} $, and preserving both the additive and multiplicative structures (including zero and one).

RingHom.coe_rangeSRestrict theorem

(f : R →+* S) (x : R) : (f.rangeSRestrict x : S) = f x

Full source

@[simp]
theorem coe_rangeSRestrict (f : R →+* S) (x : R) : (f.rangeSRestrict x : S) = f x :=
  rfl

Coercion of Range-Restricted Homomorphism Equals Original Homomorphism

Informal description

For any ring homomorphism $f \colon R \to S$ between non-associative semirings and any element $x \in R$, the image of $x$ under the range-restricted homomorphism $f.\text{rangeSRestrict}$, when viewed as an element of $S$, equals $f(x)$. In other words, if we let $f' = f.\text{rangeSRestrict} \colon R \to f.\text{rangeS}$ be the restriction of $f$ to its range subsemiring, then for any $x \in R$, the coercion of $f'(x)$ back to $S$ equals $f(x)$.

RingHom.rangeSRestrict_surjective theorem

(f : R →+* S) : Function.Surjective f.rangeSRestrict

Full source

theorem rangeSRestrict_surjective (f : R →+* S) : Function.Surjective f.rangeSRestrict :=
  fun ⟨_, hy⟩ =>
  let ⟨x, hx⟩ := mem_rangeS.mp hy
  ⟨x, Subtype.ext hx⟩

Surjectivity of the Range-Restricted Ring Homomorphism

Informal description

For any ring homomorphism $f \colon R \to S$ between non-associative semirings, the restricted homomorphism $f.\text{rangeSRestrict} \colon R \to f.\text{rangeS}$ is surjective. That is, for every $y \in f.\text{rangeS}$, there exists an $x \in R$ such that $f.\text{rangeSRestrict}(x) = y$.

RingHom.rangeS_top_iff_surjective theorem

{f : R →+* S} : f.rangeS = (⊤ : Subsemiring S) ↔ Function.Surjective f

Full source

theorem rangeS_top_iff_surjective {f : R →+* S} :
    f.rangeS = (⊤ : Subsemiring S) ↔ Function.Surjective f :=
  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_rangeS, coe_top]) Set.range_eq_univ

Range Equals Top Subsemiring iff Ring Homomorphism is Surjective

Informal description

For a ring homomorphism $f \colon R \to S$ between non-associative semirings, the range of $f$ is equal to the top subsemiring of $S$ (i.e., $S$ itself) if and only if $f$ is surjective. In other words, $\text{rangeS}(f) = S \leftrightarrow f \text{ is surjective}$.

RingHom.rangeS_top_of_surjective theorem

(f : R →+* S) (hf : Function.Surjective f) : f.rangeS = (⊤ : Subsemiring S)

Full source

/-- The range of a surjective ring homomorphism is the whole of the codomain. -/
@[simp]
theorem rangeS_top_of_surjective (f : R →+* S) (hf : Function.Surjective f) :
    f.rangeS = (⊤ : Subsemiring S) :=
  rangeS_top_iff_surjective.2 hf

Surjective Ring Homomorphism Has Full Range

Informal description

Let $f \colon R \to S$ be a surjective ring homomorphism between non-associative semirings. Then the range of $f$ is equal to the entire codomain $S$, i.e., $\text{range}(f) = S$.

RingHom.eqOn_sclosure theorem

{f g : R →+* S} {s : Set R} (h : Set.EqOn f g s) : Set.EqOn f g (closure s)

Full source

/-- If two ring homomorphisms are equal on a set, then they are equal on its subsemiring closure. -/
theorem eqOn_sclosure {f g : R →+* S} {s : Set R} (h : Set.EqOn f g s) : Set.EqOn f g (closure s) :=
  show closure s ≤ f.eqLocusS g from closure_le.2 h

Agreement of Ring Homomorphisms on Subsemiring Closure

Informal description

Let $f, g \colon R \to S$ be two ring homomorphisms between non-associative semirings, and let $s \subseteq R$ be a subset. If $f$ and $g$ agree on $s$ (i.e., $f(x) = g(x)$ for all $x \in s$), then they also agree on the subsemiring closure of $s$ (i.e., $f(x) = g(x)$ for all $x$ in the smallest subsemiring containing $s$).

RingHom.sclosure_preimage_le theorem

(f : R →+* S) (s : Set S) : closure (f ⁻¹' s) ≤ (closure s).comap f

Full source

theorem sclosure_preimage_le (f : R →+* S) (s : Set S) : closure (f ⁻¹' s) ≤ (closure s).comap f :=
  closure_le.2 fun _ hx => SetLike.mem_coe.2 <| mem_comap.2 <| subset_closure hx

Subsemiring Closure of Preimage is Contained in Preimage of Closure

Informal description

For any ring homomorphism $f \colon R \to S$ and any subset $s \subseteq S$, the subsemiring generated by the preimage $f^{-1}(s)$ is contained in the preimage of the subsemiring generated by $s$ under $f$. In other words: $$\text{closure}(f^{-1}(s)) \leq f^{-1}(\text{closure}(s)).$$

RingHom.map_closureS theorem

(f : R →+* S) (s : Set R) : (closure s).map f = closure (f '' 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_closureS (f : R →+* S) (s : Set R) : (closure s).map f = closure (f '' s) :=
  Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) (Subsemiring.gi S).gc (Subsemiring.gi R).gc
    fun _ ↦ coe_comap _ _

Image of Generated Subsemiring Equals Generated Image

Informal description

Let $R$ and $S$ be non-associative semirings, and let $f : R \to S$ be a ring homomorphism. For any subset $s \subseteq R$, the image under $f$ of the subsemiring generated by $s$ equals the subsemiring generated by the image $f(s)$. That is, $$ f(\text{closure}(s)) = \text{closure}(f(s)). $$

Subsemiring.inclusion definition

{S T : Subsemiring R} (h : S ≤ T) : S →+* T

Full source

/-- The ring homomorphism associated to an inclusion of subsemirings. -/
def inclusion {S T : Subsemiring R} (h : S ≤ T) : S →+* T :=
  S.subtype.codRestrict _ fun x => h x.2

Inclusion homomorphism of subsemirings

Informal description

Given two subsemirings $ S $ and $ T $ of a semiring $ R $ such that $ S \subseteq T $, the function `Subsemiring.inclusion` is the canonical ring homomorphism from $ S $ to $ T $ that maps each element $ x \in S $ to itself (viewed as an element of $ T $). This homomorphism preserves both the additive and multiplicative structures of the subsemirings.

Subsemiring.inclusion_injective theorem

{S T : Subsemiring R} (h : S ≤ T) : Function.Injective (inclusion h)

Full source

theorem inclusion_injective {S T : Subsemiring R} (h : S ≤ T) :
    Function.Injective (inclusion h) := Set.inclusion_injective h

Injectivity of Subsemiring Inclusion Homomorphism

Informal description

For any two subsemirings $S$ and $T$ of a semiring $R$ with $S \subseteq T$, the inclusion homomorphism $\text{inclusion}(h) : S \to T$ is injective. That is, for any $x, y \in S$, if $\text{inclusion}(h)(x) = \text{inclusion}(h)(y)$, then $x = y$.

Subsemiring.rangeS_subtype theorem

(s : Subsemiring R) : s.subtype.rangeS = s

Full source

@[simp]
theorem rangeS_subtype (s : Subsemiring R) : s.subtype.rangeS = s :=
  SetLike.coe_injective <| (coe_rangeS _).trans Subtype.range_coe

Range of Subsemiring Inclusion Equals Subsemiring

Informal description

For any subsemiring $s$ of a semiring $R$, the range of the canonical inclusion homomorphism $s \hookrightarrow R$ is equal to $s$ itself. That is, $\text{rangeS}(s.subtype) = s$.

Subsemiring.range_fst theorem

: (fst R S).rangeS = ⊤

Full source

@[simp]
theorem range_fst : (fst R S).rangeS = ⊤ :=
  (fst R S).rangeS_top_of_surjective <| Prod.fst_surjective

First Projection Ring Homomorphism Has Full Range

Informal description

The range of the first projection ring homomorphism $\operatorname{fst} \colon R \times S \to R$ is equal to the entire codomain $R$, i.e., $\text{range}(\operatorname{fst}) = R$.

Subsemiring.range_snd theorem

: (snd R S).rangeS = ⊤

Full source

@[simp]
theorem range_snd : (snd R S).rangeS = ⊤ :=
  (snd R S).rangeS_top_of_surjective <| Prod.snd_surjective

Second Projection Homomorphism Has Full Range

Informal description

The range of the second projection homomorphism $\operatorname{snd} \colon R \times S \to S$ is equal to the entire semiring $S$.

Subsemiring.prod_bot_sup_bot_prod theorem

(s : Subsemiring R) (t : Subsemiring S) : s.prod ⊥ ⊔ prod ⊥ t = s.prod t

Full source

@[simp]
theorem prod_bot_sup_bot_prod (s : Subsemiring R) (t : Subsemiring S) :
    s.prod ⊥ ⊔ prod ⊥ t = s.prod t :=
  le_antisymm (sup_le (prod_mono_right s bot_le) (prod_mono_left t bot_le)) fun p hp =>
    Prod.fst_mul_snd p ▸
      mul_mem
        ((le_sup_left : s.prod ⊥ ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨hp.1, SetLike.mem_coe.2 <| one_mem ⊥⟩)
        ((le_sup_right : prod ⊥ t ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨SetLike.mem_coe.2 <| one_mem ⊥, hp.2⟩)

Supremum of Product Subsemirings with Bottom Elements Equals Full Product Subsemiring

Informal description

For any subsemirings $s$ of a non-associative semiring $R$ and $t$ of a non-associative semiring $S$, the supremum of the product subsemiring $s \times \{\bot_S\}$ and $\{\bot_R\} \times t$ equals the product subsemiring $s \times t$, where $\bot_R$ and $\bot_S$ denote the bottom elements of the subsemiring lattices of $R$ and $S$ respectively.

RingEquiv.subsemiringCongr definition

(h : s = t) : s ≃+* t

Full source

/-- Makes the identity isomorphism from a proof two subsemirings of a multiplicative
    monoid are equal. -/
def subsemiringCongr (h : s = t) : s ≃+* t :=
  { Equiv.setCongr <| congr_arg _ h with
    map_mul' := fun _ _ => rfl
    map_add' := fun _ _ => rfl }

Identity isomorphism of equal subsemirings

Informal description

Given two subsemirings $ s $ and $ t $ of a semiring that are equal ($ s = t $), the equivalence $ s \simeq+* t $ is the identity isomorphism between them, preserving both the multiplicative and additive structures.

RingEquiv.ofLeftInverseS definition

{g : S → R} {f : R →+* S} (h : Function.LeftInverse g f) : R ≃+* f.rangeS

Full source

/-- Restrict a ring homomorphism with a left inverse to a ring isomorphism to its
`RingHom.rangeS`. -/
def ofLeftInverseS {g : S → R} {f : R →+* S} (h : Function.LeftInverse g f) : R ≃+* f.rangeS :=
  { f.rangeSRestrict with
    toFun := fun x => f.rangeSRestrict x
    invFun := fun x => (g ∘ f.rangeS.subtype) x
    left_inv := h
    right_inv := fun x =>
      Subtype.ext <| by
        let ⟨x', hx'⟩ := RingHom.mem_rangeS.mp x.prop
        simp [← hx', h x'] }

Ring isomorphism from a left inverse to the range subsemiring

Informal description

Given a ring homomorphism $f \colon R \to S$ and a left inverse $g \colon S \to R$ of $f$ (i.e., $g \circ f = \text{id}_R$), the function constructs a ring isomorphism between $R$ and the range subsemiring $f.\text{rangeS}$ of $S$. The isomorphism maps each $x \in R$ to $f(x) \in f.\text{rangeS}$, and its inverse maps each $y \in f.\text{rangeS}$ to $g(y) \in R$.

RingEquiv.ofLeftInverseS_apply theorem

{g : S → R} {f : R →+* S} (h : Function.LeftInverse g f) (x : R) : ↑(ofLeftInverseS h x) = f x

Full source

@[simp]
theorem ofLeftInverseS_apply {g : S → R} {f : R →+* S} (h : Function.LeftInverse g f) (x : R) :
    ↑(ofLeftInverseS h x) = f x :=
  rfl

Image of Element under Ring Isomorphism Induced by Left Inverse Equals Homomorphism Value

Informal description

Given a ring homomorphism $f \colon R \to S$ and a left inverse $g \colon S \to R$ of $f$ (i.e., $g \circ f = \text{id}_R$), for any $x \in R$, the image of $x$ under the ring isomorphism $\text{ofLeftInverseS}\ h$ (where $h$ is the proof that $g$ is a left inverse of $f$) is equal to $f(x)$ when viewed as an element of $S$. In other words, if $\varphi \colon R \simeq+* f.\text{rangeS}$ is the isomorphism constructed from $h$, then $\varphi(x) = f(x)$ for all $x \in R$.

RingEquiv.ofLeftInverseS_symm_apply theorem

{g : S → R} {f : R →+* S} (h : Function.LeftInverse g f) (x : f.rangeS) : (ofLeftInverseS h).symm x = g x

Full source

@[simp]
theorem ofLeftInverseS_symm_apply {g : S → R} {f : R →+* S} (h : Function.LeftInverse g f)
    (x : f.rangeS) : (ofLeftInverseS h).symm x = g x :=
  rfl

Inverse of Ring Isomorphism from Left Inverse Maps Range Elements via $g$

Informal description

Given a ring homomorphism $f \colon R \to S$ and a left inverse $g \colon S \to R$ of $f$ (i.e., $g \circ f = \text{id}_R$), for any element $x$ in the range subsemiring $f.\text{rangeS}$ of $S$, the inverse of the isomorphism $\text{ofLeftInverseS}\ h$ maps $x$ to $g(x)$.

RingEquiv.subsemiringMap definition

(e : R ≃+* S) (s : Subsemiring R) : s ≃+* s.map (e : R →+* S)

Full source

/-- Given an equivalence `e : R ≃+* S` of semirings and a subsemiring `s` of `R`,
`subsemiringMap e s` is the induced equivalence between `s` and `s.map e` -/
def subsemiringMap (e : R ≃+* S) (s : Subsemiring R) : s ≃+* s.map (e : R →+* S) :=
  { e.toAddEquiv.addSubmonoidMap s.toAddSubmonoid, e.toMulEquiv.submonoidMap s.toSubmonoid with }

Subsemiring equivalence induced by a semiring isomorphism

Informal description

Given a semiring equivalence (isomorphism) $e \colon R \simeq+* S$ and a subsemiring $s$ of $R$, the function `subsemiringMap e s` constructs an equivalence between the subsemiring $s$ and its image under $e$ in $S$. More precisely, this establishes an isomorphism $s \simeq+* e(s)$ where $e(s)$ is the subsemiring of $S$ consisting of all elements of the form $e(x)$ for $x \in s$.

RingEquiv.subsemiringMap_apply_coe theorem

(e : R ≃+* S) (s : Subsemiring R) (x : s) : ((subsemiringMap e s) x : S) = e x

Full source

@[simp]
theorem subsemiringMap_apply_coe (e : R ≃+* S) (s : Subsemiring R) (x : s) :
    ((subsemiringMap e s) x : S) = e x :=
  rfl

Commutativity of Subsemiring Map with Semiring Isomorphism

Informal description

Given a semiring isomorphism $e \colon R \simeq+* S$ and a subsemiring $s$ of $R$, for any element $x \in s$, the image of $x$ under the induced isomorphism $s \simeq+* e(s)$ (when viewed as an element of $S$) equals $e(x)$. In other words, the following diagram commutes: $$\begin{CD} s @>{\text{subsemiringMap } e}>> e(s) \\ @V{\text{inclusion}}VV @VV{\text{inclusion}}V \\ R @>{e}>> S \end{CD}$$ where the vertical arrows are the inclusion maps.

RingEquiv.subsemiringMap_symm_apply_coe theorem

(e : R ≃+* S) (s : Subsemiring R) (x : s.map e.toRingHom) : ((subsemiringMap e s).symm x : R) = e.symm x

Full source

@[simp]
theorem subsemiringMap_symm_apply_coe (e : R ≃+* S) (s : Subsemiring R) (x : s.map e.toRingHom) :
    ((subsemiringMap e s).symm x : R) = e.symm x :=
  rfl

Inverse Image under Restricted Ring Isomorphism Equals Global Inverse

Informal description

Let $e \colon R \simeq^{+*} S$ be a ring isomorphism between semirings $R$ and $S$, and let $s$ be a subsemiring of $R$. For any element $x$ in the image subsemiring $e(s) \subseteq S$, the inverse image under the restricted isomorphism $(e|_{s})^{-1}(x)$ (as an element of $R$) equals the inverse image $e^{-1}(x)$. In other words, for $x \in e(s)$, we have $(e|_{s})^{-1}(x) = e^{-1}(x)$ where $e|_{s} \colon s \simeq^{+*} e(s)$ is the isomorphism obtained by restricting $e$ to $s$.

Subsemiring.smul instance

[SMul R' α] (S : Subsemiring R') : SMul S α

Full source

/-- The action by a subsemiring is the action by the underlying semiring. -/
instance smul [SMul R' α] (S : Subsemiring R') : SMul S α :=
  inferInstance

Scalar Multiplication Action Inherited by Subsemiring

Informal description

For any subsemiring $S$ of a semiring $R'$ with a scalar multiplication action on a type $\alpha$, the subsemiring $S$ inherits a scalar multiplication action on $\alpha$ defined by $s \bullet a = (s : R') \bullet a$ for $s \in S$ and $a \in \alpha$.

Subsemiring.smul_def theorem

[SMul R' α] {S : Subsemiring R'} (g : S) (m : α) : g • m = (g : R') • m

Full source

theorem smul_def [SMul R' α] {S : Subsemiring R'} (g : S) (m : α) : g • m = (g : R') • m :=
  rfl

Subsemiring Scalar Multiplication Definition

Informal description

For any subsemiring $S$ of a semiring $R'$ with a scalar multiplication action on a type $\alpha$, the scalar multiplication of an element $g \in S$ on an element $m \in \alpha$ is equal to the scalar multiplication of $g$ (viewed as an element of $R'$) on $m$, i.e., $g \bullet m = (g : R') \bullet m$.

Subsemiring.smulCommClass_left instance

[SMul R' β] [SMul α β] [SMulCommClass R' α β] (S : Subsemiring R') : SMulCommClass S α β

Full source

instance smulCommClass_left [SMul R' β] [SMul α β] [SMulCommClass R' α β] (S : Subsemiring R') :
    SMulCommClass S α β :=
  inferInstance

Commutativity of Scalar Multiplication between Subsemiring and Another Action

Informal description

For any subsemiring $S$ of a semiring $R'$ with scalar multiplication actions on a type $\beta$, and given a scalar multiplication action of $\alpha$ on $\beta$ that commutes with the action of $R'$ (i.e., $r \bullet (a \bullet b) = a \bullet (r \bullet b)$ for all $r \in R'$, $a \in \alpha$, $b \in \beta$), the scalar multiplication actions of $S$ and $\alpha$ on $\beta$ also commute. That is, for any $s \in S$, $a \in \alpha$, and $b \in \beta$, we have $s \bullet (a \bullet b) = a \bullet (s \bullet b)$.

Subsemiring.smulCommClass_right instance

[SMul α β] [SMul R' β] [SMulCommClass α R' β] (S : Subsemiring R') : SMulCommClass α S β

Full source

instance smulCommClass_right [SMul α β] [SMul R' β] [SMulCommClass α R' β] (S : Subsemiring R') :
    SMulCommClass α S β :=
  inferInstance

Commutativity of Scalar Multiplication between $\alpha$ and a Subsemiring of $R'$ on $\beta$

Informal description

For any type $\beta$ with scalar multiplication actions by $\alpha$ and a semiring $R'$, if these actions commute (i.e., $a \bullet (r \bullet b) = r \bullet (a \bullet b)$ for all $a \in \alpha$, $r \in R'$, $b \in \beta$), then for any subsemiring $S$ of $R'$, the actions of $\alpha$ and $S$ on $\beta$ also commute. That is, $a \bullet (s \bullet b) = s \bullet (a \bullet b)$ for all $a \in \alpha$, $s \in S$, $b \in \beta$.

Subsemiring.isScalarTower instance

[SMul α β] [SMul R' α] [SMul R' β] [IsScalarTower R' α β] (S : Subsemiring R') : IsScalarTower S α β

Full source

/-- Note that this provides `IsScalarTower S R R` which is needed by `smul_mul_assoc`. -/
instance isScalarTower [SMul α β] [SMul R' α] [SMul R' β] [IsScalarTower R' α β]
    (S : Subsemiring R') :
    IsScalarTower S α β :=
  inferInstance

Scalar Tower Property for Subsemiring Actions

Informal description

For any subsemiring $S$ of a semiring $R'$ with scalar multiplication actions on types $\alpha$ and $\beta$, if the actions of $R'$ on $\alpha$ and $\beta$ form a scalar tower (i.e., $(r \cdot a) \cdot b = r \cdot (a \cdot b)$ for all $r \in R'$, $a \in \alpha$, $b \in \beta$), then the actions of $S$ on $\alpha$ and $\beta$ also form a scalar tower. That is, for any $s \in S$, $a \in \alpha$, and $b \in \beta$, we have $(s \cdot a) \cdot b = s \cdot (a \cdot b)$.

Subsemiring.instFaithfulSMulSubtypeMem instance

{M' α : Type*} [SMul M' α] {S' : Type*} [SetLike S' M'] (s : S') [FaithfulSMul M' α] : FaithfulSMul s α

Full source

instance (priority := low) {M' α : Type*} [SMul M' α] {S' : Type*}
    [SetLike S' M'] (s : S') [FaithfulSMul M' α] : FaithfulSMul s α :=
  ⟨fun h => Subtype.ext <| eq_of_smul_eq_smul h⟩

Faithfulness of Scalar Multiplication Inherited by Subsemirings

Informal description

For any type $M'$ with a scalar multiplication action on a type $\alpha$, and any set-like structure $S'$ over $M'$, if the scalar multiplication action of $M'$ on $\alpha$ is faithful, then the induced scalar multiplication action of any subset $s$ of $S'$ on $\alpha$ is also faithful.

Subsemiring.faithfulSMul instance

[SMul R' α] [FaithfulSMul R' α] (S : Subsemiring R') : FaithfulSMul S α

Full source

instance faithfulSMul [SMul R' α] [FaithfulSMul R' α] (S : Subsemiring R') : FaithfulSMul S α :=
  inferInstance

Faithfulness of Scalar Multiplication Inherited by Subsemirings

Informal description

For any subsemiring $S$ of a semiring $R'$ with a faithful scalar multiplication action on a type $\alpha$, the induced scalar multiplication action of $S$ on $\alpha$ is also faithful. That is, if distinct elements of $R'$ act differently on $\alpha$, then distinct elements of $S$ also act differently on $\alpha$.

Subsemiring.instSMulWithZeroSubtypeMem instance

{S' : Type*} [SetLike S' R'] [SubsemiringClass S' R'] (s : S') [Zero α] [SMulWithZero R' α] : SMulWithZero s α

Full source

instance (priority := low) {S' : Type*} [SetLike S' R'] [SubsemiringClass S' R'] (s : S')
    [Zero α] [SMulWithZero R' α] : SMulWithZero s α where
  smul_zero r := smul_zero (r : R')
  zero_smul := zero_smul R'

Subsemiring Inherits Scalar Multiplication with Zero

Informal description

For any set-like structure $S'$ of a non-associative semiring $R'$ (where $S'$ is a subsemiring class), and any type $\alpha$ with a zero element and a scalar multiplication action by $R'$ that respects zero (i.e., $r \cdot a = 0$ if either $r = 0$ or $a = 0$), the subsemiring $s : S'$ inherits a scalar multiplication action on $\alpha$ that also respects zero.

Subsemiring.instSMulWithZeroSubtypeMem_1 instance

[Zero α] [SMulWithZero R' α] (S : Subsemiring R') : SMulWithZero S α

Full source

/-- The action by a subsemiring is the action by the underlying semiring. -/
instance [Zero α] [SMulWithZero R' α] (S : Subsemiring R') : SMulWithZero S α :=
  inferInstance

Subsemiring Inherits Scalar Multiplication with Zero

Informal description

For any subsemiring $S$ of a non-associative semiring $R'$, and any type $\alpha$ with a zero element and a scalar multiplication action by $R'$ that respects zero (i.e., $r \cdot a = 0$ if either $r = 0$ or $a = 0$), the subsemiring $S$ inherits a scalar multiplication action on $\alpha$ that also respects zero.

Subsemiring.mulAction instance

[MulAction R' α] (S : Subsemiring R') : MulAction S α

Full source

/-- The action by a subsemiring is the action by the underlying semiring. -/
instance mulAction [MulAction R' α] (S : Subsemiring R') : MulAction S α :=
  inferInstance

Restriction of Multiplicative Action to Subsemirings

Informal description

For any semiring $R'$ with a multiplicative action on a type $\alpha$, and any subsemiring $S$ of $R'$, the multiplicative action of $R'$ on $\alpha$ restricts to a multiplicative action of $S$ on $\alpha$.

Subsemiring.distribMulAction instance

[AddMonoid α] [DistribMulAction R' α] (S : Subsemiring R') : DistribMulAction S α

Full source

/-- The action by a subsemiring is the action by the underlying semiring. -/
instance distribMulAction [AddMonoid α] [DistribMulAction R' α] (S : Subsemiring R') :
    DistribMulAction S α :=
  inferInstance

Distributive Action Inherited by Subsemirings

Informal description

For any additive monoid $\alpha$ equipped with a distributive multiplicative action by a semiring $R'$, and any subsemiring $S$ of $R'$, the action of $S$ on $\alpha$ is also distributive. That is, for all $s \in S$ and $a, b \in \alpha$, we have $s \cdot (a + b) = s \cdot a + s \cdot b$ and $s \cdot 0 = 0$.

Subsemiring.instModuleSubtypeMem instance

[AddCommMonoid α] [Module R' α] {S' : Type*} [SetLike S' R'] [SubsemiringClass S' R'] (s : S') : Module s α

Full source

instance (priority := low) [AddCommMonoid α] [Module R' α] {S' : Type*} [SetLike S' R']
    [SubsemiringClass S' R'] (s : S') : Module s α where
  add_smul r₁ r₂ := add_smul (r₁ : R') r₂
  zero_smul := zero_smul R'

Module Structure Inherited by Subsemirings

Informal description

For any additive commutative monoid $\alpha$ equipped with a module structure over a semiring $R'$, and any subsemiring $s$ of $R'$, $\alpha$ inherits a module structure over $s$.

Subsemiring.mulDistribMulAction instance

[Monoid α] [MulDistribMulAction R' α] (S : Subsemiring R') : MulDistribMulAction S α

Full source

/-- The action by a subsemiring is the action by the underlying semiring. -/
instance mulDistribMulAction [Monoid α] [MulDistribMulAction R' α] (S : Subsemiring R') :
    MulDistribMulAction S α :=
  inferInstance

Subsemirings Inherit Multiplicative Distributive Actions

Informal description

For any monoid $\alpha$ and any semiring $R'$ with a multiplicative distributive action on $\alpha$, a subsemiring $S$ of $R'$ inherits a multiplicative distributive action on $\alpha$. This means that the action of $S$ on $\alpha$ preserves multiplication and scalar multiplication, satisfying the distributive laws $(a \cdot b) \cdot s = (a \cdot s) \cdot (b \cdot s)$ for all $a, b \in \alpha$ and $s \in S$.

Subsemiring.instMulActionWithZeroSubtypeMem instance

 {S' : Type*} [SetLike S' R'] [SubsemiringClass S' R'] (s : S') [Zero α] [MulActionWithZero R' α] :
  MulActionWithZero s α

Full source

instance (priority := low) {S' : Type*} [SetLike S' R'] [SubsemiringClass S' R'] (s : S')
    [Zero α] [MulActionWithZero R' α] : MulActionWithZero s α where
  smul_zero r := smul_zero (r : R')
  zero_smul := zero_smul R'

Subsemirings Inherit Multiplicative Actions with Zero

Informal description

For any subsemiring $s$ of a semiring $R'$, and any type $\alpha$ with a zero element and a multiplicative action with zero by $R'$, the subsemiring $s$ inherits a multiplicative action with zero on $\alpha$.

Subsemiring.mulActionWithZero instance

[Zero α] [MulActionWithZero R' α] (S : Subsemiring R') : MulActionWithZero S α

Full source

/-- The action by a subsemiring is the action by the underlying semiring. -/
instance mulActionWithZero [Zero α] [MulActionWithZero R' α] (S : Subsemiring R') :
    MulActionWithZero S α :=
  inferInstance

Subsemirings Inherit Multiplicative Actions with Zero

Informal description

For any subsemiring $S$ of a semiring $R'$, and any type $\alpha$ with a zero element and a multiplicative action with zero by $R'$, the subsemiring $S$ inherits a multiplicative action with zero on $\alpha$. This means that the action of $S$ on $\alpha$ preserves the zero element and satisfies the properties of a multiplicative action with zero.

Subsemiring.instModuleSubtypeMem_1 instance

[AddCommMonoid α] [Module R' α] {S' : Type*} [SetLike S' R'] [SubsemiringClass S' R'] (s : S') : Module s α

Full source

instance (priority := low) [AddCommMonoid α] [Module R' α] {S' : Type*} [SetLike S' R']
    [SubsemiringClass S' R'] (s : S') : Module s α where
  toDistribMulAction := inferInstance
  add_smul r₁ r₂ := add_smul (r₁ : R') r₂
  zero_smul := zero_smul R'

Module Structure on Subsemirings

Informal description

For any additive commutative monoid $\alpha$ equipped with a module structure over a semiring $R'$, and any subsemiring $s$ of $R'$ (where $S'$ is a set-like structure representing subsemirings of $R'$), $\alpha$ inherits a module structure over $s$.

Subsemiring.module instance

[AddCommMonoid α] [Module R' α] (S : Subsemiring R') : Module S α

Full source

/-- The action by a subsemiring is the action by the underlying semiring. -/
instance module [AddCommMonoid α] [Module R' α] (S : Subsemiring R') : Module S α :=
  inferInstance

Module Structure Induced by a Subsemiring

Informal description

For any additive commutative monoid $\alpha$ equipped with a module structure over a semiring $R'$, and any subsemiring $S$ of $R'$, $\alpha$ inherits a module structure over $S$ where the scalar multiplication is given by the restriction of the original scalar multiplication to $S$.

Subsemiring.instMulSemiringActionSubtypeMem instance

[Semiring α] [MulSemiringAction R' α] (S : Subsemiring R') : MulSemiringAction S α

Full source

/-- The action by a subsemiring is the action by the underlying semiring. -/
instance [Semiring α] [MulSemiringAction R' α] (S : Subsemiring R') : MulSemiringAction S α :=
  inferInstance

Subsemirings Inherit Multiplicative Semiring Actions

Informal description

For any semiring $\alpha$ and any monoid $R'$ acting multiplicatively and distributively on $\alpha$ (i.e., a `MulSemiringAction`), every subsemiring $S$ of $R'$ inherits a `MulSemiringAction` structure on $\alpha$. This means the action of $S$ on $\alpha$ preserves both the additive and multiplicative structures of $\alpha$.

Subsemiring.center.smulCommClass_left instance

: SMulCommClass (center R') R' R'

Full source

/-- The center of a semiring acts commutatively on that semiring. -/
instance center.smulCommClass_left : SMulCommClass (center R') R' R' :=
  Submonoid.center.smulCommClass_left

Commutative Action of the Center on a Semiring

Informal description

For any semiring $R'$, the center of $R'$ acts commutatively on $R'$ itself. That is, for any element $z$ in the center of $R'$ and any element $r \in R'$, we have $z \cdot r = r \cdot z$.

Subsemiring.center.smulCommClass_right instance

: SMulCommClass R' (center R') R'

Full source

/-- The center of a semiring acts commutatively on that semiring. -/
instance center.smulCommClass_right : SMulCommClass R' (center R') R' :=
  Submonoid.center.smulCommClass_right

Commutativity of Scalar Multiplication with Central Elements

Informal description

For any semiring $R'$, the scalar multiplication action of $R'$ on itself commutes with the action of its center. That is, for any $r \in R'$ and any $z$ in the center of $R'$, we have $r \cdot z = z \cdot r$.

Subsemiring.closure_le_centralizer_centralizer theorem

(s : Set R') : closure s ≤ centralizer (centralizer s)

Full source

lemma closure_le_centralizer_centralizer (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 semiring $R'$, the subsemiring generated by $s$ is contained in the centralizer of the centralizer of $s$. In other words: $$\text{closure}(s) \subseteq \text{centralizer}(\text{centralizer}(s)).$$

Subsemiring.closureCommSemiringOfComm abbrev

{s : Set R'} (hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x) : CommSemiring (closure s)

Full source

/-- If all the elements of a set `s` commute, then `closure s` is a commutative semiring. -/
abbrev closureCommSemiringOfComm {s : Set R'} (hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x) :
    CommSemiring (closure s) :=
  { (closure s).toSemiring 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₂) }

Commutativity of Subsemiring Closure for Commuting Elements

Informal description

Let $R'$ be a semiring and $s$ a subset of $R'$. If all elements of $s$ commute with each other (i.e., $x \cdot y = y \cdot x$ for all $x, y \in s$), then the subsemiring generated by $s$ is a commutative semiring.

Subsemiring.map_comap_eq theorem

(f : R →+* S) (t : Subsemiring S) : (t.comap f).map f = t ⊓ f.rangeS

Full source

theorem map_comap_eq (f : R →+* S) (t : Subsemiring S) : (t.comap f).map f = t ⊓ f.rangeS :=
  SetLike.coe_injective Set.image_preimage_eq_inter_range

Image-Preimage Equality for Ring Homomorphisms and Subsemirings: $f(f^{-1}(t)) = t \cap \mathrm{range}(f)$

Informal description

Let $f \colon R \to S$ be a ring homomorphism and let $t$ be a subsemiring of $S$. Then the image under $f$ of the preimage of $t$ under $f$ is equal to the intersection of $t$ with the range of $f$, i.e., $$ f(f^{-1}(t)) = t \cap \mathrm{range}(f). $$

Subsemiring.map_comap_eq_self theorem

{f : R →+* S} {t : Subsemiring S} (h : t ≤ f.rangeS) : (t.comap f).map f = t

Full source

theorem map_comap_eq_self
    {f : R →+* S} {t : Subsemiring S} (h : t ≤ f.rangeS) : (t.comap f).map f = t := by
  simpa only [inf_of_le_left h] using map_comap_eq f t

Image-Preimage Identity for Subsemirings in Range: $f(f^{-1}(t)) = t$ when $t \subseteq \mathrm{range}(f)$

Informal description

Let $f \colon R \to S$ be a ring homomorphism between non-associative semirings, and let $t$ be a subsemiring of $S$ that is contained in the range of $f$. Then the image under $f$ of the preimage of $t$ equals $t$ itself, i.e., $$ f(f^{-1}(t)) = t. $$

Subsemiring.map_comap_eq_self_of_surjective theorem

{f : R →+* S} (hf : Function.Surjective f) (t : Subsemiring S) : (t.comap f).map f = t

Full source

theorem map_comap_eq_self_of_surjective
    {f : R →+* S} (hf : Function.Surjective f) (t : Subsemiring S) : (t.comap f).map f = t :=
  map_comap_eq_self <| by simp [hf]

Image-Preimage Identity for Subsemirings under Surjective Ring Homomorphisms

Informal description

Let $f \colon R \to S$ be a surjective ring homomorphism between non-associative semirings, and let $t$ be a subsemiring of $S$. Then the image under $f$ of the preimage of $t$ equals $t$ itself, i.e., $$ f(f^{-1}(t)) = t. $$

Subsemiring.comap_map_eq_self_of_injective theorem

{f : R →+* S} (hf : Function.Injective f) (s : Subsemiring R) : (s.map f).comap f = s

Full source

theorem comap_map_eq_self_of_injective
    {f : R →+* S} (hf : Function.Injective f) (s : Subsemiring R) : (s.map f).comap f = s :=
  SetLike.coe_injective (Set.preimage_image_eq _ hf)

Preimage of Image Equals Original Subsemiring for Injective Ring Homomorphisms

Informal description

Let $f \colon R \to S$ be an injective ring homomorphism between non-associative semirings, and let $s$ be a subsemiring of $R$. Then the preimage of the image of $s$ under $f$ equals $s$ itself, i.e., $f^{-1}(f(s)) = s$.