mathlib3 documentation

group_theory.submonoid.basic

Submonoids: 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 submonoids. We also define a complete_lattice structure on submonoids, define the closure of a set as the minimal submonoid that includes this set, and prove a few results about extending properties from a dense set (i.e. a set with closure s = ⊤) to the whole monoid, see submonoid.dense_induction and monoid_hom.of_mclosure_eq_top_left/monoid_hom.of_mclosure_eq_top_right.

Main definitions #

submonoid M: the type of bundled submonoids of a monoid 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_submonoid M : the type of bundled submonoids of an additive monoid M.

For each of the following definitions in the submonoid namespace, there is a corresponding definition in the add_submonoid namespace.

submonoid.copy : copy of a submonoid with carrier replaced by a set that is equal but possibly not definitionally equal to the carrier of the original submonoid.
submonoid.closure : monoid closure of a set, i.e., the least submonoid that includes the set.
submonoid.gi : closure : set M → submonoid M and coercion coe : submonoid M → set M form a galois_insertion;
monoid_hom.eq_mlocus: the submonoid of elements x : M such that f x = g x;
monoid_hom.of_mclosure_eq_top_right: if a map f : M → N between two monoids satisfies f 1 = 1 and f (x * y) = f x * f y for y from some dense set s, then f is a monoid homomorphism. E.g., if f : ℕ → M satisfies f 0 = 0 and f (x + 1) = f x + f 1, then f is an additive monoid homomorphism.

Implementation notes #

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

Note that submonoid M does not actually require monoid M, instead requiring only the weaker mul_one_class M.

This file is designed to have very few dependencies. In particular, it should not use natural numbers. submonoid is implemented by extending subsemigroup requiring one_mem'.

Tags #

submonoid, submonoids

@[class]

structure one_mem_class (S : Type u_4) (M : Type u_5) [has_one M] [set_like S M] :

Prop

one_mem : ∀ (s : S), 1 ∈ s

one_mem_class S M says S is a type of subsets s ≤ M, such that 1 ∈ s for all s.

Instances of this typeclass

@[class]

structure zero_mem_class (S : Type u_4) (M : Type u_5) [has_zero M] [set_like S M] :

Prop

zero_mem : ∀ (s : S), 0 ∈ s

zero_mem_class S M says S is a type of subsets s ≤ M, such that 0 ∈ s for all s.

Instances of this typeclass

structure submonoid (M : Type u_4) [mul_one_class M] :

Type u_4

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

A submonoid of a monoid M is a subset containing 1 and closed under multiplication.

Instances for submonoid

def submonoid.to_subsemigroup {M : Type u_4} [mul_one_class M] (self : submonoid M) :

A submonoid of a monoid M can be considered as a subsemigroup of that monoid.

@[class]

structure submonoid_class (S : Type u_4) (M : Type u_5) [mul_one_class M] [set_like S M] :

Prop

to_mul_mem_class : mul_mem_class S M
to_one_mem_class : one_mem_class S M

submonoid_class S M says S is a type of subsets s ≤ M that contain 1 and are closed under (*)

Instances of this typeclass

def add_submonoid.to_add_subsemigroup {M : Type u_4} [add_zero_class M] (self : add_submonoid M) :

add_subsemigroup M

An additive submonoid of an additive monoid M can be considered as an additive subsemigroup of that additive monoid.

structure add_submonoid (M : Type u_4) [add_zero_class M] :

Type u_4

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

An additive submonoid of an additive monoid M is a subset containing 0 and closed under addition.

Instances for add_submonoid

@[class]

structure add_submonoid_class (S : Type u_4) (M : Type u_5) [add_zero_class M] [set_like S M] :

Prop

to_add_mem_class : add_mem_class S M
to_zero_mem_class : zero_mem_class S M

add_submonoid_class S M says S is a type of subsets s ≤ M that contain 0 and are closed under (+)

Instances of this typeclass

theorem pow_mem {M : Type u_1} [monoid M] {A : Type u_2} [set_like A M] [submonoid_class A M] {S : A} {x : M} (hx : x ∈ S) (n : ℕ) :

