Mathlib.Data.Set.Semiring

SetSemiring definition

(α : Type*) : Type _

Full source

/-- An alias for `Set α`, which has a semiring structure given by `∪` as "addition" and pointwise
  multiplication `*` as "multiplication". -/
def SetSemiring (α : Type*) : Type _ :=
  Set α

Semiring of sets under union and pointwise multiplication

Informal description

The type `SetSemiring α` is defined as an alias for the type of subsets of `α` (i.e., `Set α`), endowed with a semiring structure where the addition operation is given by set union `∪` and the multiplication operation is given by pointwise multiplication `*` of sets. When `α` is a (commutative) monoid, `SetSemiring α` forms a (commutative) semiring under these operations.

instInhabitedSetSemiring instance

(α : Type*) : Inhabited (SetSemiring α)

Full source

noncomputable instance (α : Type*) : Inhabited (SetSemiring α) :=
  inferInstanceAs <| Inhabited (Set _)

Inhabitedness of the Semiring of Sets

Informal description

For any type $\alpha$, the semiring of sets $\text{SetSemiring}\,\alpha$ is inhabited (i.e., contains at least one element).

instPartialOrderSetSemiring instance

(α : Type*) : PartialOrder (SetSemiring α)

Full source

instance (α : Type*) : PartialOrder (SetSemiring α) :=
  inferInstanceAs <| PartialOrder (Set _)

Partial Order on the Semiring of Sets

Informal description

For any type $\alpha$, the semiring of sets $\text{SetSemiring}\,\alpha$ is equipped with a partial order structure inherited from the inclusion order on subsets of $\alpha$.

instOrderBotSetSemiring instance

(α : Type*) : OrderBot (SetSemiring α)

Full source

instance (α : Type*) : OrderBot (SetSemiring α) :=
  inferInstanceAs <| OrderBot (Set _)

Bottom Element in the Semiring of Sets

Informal description

For any type $\alpha$, the semiring of sets $\text{SetSemiring}\,\alpha$ has a bottom element $\emptyset$ with respect to the inclusion order.

Set.up definition

: Set α ≃ SetSemiring α

Full source

/-- The identity function `Set α → SetSemiring α`. -/
protected def Set.up : SetSet α ≃ SetSemiring α :=
  Equiv.refl _

Embedding of sets into the semiring of sets

Informal description

The identity function that maps a subset $S$ of $\alpha$ (i.e., an element of $\text{Set}\,\alpha$) to itself in $\text{SetSemiring}\,\alpha$, establishing an equivalence between these two types.

SetSemiring.down definition

: SetSemiring α ≃ Set α

Full source

/-- The identity function `SetSemiring α → Set α`. -/
protected def down : SetSemiringSetSemiring α ≃ Set α :=
  Equiv.refl _

Projection from semiring of sets to sets

Informal description

The function maps an element of the semiring of sets $\text{SetSemiring}\,\alpha$ back to its underlying subset of $\alpha$ (i.e., an element of $\text{Set}\,\alpha$). This is the inverse of the embedding $\text{Set.up}$ and forms an equivalence between $\text{SetSemiring}\,\alpha$ and $\text{Set}\,\alpha$.

SetSemiring.down_up theorem

(s : Set α) : s.up.down = s

Full source

@[simp]
protected theorem down_up (s : Set α) : s.up.down = s :=
  rfl

Projection after embedding returns original set: $\text{down}(\text{up}(s)) = s$

Informal description

For any subset $s$ of a type $\alpha$, the composition of the embedding `Set.up` followed by the projection `SetSemiring.down` returns the original subset, i.e., $\text{down}(\text{up}(s)) = s$.

SetSemiring.up_down theorem

(s : SetSemiring α) : s.down.up = s

Full source

@[simp]
protected theorem up_down (s : SetSemiring α) : s.down.up = s :=
  rfl

Embedding-Projection Identity for Semiring of Sets

Informal description

