Subsemigroups: membership criteria #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

mem_supr_of_directed, coe_supr_of_directed, mem_Sup_of_directed_on, coe_Sup_of_directed_on: the supremum of a directed collection of subsemigroup is their union.

TODO #

Define the free_semigroup 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 free_semigroup as the subsemigroup (pushed to be a semigroup) of the free_monoid consisting of non-identity elements.

Tags #

subsemigroup

source

theorem subsemigroup.mem_supr_of_directed {ι : Sort u_1} {M : Type u_2} [has_mul M] {S : ι → subsemigroup M} (hS : directed has_le.le S) {x : M} :

(x ∈ ⨆ (i : ι), S i) ↔ ∃ (i : ι), x ∈ S i

source

theorem add_subsemigroup.mem_supr_of_directed {ι : Sort u_1} {M : Type u_2} [has_add M] {S : ι → add_subsemigroup M} (hS : directed has_le.le S) {x : M} :

(x ∈ ⨆ (i : ι), S i) ↔ ∃ (i : ι), x ∈ S i

source

theorem add_subsemigroup.coe_supr_of_directed {ι : Sort u_1} {M : Type u_2} [has_add M] {S : ι → add_subsemigroup M} (hS : directed has_le.le S) :

(↑⨆ (i : ι), S i) = ⋃ (i : ι), ↑(S i)

source

theorem subsemigroup.coe_supr_of_directed {ι : Sort u_1} {M : Type u_2} [has_mul M] {S : ι → subsemigroup M} (hS : directed has_le.le S) :

(↑⨆ (i : ι), S i) = ⋃ (i : ι), ↑(S i)

source

theorem subsemigroup.mem_Sup_of_directed_on {M : Type u_2} [has_mul M] {S : set (subsemigroup M)} (hS : directed_on has_le.le S) {x : M} :

x ∈ has_Sup.Sup S ↔ ∃ (s : subsemigroup M) (H : s ∈ S), x ∈ s

source

theorem add_subsemigroup.mem_Sup_of_directed_on {M : Type u_2} [has_add M] {S : set (add_subsemigroup M)} (hS : directed_on has_le.le S) {x : M} :

x ∈ has_Sup.Sup S ↔ ∃ (s : add_subsemigroup M) (H : s ∈ S), x ∈ s

source

theorem subsemigroup.coe_Sup_of_directed_on {M : Type u_2} [has_mul M] {S : set (subsemigroup M)} (hS : directed_on has_le.le S) :

↑(has_Sup.Sup S) = ⋃ (s : subsemigroup M) (H : s ∈ S), ↑s

source

theorem add_subsemigroup.coe_Sup_of_directed_on {M : Type u_2} [has_add M] {S : set (add_subsemigroup M)} (hS : directed_on has_le.le S) :

↑(has_Sup.Sup S) = ⋃ (s : add_subsemigroup M) (H : s ∈ S), ↑s

source

theorem subsemigroup.mem_sup_left {M : Type u_2} [has_mul M] {S T : subsemigroup M} {x : M} :

x ∈ S → x ∈ S ⊔ T

source

theorem add_subsemigroup.mem_sup_left {M : Type u_2} [has_add M] {S T : add_subsemigroup M} {x : M} :

x ∈ S → x ∈ S ⊔ T

source

theorem add_subsemigroup.mem_sup_right {M : Type u_2} [has_add M] {S T : add_subsemigroup M} {x : M} :

x ∈ T → x ∈ S ⊔ T

source

theorem subsemigroup.mem_sup_right {M : Type u_2} [has_mul M] {S T : subsemigroup M} {x : M} :

x ∈ T → x ∈ S ⊔ T

source

theorem add_subsemigroup.add_mem_sup {M : Type u_2} [has_add M] {S T : add_subsemigroup M} {x y : M} (hx : x ∈ S) (hy : y ∈ T) :

x + y ∈ S ⊔ T

source

theorem subsemigroup.mul_mem_sup {M : Type u_2} [has_mul M] {S T : subsemigroup M} {x y : M} (hx : x ∈ S) (hy : y ∈ T) :

x * y ∈ S ⊔ T

source

theorem subsemigroup.mem_supr_of_mem {ι : Sort u_1} {M : Type u_2} [has_mul M] {S : ι → subsemigroup M} (i : ι) {x : M} :

x ∈ S i → x ∈ supr S

source

theorem add_subsemigroup.mem_supr_of_mem {ι : Sort u_1} {M : Type u_2} [has_add M] {S : ι → add_subsemigroup M} (i : ι) {x : M} :

x ∈ S i → x ∈ supr S

source

theorem subsemigroup.mem_Sup_of_mem {M : Type u_2} [has_mul M] {S : set (subsemigroup M)} {s : subsemigroup M} (hs : s ∈ S) {x : M} :

x ∈ s → x ∈ has_Sup.Sup S

source

theorem add_subsemigroup.mem_Sup_of_mem {M : Type u_2} [has_add M] {S : set (add_subsemigroup M)} {s : add_subsemigroup M} (hs : s ∈ S) {x : M} :

x ∈ s → x ∈ has_Sup.Sup S

source

theorem add_subsemigroup.supr_induction {ι : Sort u_1} {M : Type u_2} [has_add M] (S : ι → add_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 addition, then it holds for all elements of the supremum of S.

source

theorem subsemigroup.supr_induction {ι : Sort u_1} {M : Type u_2} [has_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.

source

theorem subsemigroup.supr_induction' {ι : Sort u_1} {M : Type u_2} [has_mul M] (S : ι → subsemigroup M) {C : Π (x : M), (x ∈ ⨆ (i : ι), S i) → Prop} (hp : ∀ (i : ι) (x : M) (H : x ∈ S i), C x _) (hmul : ∀ (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.supr_induction.

source

theorem add_subsemigroup.supr_induction' {ι : Sort u_1} {M : Type u_2} [has_add M] (S : ι → add_subsemigroup M) {C : Π (x : M), (x ∈ ⨆ (i : ι), S i) → Prop} (hp : ∀ (i : ι) (x : M) (H : x ∈ S i), C x _) (hmul : ∀ (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 add_subsemigroup.supr_induction.