x ^ n ∈ S

theorem nsmul_mem {M : Type u_1} [add_monoid M] {A : Type u_2} [set_like A M] [add_submonoid_class A M] {S : A} {x : M} (hx : x ∈ S) (n : ℕ) :

n • x ∈ S

@[protected, instance]

def add_submonoid.set_like {M : Type u_1} [add_zero_class M] :

set_like (add_submonoid M) M

Equations

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

@[protected, instance]

def submonoid.set_like {M : Type u_1} [mul_one_class M] :

set_like (submonoid M) M

Equations

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

@[protected, instance]

def add_submonoid.add_submonoid_class {M : Type u_1} [add_zero_class M] :

add_submonoid_class (add_submonoid M) M

@[protected, instance]

def submonoid.submonoid_class {M : Type u_1} [mul_one_class M] :

submonoid_class (submonoid M) M

def add_submonoid.simps.coe {M : Type u_1} [add_zero_class M] (S : add_submonoid M) :

See Note [custom simps projection]

Equations

add_submonoid.simps.coe S = ↑S

def submonoid.simps.coe {M : Type u_1} [mul_one_class M] (S : submonoid M) :

See Note [custom simps projection]

Equations

submonoid.simps.coe S = ↑S

@[simp]

theorem add_submonoid.mem_carrier {M : Type u_1} [add_zero_class M] {s : add_submonoid M} {x : M} :

x ∈ s.carrier ↔ x ∈ s

@[simp]

theorem submonoid.mem_carrier {M : Type u_1} [mul_one_class M] {s : submonoid M} {x : M} :

x ∈ s.carrier ↔ x ∈ s

@[simp]

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

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

@[simp]

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

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

@[simp]

theorem add_submonoid.coe_set_mk {M : Type u_1} [add_zero_class M] {s : set M} (h_one : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) (h_mul : 0 ∈ s) :

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

@[simp]

theorem submonoid.coe_set_mk {M : Type u_1} [mul_one_class M] {s : set M} (h_one : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s) (h_mul : 1 ∈ s) :

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

@[simp]

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

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

@[simp]

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

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

@[ext]

theorem add_submonoid.ext {M : Type u_1} [add_zero_class M] {S T : add_submonoid M} (h : ∀ (x : M), x ∈ S ↔ x ∈ T) :

S = T

Two add_submonoids are equal if they have the same elements.

@[ext]

theorem submonoid.ext {M : Type u_1} [mul_one_class M] {S T : submonoid M} (h : ∀ (x : M), x ∈ S ↔ x ∈ T) :

S = T

Two submonoids are equal if they have the same elements.

@[protected]

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

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

Equations

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

@[protected]

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

add_submonoid M

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

Equations

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

@[simp]

theorem add_submonoid.coe_copy {M : Type u_1} [add_zero_class M] {S : add_submonoid M} {s : set M} (hs : s = ↑S) :

↑(S.copy s hs) = s

@[simp]

theorem submonoid.coe_copy {M : Type u_1} [mul_one_class M] {S : submonoid M} {s : set M} (hs : s = ↑S) :

↑(S.copy s hs) = s

theorem submonoid.copy_eq {M : Type u_1} [mul_one_class M] {S : submonoid M} {s : set M} (hs : s = ↑S) :

S.copy s hs = S

theorem add_submonoid.copy_eq {M : Type u_1} [add_zero_class M] {S : add_submonoid M} {s : set M} (hs : s = ↑S) :

S.copy s hs = S

@[protected]

theorem submonoid.one_mem {M : Type u_1} [mul_one_class M] (S : submonoid M) :

1 ∈ S

A submonoid contains the monoid's 1.

@[protected]

theorem add_submonoid.zero_mem {M : Type u_1} [add_zero_class M] (S : add_submonoid M) :

0 ∈ S

An add_submonoid contains the monoid's 0.

@[protected]

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

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

An add_submonoid is closed under addition.