For any element $s$ of the semiring of sets $\text{SetSemiring}\,\alpha$, the embedding of its underlying subset $s.\text{down}$ back into $\text{SetSemiring}\,\alpha$ equals $s$ itself, i.e., $s.\text{down}.\text{up} = s$.

SetSemiring.up_le_up theorem

{s t : Set α} : s.up ≤ t.up ↔ s ⊆ t

Full source

theorem up_le_up {s t : Set α} : s.up ≤ t.up ↔ s ⊆ t :=
  Iff.rfl

Order Embedding of Sets into Semiring of Sets via Subset Relation

Informal description

For any two subsets $s$ and $t$ of a type $\alpha$, the inequality $s^{\text{up}} \leq t^{\text{up}}$ holds in the semiring of sets $\text{SetSemiring}\,\alpha$ if and only if $s$ is a subset of $t$ in the usual set inclusion sense, i.e., $s \subseteq t$.

SetSemiring.up_lt_up theorem

{s t : Set α} : s.up < t.up ↔ s ⊂ t

Full source

theorem up_lt_up {s t : Set α} : s.up < t.up ↔ s ⊂ t :=
  Iff.rfl

Proper Subset Order in Semiring of Sets: $s.\text{up} < t.\text{up} \leftrightarrow s \subset t$

Informal description

For any subsets $s$ and $t$ of a type $\alpha$, the inequality $s.\text{up} < t.\text{up}$ holds in the semiring of sets $\text{SetSemiring}\,\alpha$ if and only if $s$ is a proper subset of $t$, i.e., $s \subset t$.

SetSemiring.down_subset_down theorem

{s t : SetSemiring α} : s.down ⊆ t.down ↔ s ≤ t

Full source

@[simp]
theorem down_subset_down {s t : SetSemiring α} : s.down ⊆ t.downs.down ⊆ t.down ↔ s ≤ t :=
  Iff.rfl

Subset Order Correspondence in Semiring of Sets

Informal description

For any two elements $s$ and $t$ in the semiring of sets $\text{SetSemiring}\,\alpha$, the underlying subset of $s$ is contained in the underlying subset of $t$ if and only if $s$ is less than or equal to $t$ in the partial order on $\text{SetSemiring}\,\alpha$. In other words, $s.\text{down} \subseteq t.\text{down} \leftrightarrow s \leq t$.

SetSemiring.down_ssubset_down theorem

{s t : SetSemiring α} : s.down ⊂ t.down ↔ s < t

Full source

@[simp]
theorem down_ssubset_down {s t : SetSemiring α} : s.down ⊂ t.downs.down ⊂ t.down ↔ s < t :=
  Iff.rfl

Strict Subset Correspondence in Semiring of Sets

Informal description

For any two elements $s$ and $t$ in the semiring of sets $\text{SetSemiring}\,\alpha$, the projection $\text{down}(s)$ is a strict subset of $\text{down}(t)$ if and only if $s$ is strictly less than $t$ in the partial order on $\text{SetSemiring}\,\alpha$.

SetSemiring.instZero instance

: Zero (SetSemiring α)

Full source

instance : Zero (SetSemiring α) where zero := (∅ : Set α).up

Zero Element in the Semiring of Sets

Informal description

The semiring of sets $\text{SetSemiring}\,\alpha$ has a zero element given by the empty set $\emptyset$.

SetSemiring.instAdd instance

: Add (SetSemiring α)

Full source

instance : Add (SetSemiring α) where add s t := (s.down ∪ t.down).up

Addition Operation on the Semiring of Sets

Informal description

The type `SetSemiring α` is equipped with an addition operation given by set union `∪`.

SetSemiring.instAddCommMonoid instance

: AddCommMonoid (SetSemiring α)

Full source

instance : AddCommMonoid (SetSemiring α) where
  add_assoc := union_assoc
  zero_add := empty_union
  add_zero := union_empty
  add_comm := union_comm
  nsmul := nsmulRec

Commutative Additive Monoid Structure on the Semiring of Sets

Informal description

