mathlib documentation

group_theory.subsemigroup.basic

Subsemigroups: definition and complete_lattice structure #

This file defines bundled multiplicative and additive subsemigroups. We also define a complete_lattice 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 add_subsemigroup namespace.

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 has_mul M.

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

Tags #

subsemigroup, subsemigroups

@[class]
structure mul_mem_class (S : Type u_4) (M : out_param (Type u_5)) [has_mul M] [set_like S M] :
Type
  • mul_mem : ∀ {s : S} {a b : M}, a sb sa * b s

mul_mem_class S M says S is a type of subsets s ≤ M that are closed under (*)

Instances of this typeclass
Instances of other typeclasses for mul_mem_class
  • mul_mem_class.has_sizeof_inst
@[class]
structure add_mem_class (S : Type u_4) (M : out_param (Type u_5)) [has_add M] [set_like S M] :
Type
  • add_mem : ∀ {s : S} {a b : M}, a sb sa + b s

add_mem_class S M says S is a type of subsets s ≤ M that are closed under (+)

Instances of this typeclass
Instances of other typeclasses for add_mem_class
  • add_mem_class.has_sizeof_inst
structure subsemigroup (M : Type u_4) [has_mul M] :
Type u_4

A subsemigroup of a magma M is a subset closed under multiplication.

Instances for subsemigroup
structure add_subsemigroup (M : Type u_4) [has_add M] :
Type u_4

An additive subsemigroup of an additive magma M is a subset closed under addition.

