Subsemigroups: CompleteLattice structure

This file defines a CompleteLattice structure on Subsemigroups, and define the closure of a set as the minimal subsemigroup that includes this set.

Main definitions

For each of the following definitions in the Subsemigroup namespace, there is a corresponding definition in the AddSubsemigroup namespace.

• Subsemigroup.copy : copy of a subsemigroup with carrier replaced by a set that is equal but possibly not definitionally equal to the carrier of the original Subsemigroup.
• Subsemigroup.closure : semigroup closure of a set, i.e., the least subsemigroup that includes the set.
• Subsemigroup.gi : closure : Set M → Subsemigroup M and coercion coe : Subsemigroup M → Set M form a GaloisInsertion;

Implementation notes

Subsemigroup inclusion is denoted ≤ rather than ⊆, although ∈ is defined as membership of a subsemigroup's underlying set.

Note that Subsemigroup M does not actually require Semigroup M, instead requiring only the weaker Mul M.

This file is designed to have very few dependencies. In particular, it should not use natural numbers.

Tags

subsemigroup, subsemigroups

instance Subsemigroup.instInfSet {M : Type u_1} [Mul M] : InfSet (Subsemigroup M)

Equations

• Subsemigroup.instInfSet = { sInf := fun (s : Set (Subsemigroup M)) => { carrier := ⋂ t ∈ s, ↑t, mul_mem' := ⋯ } }

instance AddSubsemigroup.instInfSet {M : Type u_1} [Add M] : InfSet (AddSubsemigroup M)

Equations

• AddSubsemigroup.instInfSet = { sInf := fun (s : Set (AddSubsemigroup M)) => { carrier := ⋂ t ∈ s, ↑t, add_mem' := ⋯ } }

@[simp]

theorem Subsemigroup.coe_sInf {M : Type u_1} [Mul M] (S : Set (Subsemigroup M)) : ↑(sInf S) = ⋂ s ∈ S, ↑s

@[simp]

theorem AddSubsemigroup.coe_sInf {M : Type u_1} [Add M] (S : Set (AddSubsemigroup M)) : ↑(sInf S) = ⋂ s ∈ S, ↑s

theorem Subsemigroup.mem_sInf {M : Type u_1} [Mul M] {S : Set (Subsemigroup M)} {x : M} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

theorem AddSubsemigroup.mem_sInf {M : Type u_1} [Add M] {S : Set (AddSubsemigroup M)} {x : M} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

theorem Subsemigroup.mem_iInf {M : Type u_1} [Mul M] {ι : Sort u_4} {S : ι → Subsemigroup M} {x : M} : x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i

theorem AddSubsemigroup.mem_iInf {M : Type u_1} [Add M] {ι : Sort u_4} {S : ι → AddSubsemigroup M} {x : M} : x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i

@[simp]

theorem Subsemigroup.coe_iInf {M : Type u_1} [Mul M] {ι : Sort u_4} {S : ι → Subsemigroup M} : ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)

@[simp]

theorem AddSubsemigroup.coe_iInf {M : Type u_1} [Add M] {ι : Sort u_4} {S : ι → AddSubsemigroup M} : ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)

instance Subsemigroup.instCompleteLattice {M : Type u_1} [Mul M] : CompleteLattice (Subsemigroup M)

subsemigroups of a monoid form a complete lattice.

Equations

• Subsemigroup.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance AddSubsemigroup.instCompleteLattice {M : Type u_1} [Add M] : CompleteLattice (AddSubsemigroup M)

The AddSubsemigroups of an AddMonoid form a complete lattice.

Equations

• AddSubsemigroup.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def Subsemigroup.closure {M : Type u_1} [Mul M] (s : Set M) : Subsemigroup M

The Subsemigroup generated by a set.

Equations

• Subsemigroup.closure s = sInf {S : Subsemigroup M | s ⊆ ↑S}

def AddSubsemigroup.closure {M : Type u_1} [Add M] (s : Set M) : AddSubsemigroup M

The AddSubsemigroup generated by a set

Equations

• AddSubsemigroup.closure s = sInf {S : AddSubsemigroup M | s ⊆ ↑S}

theorem Subsemigroup.mem_closure {M : Type u_1} [Mul M] {s : Set M} {x : M} : x ∈ Subsemigroup.closure s ↔ ∀ (S : Subsemigroup M), s ⊆ ↑S → x ∈ S

theorem AddSubsemigroup.mem_closure {M : Type u_1} [Add M] {s : Set M} {x : M} : x ∈ AddSubsemigroup.closure s ↔ ∀ (S : AddSubsemigroup M), s ⊆ ↑S → x ∈ S

@[simp]

theorem Subsemigroup.subset_closure {M : Type u_1} [Mul M] {s : Set M} : s ⊆ ↑(Subsemigroup.closure s)

The subsemigroup generated by a set includes the set.

@[simp]

theorem AddSubsemigroup.subset_closure {M : Type u_1} [Add M] {s : Set M} : s ⊆ ↑(AddSubsemigroup.closure s)

The AddSubsemigroup generated by a set includes the set.

theorem Subsemigroup.not_mem_of_not_mem_closure {M : Type u_1} [Mul M] {s : Set M} {P : M} (hP : P ∉ Subsemigroup.closure s) : P ∉ s

theorem AddSubsemigroup.not_mem_of_not_mem_closure {M : Type u_1} [Add M] {s : Set M} {P : M} (hP : P ∉ AddSubsemigroup.closure s) : P ∉ s

@[simp]

theorem Subsemigroup.closure_le {M : Type u_1} [Mul M] {s : Set M} {S : Subsemigroup M} : Subsemigroup.closure s ≤ S ↔ s ⊆ ↑S

A subsemigroup S includes closure s if and only if it includes s.

@[simp]

theorem AddSubsemigroup.closure_le {M : Type u_1} [Add M] {s : Set M} {S : AddSubsemigroup M} : AddSubsemigroup.closure s ≤ S ↔ s ⊆ ↑S

An additive subsemigroup S includes closure s if and only if it includes s

theorem Subsemigroup.closure_mono {M : Type u_1} [Mul M] ⦃s : Set M⦄ ⦃t : Set M⦄ (h : s ⊆ t) : Subsemigroup.closure s ≤ Subsemigroup.closure t

subsemigroup closure of a set is monotone in its argument: if s ⊆ t, then closure s ≤ closure t.

theorem AddSubsemigroup.closure_mono {M : Type u_1} [Add M] ⦃s : Set M⦄ ⦃t : Set M⦄ (h : s ⊆ t) : AddSubsemigroup.closure s ≤ AddSubsemigroup.closure t

Additive subsemigroup closure of a set is monotone in its argument: if s ⊆ t, then closure s ≤ closure t

theorem Subsemigroup.closure_eq_of_le {M : Type u_1} [Mul M] {s : Set M} {S : Subsemigroup M} (h₁ : s ⊆ ↑S) (h₂ : S ≤ Subsemigroup.closure s) : Subsemigroup.closure s = S

theorem AddSubsemigroup.closure_eq_of_le {M : Type u_1} [Add M] {s : Set M} {S : AddSubsemigroup M} (h₁ : s ⊆ ↑S) (h₂ : S ≤ AddSubsemigroup.closure s) : AddSubsemigroup.closure s = S

theorem Subsemigroup.closure_induction {M : Type u_1} [Mul M] {s : Set M} {p : (x : M) → x ∈ Subsemigroup.closure s → Prop} (mem : ∀ (x : M) (h : x ∈ s), p x ⋯) (mul : ∀ (x y : M) (hx : x ∈ Subsemigroup.closure s) (hy : y ∈ Subsemigroup.closure s), p x hx → p y hy → p (x * y) ⋯) {x : M} (hx : x ∈ Subsemigroup.closure s) : p x hx

An induction principle for closure membership. If p holds for all elements of s, and is preserved under multiplication, then p holds for all elements of the closure of s.

theorem AddSubsemigroup.closure_induction {M : Type u_1} [Add M] {s : Set M} {p : (x : M) → x ∈ AddSubsemigroup.closure s → Prop} (mem : ∀ (x : M) (h : x ∈ s), p x ⋯) (mul : ∀ (x y : M) (hx : x ∈ AddSubsemigroup.closure s) (hy : y ∈ AddSubsemigroup.closure s), p x hx → p y hy → p (x + y) ⋯) {x : M} (hx : x ∈ AddSubsemigroup.closure s) : p x hx

An induction principle for additive closure membership. If p holds for all elements of s, and is preserved under addition, then p holds for all elements of the additive closure of s.

@[deprecated Subsemigroup.closure_induction]

theorem Subsemigroup.closure_induction' {M : Type u_1} [Mul M] {s : Set M} {p : (x : M) → x ∈ Subsemigroup.closure s → Prop} (mem : ∀ (x : M) (h : x ∈ s), p x ⋯) (mul : ∀ (x y : M) (hx : x ∈ Subsemigroup.closure s) (hy : y ∈ Subsemigroup.closure s), p x hx → p y hy → p (x * y) ⋯) {x : M} (hx : x ∈ Subsemigroup.closure s) : p x hx

Alias of Subsemigroup.closure_induction.

---

An induction principle for closure membership. If p holds for all elements of s, and is preserved under multiplication, then p holds for all elements of the closure of s.

theorem Subsemigroup.closure_induction₂ {M : Type u_1} [Mul M] {s : Set M} {p : (x y : M) → x ∈ Subsemigroup.closure s → y ∈ Subsemigroup.closure s → Prop} (mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) (mul_left : ∀ (x y z : M) (hx : x ∈ Subsemigroup.closure s) (hy : y ∈ Subsemigroup.closure s) (hz : z ∈ Subsemigroup.closure s), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) (mul_right : ∀ (x y z : M) (hx : x ∈ Subsemigroup.closure s) (hy : y ∈ Subsemigroup.closure s) (hz : z ∈ Subsemigroup.closure s), p z x hz hx → p z y hz hy → p z (x * y) hz ⋯) {x : M} {y : M} (hx : x ∈ Subsemigroup.closure s) (hy : y ∈ Subsemigroup.closure s) : p x y hx hy

An induction principle for closure membership for predicates with two arguments.

theorem AddSubsemigroup.closure_induction₂ {M : Type u_1} [Add M] {s : Set M} {p : (x y : M) → x ∈ AddSubsemigroup.closure s → y ∈ AddSubsemigroup.closure s → Prop} (mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) (mul_left : ∀ (x y z : M) (hx : x ∈ AddSubsemigroup.closure s) (hy : y ∈ AddSubsemigroup.closure s) (hz : z ∈ AddSubsemigroup.closure s), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) (mul_right : ∀ (x y z : M) (hx : x ∈ AddSubsemigroup.closure s) (hy : y ∈ AddSubsemigroup.closure s) (hz : z ∈ AddSubsemigroup.closure s), p z x hz hx → p z y hz hy → p z (x + y) hz ⋯) {x : M} {y : M} (hx : x ∈ AddSubsemigroup.closure s) (hy : y ∈ AddSubsemigroup.closure s) : p x y hx hy

An induction principle for additive closure membership for predicates with two arguments.

theorem Subsemigroup.dense_induction {M : Type u_1} [Mul M] {p : M → Prop} (s : Set M) (closure : Subsemigroup.closure s = ⊤) (mem : ∀ x ∈ s, p x) (mul : ∀ (x y : M), p x → p y → p (x * y)) (x : M) : p x

If s is a dense set in a magma M, Subsemigroup.closure s = ⊤, then in order to prove that some predicate p holds for all x : M it suffices to verify p x for x ∈ s, and verify that p x and p y imply p (x * y).

theorem AddSubsemigroup.dense_induction {M : Type u_1} [Add M] {p : M → Prop} (s : Set M) (closure : AddSubsemigroup.closure s = ⊤) (mem : ∀ x ∈ s, p x) (mul : ∀ (x y : M), p x → p y → p (x + y)) (x : M) : p x

If s is a dense set in an additive monoid M, AddSubsemigroup.closure s = ⊤, then in order to prove that some predicate p holds for all x : M it suffices to verify p x for x ∈ s, and verify that p x and p y imply p (x + y).

def Subsemigroup.gi (M : Type u_1) [Mul M] : GaloisInsertion Subsemigroup.closure SetLike.coe

closure forms a Galois insertion with the coercion to set.

Equations

• Subsemigroup.gi M = GaloisConnection.toGaloisInsertion ⋯ ⋯

def AddSubsemigroup.gi (M : Type u_1) [Add M] : GaloisInsertion AddSubsemigroup.closure SetLike.coe

closure forms a Galois insertion with the coercion to set.

Equations

• AddSubsemigroup.gi M = GaloisConnection.toGaloisInsertion ⋯ ⋯

@[simp]

theorem Subsemigroup.closure_eq {M : Type u_1} [Mul M] (S : Subsemigroup M) : Subsemigroup.closure ↑S = S

Closure of a subsemigroup S equals S.

@[simp]

theorem AddSubsemigroup.closure_eq {M : Type u_1} [Add M] (S : AddSubsemigroup M) : AddSubsemigroup.closure ↑S = S

Additive closure of an additive subsemigroup S equals S

@[simp]

theorem Subsemigroup.closure_empty {M : Type u_1} [Mul M] : Subsemigroup.closure ∅ = ⊥

@[simp]

theorem AddSubsemigroup.closure_empty {M : Type u_1} [Add M] : AddSubsemigroup.closure ∅ = ⊥

@[simp]

theorem Subsemigroup.closure_univ {M : Type u_1} [Mul M] : Subsemigroup.closure Set.univ = ⊤

@[simp]

theorem AddSubsemigroup.closure_univ {M : Type u_1} [Add M] : AddSubsemigroup.closure Set.univ = ⊤

theorem Subsemigroup.closure_union {M : Type u_1} [Mul M] (s : Set M) (t : Set M) : Subsemigroup.closure (s ∪ t) = Subsemigroup.closure s ⊔ Subsemigroup.closure t

theorem AddSubsemigroup.closure_union {M : Type u_1} [Add M] (s : Set M) (t : Set M) : AddSubsemigroup.closure (s ∪ t) = AddSubsemigroup.closure s ⊔ AddSubsemigroup.closure t

theorem Subsemigroup.closure_iUnion {M : Type u_1} [Mul M] {ι : Sort u_4} (s : ι → Set M) : Subsemigroup.closure (⋃ (i : ι), s i) = ⨆ (i : ι), Subsemigroup.closure (s i)

theorem AddSubsemigroup.closure_iUnion {M : Type u_1} [Add M] {ι : Sort u_4} (s : ι → Set M) : AddSubsemigroup.closure (⋃ (i : ι), s i) = ⨆ (i : ι), AddSubsemigroup.closure (s i)

theorem Subsemigroup.closure_singleton_le_iff_mem {M : Type u_1} [Mul M] (m : M) (p : Subsemigroup M) : Subsemigroup.closure {m} ≤ p ↔ m ∈ p

theorem AddSubsemigroup.closure_singleton_le_iff_mem {M : Type u_1} [Add M] (m : M) (p : AddSubsemigroup M) : AddSubsemigroup.closure {m} ≤ p ↔ m ∈ p

theorem Subsemigroup.mem_iSup {M : Type u_1} [Mul M] {ι : Sort u_4} (p : ι → Subsemigroup M) {m : M} : m ∈ ⨆ (i : ι), p i ↔ ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N

theorem AddSubsemigroup.mem_iSup {M : Type u_1} [Add M] {ι : Sort u_4} (p : ι → AddSubsemigroup M) {m : M} : m ∈ ⨆ (i : ι), p i ↔ ∀ (N : AddSubsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N

theorem Subsemigroup.iSup_eq_closure {M : Type u_1} [Mul M] {ι : Sort u_4} (p : ι → Subsemigroup M) : ⨆ (i : ι), p i = Subsemigroup.closure (⋃ (i : ι), ↑(p i))

theorem AddSubsemigroup.iSup_eq_closure {M : Type u_1} [Add M] {ι : Sort u_4} (p : ι → AddSubsemigroup M) : ⨆ (i : ι), p i = AddSubsemigroup.closure (⋃ (i : ι), ↑(p i))

theorem MulHom.eqOn_closure {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : M →ₙ* N} {g : M →ₙ* N} {s : Set M} (h : Set.EqOn (⇑f) (⇑g) s) : Set.EqOn ⇑f ⇑g ↑(Subsemigroup.closure s)

If two mul homomorphisms are equal on a set, then they are equal on its subsemigroup closure.

theorem AddHom.eqOn_closure {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : AddHom M N} {g : AddHom M N} {s : Set M} (h : Set.EqOn (⇑f) (⇑g) s) : Set.EqOn ⇑f ⇑g ↑(AddSubsemigroup.closure s)

If two add homomorphisms are equal on a set, then they are equal on its additive subsemigroup closure.

theorem MulHom.eq_of_eqOn_dense {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {s : Set M} (hs : Subsemigroup.closure s = ⊤) {f : M →ₙ* N} {g : M →ₙ* N} (h : Set.EqOn (⇑f) (⇑g) s) : f = g

theorem AddHom.eq_of_eqOn_dense {M : Type u_1} {N : Type u_2} [Add M] [Add N] {s : Set M} (hs : AddSubsemigroup.closure s = ⊤) {f : AddHom M N} {g : AddHom M N} (h : Set.EqOn (⇑f) (⇑g) s) : f = g

def MulHom.ofDense {M : Type u_4} {N : Type u_5} [Semigroup M] [Semigroup N] {s : Set M} (f : M → N) (hs : Subsemigroup.closure s = ⊤) (hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y) : M →ₙ* N

Let s be a subset of a semigroup M such that the closure of s is the whole semigroup. Then MulHom.ofDense defines a mul homomorphism from M asking for a proof of f (x * y) = f x * f y only for y ∈ s.

Equations

• MulHom.ofDense f hs hmul = { toFun := f, map_mul' := ⋯ }

def AddHom.ofDense {M : Type u_4} {N : Type u_5} [AddSemigroup M] [AddSemigroup N] {s : Set M} (f : M → N) (hs : AddSubsemigroup.closure s = ⊤) (hmul : ∀ (x y : M), y ∈ s → f (x + y) = f x + f y) : AddHom M N

Let s be a subset of an additive semigroup M such that the closure of s is the whole semigroup. Then AddHom.ofDense defines an additive homomorphism from M asking for a proof of f (x + y) = f x + f y only for y ∈ s.

Equations

• AddHom.ofDense f hs hmul = { toFun := f, map_add' := ⋯ }

@[simp]

theorem MulHom.coe_ofDense {M : Type u_1} {N : Type u_2} [Semigroup M] [Semigroup N] {s : Set M} (f : M → N) (hs : Subsemigroup.closure s = ⊤) (hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y) : ⇑(MulHom.ofDense f hs hmul) = f

@[simp]

theorem AddHom.coe_ofDense {M : Type u_1} {N : Type u_2} [AddSemigroup M] [AddSemigroup N] {s : Set M} (f : M → N) (hs : AddSubsemigroup.closure s = ⊤) (hmul : ∀ (x y : M), y ∈ s → f (x + y) = f x + f y) : ⇑(AddHom.ofDense f hs hmul) = f