Mathlib.Algebra.Group.Subsemigroup.Membership

Module docstring

{"# 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 "}

Subsemigroup.mem_iSup_of_directed theorem

{S : ι → Subsemigroup M} (hS : Directed (· ≤ ·) S) {x : M} : (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i

Full source

@[to_additive]
theorem mem_iSup_of_directed {S : ι → Subsemigroup M} (hS : Directed (· ≤ ·) S) {x : M} :
    (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i := by
  refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
  suffices x ∈ closure (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by
    simpa only [closure_iUnion, closure_eq (S _)] using this
  refine fun hx ↦ closure_induction (fun y hy ↦ mem_iUnion.mp hy) ?_ hx
  rintro x y - - ⟨i, hi⟩ ⟨j, hj⟩
  rcases hS i j with ⟨k, hki, hkj⟩
  exact ⟨k, (S k).mul_mem (hki hi) (hkj hj)⟩

Membership in Directed Supremum of Subsemigroups: $x \in \bigsqcup_i S_i \leftrightarrow \exists i, x \in S_i$

Informal description

Let $M$ be a semigroup and $\{S_i\}_{i \in \iota}$ be a directed family of subsemigroups of $M$ with respect to the inclusion relation $\leq$. For any element $x \in M$, we have that $x$ belongs to the supremum $\bigsqcup_i S_i$ of the family if and only if there exists an index $i \in \iota$ such that $x \in S_i$.

Subsemigroup.coe_iSup_of_directed theorem

{S : ι → Subsemigroup M} (hS : Directed (· ≤ ·) S) : ((⨆ i, S i : Subsemigroup M) : Set M) = ⋃ i, S i

Full source

@[to_additive]
theorem coe_iSup_of_directed {S : ι → Subsemigroup M} (hS : Directed (· ≤ ·) S) :
    ((⨆ i, S i : Subsemigroup M) : Set M) = ⋃ i, S i :=
  Set.ext fun x => by simp [mem_iSup_of_directed hS]

Supremum of Directed Family of Subsemigroups Equals Union of Their Underlying Sets

Informal description

Let $M$ be a semigroup and $\{S_i\}_{i \in \iota}$ be a directed family of subsemigroups of $M$ with respect to the inclusion relation $\leq$. Then the underlying set of the supremum $\bigsqcup_i S_i$ of the family is equal to the union $\bigcup_i S_i$ of the underlying sets of the subsemigroups.

Subsemigroup.mem_sSup_of_directed_on theorem

{S : Set (Subsemigroup M)} (hS : DirectedOn (· ≤ ·) S) {x : M} : x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Full source

@[to_additive]
theorem mem_sSup_of_directed_on {S : Set (Subsemigroup M)} (hS : DirectedOn (· ≤ ·) S) {x : M} :
    x ∈ sSup Sx ∈ sSup S ↔ ∃ s ∈ S, x ∈ s := by
  simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, Subtype.coe_mk,
    exists_prop]

Membership in Directed Supremum of Subsemigroups: $x \in \mathrm{sSup}(S) \leftrightarrow \exists s \in S, x \in s$

Informal description

Let $M$ be a semigroup and $S$ be a set of subsemigroups of $M$ that is directed with respect to the inclusion relation $\leq$. For any element $x \in M$, we have that $x$ belongs to the supremum $\mathrm{sSup}(S)$ of $S$ if and only if there exists a subsemigroup $s \in S$ such that $x \in s$.

Subsemigroup.coe_sSup_of_directed_on theorem

{S : Set (Subsemigroup M)} (hS : DirectedOn (· ≤ ·) S) : (↑(sSup S) : Set M) = ⋃ s ∈ S, ↑s

Full source

@[to_additive]
theorem coe_sSup_of_directed_on {S : Set (Subsemigroup M)} (hS : DirectedOn (· ≤ ·) S) :
    (↑(sSup S) : Set M) = ⋃ s ∈ S, ↑s :=
  Set.ext fun x => by simp [mem_sSup_of_directed_on hS]

Supremum of Directed Set of Subsemigroups Equals Union of Their Underlying Sets

Informal description

Let $M$ be a semigroup and $S$ be a set of subsemigroups of $M$ that is directed with respect to the inclusion relation $\leq$. Then the underlying set of the supremum $\mathrm{sSup}(S)$ is equal to the union $\bigcup_{s \in S} s$ of the underlying sets of the subsemigroups in $S$.

Subsemigroup.mem_sup_left theorem

{S T : Subsemigroup M} : ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Full source

@[to_additive]
theorem mem_sup_left {S T : Subsemigroup M} : ∀ {x : M}, x ∈ S → x ∈ S ⊔ T := by
  have : S ≤ S ⊔ T := le_sup_left
  tauto

Membership in Left Subsemigroup Implies Membership in Supremum

Informal description

For any subsemigroups $S$ and $T$ of a semigroup $M$, if an element $x \in M$ belongs to $S$, then it also belongs to the supremum $S \sqcup T$ of $S$ and $T$.

Subsemigroup.mem_sup_right theorem

{S T : Subsemigroup M} : ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Full source

@[to_additive]
theorem mem_sup_right {S T : Subsemigroup M} : ∀ {x : M}, x ∈ T → x ∈ S ⊔ T := by
  have : T ≤ S ⊔ T := le_sup_right
  tauto

Membership in Right Supremand Implies Membership in Supremum of Subsemigroups

Informal description

For any subsemigroups $S$ and $T$ of a semigroup $M$, if an element $x \in M$ belongs to $T$, then $x$ also belongs to the supremum $S \sqcup T$ of $S$ and $T$.

Subsemigroup.mul_mem_sup theorem

{S T : Subsemigroup M} {x y : M} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T

Full source

@[to_additive]
theorem mul_mem_sup {S T : Subsemigroup M} {x y : M} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T :=
  mul_mem (mem_sup_left hx) (mem_sup_right hy)

Product of Elements from Two Subsemigroups Belongs to Their Supremum

Informal description

For any subsemigroups $S$ and $T$ of a semigroup $M$, if $x \in S$ and $y \in T$, then their product $x * y$ belongs to the supremum $S \sqcup T$ of $S$ and $T$.

Subsemigroup.mem_iSup_of_mem theorem

{S : ι → Subsemigroup M} (i : ι) : ∀ {x : M}, x ∈ S i → x ∈ iSup S

Full source

@[to_additive]
theorem mem_iSup_of_mem {S : ι → Subsemigroup M} (i : ι) : ∀ {x : M}, x ∈ S i → x ∈ iSup S := by
  have : S i ≤ iSup S := le_iSup _ _
  tauto

Membership in a Subsemigroup Implies Membership in its Supremum

Informal description

For any family of subsemigroups $(S_i)_{i \in \iota}$ of a semigroup $M$ and any index $i \in \iota$, if an element $x \in M$ belongs to $S_i$, then $x$ also belongs to the supremum $\bigsqcup_{i \in \iota} S_i$.

Subsemigroup.mem_sSup_of_mem theorem

{S : Set (Subsemigroup M)} {s : Subsemigroup M} (hs : s ∈ S) : ∀ {x : M}, x ∈ s → x ∈ sSup S

Full source

@[to_additive]
theorem mem_sSup_of_mem {S : Set (Subsemigroup M)} {s : Subsemigroup M} (hs : s ∈ S) :
    ∀ {x : M}, x ∈ s → x ∈ sSup S := by
  have : s ≤ sSup S := le_sSup hs
  tauto

Membership in Supremum of Subsemigroups

Informal description

For any subset $S$ of subsemigroups of a semigroup $M$ and any subsemigroup $s \in S$, if an element $x \in M$ belongs to $s$, then $x$ also belongs to the supremum of $S$ (i.e., the smallest subsemigroup containing all subsemigroups in $S$).

Subsemigroup.iSup_induction theorem

 (S : ι → Subsemigroup M) {C : M → Prop} {x₁ : M} (hx₁ : x₁ ∈ ⨆ i, S i) (mem : ∀ i, ∀ x₂ ∈ S i, C x₂)
  (mul : ∀ x y, C x → C y → C (x * y)) : C x₁

Full source

/-- 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`. -/
@[to_additive (attr := elab_as_elim)
"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 iSup_induction (S : ι → Subsemigroup M) {C : M → Prop} {x₁ : M} (hx₁ : x₁ ∈ ⨆ i, S i)
    (mem : ∀ i, ∀ x₂ ∈ S i, C x₂) (mul : ∀ x y, C x → C y → C (x * y)) : C x₁ := by
  rw [iSup_eq_closure] at hx₁
  refine closure_induction (fun x₂ hx₂ => ?_) (fun x y _ _ ↦ mul x y) hx₁
  obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx₂
  exact mem _ _ hi

Induction Principle for Elements of Directed Supremum of Subsemigroups

Informal description

Let $M$ be a semigroup and $(S_i)_{i \in \iota}$ be a family of subsemigroups of $M$. Given a property $C : M \to \mathrm{Prop}$ such that: 1. $C$ holds for all elements of each $S_i$, and 2. $C$ is preserved under multiplication (i.e., for any $x, y \in M$, if $C(x)$ and $C(y)$ hold, then $C(x * y)$ holds), then $C$ holds for every element in the supremum $\bigsqcup_i S_i$ (i.e., for any $x_1 \in \bigsqcup_i S_i$, we have $C(x_1)$).

Subsemigroup.iSup_induction' theorem

 (S : ι → Subsemigroup M) {C : ∀ x, (x ∈ ⨆ i, S i) → Prop}
  (mem : ∀ (i) (x) (hxS : x ∈ S i), C x (mem_iSup_of_mem i ‹_›))
  (mul : ∀ x y hx hy, C x hx → C y hy → C (x * y) (mul_mem ‹_› ‹_›)) {x₁ : M} (hx₁ : x₁ ∈ ⨆ i, S i) : C x₁ hx₁

Full source

/-- A dependent version of `Subsemigroup.iSup_induction`. -/
@[to_additive (attr := elab_as_elim)
"A dependent version of `AddSubsemigroup.iSup_induction`."]
theorem iSup_induction' (S : ι → Subsemigroup M) {C : ∀ x, (x ∈ ⨆ i, S i) → Prop}
    (mem : ∀ (i) (x) (hxS : x ∈ S i), C x (mem_iSup_of_mem i ‹_›))
    (mul : ∀ x y hx hy, C x hx → C y hy → C (x * y) (mul_mem ‹_› ‹_›)) {x₁ : M}
    (hx₁ : x₁ ∈ ⨆ i, S i) : C x₁ hx₁ := by
  refine Exists.elim ?_ fun (hx₁' : x₁ ∈ ⨆ i, S i) (hc : C x₁ hx₁') => hc
  refine @iSup_induction _ _ _ S (fun x' => ∃ hx'', C x' hx'') _ hx₁
      (fun i x₂ hx₂ => ?_) fun x₃ y => ?_
  · exact ⟨_, mem _ _ hx₂⟩
  · rintro ⟨_, Cx⟩ ⟨_, Cy⟩
    exact ⟨_, mul _ _ _ _ Cx Cy⟩

Dependent Induction Principle for Elements of Directed Supremum of Subsemigroups

Informal description

Let $M$ be a semigroup and $(S_i)_{i \in \iota}$ be a family of subsemigroups of $M$. Given a property $C : \forall x \in M, (x \in \bigsqcup_i S_i) \to \mathrm{Prop}$ such that: 1. For any $i \in \iota$ and $x \in S_i$, the property $C$ holds for $x$ (with proof of membership in $\bigsqcup_i S_i$), and 2. For any $x, y \in \bigsqcup_i S_i$, if $C$ holds for $x$ and $y$, then $C$ holds for $x * y$, then $C$ holds for every element $x_1 \in \bigsqcup_i S_i$ (with its given proof of membership).