Monoid division and local divisors

• MonoidDivides M N — M is a quotient of a submonoid of N; MonoidDivides.trans shows division is transitive.
• LocalDivisor M c — the local divisor M_c of M at c: the set cM ∩ Mc with the product x ∘ y = x · y₀ for y = c · y₀ and identity c, with its Monoid and Finite instances; LocalDivisor.localDivides shows M_c divides M.

References

• [V. Diekert, M. Kufleitner, B. Steinberg, The Krohn–Rhodes Theorem and Local Divisors, Fundamenta Informaticae 116 (2012); arXiv:1111.1585]

Monoid division

def LeanPool.KrohnRhodes.MonoidDivides (M : Type u_1) (N : Type u_2) [Monoid M] [Monoid N] : Prop

A monoid M divides a monoid N if M is a quotient of a submonoid of N. Equivalently, there exists a surjective monoid homomorphism from a submonoid of N onto M.

Equations

• LeanPool.KrohnRhodes.MonoidDivides M N = ∃ (S : Submonoid N) (φ : ↥S →* M), Function.Surjective ⇑φ

theorem LeanPool.KrohnRhodes.MonoidDivides.trans {M : Type u_1} {N : Type u_2} {P : Type u_3} [Monoid M] [Monoid N] [Monoid P] (h1 : MonoidDivides M N) (h2 : MonoidDivides N P) : MonoidDivides M P

Monoid division is transitive. If M ≼ N (witnessed by S ≤ N, φ : S ↠ M) and N ≼ P (witnessed by T ≤ P, ψ : T ↠ N), then M ≼ P. The witnessing submonoid of P is the image under T ↪ P of the pre-image ψ⁻¹(S) ≤ T; the surjection is φ ∘ (ψ restricted) ∘ (the submonoid iso). This is the standard composition of "quotient of a submonoid" relations.

The local divisor M_c = cM ∩ Mc

For c ∈ M, the local divisor (Diekert–Kufleitner–Steinberg) is

M_c := cM ∩ Mc, with the twisted product x ∘ y := x · y₀ (any y₀ with y = c·y₀), identity c.

The twisted product is well-defined because for x ∈ Mc and y = c·y₀ the value x·y₀ does not depend on the choice of y₀. M_c divides M (localDivides). This is the larger local divisor described in DKS Section 2.5; their decomposition uses the potentially smaller submonoid cMc ∪ {c}.

def LeanPool.KrohnRhodes.LocalDivisor (M : Type u_1) [Monoid M] (c : M) : Type u_1

The carrier of the local divisor of a monoid M at c: the two-sided set cM ∩ Mc = {x | (∃ a, x = c*a) ∧ (∃ b, x = b*c)}. As a subtype of M.

Equations

• LeanPool.KrohnRhodes.LocalDivisor M c = { x : M // (∃ (a : M), x = c * a) ∧ ∃ (b : M), x = b * c }

def LeanPool.KrohnRhodes.LocalDivisor.val {M : Type u_1} [Monoid M] {c : M} (x : LocalDivisor M c) : M

The underlying element of M of a local-divisor element.

Equations

• x.val = ↑x

theorem LeanPool.KrohnRhodes.LocalDivisor.ext {M : Type u_1} [Monoid M] {c : M} {x y : LocalDivisor M c} (h : x.val = y.val) : x = y

theorem LeanPool.KrohnRhodes.LocalDivisor.ext_iff {M : Type u_1} [Monoid M] {c : M} {x y : LocalDivisor M c} : x = y ↔ x.val = y.val

theorem LeanPool.KrohnRhodes.LocalDivisor.mem_left {M : Type u_1} [Monoid M] {c : M} (x : LocalDivisor M c) : ∃ (a : M), x.val = c * a

theorem LeanPool.KrohnRhodes.LocalDivisor.mem_right {M : Type u_1} [Monoid M] {c : M} (x : LocalDivisor M c) : ∃ (b : M), x.val = b * c

@[instance_reducible]

noncomputable instance LeanPool.KrohnRhodes.LocalDivisor.instMul {M : Type u_1} [Monoid M] {c : M} : Mul (LocalDivisor M c)

The twisted product x ∘ y = x · y₀ where y = c · y₀ (the value is independent of the choice of y₀, by x ∈ Mc). Implemented via Classical.choose of the left-membership of y.

Equations

• LeanPool.KrohnRhodes.LocalDivisor.instMul = { mul := fun (x y : LeanPool.KrohnRhodes.LocalDivisor M c) => ⟨x.val * Classical.choose ⋯, ⋯⟩ }

theorem LeanPool.KrohnRhodes.LocalDivisor.mul_val {M : Type u_1} [Monoid M] {c : M} (x y : LocalDivisor M c) : (x * y).val = x.val * Classical.choose ⋯

theorem LeanPool.KrohnRhodes.LocalDivisor.mul_val_of_eq {M : Type u_1} [Monoid M] {c : M} (x y : LocalDivisor M c) {y₀ : M} (hy₀ : y.val = c * y₀) : (x * y).val = x.val * y₀

The defining identity for the product: if y.val = c * y₀ for any y₀, then (x * y).val = x.val * y₀. (Independence of the chosen witness, using x.val ∈ Mc.)

@[instance_reducible]

noncomputable instance LeanPool.KrohnRhodes.LocalDivisor.instOne {M : Type u_1} [Monoid M] {c : M} : One (LocalDivisor M c)

The identity element of the local divisor is c itself (c = c*1 = 1*c ∈ cM ∩ Mc).

Equations

• LeanPool.KrohnRhodes.LocalDivisor.instOne = { one := ⟨c, ⋯⟩ }

theorem LeanPool.KrohnRhodes.LocalDivisor.one_val {M : Type u_1} [Monoid M] {c : M} : val 1 = c

@[instance_reducible]

noncomputable instance LeanPool.KrohnRhodes.LocalDivisor.instMonoid {M : Type u_1} [Monoid M] {c : M} : Monoid (LocalDivisor M c)

Equations

• One or more equations did not get rendered due to their size.

instance LeanPool.KrohnRhodes.LocalDivisor.instFinite {M : Type u_1} [Monoid M] {c : M} [Finite M] : Finite (LocalDivisor M c)

The local divisor is finite when M is (it is a subtype of M).

theorem LeanPool.KrohnRhodes.LocalDivisor.localDivides {M : Type u_1} [Monoid M] {c : M} : MonoidDivides (LocalDivisor M c) M

The local divisor M_c divides M. The witnessing submonoid is S = {t : M | c·t ∈ Mc} (so that c·t ∈ cM ∩ Mc), and the surjection is γ(t) = c·t. This is a monoid homomorphism for the twisted product, and every x ∈ cM ∩ Mc is γ(a) for the witness a of x ∈ cM.