Mathlib.Algebra.Group.Submonoid.Defs

OneMemClass structure

(S : Type*) (M : outParam Type*) [One M] [SetLike S M]

Full source

/-- `OneMemClass S M` says `S` is a type of subsets `s ≤ M`, such that `1 ∈ s` for all `s`. -/
class OneMemClass (S : Type*) (M : outParam Type*) [One M] [SetLike S M] : Prop where
  /-- By definition, if we have `OneMemClass S M`, we have `1 ∈ s` for all `s : S`. -/
  one_mem : ∀ s : S, (1 : M) ∈ s

Class of subsets containing the identity element

Informal description

A class `OneMemClass S M` asserts that `S` is a type of subsets of `M` (where `M` is equipped with a distinguished element `1`) such that every subset `s` in `S` contains the element `1`. In other words, for any `s : S`, we have `1 ∈ s` when `s` is viewed as a subset of `M` via the coercion from `S` to `Set M`.

ZeroMemClass structure

(S : Type*) (M : outParam Type*) [Zero M] [SetLike S M]

Full source

/-- `ZeroMemClass S M` says `S` is a type of subsets `s ≤ M`, such that `0 ∈ s` for all `s`. -/
class ZeroMemClass (S : Type*) (M : outParam Type*) [Zero M] [SetLike S M] : Prop where
  /-- By definition, if we have `ZeroMemClass S M`, we have `0 ∈ s` for all `s : S`. -/
  zero_mem : ∀ s : S, (0 : M) ∈ s

Class of Zero-Containing Subsets

Informal description

A class `ZeroMemClass S M` asserts that for any subset `s` of type `S` of a type `M` with a zero element, the zero element is contained in `s`. Here, `S` is a type of subsets of `M` represented through a `SetLike` instance.

Submonoid structure

(M : Type*) [MulOneClass M] extends Subsemigroup M

Full source

/-- A submonoid of a monoid `M` is a subset containing 1 and closed under multiplication. -/
structure Submonoid (M : Type*) [MulOneClass M] extends Subsemigroup M where
  /-- A submonoid contains `1`. -/
  one_mem' : (1 : M) ∈ carrier

Submonoid of a monoid

Informal description

A submonoid of a monoid $M$ is a subset of $M$ that contains the multiplicative identity and is closed under multiplication.

SubmonoidClass structure

(S : Type*) (M : outParam Type*) [MulOneClass M] [SetLike S M] : Prop
    extends MulMemClass S M, OneMemClass S M

Full source

/-- `SubmonoidClass S M` says `S` is a type of subsets `s ≤ M` that contain `1`
and are closed under `(*)` -/
class SubmonoidClass (S : Type*) (M : outParam Type*) [MulOneClass M] [SetLike S M] : Prop
    extends MulMemClass S M, OneMemClass S M

Submonoid Class

Informal description

A typeclass `SubmonoidClass S M` asserts that `S` is a type of subsets of a monoid `M` that contain the multiplicative identity and are closed under multiplication. This means for any subset `s : S`, we have `1 ∈ s` and for any `x, y ∈ s`, the product `x * y` is also in `s`.

AddSubmonoid structure

(M : Type*) [AddZeroClass M] extends AddSubsemigroup M

Full source

/-- An additive submonoid of an additive monoid `M` is a subset containing 0 and
  closed under addition. -/
structure AddSubmonoid (M : Type*) [AddZeroClass M] extends AddSubsemigroup M where
  /-- An additive submonoid contains `0`. -/
  zero_mem' : (0 : M) ∈ carrier

Additive submonoid

Informal description

An additive submonoid of an additive monoid $M$ is a subset of $M$ that contains the additive identity (0) and is closed under addition.

AddSubmonoidClass structure

(S : Type*) (M : outParam Type*) [AddZeroClass M] [SetLike S M] : Prop
  extends AddMemClass S M, ZeroMemClass S M

Full source

/-- `AddSubmonoidClass S M` says `S` is a type of subsets `s ≤ M` that contain `0`
and are closed under `(+)` -/
class AddSubmonoidClass (S : Type*) (M : outParam Type*) [AddZeroClass M] [SetLike S M] : Prop
  extends AddMemClass S M, ZeroMemClass S M

Additive Submonoid Class

Informal description

The typeclass `AddSubmonoidClass S M` asserts that `S` is a type of subsets of an additive monoid `M` that contain the additive identity (zero) and are closed under addition. This means for any subset `s : S`, we have `0 ∈ s` and for any `x, y ∈ s`, the sum `x + y` is also in `s`.

pow_mem theorem

{M A} [Monoid M] [SetLike A M] [SubmonoidClass A M] {S : A} {x : M} (hx : x ∈ S) : ∀ n : ℕ, x ^ n ∈ S

Full source

@[to_additive (attr := aesop safe apply (rule_sets := [SetLike]))]
theorem pow_mem {M A} [Monoid M] [SetLike A M] [SubmonoidClass A M] {S : A} {x : M}
    (hx : x ∈ S) : ∀ n : ℕ, x ^ n ∈ S
  | 0 => by
    rw [pow_zero]
    exact OneMemClass.one_mem S
  | n + 1 => by
    rw [pow_succ]
    exact mul_mem (pow_mem hx n) hx

Closure under Powers in Submonoids

Informal description

Let $M$ be a monoid and $A$ a type of subsets of $M$ that forms a submonoid class. For any subset $S$ of $M$ in $A$ and any element $x \in S$, the power $x^n$ belongs to $S$ for every natural number $n$.

Submonoid.instSetLike instance

: SetLike (Submonoid M) M

Full source

@[to_additive]
instance : SetLike (Submonoid M) M where
  coe s := s.carrier
  coe_injective' p q h := by cases p; cases q; congr; exact SetLike.coe_injective' h

Submonoids as Set-like Structures

Informal description