The semiring of sets $\text{SetSemiring}\,\alpha$ forms a commutative additive monoid under set union $\cup$ with the empty set $\emptyset$ as the zero element.

SetSemiring.zero_def theorem

: (0 : SetSemiring α) = Set.up ∅

Full source

theorem zero_def : (0 : SetSemiring α) = Set.up ∅ :=
  rfl

Zero in Semiring of Sets is Embedding of Empty Set

Informal description

The zero element in the semiring of sets $\text{SetSemiring}\,\alpha$ is equal to the embedding of the empty set $\emptyset$ via the map $\text{Set.up}$, i.e., $0 = \text{Set.up}(\emptyset)$.

SetSemiring.down_zero theorem

: (0 : SetSemiring α).down = ∅

Full source

@[simp]
theorem down_zero : (0 : SetSemiring α).down = ∅ :=
  rfl

Projection of Zero in Semiring of Sets Yields Empty Set

Informal description

The projection of the zero element in the semiring of sets $\text{SetSemiring}\,\alpha$ is the empty set, i.e., $(0 : \text{SetSemiring}\,\alpha).\text{down} = \emptyset$.

Set.up_empty theorem

: (∅ : Set α).up = 0

Full source

@[simp]
theorem _root_.Set.up_empty : (∅ : Set α).up = 0 :=
  rfl

Embedding of Empty Set as Zero in Semiring of Sets

Informal description

The embedding of the empty set $\emptyset$ in $\text{Set}\,\alpha$ into the semiring of sets $\text{SetSemiring}\,\alpha$ is equal to the zero element of the semiring, i.e., $(\emptyset : \text{Set}\,\alpha).\text{up} = 0$.

SetSemiring.add_def theorem

(s t : SetSemiring α) : s + t = (s.down ∪ t.down).up

Full source

theorem add_def (s t : SetSemiring α) : s + t = (s.down ∪ t.down).up :=
  rfl

Addition in the Semiring of Sets as Union of Underlying Sets

Informal description

For any two elements $s$ and $t$ in the semiring of sets $\text{SetSemiring}\,\alpha$, their addition $s + t$ is equal to the embedding of the union of their underlying sets, i.e., $(s \cup t).\text{up}$.

SetSemiring.down_add theorem

(s t : SetSemiring α) : (s + t).down = s.down ∪ t.down

Full source

@[simp]
theorem down_add (s t : SetSemiring α) : (s + t).down = s.down ∪ t.down :=
  rfl

Underlying Set of Sum in Semiring of Sets Equals Union of Underlying Sets

Informal description

For any two elements $s$ and $t$ in the semiring of sets $\text{SetSemiring}\,\alpha$, the underlying set of their sum $s + t$ is equal to the union of their underlying sets, i.e., $(s + t).\text{down} = s.\text{down} \cup t.\text{down}$.

Set.up_union theorem

(s t : Set α) : (s ∪ t).up = s.up + t.up

Full source

@[simp]
theorem _root_.Set.up_union (s t : Set α) : (s ∪ t).up = s.up + t.up :=
  rfl

Embedding Preserves Union in Semiring of Sets

Informal description

For any two subsets $s$ and $t$ of a type $\alpha$, the embedding of their union into the semiring of sets equals the sum of their individual embeddings, i.e., $(s \cup t).\text{up} = s.\text{up} + t.\text{up}$.

SetSemiring.addLeftMono instance

: AddLeftMono (SetSemiring α)

Full source

instance addLeftMono : AddLeftMono (SetSemiring α) :=
  ⟨fun _ _ _ => union_subset_union_right _⟩

Left Monotonicity of Addition in the Semiring of Sets

Informal description

The addition operation on the semiring of sets $\text{SetSemiring}\,\alpha$ is left-monotonic. That is, for any sets $s, t, u \in \text{SetSemiring}\,\alpha$, if $s \subseteq t$, then $s + u \subseteq t + u$, where $+$ denotes the union operation.

SetSemiring.instNonUnitalNonAssocSemiring instance

