Subsemigroups: membership criteria

In this file we prove various facts about membership in a subsemigroup. The intent is to mimic GroupTheory/Submonoid/Membership, but currently this file is mostly a stub and only provides rudimentary support.

• mem_iSup_of_directed, coe_iSup_of_directed, mem_sSup_of_directed_on, coe_sSup_of_directed_on: the supremum of a directed collection of subsemigroup is their union.

TODO

• Define the FreeSemigroup generated by a set. This might require some rather substantial additions to low-level API. For example, developing the subtype of nonempty lists, then defining a product on nonempty lists, powers where the exponent is a positive natural, et cetera. Another option would be to define the FreeSemigroup as the subsemigroup (pushed to be a semigroup) of the FreeMonoid consisting of non-identity elements.

Tags

subsemigroup

theorem Subsemigroup.mem_iSup_of_directed {M : Type u_2} [Mul M] {ι : Sort u_3} {S : ι → Subsemigroup M} (hS : Directed (fun (x1 x2 : Subsemigroup M) => x1 ≤ x2) S) {x : M} : x ∈ ⨆ (i : ι), S i ↔ ∃ (i : ι), x ∈ S i

theorem AddSubsemigroup.mem_iSup_of_directed {M : Type u_2} [Add M] {ι : Sort u_3} {S : ι → AddSubsemigroup M} (hS : Directed (fun (x1 x2 : AddSubsemigroup M) => x1 ≤ x2) S) {x : M} : x ∈ ⨆ (i : ι), S i ↔ ∃ (i : ι), x ∈ S i

theorem Subsemigroup.mem_biSup_of_directedOn {M : Type u_2} [Mul M] {ι : Type u_3} {p : ι → Prop} {S : ι → Subsemigroup M} (hS : DirectedOn (Function.onFun (fun (x1 x2 : Subsemigroup M) => x1 ≤ x2) S) {i : ι | p i}) {x : M} : x ∈ ⨆ (i : ι), ⨆ (_ : p i), S i ↔ ∃ (i : ι), p i ∧ x ∈ S i

theorem AddSubsemigroup.mem_biSup_of_directedOn {M : Type u_2} [Add M] {ι : Type u_3} {p : ι → Prop} {S : ι → AddSubsemigroup M} (hS : DirectedOn (Function.onFun (fun (x1 x2 : AddSubsemigroup M) => x1 ≤ x2) S) {i : ι | p i}) {x : M} : x ∈ ⨆ (i : ι), ⨆ (_ : p i), S i ↔ ∃ (i : ι), p i ∧ x ∈ S i

@[simp]

theorem Subsemigroup.mem_iSup_prop {M : Type u_2} [Mul M] {p : Prop} {S : p → Subsemigroup M} {x : M} : x ∈ ⨆ (h : p), S h ↔ ∃ (h : p), x ∈ S h

@[simp]

theorem AddSubsemigroup.mem_iSup_prop {M : Type u_2} [Add M] {p : Prop} {S : p → AddSubsemigroup M} {x : M} : x ∈ ⨆ (h : p), S h ↔ ∃ (h : p), x ∈ S h

theorem Subsemigroup.coe_iSup_of_directed {ι : Sort u_1} {M : Type u_2} [Mul M] {S : ι → Subsemigroup M} (hS : Directed (fun (x1 x2 : Subsemigroup M) => x1 ≤ x2) S) : ↑(⨆ (i : ι), S i) = ⋃ (i : ι), ↑(S i)

theorem AddSubsemigroup.coe_iSup_of_directed {ι : Sort u_1} {M : Type u_2} [Add M] {S : ι → AddSubsemigroup M} (hS : Directed (fun (x1 x2 : AddSubsemigroup M) => x1 ≤ x2) S) : ↑(⨆ (i : ι), S i) = ⋃ (i : ι), ↑(S i)

theorem Subsemigroup.isMulCommutative_iSup {ι : Sort u_1} {M : Type u_2} [Mul M] {S : ι → Subsemigroup M} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)] (dir : Directed (fun (x1 x2 : Subsemigroup M) => x1 ≤ x2) S) : IsMulCommutative ↥(⨆ (i : ι), S i)

The supremum of a directed family of commutative subsemigroups is commutative.

theorem AddSubsemigroup.isAddCommutative_iSup {ι : Sort u_1} {M : Type u_2} [Add M] {S : ι → AddSubsemigroup M} [hS : ∀ (i : ι), IsAddCommutative ↥(S i)] (dir : Directed (fun (x1 x2 : AddSubsemigroup M) => x1 ≤ x2) S) : IsAddCommutative ↥(⨆ (i : ι), S i)

instance Subsemigroup.instIsMulCommutative_iSup {M : Type u_2} [Mul M] {ι : Type u_3} [Preorder ι] [IsDirectedOrder ι] (S : ι →o Subsemigroup M) [hS : ∀ (i : ι), IsMulCommutative ↥(S i)] : IsMulCommutative ↥(⨆ (i : ι), S i)

The supremum of a directed family of commutative subsemigroups is commutative.

instance AddSubsemigroup.instIsAddCommutative_iSup {M : Type u_2} [Add M] {ι : Type u_3} [Preorder ι] [IsDirectedOrder ι] (S : ι →o AddSubsemigroup M) [hS : ∀ (i : ι), IsAddCommutative ↥(S i)] : IsAddCommutative ↥(⨆ (i : ι), S i)