@[protected]

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

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

A submonoid is closed under multiplication.

@[protected, instance]

def submonoid.has_top {M : Type u_1} [mul_one_class M] :

has_top (submonoid M)

The submonoid M of the monoid M.

Equations

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

@[protected, instance]

def add_submonoid.has_top {M : Type u_1} [add_zero_class M] :

has_top (add_submonoid M)

The additive submonoid M of the add_monoid M.

Equations

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

@[protected, instance]

def add_submonoid.has_bot {M : Type u_1} [add_zero_class M] :

has_bot (add_submonoid M)

The trivial add_submonoid {0} of an add_monoid M.

Equations

add_submonoid.has_bot = {bot := {carrier := {0}, add_mem' := _, zero_mem' := _}}

@[protected, instance]

def submonoid.has_bot {M : Type u_1} [mul_one_class M] :

has_bot (submonoid M)

The trivial submonoid {1} of an monoid M.

Equations

submonoid.has_bot = {bot := {carrier := {1}, mul_mem' := _, one_mem' := _}}

@[protected, instance]

def add_submonoid.inhabited {M : Type u_1} [add_zero_class M] :

inhabited (add_submonoid M)

Equations

add_submonoid.inhabited = {default := ⊥}

@[protected, instance]

def submonoid.inhabited {M : Type u_1} [mul_one_class M] :

inhabited (submonoid M)

Equations

submonoid.inhabited = {default := ⊥}

@[simp]

theorem submonoid.mem_bot {M : Type u_1} [mul_one_class M] {x : M} :

x ∈ ⊥ ↔ x = 1

@[simp]

theorem add_submonoid.mem_bot {M : Type u_1} [add_zero_class M] {x : M} :

x ∈ ⊥ ↔ x = 0

@[simp]

theorem submonoid.mem_top {M : Type u_1} [mul_one_class M] (x : M) :

@[simp]

theorem add_submonoid.mem_top {M : Type u_1} [add_zero_class M] (x : M) :

@[simp]

theorem add_submonoid.coe_top {M : Type u_1} [add_zero_class M] :

↑⊤ = set.univ

@[simp]

theorem submonoid.coe_top {M : Type u_1} [mul_one_class M] :

↑⊤ = set.univ

@[simp]

theorem submonoid.coe_bot {M : Type u_1} [mul_one_class M] :

@[simp]

theorem add_submonoid.coe_bot {M : Type u_1} [add_zero_class M] :

@[protected, instance]

def add_submonoid.has_inf {M : Type u_1} [add_zero_class M] :

has_inf (add_submonoid M)

The inf of two add_submonoids is their intersection.

Equations

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

@[protected, instance]

def submonoid.has_inf {M : Type u_1} [mul_one_class M] :

has_inf (submonoid M)

The inf of two submonoids is their intersection.

Equations

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

@[simp]