: NonUnitalNonAssocSemiring (SetSemiring α)

Full source

instance : NonUnitalNonAssocSemiring (SetSemiring α) :=
  { (inferInstance : AddCommMonoid (SetSemiring α)) with
    mul := fun s t => (image2 (· * ·) s.down t.down).up
    zero_mul := fun _ => empty_mul
    mul_zero := fun _ => mul_empty
    left_distrib := fun _ _ _ => mul_union
    right_distrib := fun _ _ _ => union_mul }

Non-Unital Non-Associative Semiring Structure on Sets under Union and Pointwise Multiplication

Informal description

The semiring of sets $\text{SetSemiring}\,\alpha$ forms a non-unital non-associative semiring under the operations of set union (as addition) and pointwise multiplication (as multiplication).

SetSemiring.mul_def theorem

(s t : SetSemiring α) : s * t = (s.down * t.down).up

Full source

theorem mul_def (s t : SetSemiring α) : s * t = (s.down * t.down).up :=
  rfl

Definition of Multiplication in the Semiring of Sets via Pointwise Product

Informal description

For any two elements $s$ and $t$ in the semiring of sets $\text{SetSemiring}\,\alpha$, their product $s * t$ is equal to the image under the embedding $\text{Set.up}$ of the pointwise product of their underlying sets $s.\text{down}$ and $t.\text{down}$. In other words, $s * t = \text{Set.up}(s.\text{down} * t.\text{down})$.

SetSemiring.down_mul theorem

(s t : SetSemiring α) : (s * t).down = s.down * t.down

Full source

@[simp]
theorem down_mul (s t : SetSemiring α) : (s * t).down = s.down * t.down :=
  rfl

Compatibility of Multiplication with Underlying Sets in Semiring of Sets

Informal description

For any two elements $s$ and $t$ in the semiring of sets $\text{SetSemiring}\,\alpha$, the underlying set of their product $s * t$ is equal to the pointwise product of their underlying sets, i.e., $(s * t).\text{down} = s.\text{down} * t.\text{down}$.

Set.up_mul theorem

(s t : Set α) : (s * t).up = s.up * t.up

Full source

@[simp]
theorem _root_.Set.up_mul (s t : Set α) : (s * t).up = s.up * t.up :=
  rfl

Embedding Preserves Pointwise Product of Sets

Informal description

For any subsets $s$ and $t$ of a type $\alpha$, the embedding of their pointwise product into the semiring of sets equals the product of their embeddings, i.e., $(s * t)^\uparrow = s^\uparrow * t^\uparrow$ where $^\uparrow$ denotes the embedding map from $\text{Set}\,\alpha$ to $\text{SetSemiring}\,\alpha$.

SetSemiring.instNoZeroDivisors instance

: NoZeroDivisors (SetSemiring α)

Full source

instance : NoZeroDivisors (SetSemiring α) :=
  ⟨fun {a b} ab =>
    a.eq_empty_or_nonempty.imp_right fun ha =>
      b.eq_empty_or_nonempty.resolve_right fun hb =>
        Nonempty.ne_empty ⟨_, mul_mem_mul ha.some_mem hb.some_mem⟩ ab⟩

No Zero Divisors in the Semiring of Sets

Informal description

The semiring of sets $\text{SetSemiring}\,\alpha$ has no zero divisors. That is, for any two subsets $s$ and $t$ of $\alpha$, if their product $s * t$ is the empty set, then either $s$ or $t$ must be the empty set.

SetSemiring.mulLeftMono instance

: MulLeftMono (SetSemiring α)

Full source

instance mulLeftMono : MulLeftMono (SetSemiring α) :=
  ⟨fun _ _ _ => mul_subset_mul_left⟩

Left-Multiplicative Monotonicity in the Semiring of Sets

Informal description

For any type $\alpha$, the semiring of sets $\text{SetSemiring}\,\alpha$ is left-multiplicative monotone. That is, for any subsets $s, t, u$ of $\alpha$, if $s \subseteq t$, then $u * s \subseteq u * t$ under pointwise multiplication.

