Defining a monoid given by generators and relations

Given relations rels on the free monoid on a type α, this file constructs the monoid given by generators x : α and relations rels.

Main definitions

• PresentedMonoid rels: the quotient of the free monoid on a type α by the closure of one-step reductions (arising from a binary relation on free monoid elements rels).
• PresentedMonoid.of: The canonical map from α to a presented monoid with generators α.
• PresentedMonoid.lift f: the canonical monoid homomorphism PresentedMonoid rels → M, given a function f : α → G from a type α to a monoid M which satisfies the relations rels.

Tags

generators, relations, monoid presentations

def PresentedMonoid {α : Type u_1} (rel : FreeMonoid α → FreeMonoid α → Prop) : Type u_1

Given a set of relations, rels, over a type α, PresentedMonoid constructs the monoid with generators x : α and relations rels as a quotient of a congruence structure over rels.

Equations

• PresentedMonoid rel = (conGen rel).Quotient

def PresentedAddMonoid {α : Type u_1} (rel : FreeAddMonoid α → FreeAddMonoid α → Prop) : Type u_1

Given a set of relations, rels, over a type α, PresentedAddMonoid constructs the monoid with generators x : α and relations rels as a quotient of an AddCon structure over rels

Equations

• PresentedAddMonoid rel = (addConGen rel).Quotient

instance PresentedMonoid.instMonoid {α : Type u_1} {rels : FreeMonoid α → FreeMonoid α → Prop} : Monoid (PresentedMonoid rels)

Equations

• PresentedMonoid.instMonoid = (conGen rels).monoid

instance PresentedAddMonoid.instAddMonoid {α : Type u_1} {rels : FreeAddMonoid α → FreeAddMonoid α → Prop} : AddMonoid (PresentedAddMonoid rels)

Equations

• PresentedAddMonoid.instAddMonoid = (addConGen rels).addMonoid

def PresentedMonoid.mk {α : Type u_1} (rels : FreeMonoid α → FreeMonoid α → Prop) : FreeMonoid α →* PresentedMonoid rels

The quotient map from the free monoid on α to the presented monoid with the same generators and the given relations rels.

Equations

• PresentedMonoid.mk rels = { toFun := Quotient.mk (conGen rels).toSetoid, map_one' := ⋯, map_mul' := ⋯ }

def PresentedAddMonoid.mk {α : Type u_1} (rels : FreeAddMonoid α → FreeAddMonoid α → Prop) : FreeAddMonoid α →+ PresentedAddMonoid rels

The quotient map from the free additive monoid on α to the presented additive monoid with the same generators and the given relations rels

Equations

• PresentedAddMonoid.mk rels = { toFun := Quotient.mk (addConGen rels).toSetoid, map_zero' := ⋯, map_add' := ⋯ }

def PresentedMonoid.of {α : Type u_1} (rels : FreeMonoid α → FreeMonoid α → Prop) (x : α) : PresentedMonoid rels

of is the canonical map from α to a presented monoid with generators x : α. The term x is mapped to the equivalence class of the image of x in FreeMonoid α.

Equations

• PresentedMonoid.of rels x = (PresentedMonoid.mk rels) (FreeMonoid.of x)

def PresentedAddMonoid.of {α : Type u_1} (rels : FreeAddMonoid α → FreeAddMonoid α → Prop) (x : α) : PresentedAddMonoid rels

of is the canonical map from α to a presented additive monoid with generators x : α. The term x is mapped to the equivalence class of the image of x in FreeAddMonoid α

Equations

• PresentedAddMonoid.of rels x = (PresentedAddMonoid.mk rels) (FreeAddMonoid.of x)

theorem PresentedMonoid.inductionOn {α₁ : Type u_2} {rels₁ : FreeMonoid α₁ → FreeMonoid α₁ → Prop} {δ : PresentedMonoid rels₁ → Prop} (q : PresentedMonoid rels₁) (h : ∀ (a : FreeMonoid α₁), δ ((PresentedMonoid.mk rels₁) a)) : δ q

theorem PresentedAddMonoid.inductionOn {α₁ : Type u_2} {rels₁ : FreeAddMonoid α₁ → FreeAddMonoid α₁ → Prop} {δ : PresentedAddMonoid rels₁ → Prop} (q : PresentedAddMonoid rels₁) (h : ∀ (a : FreeAddMonoid α₁), δ ((PresentedAddMonoid.mk rels₁) a)) : δ q

