Subsemigroups: definition and `complete_lattice` structure #

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

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 #

subsemigroup M: the type of bundled subsemigroup of a magma M; the underlying set is given in the carrier field of the structure, and should be accessed through coercion as in (S : set M).
add_subsemigroup M : the type of bundled subsemigroups of an additive magma M.

For each of the following definitions in the subsemigroup namespace, there is a corresponding definition in the add_subsemigroup 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 galois_insertion;

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

source

@[class]

structure mul_mem_class (S : Type u_4) (M : Type u_5) [has_mul M] [set_like S M] :

Prop

mul_mem : ∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a * b ∈ s

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

Instances of this typeclass

source

@[class]

structure add_mem_class (S : Type u_4) (M : Type u_5) [has_add M] [set_like S M] :

Prop

add_mem : ∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a + b ∈ s

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

Instances of this typeclass

source

structure subsemigroup (M : Type u_4) [has_mul M] :

Type u_4

carrier : set M
mul_mem' : ∀ {a b : M}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier

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

Instances for subsemigroup

source

structure add_subsemigroup (M : Type u_4) [has_add M] :

Type u_4

carrier : set M
add_mem' : ∀ {a b : M}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier

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

Instances for add_subsemigroup

source

@[protected, instance]

def subsemigroup.set_like {M : Type u_1} [has_mul M] :

set_like (subsemigroup M) M

Equations