SetSemiring.mulRightMono instance

: MulRightMono (SetSemiring α)

Full source

instance mulRightMono : MulRightMono (SetSemiring α) :=
  ⟨fun _ _ _ => mul_subset_mul_right⟩

Right Multiplication is Monotone in the Semiring of Sets

Informal description

For any type $\alpha$, the semiring of sets $\text{SetSemiring}\,\alpha$ satisfies the property of right multiplication being monotone with respect to the inclusion order. That is, for any sets $A, B, C \subseteq \alpha$, if $A \subseteq B$, then $A * C \subseteq B * C$.

SetSemiring.instOne instance

: One (SetSemiring α)

Full source

instance : One (SetSemiring α) where one := (1 : Set α).up

Multiplicative Identity in the Semiring of Sets

Informal description

The semiring of sets $\text{SetSemiring}\,\alpha$ has a multiplicative identity element, which is the image of the singleton set containing the multiplicative identity of $\alpha$ under the canonical embedding $\text{Set.up}$.

SetSemiring.one_def theorem

: (1 : SetSemiring α) = Set.up 1

Full source

theorem one_def : (1 : SetSemiring α) = Set.up 1 :=
  rfl

Multiplicative Identity in Semiring of Sets via Canonical Embedding

Informal description

The multiplicative identity element in the semiring of sets $\text{SetSemiring}\,\alpha$ is equal to the image of the singleton set containing the multiplicative identity of $\alpha$ under the canonical embedding $\text{Set.up}$.

SetSemiring.down_one theorem

: (1 : SetSemiring α).down = 1

Full source

@[simp]
theorem down_one : (1 : SetSemiring α).down = 1 :=
  rfl

Projection of Multiplicative Identity in Semiring of Sets

Informal description

The projection of the multiplicative identity element in the semiring of sets $\text{SetSemiring}\,\alpha$ to its underlying subset is equal to the multiplicative identity of $\alpha$, i.e., $(1 : \text{SetSemiring}\,\alpha).\text{down} = 1$.

Set.up_one theorem

: (1 : Set α).up = 1

Full source

@[simp]
theorem _root_.Set.up_one : (1 : Set α).up = 1 :=
  rfl

Embedding Preserves Multiplicative Identity in Semiring of Sets

Informal description

The canonical embedding $\text{Set.up}$ maps the multiplicative identity $1$ in $\text{Set}\,\alpha$ to the multiplicative identity $1$ in $\text{SetSemiring}\,\alpha$.

SetSemiring.instNonAssocSemiringOfMulOneClass instance

[MulOneClass α] : NonAssocSemiring (SetSemiring α)

Full source

instance [MulOneClass α] : NonAssocSemiring (SetSemiring α) :=
  { (inferInstance : NonUnitalNonAssocSemiring (SetSemiring α)),
    Set.mulOneClass with }

Non-Associative Semiring Structure on Sets with Identity

Informal description

For any type $\alpha$ equipped with a multiplication operation and a multiplicative identity (i.e., a `MulOneClass` structure), the semiring of sets $\text{SetSemiring}\,\alpha$ forms a non-associative semiring under the operations of set union (as addition) and pointwise multiplication (as multiplication).

SetSemiring.instNonUnitalSemiringOfSemigroup instance

[Semigroup α] : NonUnitalSemiring (SetSemiring α)

Full source

instance [Semigroup α] : NonUnitalSemiring (SetSemiring α) :=
  { (inferInstance : NonUnitalNonAssocSemiring (SetSemiring α)), Set.semigroup with }

Non-Unital Semiring Structure on Sets of a Semigroup

Informal description

For any semigroup $\alpha$, the semiring of sets $\text{SetSemiring}\,\alpha$ forms a non-unital semiring under the operations of set union (as addition) and pointwise multiplication (as multiplication).

SetSemiring.instIdemSemiringOfMonoid instance