theorem add_submonoid.coe_inf {M : Type u_1} [add_zero_class M] (p p' : add_submonoid M) :

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

@[simp]

theorem submonoid.coe_inf {M : Type u_1} [mul_one_class M] (p p' : submonoid M) :

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

@[simp]

theorem add_submonoid.mem_inf {M : Type u_1} [add_zero_class M] {p p' : add_submonoid M} {x : M} :

x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

@[simp]

theorem submonoid.mem_inf {M : Type u_1} [mul_one_class M] {p p' : submonoid M} {x : M} :

x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

@[protected, instance]

def submonoid.has_Inf {M : Type u_1} [mul_one_class M] :

has_Inf (submonoid M)

Equations

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

@[protected, instance]

def add_submonoid.has_Inf {M : Type u_1} [add_zero_class M] :

has_Inf (add_submonoid M)

Equations

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

@[simp, norm_cast]

theorem submonoid.coe_Inf {M : Type u_1} [mul_one_class M] (S : set (submonoid M)) :

↑(has_Inf.Inf S) = ⋂ (s : submonoid M) (H : s ∈ S), ↑s

@[simp, norm_cast]

theorem add_submonoid.coe_Inf {M : Type u_1} [add_zero_class M] (S : set (add_submonoid M)) :

↑(has_Inf.Inf S) = ⋂ (s : add_submonoid M) (H : s ∈ S), ↑s

theorem add_submonoid.mem_Inf {M : Type u_1} [add_zero_class M] {S : set (add_submonoid M)} {x : M} :

x ∈ has_Inf.Inf S ↔ ∀ (p : add_submonoid M), p ∈ S → x ∈ p

theorem submonoid.mem_Inf {M : Type u_1} [mul_one_class M] {S : set (submonoid M)} {x : M} :

x ∈ has_Inf.Inf S ↔ ∀ (p : submonoid M), p ∈ S → x ∈ p

theorem submonoid.mem_infi {M : Type u_1} [mul_one_class M] {ι : Sort u_2} {S : ι → submonoid M} {x : M} :

(x ∈ ⨅ (i : ι), S i) ↔ ∀ (i : ι), x ∈ S i

theorem add_submonoid.mem_infi {M : Type u_1} [add_zero_class M] {ι : Sort u_2} {S : ι → add_submonoid M} {x : M} :

(x ∈ ⨅ (i : ι), S i) ↔ ∀ (i : ι), x ∈ S i

@[simp, norm_cast]

theorem submonoid.coe_infi {M : Type u_1} [mul_one_class M] {ι : Sort u_2} {S : ι → submonoid M} :

(↑⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)

@[simp, norm_cast]

theorem add_submonoid.coe_infi {M : Type u_1} [add_zero_class M] {ι : Sort u_2} {S : ι → add_submonoid M} :

(↑⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)

@[protected, instance]

def submonoid.complete_lattice {M : Type u_1} [mul_one_class M] :

complete_lattice (submonoid M)

Submonoids of a monoid form a complete lattice.

Equations

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

@[protected, instance]

def add_submonoid.complete_lattice {M : Type u_1} [add_zero_class M] :

complete_lattice (add_submonoid M)

The add_submonoids of an add_monoid form a complete lattice.

Equations

add_submonoid.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (add_submonoid M) add_submonoid.complete_lattice._proof_1), le := has_le.le (preorder.to_has_le (add_submonoid M)), lt := has_lt.lt (preorder.to_has_lt (add_submonoid 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_submonoid.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (add_submonoid M) add_submonoid.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := has_Inf.Inf add_submonoid.has_Inf, Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}

@[simp]

theorem add_submonoid.subsingleton_iff {M : Type u_1} [add_zero_class M] :

subsingleton (add_submonoid M) ↔ subsingleton M

@[simp]

theorem submonoid.subsingleton_iff {M : Type u_1} [mul_one_class M] :

subsingleton (submonoid M) ↔ subsingleton M

@[simp]

theorem add_submonoid.nontrivial_iff {M : Type u_1} [add_zero_class M] :

nontrivial (add_submonoid M) ↔ nontrivial M

@[simp]

theorem submonoid.nontrivial_iff {M : Type u_1} [mul_one_class M] :

nontrivial (submonoid M) ↔ nontrivial M

@[protected, instance]

def add_submonoid.unique {M : Type u_1} [add_zero_class M] [subsingleton M] :

unique (add_submonoid M)

Equations

add_submonoid.unique = {to_inhabited := {default := ⊥}, uniq := _}

@[protected, instance]

def submonoid.unique {M : Type u_1} [mul_one_class M] [subsingleton M] :

unique (submonoid M)

Equations

submonoid.unique = {to_inhabited := {default := ⊥}, uniq := _}

@[protected, instance]

def submonoid.nontrivial {M : Type u_1} [mul_one_class M] [nontrivial M] :

nontrivial (submonoid M)

@[protected, instance]

def add_submonoid.nontrivial {M : Type u_1} [add_zero_class M] [nontrivial M] :

nontrivial (add_submonoid M)

def submonoid.closure {M : Type u_1} [mul_one_class M] (s : set M) :

The submonoid generated by a set.

Equations

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

Instances for ↥submonoid.closure

def add_submonoid.closure {M : Type u_1} [add_zero_class M] (s : set M) :

add_submonoid M

The add_submonoid generated by a set

Equations

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

Instances for ↥add_submonoid.closure

theorem add_submonoid.mem_closure {M : Type u_1} [add_zero_class M] {s : set M} {x : M} :

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

theorem submonoid.mem_closure {M : Type u_1} [mul_one_class M] {s : set M} {x : M} :

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

@[simp]

theorem submonoid.subset_closure {M : Type u_1} [mul_one_class M] {s : set M} :

s ⊆ ↑(submonoid.closure s)

The submonoid generated by a set includes the set.

@[simp]

theorem add_submonoid.subset_closure {M : Type u_1} [add_zero_class M] {s : set M} :

s ⊆ ↑(add_submonoid.closure s)

The add_submonoid generated by a set includes the set.

theorem submonoid.not_mem_of_not_mem_closure {M : Type u_1} [mul_one_class M] {s : set M} {P : M} (hP : P ∉ submonoid.closure s) :

P ∉ s

theorem add_submonoid.not_mem_of_not_mem_closure {M : Type u_1} [add_zero_class M] {s : set M} {P : M} (hP : P ∉ add_submonoid.closure s) :

P ∉ s

@[simp]

theorem submonoid.closure_le {M : Type u_1} [mul_one_class M] {s : set M} {S : submonoid M} :

submonoid.closure s ≤ S ↔ s ⊆ ↑S

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

@[simp]

theorem add_submonoid.closure_le {M : Type u_1} [add_zero_class M] {s : set M} {S : add_submonoid M} :

add_submonoid.closure s ≤ S ↔ s ⊆ ↑S

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

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

add_submonoid.closure s ≤ add_submonoid.closure t

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

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

submonoid.closure s ≤ submonoid.closure t

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

theorem add_submonoid.closure_eq_of_le {M : Type u_1} [add_zero_class M] {s : set M} {S : add_submonoid M} (h₁ : s ⊆ ↑S) (h₂ : S ≤ add_submonoid.closure s) :

add_submonoid.closure s = S

theorem submonoid.closure_eq_of_le {M : Type u_1} [mul_one_class M] {s : set M} {S : submonoid M} (h₁ : s ⊆ ↑S) (h₂ : S ≤ submonoid.closure s) :

submonoid.closure s = S

theorem submonoid.closure_induction {M : Type u_1} [mul_one_class M] {s : set M} {p : M → Prop} {x : M} (h : x ∈ submonoid.closure s) (Hs : ∀ (x : M), x ∈ s → p x) (H1 : p 1) (Hmul : ∀ (x y : M), p x → p y → p (x * y)) :

p x

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

theorem add_submonoid.closure_induction {M : Type u_1} [add_zero_class M] {s : set M} {p : M → Prop} {x : M} (h : x ∈ add_submonoid.closure s) (Hs : ∀ (x : M), x ∈ s → p x) (H1 : p 0) (Hmul : ∀ (x y : M), p x → p y → p (x + y)) :

p x

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

theorem add_submonoid.closure_induction' {M : Type u_1} [add_zero_class M] (s : set M) {p : Π (x : M), x ∈ add_submonoid.closure s → Prop} (Hs : ∀ (x : M) (h : x ∈ s), p x _) (H1 : p 0 _) (Hmul : ∀ (x : M) (hx : x ∈ add_submonoid.closure s) (y : M) (hy : y ∈ add_submonoid.closure s), p x hx → p y hy → p (x + y) _) {x : M} (hx : x ∈ add_submonoid.closure s) :

p x hx

A dependent version of add_submonoid.closure_induction.

theorem submonoid.closure_induction' {M : Type u_1} [mul_one_class M] (s : set M) {p : Π (x : M), x ∈ submonoid.closure s → Prop} (Hs : ∀ (x : M) (h : x ∈ s), p x _) (H1 : p 1 _) (Hmul : ∀ (x : M) (hx : x ∈ submonoid.closure s) (y : M) (hy : y ∈ submonoid.closure s), p x hx → p y hy → p (x * y) _) {x : M} (hx : x ∈ submonoid.closure s) :

p x hx

A dependent version of submonoid.closure_induction.

theorem add_submonoid.closure_induction₂ {M : Type u_1} [add_zero_class M] {s : set M} {p : M → M → Prop} {x y : M} (hx : x ∈ add_submonoid.closure s) (hy : y ∈ add_submonoid.closure s) (Hs : ∀ (x : M), x ∈ s → ∀ (y : M), y ∈ s → p x y) (H1_left : ∀ (x : M), p 0 x) (H1_right : ∀ (x : M), p x 0) (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.

theorem submonoid.closure_induction₂ {M : Type u_1} [mul_one_class M] {s : set M} {p : M → M → Prop} {x y : M} (hx : x ∈ submonoid.closure s) (hy : y ∈ submonoid.closure s) (Hs : ∀ (x : M), x ∈ s → ∀ (y : M), y ∈ s → p x y) (H1_left : ∀ (x : M), p 1 x) (H1_right : ∀ (x : M), p x 1) (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.

theorem add_submonoid.dense_induction {M : Type u_1} [add_zero_class M] {p : M → Prop} (x : M) {s : set M} (hs : add_submonoid.closure s = ⊤) (Hs : ∀ (x : M), x ∈ s → p x) (H1 : p 0) (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_submonoid.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, verify p 0, and verify that p x and p y imply p (x + y).

theorem submonoid.dense_induction {M : Type u_1} [mul_one_class M] {p : M → Prop} (x : M) {s : set M} (hs : submonoid.closure s = ⊤) (Hs : ∀ (x : M), x ∈ s → p x) (H1 : p 1) (Hmul : ∀ (x y : M), p x → p y → p (x * y)) :

p x

If s is a dense set in a monoid M, submonoid.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, verify p 1, and verify that p x and p y imply p (x * y).

@[protected]

def add_submonoid.gi (M : Type u_1) [add_zero_class M] :

galois_insertion add_submonoid.closure coe

closure forms a Galois insertion with the coercion to set.

Equations

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

@[protected]

def submonoid.gi (M : Type u_1) [mul_one_class M] :

galois_insertion submonoid.closure coe

closure forms a Galois insertion with the coercion to set.

Equations

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

@[simp]

theorem submonoid.closure_eq {M : Type u_1} [mul_one_class M] (S : submonoid M) :

submonoid.closure ↑S = S

Closure of a submonoid S equals S.

@[simp]

theorem add_submonoid.closure_eq {M : Type u_1} [add_zero_class M] (S : add_submonoid M) :

add_submonoid.closure ↑S = S

Additive closure of an additive submonoid S equals S

@[simp]

theorem add_submonoid.closure_empty {M : Type u_1} [add_zero_class M] :

add_submonoid.closure ∅ = ⊥

@[simp]

theorem submonoid.closure_empty {M : Type u_1} [mul_one_class M] :

submonoid.closure ∅ = ⊥

@[simp]

theorem add_submonoid.closure_univ {M : Type u_1} [add_zero_class M] :

add_submonoid.closure set.univ = ⊤

@[simp]

theorem submonoid.closure_univ {M : Type u_1} [mul_one_class M] :

submonoid.closure set.univ = ⊤

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

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

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

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

theorem add_submonoid.closure_Union {M : Type u_1} [add_zero_class M] {ι : Sort u_2} (s : ι → set M) :

add_submonoid.closure (⋃ (i : ι), s i) = ⨆ (i : ι), add_submonoid.closure (s i)

theorem submonoid.closure_Union {M : Type u_1} [mul_one_class M] {ι : Sort u_2} (s : ι → set M) :

submonoid.closure (⋃ (i : ι), s i) = ⨆ (i : ι), submonoid.closure (s i)

@[simp]

theorem submonoid.closure_singleton_le_iff_mem {M : Type u_1} [mul_one_class M] (m : M) (p : submonoid M) :

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

@[simp]

theorem add_submonoid.closure_singleton_le_iff_mem {M : Type u_1} [add_zero_class M] (m : M) (p : add_submonoid M) :

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

theorem submonoid.mem_supr {M : Type u_1} [mul_one_class M] {ι : Sort u_2} (p : ι → submonoid M) {m : M} :

(m ∈ ⨆ (i : ι), p i) ↔ ∀ (N : submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N

theorem add_submonoid.mem_supr {M : Type u_1} [add_zero_class M] {ι : Sort u_2} (p : ι → add_submonoid M) {m : M} :

(m ∈ ⨆ (i : ι), p i) ↔ ∀ (N : add_submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N

theorem add_submonoid.supr_eq_closure {M : Type u_1} [add_zero_class M] {ι : Sort u_2} (p : ι → add_submonoid M) :

(⨆ (i : ι), p i) = add_submonoid.closure (⋃ (i : ι), ↑(p i))

theorem submonoid.supr_eq_closure {M : Type u_1} [mul_one_class M] {ι : Sort u_2} (p : ι → submonoid M) :

(⨆ (i : ι), p i) = submonoid.closure (⋃ (i : ι), ↑(p i))

theorem submonoid.disjoint_def {M : Type u_1} [mul_one_class M] {p₁ p₂ : submonoid M} :

disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1

theorem add_submonoid.disjoint_def {M : Type u_1} [add_zero_class M] {p₁ p₂ : add_submonoid M} :

disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 0

theorem add_submonoid.disjoint_def' {M : Type u_1} [add_zero_class M] {p₁ p₂ : add_submonoid M} :

disjoint p₁ p₂ ↔ ∀ {x y : M}, x ∈ p₁ → y ∈ p₂ → x = y → x = 0

theorem submonoid.disjoint_def' {M : Type u_1} [mul_one_class M] {p₁ p₂ : submonoid M} :

disjoint p₁ p₂ ↔ ∀ {x y : M}, x ∈ p₁ → y ∈ p₂ → x = y → x = 1

def add_monoid_hom.eq_mlocus {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f g : M →+ N) :

add_submonoid M

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

Equations

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

def monoid_hom.eq_mlocus {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f g : M →* N) :

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

Equations

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

@[simp]

theorem add_monoid_hom.eq_mlocus_same {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) :

f.eq_mlocus f = ⊤

@[simp]

theorem monoid_hom.eq_mlocus_same {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) :

f.eq_mlocus f = ⊤

theorem monoid_hom.eq_on_mclosure {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {f g : M →* N} {s : set M} (h : set.eq_on ⇑f ⇑g s) :

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

If two monoid homomorphisms are equal on a set, then they are equal on its submonoid closure.

theorem add_monoid_hom.eq_on_mclosure {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {f g : M →+ N} {s : set M} (h : set.eq_on ⇑f ⇑g s) :

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

If two monoid homomorphisms are equal on a set, then they are equal on its submonoid closure.

theorem monoid_hom.eq_of_eq_on_mtop {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {f g : M →* N} (h : set.eq_on ⇑f ⇑g ↑⊤) :

f = g

theorem add_monoid_hom.eq_of_eq_on_mtop {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {f g : M →+ N} (h : set.eq_on ⇑f ⇑g ↑⊤) :

f = g

theorem add_monoid_hom.eq_of_eq_on_mdense {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] {s : set M} (hs : add_submonoid.closure s = ⊤) {f g : M →+ N} (h : set.eq_on ⇑f ⇑g s) :

f = g

theorem monoid_hom.eq_of_eq_on_mdense {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] {s : set M} (hs : submonoid.closure s = ⊤) {f g : M →* N} (h : set.eq_on ⇑f ⇑g s) :

f = g

def is_add_unit.add_submonoid (M : Type u_1) [add_monoid M] :

add_submonoid M

The additive submonoid consisting of the additive units of an additive monoid

Equations

is_add_unit.add_submonoid M = {carrier := set_of is_add_unit, add_mem' := _, zero_mem' := _}

def is_unit.submonoid (M : Type u_1) [monoid M] :

The submonoid consisting of the units of a monoid

Equations

is_unit.submonoid M = {carrier := set_of is_unit, mul_mem' := _, one_mem' := _}

theorem is_unit.mem_submonoid_iff {M : Type u_1} [monoid M] (a : M) :

a ∈ is_unit.submonoid M ↔ is_unit a

theorem is_add_unit.mem_add_submonoid_iff {M : Type u_1} [add_monoid M] (a : M) :

a ∈ is_add_unit.add_submonoid M ↔ is_add_unit a

def add_monoid_hom.of_mclosure_eq_top_left {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] {s : set M} (f : M → N) (hs : add_submonoid.closure s = ⊤) (h1 : f 0 = 0) (hmul : ∀ (x : M), x ∈ s → ∀ (y : M), f (x + y) = f x + f y) :

M →+ N

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

Equations

add_monoid_hom.of_mclosure_eq_top_left f hs h1 hmul = {to_fun := f, map_zero' := h1, map_add' := _}

def monoid_hom.of_mclosure_eq_top_left {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] {s : set M} (f : M → N) (hs : submonoid.closure s = ⊤) (h1 : f 1 = 1) (hmul : ∀ (x : M), x ∈ s → ∀ (y : M), f (x * y) = f x * f y) :

M →* N

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

Equations

monoid_hom.of_mclosure_eq_top_left f hs h1 hmul = {to_fun := f, map_one' := h1, map_mul' := _}

@[simp, norm_cast]

theorem monoid_hom.coe_of_mclosure_eq_top_left {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] {s : set M} (f : M → N) (hs : submonoid.closure s = ⊤) (h1 : f 1 = 1) (hmul : ∀ (x : M), x ∈ s → ∀ (y : M), f (x * y) = f x * f y) :

⇑(monoid_hom.of_mclosure_eq_top_left f hs h1 hmul) = f

@[simp, norm_cast]

theorem add_monoid_hom.coe_of_mclosure_eq_top_left {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] {s : set M} (f : M → N) (hs : add_submonoid.closure s = ⊤) (h1 : f 0 = 0) (hmul : ∀ (x : M), x ∈ s → ∀ (y : M), f (x + y) = f x + f y) :

⇑(add_monoid_hom.of_mclosure_eq_top_left f hs h1 hmul) = f

def add_monoid_hom.of_mclosure_eq_top_right {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] {s : set M} (f : M → N) (hs : add_submonoid.closure s = ⊤) (h1 : f 0 = 0) (hmul : ∀ (x y : M), y ∈ s → f (x + y) = f x + f y) :

M →+ N

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

Equations

add_monoid_hom.of_mclosure_eq_top_right f hs h1 hmul = {to_fun := f, map_zero' := h1, map_add' := _}

def monoid_hom.of_mclosure_eq_top_right {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] {s : set M} (f : M → N) (hs : submonoid.closure s = ⊤) (h1 : f 1 = 1) (hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y) :

M →* N

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

Equations

monoid_hom.of_mclosure_eq_top_right f hs h1 hmul = {to_fun := f, map_one' := h1, map_mul' := _}

@[simp, norm_cast]

theorem monoid_hom.coe_of_mclosure_eq_top_right {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] {s : set M} (f : M → N) (hs : submonoid.closure s = ⊤) (h1 : f 1 = 1) (hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y) :

⇑(monoid_hom.of_mclosure_eq_top_right f hs h1 hmul) = f

@[simp, norm_cast]

theorem add_monoid_hom.coe_of_mclosure_eq_top_right {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] {s : set M} (f : M → N) (hs : add_submonoid.closure s = ⊤) (h1 : f 0 = 0) (hmul : ∀ (x y : M), y ∈ s → f (x + y) = f x + f y) :

⇑(add_monoid_hom.of_mclosure_eq_top_right f hs h1 hmul) = f