Sets as a semiring under union

This file defines SetSemiring α, an alias of Set α, which we endow with ∪ as addition and pointwise * as multiplication. If α is a (commutative) monoid, SetSemiring α is a (commutative) semiring.

def SetSemiring (α : Type u_3) : Type u_3

An alias for Set α, which has a semiring structure given by ∪ as "addition" and pointwise multiplication * as "multiplication".

Equations

• SetSemiring α = Set α

noncomputable instance instInhabitedSetSemiring (α : Type u_3) : Inhabited (SetSemiring α)

Equations

• instInhabitedSetSemiring α = inferInstance

instance instPartialOrderSetSemiring (α : Type u_3) : PartialOrder (SetSemiring α)

Equations

• instPartialOrderSetSemiring α = inferInstance

instance instOrderBotSetSemiring (α : Type u_3) : OrderBot (SetSemiring α)

Equations

• instOrderBotSetSemiring α = inferInstance

def Set.up {α : Type u_1} : Set α ≃ SetSemiring α

The identity function Set α → SetSemiring α.

Equations

• Set.up = Equiv.refl (Set α)

def SetSemiring.down {α : Type u_1} : SetSemiring α ≃ Set α

The identity function SetSemiring α → Set α.

Equations

• SetSemiring.down = Equiv.refl (SetSemiring α)

@[simp]

theorem SetSemiring.down_up {α : Type u_1} (s : Set α) : SetSemiring.down (Set.up s) = s

@[simp]

theorem SetSemiring.up_down {α : Type u_1} (s : SetSemiring α) : Set.up (SetSemiring.down s) = s

theorem SetSemiring.up_le_up {α : Type u_1} {s : Set α} {t : Set α} : Set.up s ≤ Set.up t ↔ s ⊆ t

theorem SetSemiring.up_lt_up {α : Type u_1} {s : Set α} {t : Set α} : Set.up s < Set.up t ↔ s ⊂ t

@[simp]

theorem SetSemiring.down_subset_down {α : Type u_1} {s : SetSemiring α} {t : SetSemiring α} : SetSemiring.down s ⊆ SetSemiring.down t ↔ s ≤ t

@[simp]

theorem SetSemiring.down_ssubset_down {α : Type u_1} {s : SetSemiring α} {t : SetSemiring α} : SetSemiring.down s ⊂ SetSemiring.down t ↔ s < t

instance SetSemiring.instZero {α : Type u_1} : Zero (SetSemiring α)

Equations

• SetSemiring.instZero = { zero := Set.up ∅ }

instance SetSemiring.instAdd {α : Type u_1} : Add (SetSemiring α)

Equations

• SetSemiring.instAdd = { add := fun (s t : SetSemiring α) => Set.up (SetSemiring.down s ∪ SetSemiring.down t) }

instance SetSemiring.instAddCommMonoid {α : Type u_1} : AddCommMonoid (SetSemiring α)

Equations

• SetSemiring.instAddCommMonoid = AddCommMonoid.mk ⋯

theorem SetSemiring.zero_def {α : Type u_1} : 0 = Set.up ∅

@[simp]

theorem SetSemiring.down_zero {α : Type u_1} : SetSemiring.down 0 = ∅

@[simp]

theorem Set.up_empty {α : Type u_1} : Set.up ∅ = 0

theorem SetSemiring.add_def {α : Type u_1} (s : SetSemiring α) (t : SetSemiring α) : s + t = Set.up (SetSemiring.down s ∪ SetSemiring.down t)

@[simp]

theorem SetSemiring.down_add {α : Type u_1} (s : SetSemiring α) (t : SetSemiring α) : SetSemiring.down (s + t) = SetSemiring.down s ∪ SetSemiring.down t

@[simp]

theorem Set.up_union {α : Type u_1} (s : Set α) (t : Set α) : Set.up (s ∪ t) = Set.up s + Set.up t

instance SetSemiring.covariantClass_add {α : Type u_1} : CovariantClass (SetSemiring α) (SetSemiring α) (fun (x x_1 : SetSemiring α) => x + x_1) fun (x x_1 : SetSemiring α) => x ≤ x_1

Equations

• ⋯ = ⋯

instance SetSemiring.instNonUnitalNonAssocSemiring {α : Type u_1} [Mul α] : NonUnitalNonAssocSemiring (SetSemiring α)

Equations

• SetSemiring.instNonUnitalNonAssocSemiring = let __src := inferInstance; NonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

theorem SetSemiring.mul_def {α : Type u_1} [Mul α] (s : SetSemiring α) (t : SetSemiring α) : s * t = Set.up (SetSemiring.down s * SetSemiring.down t)

@[simp]

theorem SetSemiring.down_mul {α : Type u_1} [Mul α] (s : SetSemiring α) (t : SetSemiring α) : SetSemiring.down (s * t) = SetSemiring.down s * SetSemiring.down t

