The algebraic layer: link-homotopy congruences and trivial elements
DefinitionHGL_algThe algebraic interface of link homotopy for generalized string links over surfaces. The definition carries: a link-homotopy congruence on a monoid - an equivalence relation together with compatibility with the concatenation product, so that equivalent factors concatenate to equivalent products, the algebraic form of Lemma 3.4 of the paper - and the triviality predicate for elements of the monoid, through which the link-homotopically trivial braids of Proposition 3.6 are expressed: an element is trivial when it is equivalent to the identity under the congruence. The congruence is the interface through which the quotient structures of the paper - the class group and the quotient of the surface braid group by its trivial braids - are constructed, and it is what makes those quotients respect the concatenation product.
import Mathlib
/-!
# The algebraic layer: link-homotopy congruences and trivial elements
The algebraic layer of the HGL mission, carrying the interface of Juliana
R. T. Theodoro de Lima, "Homotopy of braids on surfaces: extending
Goldsmith's answer to Artin" (Journal of Knot Theory and Its Ramifications
28 (2019) 1950013): the congruence on a monoid determined by the
link-homotopy moves - an equivalence relation compatible with the
concatenation product, the algebraic form of Lemma 3.4 - together with the
triviality predicate for elements equivalent to the identity, through which
the link-homotopically trivial braids of Proposition 3.6 are expressed.
-/
namespace HGL
/-- The equivalence relation generated by a relation: the inductive
closure of the relation under reflexivity, symmetry, and transitivity.
The link-homotopy relation of the world layer is the equivalence relation
generated by the elementary link-homotopy moves. -/
inductive EqvGen {S : Type*} (r : S → S → Prop) : S → S → Prop
| refl (s : S) : EqvGen r s s
| symm {s t : S} : EqvGen r s t → EqvGen r t s
| trans {s t u : S} : EqvGen r s t → EqvGen r t u → EqvGen r s u
| step {s t : S} : r s t → EqvGen r s t
/-- A link-homotopy congruence on a monoid: an equivalence relation
together with compatibility with the multiplication, the algebraic
counterpart of Lemma 3.4 of the source paper. -/
structure LinkHomotopyCongruence (S : Type*) [Monoid S] where
/-- The underlying relation. -/
rel : S → S → Prop
/-- Reflexivity. -/
refl : ∀ s : S, rel s s
/-- Symmetry. -/
symm : ∀ s t : S, rel s t → rel t s
/-- Transitivity. -/
trans : ∀ s t u : S, rel s t → rel t u → rel s u
/-- Compatibility with the multiplication: equivalent factors concatenate
to equivalent products. -/
mul_compat : ∀ s t u v : S, rel s t → rel u v → rel (s * u) (t * v)
/-- The element s is trivial under the relation rel: it is equivalent to
the identity. The link-homotopically trivial braids are the braids whose
images are trivial under link-homotopy. -/
def TrivialUnder {S : Type*} [Monoid S] (rel : S → S → Prop) (s : S) : Prop :=
rel s 1
end HGL