For any monoid $M$, the type of submonoids of $M$ forms a set-like structure, meaning that each submonoid can be naturally viewed as a subset of $M$ through a coercion.

Submonoid.ofClass definition

{S M : Type*} [Monoid M] [SetLike S M] [SubmonoidClass S M] (s : S) : Submonoid M

Full source

/-- The actual `Submonoid` obtained from an element of a `SubmonoidClass` -/
@[to_additive (attr := simps) "The actual `AddSubmonoid` obtained from an element of a
`AddSubmonoidClass`"]
def ofClass {S M : Type*} [Monoid M] [SetLike S M] [SubmonoidClass S M] (s : S) : Submonoid M :=
  ⟨⟨s, MulMemClass.mul_mem⟩, OneMemClass.one_mem s⟩

Submonoid from Submonoid Class

Informal description

Given a monoid $M$ and a type $S$ of subsets of $M$ that forms a `SubmonoidClass`, the function `Submonoid.ofClass` maps any subset $s \in S$ to the corresponding bundled submonoid of $M$ with carrier set $s$. This submonoid contains the multiplicative identity and is closed under multiplication.

Submonoid.instCanLiftSetCoeAndMemOfNatForallForallForallForallHMul instance

: CanLift (Set M) (Submonoid M) (↑) (fun s ↦ 1 ∈ s ∧ ∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s)

Full source

@[to_additive]
instance (priority := 100) : CanLift (Set M) (Submonoid M) (↑)
    (fun s ↦ 1 ∈ s1 ∈ s ∧ ∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) where
  prf s h := ⟨{ carrier := s, one_mem' := h.1, mul_mem' := h.2 }, rfl⟩

Lifting Condition for Submonoids from Subsets

Informal description

For any monoid $M$, a subset $s$ of $M$ can be lifted to a submonoid if and only if $s$ contains the multiplicative identity and is closed under multiplication.

Submonoid.instSubmonoidClass instance

: SubmonoidClass (Submonoid M) M

Full source

@[to_additive]
instance : SubmonoidClass (Submonoid M) M where
  one_mem := Submonoid.one_mem'
  mul_mem {s} := s.mul_mem'

Submonoids as Submonoid Class

Informal description

For any monoid $M$, the type of submonoids of $M$ forms a `SubmonoidClass`, meaning that every submonoid $S$ of $M$ contains the multiplicative identity and is closed under multiplication.

Submonoid.mem_toSubsemigroup theorem

{s : Submonoid M} {x : M} : x ∈ s.toSubsemigroup ↔ x ∈ s

Full source

@[to_additive (attr := simp)]
theorem mem_toSubsemigroup {s : Submonoid M} {x : M} : x ∈ s.toSubsemigroupx ∈ s.toSubsemigroup ↔ x ∈ s :=
  Iff.rfl

Membership Equivalence Between Submonoid and its Subsemigroup

Informal description

For any submonoid $s$ of a monoid $M$ and any element $x \in M$, the element $x$ belongs to the underlying subsemigroup of $s$ if and only if $x$ belongs to $s$.

Submonoid.mem_carrier theorem

{s : Submonoid M} {x : M} : x ∈ s.carrier ↔ x ∈ s

Full source

@[to_additive]
theorem mem_carrier {s : Submonoid M} {x : M} : x ∈ s.carrierx ∈ s.carrier ↔ x ∈ s :=
  Iff.rfl

Membership in Submonoid Carrier Set

Informal description

For any submonoid $s$ of a monoid $M$ and any element $x \in M$, the element $x$ belongs to the underlying set of $s$ (denoted by `s.carrier`) if and only if $x$ belongs to $s$ (denoted by $x \in s$).

Submonoid.mem_mk theorem

{s : Subsemigroup M} {x : M} (h_one) : x ∈ mk s h_one ↔ x ∈ s

Full source

@[to_additive (attr := simp)]
theorem mem_mk {s : Subsemigroup M} {x : M} (h_one) : x ∈ mk s h_onex ∈ mk s h_one ↔ x ∈ s :=
  Iff.rfl

Membership in Constructed Submonoid Equivalence

Informal description

For any subsemigroup $s$ of a monoid $M$, any element $x \in M$, and any proof $h\_one$ that $s$ contains the multiplicative identity, the element $x$ belongs to the submonoid constructed from $s$ and $h\_one$ if and only if $x$ belongs to $s$.

Submonoid.coe_set_mk theorem

{s : Subsemigroup M} (h_one) : (mk s h_one : Set M) = s

Full source

@[to_additive (attr := simp)]
theorem coe_set_mk {s : Subsemigroup M} (h_one) : (mk s h_one : Set M) = s :=
  rfl

Submonoid Construction Preserves Carrier Set

Informal description

For any subsemigroup $s$ of a monoid $M$ and any proof $h\_one$ that $s$ contains the multiplicative identity, the underlying set of the submonoid constructed from $s$ and $h\_one$ is equal to $s$ itself.

Submonoid.mk_le_mk theorem

{s t : Subsemigroup M} (h_one) (h_one') : mk s h_one ≤ mk t h_one' ↔ s ≤ t

Full source

@[to_additive (attr := simp)]
theorem mk_le_mk {s t : Subsemigroup M} (h_one) (h_one') : mkmk s h_one ≤ mk t h_one' ↔ s ≤ t :=
  Iff.rfl

Submonoid Construction Preserves Order Relation

Informal description

For any two subsemigroups $s$ and $t$ of a monoid $M$, and given proofs $h\_one$ and $h\_one'$ that $s$ and $t$ respectively contain the multiplicative identity, the submonoid constructed from $s$ and $h\_one$ is contained in the submonoid constructed from $t$ and $h\_one'$ if and only if $s$ is contained in $t$ as subsemigroups. In other words, $\text{mk}\ s\ h\_one \leq \text{mk}\ t\ h\_one' \leftrightarrow s \leq t$.

Submonoid.ext theorem

{S T : Submonoid M} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T

Full source

/-- Two submonoids are equal if they have the same elements. -/
@[to_additive (attr := ext) "Two `AddSubmonoid`s are equal if they have the same elements."]
theorem ext {S T : Submonoid M} (h : ∀ x, x ∈ Sx ∈ S ↔ x ∈ T) : S = T :=
  SetLike.ext h

Equality of Submonoids by Membership

Informal description

Two submonoids $S$ and $T$ of a monoid $M$ are equal if and only if they have the same elements, i.e., for all $x \in M$, $x \in S$ if and only if $x \in T$.

Submonoid.copy definition

(S : Submonoid M) (s : Set M) (hs : s = S) : Submonoid M

Full source

/-- Copy a submonoid replacing `carrier` with a set that is equal to it. -/
@[to_additive "Copy an additive submonoid replacing `carrier` with a set that is equal to it."]
protected def copy (S : Submonoid M) (s : Set M) (hs : s = S) : Submonoid M where
  carrier := s
  one_mem' := show 1 ∈ s from hs.symm ▸ S.one_mem'
  mul_mem' := hs.symm ▸ S.mul_mem'

Copy of a submonoid with a specified carrier set

Informal description

Given a submonoid $S$ of a monoid $M$ and a set $s$ that is equal to the underlying set of $S$, the function `Submonoid.copy` constructs a new submonoid with $s$ as its underlying set. This new submonoid has the same multiplicative identity and closure under multiplication as $S$.

Submonoid.coe_copy theorem

{s : Set M} (hs : s = S) : (S.copy s hs : Set M) = s

Full source

@[to_additive (attr := simp)]
theorem coe_copy {s : Set M} (hs : s = S) : (S.copy s hs : Set M) = s :=
  rfl

Underlying set equality for copied submonoid

Informal description

For any submonoid $S$ of a monoid $M$ and any set $s$ equal to the underlying set of $S$, the underlying set of the copied submonoid $S.\text{copy}\,s\,hs$ is equal to $s$.

Submonoid.copy_eq theorem

{s : Set M} (hs : s = S) : S.copy s hs = S

Full source

@[to_additive]
theorem copy_eq {s : Set M} (hs : s = S) : S.copy s hs = S :=
  SetLike.coe_injective hs

Equality of Submonoid Copy with Original Submonoid

Informal description

Given a submonoid $S$ of a monoid $M$ and a set $s$ such that $s = S$ (as sets), the submonoid $S.\text{copy}\, s\, \text{hs}$ is equal to $S$.

Submonoid.one_mem theorem

: (1 : M) ∈ S

Full source

/-- A submonoid contains the monoid's 1. -/
@[to_additive "An `AddSubmonoid` contains the monoid's 0."]
protected theorem one_mem : (1 : M) ∈ S :=
  one_mem S

Submonoid Contains Identity Element

Informal description

For any submonoid $S$ of a monoid $M$, the multiplicative identity $1$ is an element of $S$.

Submonoid.mul_mem theorem

{x y : M} : x ∈ S → y ∈ S → x * y ∈ S

Full source

/-- A submonoid is closed under multiplication. -/
@[to_additive "An `AddSubmonoid` is closed under addition."]
protected theorem mul_mem {x y : M} : x ∈ S → y ∈ S → x * y ∈ S :=
  mul_mem

Closure under multiplication in submonoids

Informal description

For any submonoid $S$ of a monoid $M$ and any elements $x, y \in M$, if $x \in S$ and $y \in S$, then their product $x * y$ also belongs to $S$.

Submonoid.instTop instance

: Top (Submonoid M)

Full source

/-- The submonoid `M` of the monoid `M`. -/
@[to_additive "The additive submonoid `M` of the `AddMonoid M`."]
instance : Top (Submonoid M) :=
  ⟨{  carrier := Set.univ
      one_mem' := Set.mem_univ 1
      mul_mem' := fun _ _ => Set.mem_univ _ }⟩

The Full Submonoid as the Top Element

Informal description

For any monoid $M$, the submonoid consisting of all elements of $M$ is the top element in the lattice of submonoids of $M$.

Submonoid.instBot instance

: Bot (Submonoid M)

Full source

/-- The trivial submonoid `{1}` of a monoid `M`. -/
@[to_additive "The trivial `AddSubmonoid` `{0}` of an `AddMonoid` `M`."]
instance : Bot (Submonoid M) :=
  ⟨{  carrier := {1}
      one_mem' := Set.mem_singleton 1
      mul_mem' := fun ha hb => by
        simp only [Set.mem_singleton_iff] at *
        rw [ha, hb, mul_one] }⟩

The Trivial Submonoid as the Bottom Element

Informal description

For any monoid $M$, the trivial submonoid $\{1\}$ is the bottom element in the lattice of submonoids of $M$.

Submonoid.instInhabited instance

: Inhabited (Submonoid M)

Full source

@[to_additive]
instance : Inhabited (Submonoid M) :=
  ⟨⊥⟩

Inhabitedness of Submonoids

Informal description

For any monoid $M$, the type of submonoids of $M$ is inhabited.

Submonoid.mem_bot theorem

{x : M} : x ∈ (⊥ : Submonoid M) ↔ x = 1

Full source

@[to_additive (attr := simp)]
theorem mem_bot {x : M} : x ∈ (⊥ : Submonoid M)x ∈ (⊥ : Submonoid M) ↔ x = 1 :=
  Set.mem_singleton_iff

Characterization of Elements in Trivial Submonoid: $x \in \bot \leftrightarrow x = 1$

Informal description

An element $x$ of a monoid $M$ belongs to the trivial submonoid (the bottom element in the lattice of submonoids) if and only if $x$ is equal to the multiplicative identity $1$.

Submonoid.mem_top theorem

(x : M) : x ∈ (⊤ : Submonoid M)

Full source

@[to_additive (attr := simp)]
theorem mem_top (x : M) : x ∈ (⊤ : Submonoid M) :=
  Set.mem_univ x

Membership in Top Submonoid is Universal

Informal description

For any element $x$ of a monoid $M$, $x$ belongs to the top submonoid of $M$ (which is $M$ itself).

Submonoid.coe_top theorem

: ((⊤ : Submonoid M) : Set M) = Set.univ

Full source

@[to_additive (attr := simp)]
theorem coe_top : ((⊤ : Submonoid M) : Set M) = Set.univ :=
  rfl

Top Submonoid Equals Universal Set

Informal description

The underlying set of the top submonoid of a monoid $M$ is equal to the universal set of $M$, i.e., $(\top : \text{Submonoid } M) = \text{univ}$.

Submonoid.coe_bot theorem

: ((⊥ : Submonoid M) : Set M) = { 1 }

Full source

@[to_additive (attr := simp)]
theorem coe_bot : ((⊥ : Submonoid M) : Set M) = {1} :=
  rfl

Trivial Submonoid as Singleton Identity Set

Informal description

The underlying set of the bottom submonoid (the trivial submonoid) of a monoid $M$ is the singleton set containing the multiplicative identity $1$, i.e., $\bot = \{1\}$.

Submonoid.instMin instance

: Min (Submonoid M)

Full source

/-- The inf of two submonoids is their intersection. -/
@[to_additive "The inf of two `AddSubmonoid`s is their intersection."]
instance : Min (Submonoid M) :=
  ⟨fun S₁ S₂ =>
    { carrier := S₁ ∩ S₂
      one_mem' := ⟨S₁.one_mem, S₂.one_mem⟩
      mul_mem' := fun ⟨hx, hx'⟩ ⟨hy, hy'⟩ => ⟨S₁.mul_mem hx hy, S₂.mul_mem hx' hy'⟩ }⟩

Intersection of Submonoids is a Submonoid

Informal description

For any monoid $M$, the intersection of two submonoids of $M$ is again a submonoid of $M$.

Submonoid.coe_inf theorem

(p p' : Submonoid M) : ((p ⊓ p' : Submonoid M) : Set M) = (p : Set M) ∩ p'

Full source

@[to_additive (attr := simp)]
theorem coe_inf (p p' : Submonoid M) : ((p ⊓ p' : Submonoid M) : Set M) = (p : Set M) ∩ p' :=
  rfl

Intersection of Submonoids as Set Intersection

Informal description

For any two submonoids $p$ and $p'$ of a monoid $M$, the underlying set of their intersection $p \sqcap p'$ is equal to the intersection of their underlying sets, i.e., $(p \sqcap p') = p \cap p'$ as subsets of $M$.

Submonoid.mem_inf theorem

{p p' : Submonoid M} {x : M} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

Full source

@[to_additive (attr := simp)]
theorem mem_inf {p p' : Submonoid M} {x : M} : x ∈ p ⊓ p'x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p' :=
  Iff.rfl

Membership in Intersection of Submonoids

Informal description

For any submonoids $p$ and $p'$ of a monoid $M$, and any element $x \in M$, we have $x \in p \sqcap p'$ if and only if $x \in p$ and $x \in p'$.

Submonoid.subsingleton_iff theorem

: Subsingleton (Submonoid M) ↔ Subsingleton M

Full source

@[to_additive (attr := simp)]
theorem subsingleton_iff : SubsingletonSubsingleton (Submonoid M) ↔ Subsingleton M :=
  ⟨fun _ =>
    ⟨fun x y =>
      have : ∀ i : M, i = 1 := fun i =>
        mem_bot.mp <| Subsingleton.elim (⊤ : Submonoid M) ⊥ ▸ mem_top i
      (this x).trans (this y).symm⟩,
    fun _ =>
    ⟨fun x y => Submonoid.ext fun i => Subsingleton.elim 1 i ▸ by simp [Submonoid.one_mem]⟩⟩

Subsingleton Criterion for Submonoids: $\text{Subsingleton}(\text{Submonoid}(M)) \leftrightarrow \text{Subsingleton}(M)$

Informal description

The type of submonoids of a monoid $M$ is a subsingleton (i.e., has at most one element) if and only if $M$ itself is a subsingleton.

Submonoid.nontrivial_iff theorem

: Nontrivial (Submonoid M) ↔ Nontrivial M

Full source

@[to_additive (attr := simp)]
theorem nontrivial_iff : NontrivialNontrivial (Submonoid M) ↔ Nontrivial M :=
  not_iff_not.mp
    ((not_nontrivial_iff_subsingleton.trans subsingleton_iff).trans
      not_nontrivial_iff_subsingleton.symm)

Nontriviality Criterion for Submonoids: $\text{Nontrivial}(\text{Submonoid}(M)) \leftrightarrow \text{Nontrivial}(M)$

Informal description

The type of submonoids of a monoid $M$ is nontrivial (i.e., contains at least two distinct elements) if and only if $M$ itself is nontrivial.

Submonoid.instUniqueOfSubsingleton instance

[Subsingleton M] : Unique (Submonoid M)

Full source

@[to_additive]
instance [Subsingleton M] : Unique (Submonoid M) :=
  ⟨⟨⊥⟩, fun a => @Subsingleton.elim _ (subsingleton_iff.mpr ‹_›) a _⟩

Unique Submonoid of a Subsingleton Monoid

Informal description

For any monoid $M$ that is a subsingleton (i.e., has at most one element), there is exactly one submonoid of $M$, namely the trivial submonoid $\{1\}$.

Submonoid.instNontrivial instance

[Nontrivial M] : Nontrivial (Submonoid M)

Full source

@[to_additive]
instance [Nontrivial M] : Nontrivial (Submonoid M) :=
  nontrivial_iff.mpr ‹_›

Nontrivial Monoids Have Nontrivial Submonoids

Informal description

For any nontrivial monoid $M$, the collection of submonoids of $M$ is also nontrivial (i.e., contains at least two distinct submonoids).

MonoidHom.eqLocusM definition

(f g : M →* N) : Submonoid M

Full source

/-- The submonoid of elements `x : M` such that `f x = g x` -/
@[to_additive "The additive submonoid of elements `x : M` such that `f x = g x`"]
def eqLocusM (f g : M →* N) : Submonoid M where
  carrier := { x | f x = g x }
  one_mem' := by rw [Set.mem_setOf_eq, f.map_one, g.map_one]
  mul_mem' (hx : _ = _) (hy : _ = _) := by simp [*]

Equalizer submonoid of monoid homomorphisms

Informal description

Given two monoid homomorphisms $ f, g \colon M \to N $, the submonoid $\text{eqLocusM}(f, g)$ consists of all elements $ x \in M $ such that $ f(x) = g(x) $. This submonoid contains the identity element (since $ f(1) = g(1) $) and is closed under multiplication (if $ f(x) = g(x) $ and $ f(y) = g(y) $, then $ f(xy) = g(xy) $).

MonoidHom.eqLocusM_same theorem

(f : M →* N) : f.eqLocusM f = ⊤

Full source

@[to_additive (attr := simp)]
theorem eqLocusM_same (f : M →* N) : f.eqLocusM f = ⊤ :=
  SetLike.ext fun _ => eq_self_iff_true _

Equalizer Submonoid of a Homomorphism with Itself is the Full Monoid

Informal description

For any monoid homomorphism $f \colon M \to N$, the equalizer submonoid $\text{eqLocusM}(f, f)$ is equal to the entire monoid $M$ (denoted by $\top$ in the lattice of submonoids). In other words, every element $x \in M$ satisfies $f(x) = f(x)$.

OneMemClass.one instance

: One S'

Full source

/-- A submonoid of a monoid inherits a 1. -/
@[to_additive "An `AddSubmonoid` of an `AddMonoid` inherits a zero."]
instance one : One S' :=
  ⟨⟨1, OneMemClass.one_mem S'⟩⟩

Inheritance of the Identity Element in Submonoids

Informal description

For any subset $S'$ of a monoid $M$ that contains the identity element (i.e., $S'$ is an instance of `OneMemClass`), $S'$ inherits a distinguished element $1$ from $M$.

OneMemClass.coe_one theorem

: ((1 : S') : M₁) = 1

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_one : ((1 : S') : M₁) = 1 :=
  rfl

Coercion of Identity in Submonoids Preserves Identity

Informal description

For any submonoid $S'$ of a monoid $M_1$ that contains the identity element, the coercion of the identity element $1$ of $S'$ to $M_1$ equals the identity element $1$ of $M_1$.

OneMemClass.coe_eq_one theorem

{x : S'} : (↑x : M₁) = 1 ↔ x = 1

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_eq_one {x : S'} : (↑x : M₁) = 1 ↔ x = 1 :=
  (Subtype.ext_iff.symm : (x : M₁) = (1 : S') ↔ x = 1)

Coercion to Identity in Submonoids

Informal description

For any element $x$ in a submonoid $S'$ of a monoid $M_1$ (where $S'$ contains the identity element), the coercion of $x$ to $M_1$ equals the identity element $1$ if and only if $x$ is the identity element of $S'$.

OneMemClass.one_def theorem

: (1 : S') = ⟨1, OneMemClass.one_mem S'⟩

Full source

@[to_additive]
theorem one_def : (1 : S') = ⟨1, OneMemClass.one_mem S'⟩ :=
  rfl

Definition of Identity Element in Submonoids

Informal description

For any subset $S'$ of a monoid $M$ that contains the identity element (i.e., $S'$ is an instance of `OneMemClass`), the identity element $1$ of $S'$ is defined as the pair $\langle 1, \text{OneMemClass.one\_mem}\ S' \rangle$, where the second component is a proof that $1$ belongs to $S'$.

AddSubmonoidClass.nSMul instance

{M} [AddMonoid M] {A : Type*} [SetLike A M] [AddSubmonoidClass A M] (S : A) : SMul ℕ S

Full source

/-- An `AddSubmonoid` of an `AddMonoid` inherits a scalar multiplication. -/
instance AddSubmonoidClass.nSMul {M} [AddMonoid M] {A : Type*} [SetLike A M]
    [AddSubmonoidClass A M] (S : A) : SMul ℕ S :=
  ⟨fun n a => ⟨n • a.1, nsmul_mem a.2 n⟩⟩

Natural Number Scalar Multiplication on Additive Submonoids

Informal description

For any additive monoid $M$ and any additive submonoid $S$ of $M$ (in the sense of `AddSubmonoidClass`), $S$ inherits a natural scalar multiplication by natural numbers. Specifically, for any $n \in \mathbb{N}$ and $x \in S$, the scalar multiple $n \cdot x$ is defined as the $n$-fold sum of $x$ in $M$ and belongs to $S$.

SubmonoidClass.nPow instance

{M} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] (S : A) : Pow S ℕ

Full source

/-- A submonoid of a monoid inherits a power operator. -/
instance nPow {M} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] (S : A) : Pow S ℕ :=
  ⟨fun a n => ⟨a.1 ^ n, pow_mem a.2 n⟩⟩

Power Operation on Submonoids

Informal description

For any monoid $M$ and any subset $S$ of $M$ that forms a submonoid (i.e., $S$ contains the multiplicative identity and is closed under multiplication), there is a natural power operation defined on $S$ that coincides with the power operation on $M$. Specifically, for any $x \in S$ and natural number $n$, the $n$-th power of $x$ in $S$ is equal to the $n$-th power of $x$ in $M$.

SubmonoidClass.coe_pow theorem

{M} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] {S : A} (x : S) (n : ℕ) : ↑(x ^ n) = (x : M) ^ n

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_pow {M} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] {S : A} (x : S)
    (n : ℕ) : ↑(x ^ n) = (x : M) ^ n :=
  rfl

Submonoid Power Coercion: $(x^n)_S = x^n_M$

Informal description

Let $M$ be a monoid and $S$ a submonoid of $M$ (i.e., $S$ contains the multiplicative identity and is closed under multiplication). For any element $x \in S$ and natural number $n$, the $n$-th power of $x$ in $S$ (when coerced back to $M$) equals the $n$-th power of $x$ in $M$. In other words, $(x^n)_S = x^n_M$ where $(\cdot)_S$ denotes the power operation in $S$ and $(\cdot)_M$ denotes the power operation in $M$.

SubmonoidClass.mk_pow theorem

 {M} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] {S : A} (x : M) (hx : x ∈ S) (n : ℕ) :
  (⟨x, hx⟩ : S) ^ n = ⟨x ^ n, pow_mem hx n⟩

Full source

@[to_additive (attr := simp)]
theorem mk_pow {M} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] {S : A} (x : M)
    (hx : x ∈ S) (n : ℕ) : (⟨x, hx⟩ : S) ^ n = ⟨x ^ n, pow_mem hx n⟩ :=
  rfl

Power of Submonoid Element: $\langle x, hx \rangle^n = \langle x^n, \text{pow\_mem } hx n \rangle$

Informal description

Let $M$ be a monoid and $S$ a submonoid of $M$ (i.e., $S$ contains the multiplicative identity and is closed under multiplication). For any element $x \in M$ with $x \in S$ and any natural number $n$, the $n$-th power of the element $\langle x, hx \rangle$ in $S$ is equal to $\langle x^n, \text{pow\_mem } hx n \rangle$, where $\text{pow\_mem } hx n$ is a proof that $x^n \in S$.

SubmonoidClass.toMulOneClass instance

{M : Type*} [MulOneClass M] {A : Type*} [SetLike A M] [SubmonoidClass A M] (S : A) : MulOneClass S

Full source

/-- A submonoid of a unital magma inherits a unital magma structure. -/
@[to_additive
      "An `AddSubmonoid` of a unital additive magma inherits a unital additive magma structure."]
instance (priority := 75) toMulOneClass {M : Type*} [MulOneClass M] {A : Type*} [SetLike A M]
    [SubmonoidClass A M] (S : A) : MulOneClass S := fast_instance%
  Subtype.coe_injective.mulOneClass Subtype.val rfl (fun _ _ => rfl)

Submonoid Inherits Unital Magma Structure

Informal description

For any monoid $M$ with a multiplicative identity and a subset $S$ of $M$ that forms a submonoid (i.e., $S$ contains the identity and is closed under multiplication), $S$ inherits a unital magma structure from $M$. This means $S$ is equipped with a multiplication operation and a distinguished identity element $1$ that satisfy the same properties as in $M$.

SubmonoidClass.toMonoid instance

{M : Type*} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] (S : A) : Monoid S

Full source

/-- A submonoid of a monoid inherits a monoid structure. -/
@[to_additive "An `AddSubmonoid` of an `AddMonoid` inherits an `AddMonoid` structure."]
instance (priority := 75) toMonoid {M : Type*} [Monoid M] {A : Type*} [SetLike A M]
    [SubmonoidClass A M] (S : A) : Monoid S := fast_instance%
  Subtype.coe_injective.monoid Subtype.val rfl (fun _ _ => rfl) (fun _ _ => rfl)

Submonoid Inherits Monoid Structure

Informal description

For any monoid $M$ and any subset $S$ of $M$ that forms a submonoid (i.e., $S$ contains the multiplicative identity and is closed under multiplication), $S$ inherits a monoid structure from $M$. This means $S$ is equipped with a multiplication operation, a distinguished identity element $1$, and satisfies the associativity and identity laws of a monoid.

SubmonoidClass.toCommMonoid instance

{M} [CommMonoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] (S : A) : CommMonoid S

Full source

/-- A submonoid of a `CommMonoid` is a `CommMonoid`. -/
@[to_additive "An `AddSubmonoid` of an `AddCommMonoid` is an `AddCommMonoid`."]
instance (priority := 75) toCommMonoid {M} [CommMonoid M] {A : Type*} [SetLike A M]
    [SubmonoidClass A M] (S : A) : CommMonoid S := fast_instance%
  Subtype.coe_injective.commMonoid Subtype.val rfl (fun _ _ => rfl) fun _ _ => rfl

Submonoid of Commutative Monoid is Commutative Monoid

Informal description

For any commutative monoid $M$ and any subset $S$ of $M$ that forms a submonoid (i.e., $S$ contains the multiplicative identity and is closed under multiplication), $S$ inherits a commutative monoid structure from $M$. This means $S$ is equipped with a commutative multiplication operation, a distinguished identity element $1$, and satisfies the associativity and identity laws of a commutative monoid.

SubmonoidClass.subtype definition

: S' →* M

Full source

/-- The natural monoid hom from a submonoid of monoid `M` to `M`. -/
@[to_additive "The natural monoid hom from an `AddSubmonoid` of `AddMonoid` `M` to `M`."]
def subtype : S' →* M where
  toFun := Subtype.val; map_one' := rfl; map_mul' _ _ := by simp

Inclusion homomorphism of a submonoid

Informal description

The natural inclusion homomorphism from a submonoid $ S' $ of a monoid $ M $ to $ M $, which maps each element of $ S' $ to itself in $ M $. This homomorphism preserves the multiplicative identity and the multiplication operation.

SubmonoidClass.subtype_apply theorem

(x : S') : SubmonoidClass.subtype S' x = x

Full source

@[to_additive (attr := simp)]
lemma subtype_apply (x : S') :
    SubmonoidClass.subtype S' x = x := rfl

Inclusion Homomorphism Acts as Identity on Submonoid Elements

Informal description

For any element $x$ in a submonoid $S'$ of a monoid $M$, the inclusion homomorphism $\text{subtype}$ maps $x$ to itself, i.e., $\text{subtype}(x) = x$.

SubmonoidClass.subtype_injective theorem

: Function.Injective (SubmonoidClass.subtype S')

Full source

@[to_additive]
lemma subtype_injective :
    Function.Injective (SubmonoidClass.subtype S') :=
  Subtype.coe_injective

Injectivity of Submonoid Inclusion Homomorphism

Informal description

The inclusion homomorphism from a submonoid $S'$ of a monoid $M$ to $M$ is injective. That is, for any $x, y \in S'$, if $\iota(x) = \iota(y)$ in $M$, then $x = y$ in $S'$, where $\iota$ denotes the inclusion map.

SubmonoidClass.coe_subtype theorem

: (SubmonoidClass.subtype S' : S' → M) = Subtype.val

Full source

@[to_additive (attr := simp)]
theorem coe_subtype : (SubmonoidClass.subtype S' : S' → M) = Subtype.val :=
  rfl

Inclusion Homomorphism Equals Subtype Projection for Submonoids

Informal description

The inclusion homomorphism from a submonoid $S'$ of a monoid $M$ to $M$ is equal to the canonical projection map $\text{Subtype.val} \colon S' \to M$ that sends each element of $S'$ to its underlying element in $M$.

Submonoid.mul instance

: Mul S

Full source

/-- A submonoid of a monoid inherits a multiplication. -/
@[to_additive "An `AddSubmonoid` of an `AddMonoid` inherits an addition."]
instance mul : Mul S :=
  ⟨fun a b => ⟨a.1 * b.1, S.mul_mem a.2 b.2⟩⟩

Multiplication on Submonoids

Informal description

For any submonoid $S$ of a monoid $M$, the multiplication operation on $M$ restricts to a multiplication operation on $S$.

Submonoid.one instance

: One S

Full source

/-- A submonoid of a monoid inherits a 1. -/
@[to_additive "An `AddSubmonoid` of an `AddMonoid` inherits a zero."]
instance one : One S :=
  ⟨⟨_, S.one_mem⟩⟩

Submonoid Inherits Identity Element

Informal description

Every submonoid $S$ of a monoid $M$ has a multiplicative identity element, which is the same as the identity element of $M$.

Submonoid.coe_mul theorem

(x y : S) : (↑(x * y) : M) = ↑x * ↑y

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_mul (x y : S) : (↑(x * y) : M) = ↑x * ↑y :=
  rfl

Coercion Preserves Multiplication in Submonoids

Informal description

For any elements $x$ and $y$ in a submonoid $S$ of a monoid $M$, the coercion of their product in $S$ equals the product of their coercions in $M$, i.e., $(x \cdot y) = x \cdot y$ where the left-hand side is interpreted in $S$ and the right-hand side in $M$.

Submonoid.coe_one theorem

: ((1 : S) : M) = 1

Full source

@[to_additive (attr := simp, norm_cast)]
theorem coe_one : ((1 : S) : M) = 1 :=
  rfl

Coercion of Submonoid Identity Equals Monoid Identity

Informal description

For any submonoid $S$ of a monoid $M$, the coercion of the multiplicative identity element $1 \in S$ to $M$ equals the multiplicative identity element $1 \in M$.

Submonoid.mk_eq_one theorem

{a : M} {ha} : (⟨a, ha⟩ : S) = 1 ↔ a = 1

Full source

@[to_additive (attr := simp)]
lemma mk_eq_one {a : M} {ha} : (⟨a, ha⟩ : S) = 1 ↔ a = 1 := by simp [← SetLike.coe_eq_coe]

Submonoid Element Equals Identity iff Underlying Element Equals Identity

Informal description

For any element $a$ in a monoid $M$ and a proof $ha$ that $a$ belongs to a submonoid $S$ of $M$, the submonoid element $\langle a, ha \rangle$ is equal to the identity element $1$ of $S$ if and only if $a$ is equal to the identity element $1$ of $M$.

Submonoid.mk_mul_mk theorem

(x y : M) (hx : x ∈ S) (hy : y ∈ S) : (⟨x, hx⟩ : S) * ⟨y, hy⟩ = ⟨x * y, S.mul_mem hx hy⟩

Full source

@[to_additive (attr := simp)]
theorem mk_mul_mk (x y : M) (hx : x ∈ S) (hy : y ∈ S) :
    (⟨x, hx⟩ : S) * ⟨y, hy⟩ = ⟨x * y, S.mul_mem hx hy⟩ :=
  rfl

Multiplication of Submonoid Elements via Underlying Multiplication

Informal description

For any elements $x, y$ in a monoid $M$ and a submonoid $S$ of $M$, if $x \in S$ and $y \in S$, then the product of the submonoid elements $\langle x, hx \rangle$ and $\langle y, hy \rangle$ is equal to the submonoid element $\langle x * y, S.\text{mul\_mem}\ hx\ hy \rangle$, where $S.\text{mul\_mem}\ hx\ hy$ is the proof that $x * y \in S$.

Submonoid.mul_def theorem

(x y : S) : x * y = ⟨x * y, S.mul_mem x.2 y.2⟩

Full source

@[to_additive]
theorem mul_def (x y : S) : x * y = ⟨x * y, S.mul_mem x.2 y.2⟩ :=
  rfl

Multiplication in Submonoids via Pair Construction

Informal description

For any elements $x, y$ in a submonoid $S$ of a monoid $M$, the product $x * y$ in $S$ is equal to the pair $\langle x * y, h \rangle$, where $h$ is a proof that $x * y$ belongs to $S$ (which follows from the closure under multiplication property of submonoids).

Submonoid.one_def theorem

: (1 : S) = ⟨1, S.one_mem⟩

Full source

@[to_additive]
theorem one_def : (1 : S) = ⟨1, S.one_mem⟩ :=
  rfl

Definition of the Identity Element in a Submonoid

Informal description

The multiplicative identity element $1$ in a submonoid $S$ of a monoid $M$ is equal to the pair $\langle 1, h \rangle$, where $h$ is a proof that $1 \in S$.

Submonoid.toMulOneClass instance

{M : Type*} [MulOneClass M] (S : Submonoid M) : MulOneClass S

Full source

/-- A submonoid of a unital magma inherits a unital magma structure. -/
@[to_additive
      "An `AddSubmonoid` of a unital additive magma inherits a unital additive magma structure."]
instance toMulOneClass {M : Type*} [MulOneClass M] (S : Submonoid M) :
    MulOneClass S := fast_instance%
  Subtype.coe_injective.mulOneClass Subtype.val rfl fun _ _ => rfl

Submonoid Inherits Unital Magma Structure

Informal description

For any monoid $M$ and any submonoid $S$ of $M$, $S$ inherits a unital magma structure from $M$. This means $S$ is equipped with a multiplication operation and a distinguished identity element $1$ that satisfy the same properties as in $M$.

Submonoid.pow_mem theorem

{M : Type*} [Monoid M] (S : Submonoid M) {x : M} (hx : x ∈ S) (n : ℕ) : x ^ n ∈ S

Full source

@[to_additive]
protected theorem pow_mem {M : Type*} [Monoid M] (S : Submonoid M) {x : M} (hx : x ∈ S) (n : ℕ) :
    x ^ n ∈ S :=
  pow_mem hx n

Closure under Powers in Submonoids

Informal description

Let $M$ be a monoid and $S$ a submonoid of $M$. For any element $x \in S$ and any natural number $n$, the power $x^n$ belongs to $S$.

Submonoid.toMonoid instance

{M : Type*} [Monoid M] (S : Submonoid M) : Monoid S

Full source

/-- A submonoid of a monoid inherits a monoid structure. -/
@[to_additive "An `AddSubmonoid` of an `AddMonoid` inherits an `AddMonoid` structure."]
instance toMonoid {M : Type*} [Monoid M] (S : Submonoid M) : Monoid S := fast_instance%
  Subtype.coe_injective.monoid Subtype.val rfl (fun _ _ => rfl) fun _ _ => rfl

Submonoid Inherits Monoid Structure

Informal description

For any monoid $M$ and any submonoid $S$ of $M$, $S$ inherits a monoid structure from $M$.

Submonoid.toCommMonoid instance

{M} [CommMonoid M] (S : Submonoid M) : CommMonoid S

Full source

/-- A submonoid of a `CommMonoid` is a `CommMonoid`. -/
@[to_additive "An `AddSubmonoid` of an `AddCommMonoid` is an `AddCommMonoid`."]
instance toCommMonoid {M} [CommMonoid M] (S : Submonoid M) : CommMonoid S := fast_instance%
  Subtype.coe_injective.commMonoid Subtype.val rfl (fun _ _ => rfl) fun _ _ => rfl

Submonoid of Commutative Monoid is Commutative Monoid

Informal description

For any commutative monoid $M$ and any submonoid $S$ of $M$, $S$ inherits a commutative monoid structure from $M$.

Submonoid.subtype definition

: S →* M

Full source

/-- The natural monoid hom from a submonoid of monoid `M` to `M`. -/
@[to_additive "The natural monoid hom from an `AddSubmonoid` of `AddMonoid` `M` to `M`."]
def subtype : S →* M where
  toFun := Subtype.val; map_one' := rfl; map_mul' _ _ := by simp

Inclusion homomorphism of a submonoid

Informal description

The natural inclusion homomorphism from a submonoid $ S $ of a monoid $ M $ to $ M $, mapping each element of $ S $ to itself in $ M $. This homomorphism preserves the multiplicative identity and the multiplication operation.

Submonoid.subtype_apply theorem

{s : Submonoid M} (x : s) : s.subtype x = x

Full source

@[to_additive (attr := simp)]
lemma subtype_apply {s : Submonoid M} (x : s) :
    s.subtype x = x := rfl

Inclusion Homomorphism Acts as Identity on Submonoid Elements

Informal description

For any submonoid $S$ of a monoid $M$ and any element $x \in S$, the inclusion homomorphism $\text{subtype} \colon S \to M$ maps $x$ to itself, i.e., $\text{subtype}(x) = x$.

Submonoid.subtype_injective theorem

(s : Submonoid M) : Function.Injective s.subtype

Full source

@[to_additive]
lemma subtype_injective (s : Submonoid M) :
    Function.Injective s.subtype :=
  Subtype.coe_injective

Injectivity of Submonoid Inclusion Homomorphism

Informal description

For any submonoid $S$ of a monoid $M$, the inclusion homomorphism $\text{subtype} \colon S \to M$ is injective. That is, if $\text{subtype}(x) = \text{subtype}(y)$ for $x, y \in S$, then $x = y$.

Submonoid.coe_subtype theorem

: ⇑S.subtype = Subtype.val

Full source

@[to_additive (attr := simp)]
theorem coe_subtype : ⇑S.subtype = Subtype.val :=
  rfl

Inclusion Homomorphism Equals Subtype Val for Submonoids

Informal description

The inclusion homomorphism from a submonoid $S$ of a monoid $M$ to $M$ is equal to the canonical inclusion function $\text{Subtype.val} \colon S \to M$ that maps each element of $S$ to itself in $M$.

Mathlib.Algebra.Group.Submonoid.Defs

Main definitions

Implementation notes

Tags