Instances for add_subsemigroup
@[protected, instance]
def subsemigroup.set_like {M : Type u_1} [has_mul M] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem add_subsemigroup.mem_carrier {M : Type u_1} [has_add M] {s : add_subsemigroup M} {x : M} :
x s.carrier x s
@[simp]
theorem subsemigroup.mem_carrier {M : Type u_1} [has_mul M] {s : subsemigroup M} {x : M} :
x s.carrier x s
@[simp]
theorem add_subsemigroup.mem_mk {M : Type u_1} [has_add M] {s : set M} {x : M} (h_mul : ∀ {a b : M}, a sb sa + b s) :
x {carrier := s, add_mem' := h_mul} x s
@[simp]
theorem subsemigroup.mem_mk {M : Type u_1} [has_mul M] {s : set M} {x : M} (h_mul : ∀ {a b : M}, a sb sa * b s) :
x {carrier := s, mul_mem' := h_mul} x s
@[simp]
theorem subsemigroup.coe_set_mk {M : Type u_1} [has_mul M] {s : set M} (h_mul : ∀ {a b : M}, a sb sa * b s) :
{carrier := s, mul_mem' := h_mul} = s
@[simp]
theorem add_subsemigroup.coe_set_mk {M : Type u_1} [has_add M] {s : set M} (h_mul : ∀ {a b : M}, a sb sa + b s) :
{carrier := s, add_mem' := h_mul} = s
@[simp]
theorem add_subsemigroup.mk_le_mk {M : Type u_1} [has_add M] {s t : set M} (h_mul : ∀ {a b : M}, a sb sa + b s) (h_mul' : ∀ {a b : M}, a tb ta + b t) :
{carrier := s, add_mem' := h_mul} {carrier := t, add_mem' := h_mul'} s t
@[simp]
theorem subsemigroup.mk_le_mk {M : Type u_1} [has_mul M] {s t : set M} (h_mul : ∀ {a b : M}, a sb sa * b s) (h_mul' : ∀ {a b : M}, a tb ta * b t) :
{carrier := s, mul_mem' := h_mul} {carrier := t, mul_mem' := h_mul'} s t
theorem add_subsemigroup.ext {M : Type u_1} [has_add M] {S T : add_subsemigroup M} (h : ∀ (x : M), x S x T) :
S = T

Two add_subsemigroups are equal if they have the same elements.

@[ext]
theorem subsemigroup.ext {M : Type u_1} [has_mul M] {S T : subsemigroup M} (h : ∀ (x : M), x S x T) :
S = T

Two subsemigroups are equal if they have the same elements.

@[protected]
def subsemigroup.copy {M : Type u_1} [has_mul M] (S : subsemigroup M) (s : set M) (hs : s = S) :

Copy a subsemigroup replacing carrier with a set that is equal to it.

Equations
@[protected]
def add_subsemigroup.copy {M : Type u_1} [has_add M] (S : add_subsemigroup M) (s : set M) (hs : s = S) :

Copy an additive subsemigroup replacing carrier with a set that is equal to it.

Equations
@[simp]
theorem subsemigroup.coe_copy {M : Type u_1} [has_mul M] {S : subsemigroup M} {s : set M} (hs : s = S) :
(S.copy s hs) = s
@[simp]
theorem add_subsemigroup.coe_copy {M : Type u_1} [has_add M] {S : add_subsemigroup M} {s : set M} (hs : s = S) :
(S.copy s hs) = s
theorem subsemigroup.copy_eq {M : Type u_1} [has_mul M] {S : subsemigroup M} {s : set M} (hs : s = S) :
S.copy s hs = S
theorem add_subsemigroup.copy_eq {M : Type u_1} [has_add M] {S : add_subsemigroup M} {s : set M} (hs : s = S) :
S.copy s hs = S
@[protected]
theorem subsemigroup.mul_mem {M : Type u_1} [has_mul M] (S : subsemigroup M) {x y : M} :
x Sy Sx * y S

A subsemigroup is closed under multiplication.

@[protected]
theorem add_subsemigroup.add_mem {M : Type u_1} [has_add M] (S : add_subsemigroup M) {x y : M} :
x Sy Sx + y S

An add_subsemigroup is closed under addition.

@[protected, instance]

The additive subsemigroup M of the magma M.

Equations
@[protected, instance]
def subsemigroup.has_top {M : Type u_1} [has_mul M] :

The subsemigroup M of the magma M.

Equations
@[protected, instance]
def subsemigroup.has_bot {M : Type u_1} [has_mul M] :

The trivial subsemigroup of a magma M.

Equations
@[protected, instance]

The trivial add_subsemigroup of an additive magma M.

Equations
@[protected, instance]
def subsemigroup.inhabited {M : Type u_1} [has_mul M] :
Equations
@[protected, instance]
Equations
theorem add_subsemigroup.not_mem_bot {M : Type u_1} [has_add M] {x : M} :
theorem subsemigroup.not_mem_bot {M : Type u_1} [has_mul M] {x : M} :
@[simp]
theorem subsemigroup.mem_top {M : Type u_1} [has_mul M] (x : M) :
@[simp]
theorem add_subsemigroup.mem_top {M : Type u_1} [has_add M] (x : M) :
@[simp]
theorem add_subsemigroup.coe_top {M : Type u_1} [has_add M] :
@[simp]
theorem subsemigroup.coe_top {M : Type u_1} [has_mul M] :
@[simp]
theorem add_subsemigroup.coe_bot {M : Type u_1} [has_add M] :
@[simp]
theorem subsemigroup.coe_bot {M : Type u_1} [has_mul M] :
@[protected, instance]

The inf of two add_subsemigroups is their intersection.

Equations
@[protected, instance]
def subsemigroup.has_inf {M : Type u_1} [has_mul M] :

The inf of two subsemigroups is their intersection.

Equations
@[simp]
theorem add_subsemigroup.coe_inf {M : Type u_1} [has_add M] (p p' : add_subsemigroup M) :
(p p') = p p'
@[simp]
theorem subsemigroup.coe_inf {M : Type u_1} [has_mul M] (p p' : subsemigroup M) :
(p p') = p p'
@[simp]
theorem add_subsemigroup.mem_inf {M : Type u_1} [has_add M] {p p' : add_subsemigroup M} {x : M} :
x p p' x p x p'
@[simp]
theorem subsemigroup.mem_inf {M : Type u_1} [has_mul M] {p p' : subsemigroup M} {x : M} :
x p p' x p x p'
@[protected, instance]
Equations
@[protected, instance]
def subsemigroup.has_Inf {M : Type u_1} [has_mul M] :
Equations
@[simp, norm_cast]
theorem add_subsemigroup.coe_Inf {M : Type u_1} [has_add M] (S : set (add_subsemigroup M)) :
(has_Inf.Inf S) = ⋂ (s : add_subsemigroup M) (H : s S), s
@[simp, norm_cast]
theorem subsemigroup.coe_Inf {M : Type u_1} [has_mul M] (S : set (subsemigroup M)) :
(has_Inf.Inf S) = ⋂ (s : subsemigroup M) (H : s S), s
theorem subsemigroup.mem_Inf {M : Type u_1} [has_mul M] {S : set (subsemigroup M)} {x : M} :
x has_Inf.Inf S ∀ (p : subsemigroup M), p Sx p
theorem add_subsemigroup.mem_Inf {M : Type u_1} [has_add M] {S : set (add_subsemigroup M)} {x : M} :
x has_Inf.Inf S ∀ (p : add_subsemigroup M), p Sx p
theorem subsemigroup.mem_infi {M : Type u_1} [has_mul M] {ι : Sort u_2} {S : ι → subsemigroup M} {x : M} :
(x ⨅ (i : ι), S i) ∀ (i : ι), x S i
theorem add_subsemigroup.mem_infi {M : Type u_1} [has_add M] {ι : Sort u_2} {S : ι → add_subsemigroup M} {x : M} :
(x ⨅ (i : ι), S i) ∀ (i : ι), x S i
@[simp, norm_cast]
theorem add_subsemigroup.coe_infi {M : Type u_1} [has_add M] {ι : Sort u_2} {S : ι → add_subsemigroup M} :
(⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
@[simp, norm_cast]
theorem subsemigroup.coe_infi {M : Type u_1} [has_mul M] {ι : Sort u_2} {S : ι → subsemigroup M} :
(⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
@[protected, instance]

subsemigroups of a monoid form a complete lattice.

Equations
@[protected, instance]

The add_subsemigroups of an add_monoid form a complete lattice.

Equations
@[protected, instance]
def subsemigroup.nontrivial {M : Type u_1} [has_mul M] [hn : nonempty M] :
@[protected, instance]
def subsemigroup.closure {M : Type u_1} [has_mul M] (s : set M) :

The subsemigroup generated by a set.

Equations
def add_subsemigroup.closure {M : Type u_1} [has_add M] (s : set M) :

The add_subsemigroup generated by a set

Equations
theorem subsemigroup.mem_closure {M : Type u_1} [has_mul M] {s : set M} {x : M} :
x subsemigroup.closure s ∀ (S : subsemigroup M), s Sx S
theorem add_subsemigroup.mem_closure {M : Type u_1} [has_add M] {s : set M} {x : M} :
@[simp]
theorem add_subsemigroup.subset_closure {M : Type u_1} [has_add M] {s : set M} :

The add_subsemigroup generated by a set includes the set.

@[simp]
theorem subsemigroup.subset_closure {M : Type u_1} [has_mul M] {s : set M} :

The subsemigroup generated by a set includes the set.

theorem add_subsemigroup.not_mem_of_not_mem_closure {M : Type u_1} [has_add M] {s : set M} {P : M} (hP : P add_subsemigroup.closure s) :
P s
theorem subsemigroup.not_mem_of_not_mem_closure {M : Type u_1} [has_mul M] {s : set M} {P : M} (hP : P subsemigroup.closure s) :
P s
@[simp]
theorem subsemigroup.closure_le {M : Type u_1} [has_mul M] {s : set M} {S : subsemigroup M} :

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

@[simp]
theorem add_subsemigroup.closure_le {M : Type u_1} [has_add M] {s : set M} {S : add_subsemigroup M} :

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

theorem add_subsemigroup.closure_mono {M : Type u_1} [has_add M] ⦃s t : set M⦄ (h : s t) :

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

theorem subsemigroup.closure_mono {M : Type u_1} [has_mul M] ⦃s t : set M⦄ (h : s t) :

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

theorem add_subsemigroup.closure_eq_of_le {M : Type u_1} [has_add M] {s : set M} {S : add_subsemigroup M} (h₁ : s S) (h₂ : S add_subsemigroup.closure s) :
theorem subsemigroup.closure_eq_of_le {M : Type u_1} [has_mul M] {s : set M} {S : subsemigroup M} (h₁ : s S) (h₂ : S subsemigroup.closure s) :
theorem add_subsemigroup.closure_induction {M : Type u_1} [has_add M] {s : set M} {p : M → Prop} {x : M} (h : x add_subsemigroup.closure s) (Hs : ∀ (x : M), x sp x) (Hmul : ∀ (x y : M), p xp yp (x + y)) :
p x

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.

theorem subsemigroup.closure_induction {M : Type u_1} [has_mul M] {s : set M} {p : M → Prop} {x : M} (h : x subsemigroup.closure s) (Hs : ∀ (x : M), x sp x) (Hmul : ∀ (x y : M), p xp yp (x * y)) :
p x

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 add_subsemigroup.closure_induction' {M : Type u_1} [has_add M] (s : set M) {p : Π (x : M), x add_subsemigroup.closure s → Prop} (Hs : ∀ (x : M) (h : x s), p x _) (Hmul : ∀ (x : M) (hx : x add_subsemigroup.closure s) (y : M) (hy : y add_subsemigroup.closure s), p x hxp y hyp (x + y) _) {x : M} (hx : x add_subsemigroup.closure s) :
p x hx

A dependent version of add_subsemigroup.closure_induction.

theorem subsemigroup.closure_induction' {M : Type u_1} [has_mul M] (s : set M) {p : Π (x : M), x subsemigroup.closure s → Prop} (Hs : ∀ (x : M) (h : x s), p x _) (Hmul : ∀ (x : M) (hx : x subsemigroup.closure s) (y : M) (hy : y subsemigroup.closure s), p x hxp y hyp (x * y) _) {x : M} (hx : x subsemigroup.closure s) :
p x hx

A dependent version of subsemigroup.closure_induction.

theorem add_subsemigroup.closure_induction₂ {M : Type u_1} [has_add M] {s : set M} {p : M → M → Prop} {x y : M} (hx : x add_subsemigroup.closure s) (hy : y add_subsemigroup.closure s) (Hs : ∀ (x : M), x s∀ (y : M), y sp x y) (Hmul_left : ∀ (x y z : M), p x zp y zp (x + y) z) (Hmul_right : ∀ (x y z : M), p z xp z yp z (x + y)) :
p x y

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

theorem subsemigroup.closure_induction₂ {M : Type u_1} [has_mul M] {s : set M} {p : M → M → Prop} {x y : M} (hx : x subsemigroup.closure s) (hy : y subsemigroup.closure s) (Hs : ∀ (x : M), x s∀ (y : M), y sp x y) (Hmul_left : ∀ (x y z : M), p x zp y zp (x * y) z) (Hmul_right : ∀ (x y z : M), p z xp z yp z (x * y)) :
p x y

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

theorem subsemigroup.dense_induction {M : Type u_1} [has_mul M] {p : M → Prop} (x : M) {s : set M} (hs : subsemigroup.closure s = ) (Hs : ∀ (x : M), x sp x) (Hmul : ∀ (x y : M), p xp yp (x * y)) :
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 add_subsemigroup.dense_induction {M : Type u_1} [has_add M] {p : M → Prop} (x : M) {s : set M} (hs : add_subsemigroup.closure s = ) (Hs : ∀ (x : M), x sp x) (Hmul : ∀ (x y : M), p xp yp (x + y)) :
p x

If s is a dense set in an additive monoid M, add_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).

@[protected]

closure forms a Galois insertion with the coercion to set.

Equations
@[protected]

closure forms a Galois insertion with the coercion to set.

Equations
@[simp]

Additive closure of an additive subsemigroup S equals S

@[simp]
theorem subsemigroup.closure_eq {M : Type u_1} [has_mul M] (S : subsemigroup M) :

Closure of a subsemigroup S equals S.

@[simp]
theorem add_subsemigroup.closure_Union {M : Type u_1} [has_add M] {ι : Sort u_2} (s : ι → set M) :
add_subsemigroup.closure (⋃ (i : ι), s i) = ⨆ (i : ι), add_subsemigroup.closure (s i)
theorem subsemigroup.closure_Union {M : Type u_1} [has_mul M] {ι : Sort u_2} (s : ι → set M) :
subsemigroup.closure (⋃ (i : ι), s i) = ⨆ (i : ι), subsemigroup.closure (s i)
@[simp]
@[simp]
theorem subsemigroup.closure_singleton_le_iff_mem {M : Type u_1} [has_mul M] (m : M) (p : subsemigroup M) :
theorem add_subsemigroup.mem_supr {M : Type u_1} [has_add M] {ι : Sort u_2} (p : ι → add_subsemigroup M) {m : M} :
(m ⨆ (i : ι), p i) ∀ (N : add_subsemigroup M), (∀ (i : ι), p i N)m N
theorem subsemigroup.mem_supr {M : Type u_1} [has_mul M] {ι : Sort u_2} (p : ι → subsemigroup M) {m : M} :
(m ⨆ (i : ι), p i) ∀ (N : subsemigroup M), (∀ (i : ι), p i N)m N
theorem add_subsemigroup.supr_eq_closure {M : Type u_1} [has_add M] {ι : Sort u_2} (p : ι → add_subsemigroup M) :
(⨆ (i : ι), p i) = add_subsemigroup.closure (⋃ (i : ι), (p i))
theorem subsemigroup.supr_eq_closure {M : Type u_1} [has_mul M] {ι : Sort u_2} (p : ι → subsemigroup M) :
(⨆ (i : ι), p i) = subsemigroup.closure (⋃ (i : ι), (p i))
def add_hom.eq_mlocus {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f g : add_hom M N) :

The additive subsemigroup of elements x : M such that f x = g x

Equations
def mul_hom.eq_mlocus {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f g : M →ₙ* N) :

The subsemigroup of elements x : M such that f x = g x

Equations
theorem add_hom.eq_on_mclosure {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f g : add_hom M N} {s : set M} (h : set.eq_on f g s) :

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

theorem mul_hom.eq_on_mclosure {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f g : M →ₙ* N} {s : set M} (h : set.eq_on f g s) :

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

theorem add_hom.eq_of_eq_on_mtop {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {f g : add_hom M N} (h : set.eq_on f g ) :
f = g
theorem mul_hom.eq_of_eq_on_mtop {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {f g : M →ₙ* N} (h : set.eq_on f g ) :
f = g
theorem add_hom.eq_of_eq_on_mdense {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] {s : set M} (hs : add_subsemigroup.closure s = ) {f g : add_hom M N} (h : set.eq_on f g s) :
f = g
theorem mul_hom.eq_of_eq_on_mdense {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] {s : set M} (hs : subsemigroup.closure s = ) {f g : M →ₙ* N} (h : set.eq_on f g s) :
f = g
def mul_hom.of_mdense {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 sf (x * y) = f x * f y) :

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

Equations
def add_hom.of_mdense {M : Type u_1} {N : Type u_2} [add_semigroup M] [add_semigroup N] {s : set M} (f : M → N) (hs : add_subsemigroup.closure s = ) (hmul : ∀ (x y : M), y sf (x + y) = f x + f y) :

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

Equations
@[simp, norm_cast]
theorem add_hom.coe_of_mdense {M : Type u_1} {N : Type u_2} [add_semigroup M] [add_semigroup N] {s : set M} (f : M → N) (hs : add_subsemigroup.closure s = ) (hmul : ∀ (x y : M), y sf (x + y) = f x + f y) :
(add_hom.of_mdense f hs hmul) = f
@[simp, norm_cast]
theorem mul_hom.coe_of_mdense {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 sf (x * y) = f x * f y) :
(mul_hom.of_mdense f hs hmul) = f