theorem Subsemigroup.mem_sSup_of_directed_on {M : Type u_2} [Mul M] {S : Set (Subsemigroup M)} (hS : DirectedOn (fun (x1 x2 : Subsemigroup M) => x1 ≤ x2) S) {x : M} : x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

theorem AddSubsemigroup.mem_sSup_of_directed_on {M : Type u_2} [Add M] {S : Set (AddSubsemigroup M)} (hS : DirectedOn (fun (x1 x2 : AddSubsemigroup M) => x1 ≤ x2) S) {x : M} : x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

theorem Subsemigroup.coe_sSup_of_directed_on {M : Type u_2} [Mul M] {S : Set (Subsemigroup M)} (hS : DirectedOn (fun (x1 x2 : Subsemigroup M) => x1 ≤ x2) S) : ↑(sSup S) = ⋃ s ∈ S, ↑s

theorem AddSubsemigroup.coe_sSup_of_directed_on {M : Type u_2} [Add M] {S : Set (AddSubsemigroup M)} (hS : DirectedOn (fun (x1 x2 : AddSubsemigroup M) => x1 ≤ x2) S) : ↑(sSup S) = ⋃ s ∈ S, ↑s

theorem Subsemigroup.mem_sup_left {M : Type u_2} [Mul M] {S T : Subsemigroup M} {x : M} : x ∈ S → x ∈ S ⊔ T

theorem AddSubsemigroup.mem_sup_left {M : Type u_2} [Add M] {S T : AddSubsemigroup M} {x : M} : x ∈ S → x ∈ S ⊔ T

theorem Subsemigroup.mem_sup_right {M : Type u_2} [Mul M] {S T : Subsemigroup M} {x : M} : x ∈ T → x ∈ S ⊔ T

theorem AddSubsemigroup.mem_sup_right {M : Type u_2} [Add M] {S T : AddSubsemigroup M} {x : M} : x ∈ T → x ∈ S ⊔ T

theorem Subsemigroup.mul_mem_sup {M : Type u_2} [Mul M] {S T : Subsemigroup M} {x y : M} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T

theorem AddSubsemigroup.add_mem_sup {M : Type u_2} [Add M] {S T : AddSubsemigroup M} {x y : M} (hx : x ∈ S) (hy : y ∈ T) : x + y ∈ S ⊔ T

theorem Subsemigroup.mem_iSup_of_mem {ι : Sort u_1} {M : Type u_2} [Mul M] {S : ι → Subsemigroup M} (i : ι) {x : M} : x ∈ S i → x ∈ iSup S

theorem AddSubsemigroup.mem_iSup_of_mem {ι : Sort u_1} {M : Type u_2} [Add M] {S : ι → AddSubsemigroup M} (i : ι) {x : M} : x ∈ S i → x ∈ iSup S

theorem Subsemigroup.mem_sSup_of_mem {M : Type u_2} [Mul M] {S : Set (Subsemigroup M)} {s : Subsemigroup M} (hs : s ∈ S) {x : M} : x ∈ s → x ∈ sSup S

theorem AddSubsemigroup.mem_sSup_of_mem {M : Type u_2} [Add M] {S : Set (AddSubsemigroup M)} {s : AddSubsemigroup M} (hs : s ∈ S) {x : M} : x ∈ s → x ∈ sSup S

theorem Subsemigroup.iSup_induction {ι : Sort u_1} {M : Type u_2} [Mul M] (S : ι → Subsemigroup M) {C : M → Prop} {x₁ : M} (hx₁ : x₁ ∈ ⨆ (i : ι), S i) (mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂) (mul : ∀ (x y : M), C x → C y → C (x * y)) : C x₁

An induction principle for elements of ⨆ i, S i. If C holds all elements of S i for all i, and is preserved under multiplication, then it holds for all elements of the supremum of S.

theorem AddSubsemigroup.iSup_induction {ι : Sort u_1} {M : Type u_2} [Add M] (S : ι → AddSubsemigroup M) {C : M → Prop} {x₁ : M} (hx₁ : x₁ ∈ ⨆ (i : ι), S i) (mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂) (add : ∀ (x y : M), C x → C y → C (x + y)) : C x₁

An induction principle for elements of ⨆ i, S i. If C holds all elements of S i for all i, and is preserved under addition, then it holds for all elements of the supremum of S.

theorem Subsemigroup.iSup_induction' {ι : Sort u_1} {M : Type u_2} [Mul M] (S : ι → Subsemigroup M) {C : (x : M) → x ∈ ⨆ (i : ι), S i → Prop} (mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯) (mul : ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i), C x hx → C y hy → C (x * y) ⋯) {x₁ : M} (hx₁ : x₁ ∈ ⨆ (i : ι), S i) : C x₁ hx₁

A dependent version of Subsemigroup.iSup_induction.

theorem AddSubsemigroup.iSup_induction' {ι : Sort u_1} {M : Type u_2} [Add M] (S : ι → AddSubsemigroup M) {C : (x : M) → x ∈ ⨆ (i : ι), S i → Prop} (mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯) (add : ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i), C x hx → C y hy → C (x + y) ⋯) {x₁ : M} (hx₁ : x₁ ∈ ⨆ (i : ι), S i) : C x₁ hx₁

A dependent version of AddSubsemigroup.iSup_induction.