theorem PresentedMonoid.inductionOn₂ {α₁ : Type u_2} {α₂ : Type u_3} {rels₁ : FreeMonoid α₁ → FreeMonoid α₁ → Prop} {rels₂ : FreeMonoid α₂ → FreeMonoid α₂ → Prop} {δ : PresentedMonoid rels₁ → PresentedMonoid rels₂ → Prop} (q₁ : PresentedMonoid rels₁) (q₂ : PresentedMonoid rels₂) (h : ∀ (a : FreeMonoid α₁) (b : FreeMonoid α₂), δ ((PresentedMonoid.mk rels₁) a) ((PresentedMonoid.mk rels₂) b)) : δ q₁ q₂

theorem PresentedAddMonoid.inductionOn₂ {α₁ : Type u_2} {α₂ : Type u_3} {rels₁ : FreeAddMonoid α₁ → FreeAddMonoid α₁ → Prop} {rels₂ : FreeAddMonoid α₂ → FreeAddMonoid α₂ → Prop} {δ : PresentedAddMonoid rels₁ → PresentedAddMonoid rels₂ → Prop} (q₁ : PresentedAddMonoid rels₁) (q₂ : PresentedAddMonoid rels₂) (h : ∀ (a : FreeAddMonoid α₁) (b : FreeAddMonoid α₂), δ ((PresentedAddMonoid.mk rels₁) a) ((PresentedAddMonoid.mk rels₂) b)) : δ q₁ q₂

theorem PresentedMonoid.inductionOn₃ {α₁ : Type u_2} {α₂ : Type u_3} {α₃ : Type u_4} {rels₁ : FreeMonoid α₁ → FreeMonoid α₁ → Prop} {rels₂ : FreeMonoid α₂ → FreeMonoid α₂ → Prop} {rels₃ : FreeMonoid α₃ → FreeMonoid α₃ → Prop} {δ : PresentedMonoid rels₁ → PresentedMonoid rels₂ → PresentedMonoid rels₃ → Prop} (q₁ : PresentedMonoid rels₁) (q₂ : PresentedMonoid rels₂) (q₃ : PresentedMonoid rels₃) (h : ∀ (a : FreeMonoid α₁) (b : FreeMonoid α₂) (c : FreeMonoid α₃), δ ((PresentedMonoid.mk rels₁) a) ((PresentedMonoid.mk rels₂) b) ((PresentedMonoid.mk rels₃) c)) : δ q₁ q₂ q₃

theorem PresentedAddMonoid.inductionOn₃ {α₁ : Type u_2} {α₂ : Type u_3} {α₃ : Type u_4} {rels₁ : FreeAddMonoid α₁ → FreeAddMonoid α₁ → Prop} {rels₂ : FreeAddMonoid α₂ → FreeAddMonoid α₂ → Prop} {rels₃ : FreeAddMonoid α₃ → FreeAddMonoid α₃ → Prop} {δ : PresentedAddMonoid rels₁ → PresentedAddMonoid rels₂ → PresentedAddMonoid rels₃ → Prop} (q₁ : PresentedAddMonoid rels₁) (q₂ : PresentedAddMonoid rels₂) (q₃ : PresentedAddMonoid rels₃) (h : ∀ (a : FreeAddMonoid α₁) (b : FreeAddMonoid α₂) (c : FreeAddMonoid α₃), δ ((PresentedAddMonoid.mk rels₁) a) ((PresentedAddMonoid.mk rels₂) b) ((PresentedAddMonoid.mk rels₃) c)) : δ q₁ q₂ q₃

@[simp]

theorem PresentedMonoid.closure_range_of {α : Type u_2} (rels : FreeMonoid α → FreeMonoid α → Prop) : Submonoid.closure (Set.range (PresentedMonoid.of rels)) = ⊤

The generators of a presented monoid generate the presented monoid. That is, the submonoid closure of the set of generators equals ⊤.

@[simp]

theorem PresentedAddMonoid.closure_range_of {α : Type u_2} (rels : FreeAddMonoid α → FreeAddMonoid α → Prop) : AddSubmonoid.closure (Set.range (PresentedAddMonoid.of rels)) = ⊤

The generators of a presented additive monoid generate the presented additive monoid. That is, the additive submonoid closure of the set of generators equals ⊤