[Monoid α] : IdemSemiring (SetSemiring α)

Full source

instance [Monoid α] : IdemSemiring (SetSemiring α) :=
  { (inferInstance : NonAssocSemiring (SetSemiring α)),
    (inferInstance : NonUnitalSemiring (SetSemiring α)),
    (inferInstance : CompleteBooleanAlgebra (Set α)) with }

Idempotent Semiring Structure on Sets of a Monoid

Informal description

For any monoid $\alpha$, the semiring of sets $\text{SetSemiring}\,\alpha$ forms an idempotent semiring under the operations of set union (as addition) and pointwise multiplication (as multiplication).

SetSemiring.instNonUnitalCommSemiringOfCommSemigroup instance

[CommSemigroup α] : NonUnitalCommSemiring (SetSemiring α)

Full source

instance [CommSemigroup α] : NonUnitalCommSemiring (SetSemiring α) :=
  { (inferInstance : NonUnitalSemiring (SetSemiring α)), Set.commSemigroup with }

Non-Unital Commutative Semiring Structure on Sets of a Commutative Semigroup

Informal description

For any commutative semigroup $\alpha$, the semiring of sets $\text{SetSemiring}\,\alpha$ forms a non-unital commutative semiring under the operations of set union (as addition) and pointwise multiplication (as multiplication).

SetSemiring.instIdemCommSemiringOfCommMonoid instance

[CommMonoid α] : IdemCommSemiring (SetSemiring α)

Full source

instance [CommMonoid α] : IdemCommSemiring (SetSemiring α) :=
  { (inferInstance : IdemSemiring (SetSemiring α)),
    (inferInstance : CommMonoid (Set α)) with }

Idempotent Commutative Semiring Structure on Sets of a Commutative Monoid

Informal description

For any commutative monoid $\alpha$, the semiring of sets $\text{SetSemiring}\,\alpha$ forms an idempotent commutative semiring under the operations of set union (as addition) and pointwise multiplication (as multiplication).

SetSemiring.instCommMonoid instance

[CommMonoid α] : CommMonoid (SetSemiring α)

Full source

instance [CommMonoid α] : CommMonoid (SetSemiring α) :=
  { (inferInstance : Monoid (SetSemiring α)), Set.commSemigroup with }

Commutative Monoid Structure on Sets of a Commutative Monoid

Informal description

For any commutative monoid $\alpha$, the semiring of sets $\text{SetSemiring}\,\alpha$ forms a commutative monoid under pointwise multiplication.

SetSemiring.instCanonicallyOrderedAdd instance

: CanonicallyOrderedAdd (SetSemiring α)

Full source

instance : CanonicallyOrderedAdd (SetSemiring α) where
  exists_add_of_le {_ b} ab := ⟨b, (union_eq_right.2 ab).symm⟩
  le_self_add _ _ := subset_union_left

Canonical Ordering on the Semiring of Sets

Informal description

The semiring of sets $\text{SetSemiring}\,\alpha$ is canonically ordered, where the order relation $\leq$ coincides with the subtractibility relation with respect to set union. That is, for any two sets $A, B \in \text{SetSemiring}\,\alpha$, we have $A \leq B$ if and only if there exists a set $C$ such that $B = A \cup C$.

SetSemiring.instIsOrderedRing instance

[CommMonoid α] : IsOrderedRing (SetSemiring α)

Full source

instance [CommMonoid α] : IsOrderedRing (SetSemiring α) :=
  CanonicallyOrderedAdd.toIsOrderedRing

Ordered Ring Structure on Semiring of Sets of a Commutative Monoid

Informal description

For any commutative monoid $\alpha$, the semiring of sets $\text{SetSemiring}\,\alpha$ (where addition is set union and multiplication is pointwise multiplication) is an ordered ring with respect to the inclusion order.

SetSemiring.imageHom definition

[MulOneClass α] [MulOneClass β] (f : α →* β) : SetSemiring α →+* SetSemiring β

Full source