@[simp]

theorem Set.up_mul {α : Type u_1} [Mul α] (s : Set α) (t : Set α) : Set.up (s * t) = Set.up s * Set.up t

instance SetSemiring.instNoZeroDivisors {α : Type u_1} [Mul α] : NoZeroDivisors (SetSemiring α)

Equations

• ⋯ = ⋯

instance SetSemiring.covariantClass_mul_left {α : Type u_1} [Mul α] : CovariantClass (SetSemiring α) (SetSemiring α) (fun (x x_1 : SetSemiring α) => x * x_1) fun (x x_1 : SetSemiring α) => x ≤ x_1

Equations

• ⋯ = ⋯

instance SetSemiring.covariantClass_mul_right {α : Type u_1} [Mul α] : CovariantClass (SetSemiring α) (SetSemiring α) (Function.swap fun (x x_1 : SetSemiring α) => x * x_1) fun (x x_1 : SetSemiring α) => x ≤ x_1

Equations

• ⋯ = ⋯

instance SetSemiring.instOne {α : Type u_1} [One α] : One (SetSemiring α)

Equations

• SetSemiring.instOne = { one := Set.up 1 }

theorem SetSemiring.one_def {α : Type u_1} [One α] : 1 = Set.up 1

@[simp]

theorem SetSemiring.down_one {α : Type u_1} [One α] : SetSemiring.down 1 = 1

@[simp]

theorem Set.up_one {α : Type u_1} [One α] : Set.up 1 = 1

instance SetSemiring.instNonAssocSemiringOfMulOneClass {α : Type u_1} [MulOneClass α] : NonAssocSemiring (SetSemiring α)

Equations

• SetSemiring.instNonAssocSemiringOfMulOneClass = let __src := inferInstance; let __src_1 := Set.mulOneClass; NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

instance SetSemiring.instNonUnitalSemiringOfSemigroup {α : Type u_1} [Semigroup α] : NonUnitalSemiring (SetSemiring α)

Equations

• SetSemiring.instNonUnitalSemiringOfSemigroup = let __src := inferInstance; let __src_1 := Set.semigroup; NonUnitalSemiring.mk ⋯

instance SetSemiring.instIdemSemiringOfMonoid {α : Type u_1} [Monoid α] : IdemSemiring (SetSemiring α)

Equations

• SetSemiring.instIdemSemiringOfMonoid = let __src := inferInstance; let __src_1 := inferInstance; let __src_2 := inferInstance; IdemSemiring.mk ⋯ ⊥ ⋯

instance SetSemiring.instNonUnitalCommSemiringOfCommSemigroup {α : Type u_1} [CommSemigroup α] : NonUnitalCommSemiring (SetSemiring α)

Equations

• SetSemiring.instNonUnitalCommSemiringOfCommSemigroup = let __src := inferInstance; let __src_1 := Set.commSemigroup; NonUnitalCommSemiring.mk ⋯

instance SetSemiring.instIdemCommSemiringOfCommMonoid {α : Type u_1} [CommMonoid α] : IdemCommSemiring (SetSemiring α)

Equations

• SetSemiring.instIdemCommSemiringOfCommMonoid = let __src := inferInstance; let __src_1 := inferInstance; IdemCommSemiring.mk ⋯ IdemSemiring.bot ⋯

instance SetSemiring.instCommMonoid {α : Type u_1} [CommMonoid α] : CommMonoid (SetSemiring α)

Equations

• SetSemiring.instCommMonoid = let __src := inferInstance; let __src_1 := Set.commSemigroup; CommMonoid.mk ⋯

instance SetSemiring.instCanonicallyOrderedCommSemiringOfCommMonoid {α : Type u_1} [CommMonoid α] : CanonicallyOrderedCommSemiring (SetSemiring α)

Equations

• One or more equations did not get rendered due to their size.

def SetSemiring.imageHom {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) : SetSemiring α →+* SetSemiring β

The image of a set under a multiplicative homomorphism is a ring homomorphism with respect to the pointwise operations on sets.

Equations

• SetSemiring.imageHom f = { toFun := fun (s : SetSemiring α) => Set.up (⇑f '' SetSemiring.down s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem SetSemiring.imageHom_def {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (s : SetSemiring α) : (SetSemiring.imageHom f) s = Set.up (⇑f '' SetSemiring.down s)

@[simp]

theorem SetSemiring.down_imageHom {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (s : SetSemiring α) : SetSemiring.down ((SetSemiring.imageHom f) s) = ⇑f '' SetSemiring.down s

@[simp]

theorem Set.up_image {α : Type u_1} {β : Type u_2} [MulOneClass α] [MulOneClass β] (f : α →* β) (s : Set α) : Set.up (⇑f '' s) = (SetSemiring.imageHom f) (Set.up s)