theorem PresentedMonoid.surjective_mk {α : Type u_2} {rels : FreeMonoid α → FreeMonoid α → Prop} : Function.Surjective ⇑(PresentedMonoid.mk rels)

theorem PresentedAddMonoid.surjective_mk {α : Type u_2} {rels : FreeAddMonoid α → FreeAddMonoid α → Prop} : Function.Surjective ⇑(PresentedAddMonoid.mk rels)

def PresentedMonoid.lift {α : Type u_3} {M : Type u_4} [Monoid M] (f : α → M) {rels : FreeMonoid α → FreeMonoid α → Prop} (h : ∀ (a b : FreeMonoid α), rels a b → (FreeMonoid.lift f) a = (FreeMonoid.lift f) b) : PresentedMonoid rels →* M

The extension of a map f : α → M that satisfies the given relations to a monoid homomorphism from PresentedMonoid rels → M.

Equations

• PresentedMonoid.lift f h = (conGen rels).lift (FreeMonoid.lift f) ⋯

def PresentedAddMonoid.lift {α : Type u_3} {M : Type u_4} [AddMonoid M] (f : α → M) {rels : FreeAddMonoid α → FreeAddMonoid α → Prop} (h : ∀ (a b : FreeAddMonoid α), rels a b → (FreeAddMonoid.lift f) a = (FreeAddMonoid.lift f) b) : PresentedAddMonoid rels →+ M

The extension of a map f : α → M that satisfies the given relations to an additive-monoid homomorphism from PresentedAddMonoid rels → M

Equations

• PresentedAddMonoid.lift f h = (addConGen rels).lift (FreeAddMonoid.lift f) ⋯

theorem PresentedMonoid.toMonoid.unique {α : Type u_3} {M : Type u_4} [Monoid M] (f : α → M) {rels : FreeMonoid α → FreeMonoid α → Prop} (h : ∀ (a b : FreeMonoid α), rels a b → (FreeMonoid.lift f) a = (FreeMonoid.lift f) b) (g : (conGen rels).Quotient →* M) (hg : ∀ (a : α), g (PresentedMonoid.of rels a) = f a) : g = PresentedMonoid.lift f h

theorem PresentedAddMonoid.toMonoid.unique {α : Type u_3} {M : Type u_4} [AddMonoid M] (f : α → M) {rels : FreeAddMonoid α → FreeAddMonoid α → Prop} (h : ∀ (a b : FreeAddMonoid α), rels a b → (FreeAddMonoid.lift f) a = (FreeAddMonoid.lift f) b) (g : (addConGen rels).Quotient →+ M) (hg : ∀ (a : α), g (PresentedAddMonoid.of rels a) = f a) : g = PresentedAddMonoid.lift f h

@[simp]

theorem PresentedMonoid.lift_of {α : Type u_3} {M : Type u_4} [Monoid M] (f : α → M) {rels : FreeMonoid α → FreeMonoid α → Prop} (h : ∀ (a b : FreeMonoid α), rels a b → (FreeMonoid.lift f) a = (FreeMonoid.lift f) b) {x : α} : (PresentedMonoid.lift f h) (PresentedMonoid.of rels x) = f x

@[simp]

theorem PresentedAddMonoid.lift_of {α : Type u_3} {M : Type u_4} [AddMonoid M] (f : α → M) {rels : FreeAddMonoid α → FreeAddMonoid α → Prop} (h : ∀ (a b : FreeAddMonoid α), rels a b → (FreeAddMonoid.lift f) a = (FreeAddMonoid.lift f) b) {x : α} : (PresentedAddMonoid.lift f h) (PresentedAddMonoid.of rels x) = f x

theorem PresentedAddMonoid.ext {α : Type u_2} {M : Type u_3} [AddMonoid M] (rels : FreeAddMonoid α → FreeAddMonoid α → Prop) {φ ψ : PresentedAddMonoid rels →+ M} (hx : ∀ (x : α), φ (PresentedAddMonoid.of rels x) = ψ (PresentedAddMonoid.of rels x)) : φ = ψ

theorem PresentedMonoid.ext {α : Type u_2} {M : Type u_3} [Monoid M] (rels : FreeMonoid α → FreeMonoid α → Prop) {φ ψ : PresentedMonoid rels →* M} (hx : ∀ (x : α), φ (PresentedMonoid.of rels x) = ψ (PresentedMonoid.of rels x)) : φ = ψ