subsemigroup.set_like = {coe := subsemigroup.carrier _inst_1, coe_injective' := _}

source

@[protected, instance]

def add_subsemigroup.set_like {M : Type u_1} [has_add M] :

set_like (add_subsemigroup M) M

Equations

add_subsemigroup.set_like = {coe := add_subsemigroup.carrier _inst_1, coe_injective' := _}

source

@[protected, instance]

def subsemigroup.mul_mem_class {M : Type u_1} [has_mul M] :

mul_mem_class (subsemigroup M) M

source

@[protected, instance]

def add_subsemigroup.add_mem_class {M : Type u_1} [has_add M] :

add_mem_class (add_subsemigroup M) M

source

def add_subsemigroup.simps.coe {M : Type u_1} [has_add M] (S : add_subsemigroup M) :

set M

See Note [custom simps projection]

Equations

add_subsemigroup.simps.coe S = ↑S

source

def subsemigroup.simps.coe {M : Type u_1} [has_mul M] (S : subsemigroup M) :

set M

See Note [custom simps projection]

Equations

subsemigroup.simps.coe S = ↑S

source

@[simp]

theorem add_subsemigroup.mem_carrier {M : Type u_1} [has_add M] {s : add_subsemigroup M} {x : M} :

x ∈ s.carrier ↔ x ∈ s

source

@[simp]

theorem subsemigroup.mem_carrier {M : Type u_1} [has_mul M] {s : subsemigroup M} {x : M} :

x ∈ s.carrier ↔ x ∈ s

source

@[simp]

theorem add_subsemigroup.mem_mk {M : Type u_1} [has_add M] {s : set M} {x : M} (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) :

x ∈ {carrier := s, add_mem' := h_mul} ↔ x ∈ s

source

@[simp]

theorem subsemigroup.mem_mk {M : Type u_1} [has_mul M] {s : set M} {x : M} (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s) :

x ∈ {carrier := s, mul_mem' := h_mul} ↔ x ∈ s

source

@[simp]

theorem subsemigroup.coe_set_mk {M : Type u_1} [has_mul M] {s : set M} (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s) :

↑{carrier := s, mul_mem' := h_mul} = s

source

@[simp]

theorem add_subsemigroup.coe_set_mk {M : Type u_1} [has_add M] {s : set M} (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) :

↑{carrier := s, add_mem' := h_mul} = s

source

@[simp]

theorem add_subsemigroup.mk_le_mk {M : Type u_1} [has_add M] {s t : set M} (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) (h_mul' : ∀ {a b : M}, a ∈ t → b ∈ t → a + b ∈ t) :

{carrier := s, add_mem' := h_mul} ≤ {carrier := t, add_mem' := h_mul'} ↔ s ⊆ t

source

@[simp]

theorem subsemigroup.mk_le_mk {M : Type u_1} [has_mul M] {s t : set M} (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s) (h_mul' : ∀ {a b : M}, a ∈ t → b ∈ t → a * b ∈ t) :

{carrier := s, mul_mem' := h_mul} ≤ {carrier := t, mul_mem' := h_mul'} ↔ s ⊆ t

source

@[ext]

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.

source

@[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.

source

@[protected]

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

subsemigroup M

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

Equations

S.copy s hs = {carrier := s, mul_mem' := _}

source

@[protected]

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

add_subsemigroup M

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

Equations

S.copy s hs = {carrier := s, add_mem' := _}

source

@[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

source

@[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

source

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

source

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

source

@[protected]

theorem subsemigroup.mul_mem {M : Type u_1} [has_mul M] (S : subsemigroup M) {x y : M} :

x ∈ S → y ∈ S → x * y ∈ S

A subsemigroup is closed under multiplication.

source

@[protected]

theorem add_subsemigroup.add_mem {M : Type u_1} [has_add M] (S : add_subsemigroup M) {x y : M} :

x ∈ S → y ∈ S → x + y ∈ S

An add_subsemigroup is closed under addition.

source

@[protected, instance]

def add_subsemigroup.has_top {M : Type u_1} [has_add M] :

has_top (add_subsemigroup M)

The additive subsemigroup M of the magma M.

Equations

add_subsemigroup.has_top = {top := {carrier := set.univ M, add_mem' := _}}

source

@[protected, instance]

def subsemigroup.has_top {M : Type u_1} [has_mul M] :

has_top (subsemigroup M)

The subsemigroup M of the magma M.

Equations

subsemigroup.has_top = {top := {carrier := set.univ M, mul_mem' := _}}

source

@[protected, instance]

def subsemigroup.has_bot {M : Type u_1} [has_mul M] :

has_bot (subsemigroup M)

The trivial subsemigroup ∅ of a magma M.

Equations

subsemigroup.has_bot = {bot := {carrier := ∅, mul_mem' := _}}

source

@[protected, instance]

def add_subsemigroup.has_bot {M : Type u_1} [has_add M] :

has_bot (add_subsemigroup M)

The trivial add_subsemigroup ∅ of an additive magma M.

Equations

add_subsemigroup.has_bot = {bot := {carrier := ∅, add_mem' := _}}

source

@[protected, instance]

def subsemigroup.inhabited {M : Type u_1} [has_mul M] :

inhabited (subsemigroup M)

Equations

subsemigroup.inhabited = {default := ⊥}

source

@[protected, instance]

def add_subsemigroup.inhabited {M : Type u_1} [has_add M] :

inhabited (add_subsemigroup M)

Equations

add_subsemigroup.inhabited = {default := ⊥}

source

theorem add_subsemigroup.not_mem_bot {M : Type u_1} [has_add M] {x : M} :

x ∉ ⊥

source

theorem subsemigroup.not_mem_bot {M : Type u_1} [has_mul M] {x : M} :

x ∉ ⊥

source

@[simp]

theorem subsemigroup.mem_top {M : Type u_1} [has_mul M] (x : M) :

x ∈ ⊤

source

@[simp]

theorem add_subsemigroup.mem_top {M : Type u_1} [has_add M] (x : M) :

x ∈ ⊤

source

@[simp]

theorem add_subsemigroup.coe_top {M : Type u_1} [has_add M] :

↑⊤ = set.univ

source

@[simp]

theorem subsemigroup.coe_top {M : Type u_1} [has_mul M] :

↑⊤ = set.univ

source

@[simp]

theorem add_subsemigroup.coe_bot {M : Type u_1} [has_add M] :

↑⊥ = ∅

source

@[simp]

theorem subsemigroup.coe_bot {M : Type u_1} [has_mul M] :

↑⊥ = ∅

source

@[protected, instance]

def add_subsemigroup.has_inf {M : Type u_1} [has_add M] :

has_inf (add_subsemigroup M)

The inf of two add_subsemigroups is their intersection.

Equations

add_subsemigroup.has_inf = {inf := λ (S₁ S₂ : add_subsemigroup M), {carrier := ↑S₁ ∩ ↑S₂, add_mem' := _}}

source

@[protected, instance]

def subsemigroup.has_inf {M : Type u_1} [has_mul M] :

has_inf (subsemigroup M)

The inf of two subsemigroups is their intersection.

Equations

subsemigroup.has_inf = {inf := λ (S₁ S₂ : subsemigroup M), {carrier := ↑S₁ ∩ ↑S₂, mul_mem' := _}}

source

@[simp]

theorem add_subsemigroup.coe_inf {M : Type u_1} [has_add M] (p p' : add_subsemigroup M) :

↑(p ⊓ p') = ↑p ∩ ↑p'

source

@[simp]

theorem subsemigroup.coe_inf {M : Type u_1} [has_mul M] (p p' : subsemigroup M) :

↑(p ⊓ p') = ↑p ∩ ↑p'

source

@[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'

source

@[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'

source

@[protected, instance]

def add_subsemigroup.has_Inf {M : Type u_1} [has_add M] :

has_Inf (add_subsemigroup M)

Equations

add_subsemigroup.has_Inf = {Inf := λ (s : set (add_subsemigroup M)), {carrier := ⋂ (t : add_subsemigroup M) (H : t ∈ s), ↑t, add_mem' := _}}

source

@[protected, instance]

def subsemigroup.has_Inf {M : Type u_1} [has_mul M] :

has_Inf (subsemigroup M)

Equations

subsemigroup.has_Inf = {Inf := λ (s : set (subsemigroup M)), {carrier := ⋂ (t : subsemigroup M) (H : t ∈ s), ↑t, mul_mem' := _}}

source

@[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

source

@[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

source

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 ∈ S → x ∈ p

source

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 ∈ S → x ∈ p

source

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

source

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

source

@[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)

source

@[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)

source

@[protected, instance]

def subsemigroup.complete_lattice {M : Type u_1} [has_mul M] :

complete_lattice (subsemigroup M)

subsemigroups of a monoid form a complete lattice.

Equations

subsemigroup.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (subsemigroup M) subsemigroup.complete_lattice._proof_1), le := has_le.le (preorder.to_has_le (subsemigroup M)), lt := has_lt.lt (preorder.to_has_lt (subsemigroup M)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf subsemigroup.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (subsemigroup M) subsemigroup.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := has_Inf.Inf subsemigroup.has_Inf, Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}

source

@[protected, instance]

def add_subsemigroup.complete_lattice {M : Type u_1} [has_add M] :

complete_lattice (add_subsemigroup M)

The add_subsemigroups of an add_monoid form a complete lattice.

Equations

add_subsemigroup.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (add_subsemigroup M) add_subsemigroup.complete_lattice._proof_1), le := has_le.le (preorder.to_has_le (add_subsemigroup M)), lt := has_lt.lt (preorder.to_has_lt (add_subsemigroup M)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf add_subsemigroup.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (add_subsemigroup M) add_subsemigroup.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := has_Inf.Inf add_subsemigroup.has_Inf, Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}

source

@[simp]

theorem add_subsemigroup.subsingleton_of_subsingleton {M : Type u_1} [has_add M] [subsingleton (add_subsemigroup M)] :

subsingleton M

source

@[simp]

theorem subsemigroup.subsingleton_of_subsingleton {M : Type u_1} [has_mul M] [subsingleton (subsemigroup M)] :

subsingleton M

source

@[protected, instance]

def subsemigroup.nontrivial {M : Type u_1} [has_mul M] [hn : nonempty M] :

nontrivial (subsemigroup M)

source

@[protected, instance]

def add_subsemigroup.nontrivial {M : Type u_1} [has_add M] [hn : nonempty M] :

nontrivial (add_subsemigroup M)

source

def subsemigroup.closure {M : Type u_1} [has_mul M] (s : set M) :

subsemigroup M

The subsemigroup generated by a set.

Equations

subsemigroup.closure s = has_Inf.Inf {S : subsemigroup M | s ⊆ ↑S}

source

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

add_subsemigroup M

The add_subsemigroup generated by a set

Equations

add_subsemigroup.closure s = has_Inf.Inf {S : add_subsemigroup M | s ⊆ ↑S}

source

theorem subsemigroup.mem_closure {M : Type u_1} [has_mul M] {s : set M} {x : M} :

x ∈ subsemigroup.closure s ↔ ∀ (S : subsemigroup M), s ⊆ ↑S → x ∈ S

source

theorem add_subsemigroup.mem_closure {M : Type u_1} [has_add M] {s : set M} {x : M} :

x ∈ add_subsemigroup.closure s ↔ ∀ (S : add_subsemigroup M), s ⊆ ↑S → x ∈ S

source

@[simp]

theorem add_subsemigroup.subset_closure {M : Type u_1} [has_add M] {s : set M} :

s ⊆ ↑(add_subsemigroup.closure s)

The add_subsemigroup generated by a set includes the set.

source

@[simp]

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

s ⊆ ↑(subsemigroup.closure s)

The subsemigroup generated by a set includes the set.

source

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

source

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

source

@[simp]

theorem subsemigroup.closure_le {M : Type u_1} [has_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.

source

@[simp]

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

add_subsemigroup.closure s ≤ S ↔ s ⊆ ↑S

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

source

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

add_subsemigroup.closure s ≤ add_subsemigroup.closure t

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

source

theorem subsemigroup.closure_mono {M : Type u_1} [has_mul M] ⦃s 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.

source

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) :

add_subsemigroup.closure s = S

source

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) :

subsemigroup.closure s = S

source

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 ∈ s → p x) (Hmul : ∀ (x y : M), p x → p y → p (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.

source

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 ∈ s → p x) (Hmul : ∀ (x y : M), p x → p y → p (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.

source

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 hx → p y hy → p (x + y) _) {x : M} (hx : x ∈ add_subsemigroup.closure s) :

p x hx

A dependent version of add_subsemigroup.closure_induction.

source

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 hx → p y hy → p (x * y) _) {x : M} (hx : x ∈ subsemigroup.closure s) :

p x hx

A dependent version of subsemigroup.closure_induction.

source

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 ∈ s → p x y) (Hmul_left : ∀ (x y z : M), p x z → p y z → p (x + y) z) (Hmul_right : ∀ (x y z : M), p z x → p z y → p z (x + y)) :

p x y

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

source

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 ∈ s → p x y) (Hmul_left : ∀ (x y z : M), p x z → p y z → p (x * y) z) (Hmul_right : ∀ (x y z : M), p z x → p z y → p z (x * y)) :

p x y

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

source

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 ∈ s → p x) (Hmul : ∀ (x y : M), p x → p y → p (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).

source

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 ∈ s → p x) (Hmul : ∀ (x y : M), p x → p y → p (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).

source

@[protected]

def add_subsemigroup.gi (M : Type u_1) [has_add M] :

galois_insertion add_subsemigroup.closure coe

closure forms a Galois insertion with the coercion to set.

Equations

add_subsemigroup.gi M = {choice := λ (s : set M) (_x : ↑(add_subsemigroup.closure s) ≤ s), add_subsemigroup.closure s, gc := _, le_l_u := _, choice_eq := _}

source

@[protected]

def subsemigroup.gi (M : Type u_1) [has_mul M] :

galois_insertion subsemigroup.closure coe

closure forms a Galois insertion with the coercion to set.

Equations

subsemigroup.gi M = {choice := λ (s : set M) (_x : ↑(subsemigroup.closure s) ≤ s), subsemigroup.closure s, gc := _, le_l_u := _, choice_eq := _}

source

@[simp]

theorem add_subsemigroup.closure_eq {M : Type u_1} [has_add M] (S : add_subsemigroup M) :

add_subsemigroup.closure ↑S = S

Additive closure of an additive subsemigroup S equals S

source

@[simp]

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

subsemigroup.closure ↑S = S

Closure of a subsemigroup S equals S.

source

@[simp]

theorem add_subsemigroup.closure_empty {M : Type u_1} [has_add M] :

add_subsemigroup.closure ∅ = ⊥

source

@[simp]

theorem subsemigroup.closure_empty {M : Type u_1} [has_mul M] :

subsemigroup.closure ∅ = ⊥

source

@[simp]

theorem subsemigroup.closure_univ {M : Type u_1} [has_mul M] :

subsemigroup.closure set.univ = ⊤

source

@[simp]

theorem add_subsemigroup.closure_univ {M : Type u_1} [has_add M] :

add_subsemigroup.closure set.univ = ⊤

source

theorem add_subsemigroup.closure_union {M : Type u_1} [has_add M] (s t : set M) :

add_subsemigroup.closure (s ∪ t) = add_subsemigroup.closure s ⊔ add_subsemigroup.closure t

source

theorem subsemigroup.closure_union {M : Type u_1} [has_mul M] (s t : set M) :

subsemigroup.closure (s ∪ t) = subsemigroup.closure s ⊔ subsemigroup.closure t

source

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)

source

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)

source

@[simp]

theorem add_subsemigroup.closure_singleton_le_iff_mem {M : Type u_1} [has_add M] (m : M) (p : add_subsemigroup M) :

add_subsemigroup.closure {m} ≤ p ↔ m ∈ p

source

@[simp]

theorem subsemigroup.closure_singleton_le_iff_mem {M : Type u_1} [has_mul M] (m : M) (p : subsemigroup M) :

subsemigroup.closure {m} ≤ p ↔ m ∈ p

source

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

source

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

source

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))

source

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))

source

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) :

add_subsemigroup M

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

Equations

f.eq_mlocus g = {carrier := {x : M | ⇑f x = ⇑g x}, add_mem' := _}

source

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

subsemigroup M

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

Equations

f.eq_mlocus g = {carrier := {x : M | ⇑f x = ⇑g x}, mul_mem' := _}

source

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) :

set.eq_on ⇑f ⇑g ↑(add_subsemigroup.closure s)

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

source

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) :

set.eq_on ⇑f ⇑g ↑(subsemigroup.closure s)

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

source

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

source

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

source

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

source

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

source

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 ∈ 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 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

mul_hom.of_mdense f hs hmul = {to_fun := f, map_mul' := _}

source

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 ∈ s → f (x + y) = f x + f y) :

add_hom M N

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

add_hom.of_mdense f hs hmul = {to_fun := f, map_add' := _}

source

@[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 ∈ s → f (x + y) = f x + f y) :

⇑(add_hom.of_mdense f hs hmul) = f

source

@[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 ∈ s → f (x * y) = f x * f y) :

⇑(mul_hom.of_mdense f hs hmul) = f

Subsemigroups: definition and complete_lattice structure #

Main definitions #

Implementation notes #

Tags #

Subsemigroups: definition and `complete_lattice` structure #