/-- The image of a set under a multiplicative homomorphism is a ring homomorphism
with respect to the pointwise operations on sets. -/
def imageHom [MulOneClass α] [MulOneClass β] (f : α →* β) : SetSemiringSetSemiring α →+* SetSemiring β where
  toFun s := (image f s.down).up
  map_zero' := image_empty _
  map_one' := by
    rw [down_one, image_one, map_one, singleton_one, up_one]
  map_add' := image_union _
  map_mul' _ _ := image_mul f

Image homomorphism for semiring of sets

Informal description

Given monoids $\alpha$ and $\beta$ and a monoid homomorphism $f \colon \alpha \to \beta$, the function $\text{imageHom}\,f$ maps a set $S$ in the semiring of sets $\text{SetSemiring}\,\alpha$ to the image of $S$ under $f$ in $\text{SetSemiring}\,\beta$. This function is a semiring homomorphism, meaning it preserves the additive and multiplicative structures, where addition is set union and multiplication is pointwise multiplication.

SetSemiring.imageHom_def theorem

[MulOneClass α] [MulOneClass β] (f : α →* β) (s : SetSemiring α) : imageHom f s = (image f s.down).up

Full source

lemma imageHom_def [MulOneClass α] [MulOneClass β] (f : α →* β) (s : SetSemiring α) :
    imageHom f s = (image f s.down).up :=
  rfl

Definition of Image Homomorphism for Semiring of Sets

Informal description

Let $\alpha$ and $\beta$ be monoids (with multiplication and identity), and let $f \colon \alpha \to \beta$ be a monoid homomorphism. For any subset $S$ of $\alpha$ (viewed as an element of $\text{SetSemiring}\,\alpha$), the image homomorphism $\text{imageHom}\,f$ applied to $S$ equals the image of $S$ under $f$ (viewed in $\text{SetSemiring}\,\beta$). In other words, $\text{imageHom}\,f(S) = (f(S))^\uparrow$, where $^\uparrow$ denotes the embedding into $\text{SetSemiring}\,\beta$.

SetSemiring.down_imageHom theorem

[MulOneClass α] [MulOneClass β] (f : α →* β) (s : SetSemiring α) : (imageHom f s).down = f '' s.down

Full source

@[simp]
lemma down_imageHom [MulOneClass α] [MulOneClass β] (f : α →* β) (s : SetSemiring α) :
    (imageHom f s).down = f '' s.down :=
  rfl

Image Homomorphism Preserves Underlying Set

Informal description

Let $\alpha$ and $\beta$ be monoids with multiplicative identity, and let $f \colon \alpha \to \beta$ be a monoid homomorphism. For any subset $S$ of $\alpha$ (viewed as an element of the semiring of sets $\text{SetSemiring}\,\alpha$), the underlying set of the image of $S$ under the semiring homomorphism $\text{imageHom}\,f$ is equal to the image of $S$ under $f$, i.e., $(\text{imageHom}\,f(S))^\downarrow = f(S)$.

Set.up_image theorem

[MulOneClass α] [MulOneClass β] (f : α →* β) (s : Set α) : (f '' s).up = imageHom f s.up

Full source

@[simp]
lemma _root_.Set.up_image [MulOneClass α] [MulOneClass β] (f : α →* β) (s : Set α) :
    (f '' s).up = imageHom f s.up :=
  rfl

Image Homomorphism Commutes with Set Embedding

Informal description

Let $\alpha$ and $\beta$ be monoids (with multiplication and identity), and let $f \colon \alpha \to \beta$ be a monoid homomorphism. For any subset $S$ of $\alpha$, the image of $S$ under $f$ (viewed in $\text{SetSemiring}\,\beta$) is equal to the image homomorphism $\text{imageHom}\,f$ applied to the embedding of $S$ in $\text{SetSemiring}\,\alpha$. In other words, $(f(S))^\uparrow = \text{imageHom}\,f(S^\uparrow)$, where $^\uparrow$ denotes the embedding into the semiring of sets.