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

abbrev AddSubsemigroup.mem_iSup_of_directed.match_1 {ι : Sort u_1} {M : Type u_2} [Add M] {S : ι → AddSubsemigroup M} {x : M} (motive : (∃ i, x ∈ S i) → Prop) : (x : ∃ i, x ∈ S i) → ((i : ι) → (hi : x ∈ S i) → motive (_ : ∃ i, x ∈ S i)) → motive x

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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_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_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.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.iSup_induction {ι : Sort u_1} {M : Type u_2} [Add M] (S : ι → AddSubsemigroup M) {C : M → Prop} {x₁ : M} (hx₁ : x₁ ∈ ⨆ (i : ι), S i) (hp : (i : ι) → (x₂ : M) → x₂ ∈ S i → C x₂) (hmul : (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 : M → Prop} {x₁ : M} (hx₁ : x₁ ∈ ⨆ (i : ι), S i) (hp : (i : ι) → (x₂ : M) → x₂ ∈ S i → C x₂) (hmul : (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 : (x : M) → x ∈ ⨆ (i : ι), S i → Prop} (hp : (i : ι) → (x : M) → (hxS : x ∈ S i) → C x (_ : x ∈ ⨆ (i : ι), S i)) (hmul : (x y : M) → (hx : x ∈ ⨆ (i : ι), S i) → (hy : y ∈ ⨆ (i : ι), S i) → C x hx → C y hy → C (x + y) (_ : x + y ∈ ⨆ (i : ι), S i)) {x₁ : M} (hx₁ : x₁ ∈ ⨆ (i : ι), S i) : C x₁ hx₁

A dependent version of AddSubsemigroup.iSup_induction.

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

A dependent version of Subsemigroup.iSup_induction.