Constant maps and aperiodicity

Convention: Function.End Q multiplies by composition, (f * g) x = f (g x).

• constEnd q — the constant map _ ↦ q, and the predicate IsConstEnd;
• constEnd_mul — constant maps are left zeros: constEnd p * t = constEnd p;
• eq_constEnd_of_R_constEnd — anything R-related to a constant map is that constant map;
• isAperiodicElem_of_id_or_const — in a submonoid of Function.End Q whose elements are all the identity or constant maps, every element is aperiodic. This is what makes the reset monoids used in the decomposition genuine aperiodic factors.

Reset / rank-drop transformations: the constant maps

A constant map constEnd q : Q → Q, _ ↦ q, has one-point image. It is nonsurjective when Q has more than one point. Constant maps are the aperiodic building blocks of the reset monoids used in the decomposition.

Function.End Q has multiplication (f * g) x = f (g x) and unit 1 = id. Under this convention:

• constEnd p * t = constEnd p — a constant map absorbs on the left;
• t * constEnd q = constEnd (t q) — composing a constant on the right yields the constant constEnd (t q);

so the constant maps form a two-sided ideal of Function.End Q, and among themselves constEnd p * constEnd q = constEnd p, i.e. they form a left-zero semigroup. Left-zero semigroups are aperiodic, and any transformation monoid all of whose non-identity elements are constants is therefore aperiodic.

def LeanPool.KrohnRhodes.constEnd {Q : Type u} (q : Q) : Function.End Q

The constant transformation _ ↦ q of Q, as an element of the full transformation monoid Function.End Q.

Equations

• LeanPool.KrohnRhodes.constEnd q x✝ = q

def LeanPool.KrohnRhodes.IsConstEnd {Q : Type u} (t : Function.End Q) : Prop

A transformation of Q is constant if it equals constEnd q for some q — equivalently, its image has exactly one point.

Equations

• LeanPool.KrohnRhodes.IsConstEnd t = ∃ (q : Q), t = LeanPool.KrohnRhodes.constEnd q

theorem LeanPool.KrohnRhodes.isConstEnd_constEnd {Q : Type u} (q : Q) : IsConstEnd (constEnd q)

@[simp]

theorem LeanPool.KrohnRhodes.constEnd_mul {Q : Type u} (p : Q) (t : Function.End Q) : constEnd p * t = constEnd p

A constant map absorbs on the left: constEnd p * t = constEnd p for every transformation t. ((constEnd p * t) x = constEnd p (t x) = p.)

Aperiodicity of constant transformation monoids

The constant maps are aperiodic. The key observation is purely multiplicative: anything R-related (inside Function.End Q) to a constant map equals that constant map — because constEnd p * s is always constEnd p (left absorption: (constEnd p * s) x = constEnd p (s x) = p), so constEnd p * s = b forces b = constEnd p. Hence any two H-related constants are equal.

(Note the convention: Function.End Q has (f * g) x = f (g x), so a constant map absorbs on the left of a product — it is a left zero of the monoid — and it is Green.R that collapses constants, not Green.L.)

theorem LeanPool.KrohnRhodes.eq_constEnd_of_R_constEnd {Q : Type u} {p : Q} {b : Function.End Q} (h : Green.R (constEnd p) b) : b = constEnd p

Anything right-related to a constant map is that constant map. If Green.R (constEnd p) b holds in Function.End Q, then b = constEnd p. (Green.R provides s with constEnd p * s = b, and constEnd p * s collapses to constEnd p by left absorption.)

Reset-monoid aperiodicity: monoids of constants-plus-identity

A transformation monoid S ≤ Function.End Q all of whose non-identity elements are constant maps is aperiodic. This is the structure of the reset monoids used in the decomposition (the identity together with constant maps).

We phrase the aperiodicity hypothesis on a Submonoid (Function.End Q).

theorem LeanPool.KrohnRhodes.isAperiodicElem_of_id_or_const {Q : Type u} (S : Submonoid (Function.End Q)) (hS : ∀ t ∈ S, t = 1 ∨ IsConstEnd t) (a b : ↥S) : ((∃ (s : ↥S) (t : ↥S), s * a = b ∧ t * b = a) ∧ ∃ (s : ↥S) (t : ↥S), a * s = b ∧ b * t = a) → a = b

A constants-plus-identity transformation monoid is aperiodic. Let S be a submonoid of Function.End Q such that every element of S is either the identity or a constant map (hS). Then every element of S is aperiodic: any two H-related elements a, b ∈ S are equal.

Proof by cases on a:

• if a is constant, H a b gives Green.R a b, so eq_constEnd_of_R_constEnd forces b = a;
• if a = 1, H 1 b gives Green.R 1 b, providing t with (1 : Function.End Q) * t = b and b * t' = 1. If b is also 1 we are done; if b is a constant constEnd q, then b * t' = constEnd q by left absorption, so constEnd q = 1, i.e. Q is subsingleton, and then Function.End Q is subsingleton so a = b regardless.

The conclusion is stated with H unfolded into explicit L- and R-witnesses.