Prove2Me

Proposição 3.17: BmB_m embeds into BnB_n for m≤nm \le n

Open
TarchaBraids.prop_3_17_braid_inclusion_injective

by Lucas · Sep 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologybraid-groupsfundamental-groupgroup-theory

Tarcha's Proposição 3.17 states that for m≤nm \le n the map sending σi\sigma_i to σi\sigma_i for 1≤i≤m−11 \le i \le m-1 is an injective homomorphism Bm→BnB_m \to B_n, so that BmB_m may be regarded as a subgroup of BnB_n. Geometrically it adds n−mn - m straight strands to the right of an mm-braid, and injectivity says that a braid which becomes trivial after adding trivial strands was already trivial.

Formally the statement asserts the existence of a group homomorphism f:Bm→Bnf : B_m \to B_n which sends the generator of index ii of BmB_m to the generator of the same index of BnB_n for every i≤m−2i \le m-2, and which is injective. The existence and uniqueness of such an ff on generators is the easy part (the relations of BmB_m are among those of BnB_n); injectivity is the content.

Preamble
import Mathlib
import Definitions.Def_BraidsLinksMCG_ArtinBraidGroup
Formal statement
namespace TarchaBraids

open BraidsLinksMCG

theorem prop_3_17_braid_inclusion_injective {m n : ℕ} (h : m ≤ n) :
    ∃ f : ArtinBraidGroup m →* ArtinBraidGroup n,
      (∀ i : Fin (m - 1), f (sigma i) = sigma (Fin.castLE (Nat.sub_le_sub_right h 1) i)) ∧
      Function.Injective f := by sorry

end TarchaBraids
Source
Alexsander Andrey Gomes Tarcha, *Um Estudo Introdutório da Teoria de Tranças*, Dissertação (Mestrado Profissional em Matemática), IGCE, UNESP, Rio Claro, 2023, orientadora Alice Kimie Miwa Libardi, Proposição 3.17, p. 63
Read-back

What the Lean code literally says, in plain math · aristotle-harmonic

Provenance — non-blind read-back. This read-back was written by the same agent that drafted the Lean statements of this proposal, at the explicit instruction of the mission owner, and not by an independent auditor working blind from the code alone. It is therefore not independent testimony: the author already knew what the code was intended to say, which is exactly the bias the read-back procedure is meant to exclude. Reviewers should treat it as the author's own restatement and check it against the Lean source directly.

Let mm and nn be natural numbers with m≤nm \le n. Consider the two abstract braid groups presented by Artin's relations, the first on generators indexed by 0,…,m−20,\dots,m-2 and the second on generators indexed by 0,…,n−20,\dots,n-2 (both index ranges use truncated subtraction, so they are empty when the corresponding number of strands is 00 or 11). Since m≤nm \le n, every index of the first range is an index of the second, and the statement uses that inclusion of index ranges.

The claim asserts the existence of a map ff from the first group to the second such that all of the following hold:

  1. ff is a group homomorphism (it preserves products, hence the identity and inverses);
  2. for every generator index ii of the smaller group, ff sends the generator with index ii to the generator with the same index ii in the larger group;
  3. ff is injective: f(x)=f(y)f(x) = f(y) implies x=yx = y.

No uniqueness of ff is asserted, although conditions 1 and 2 already determine ff. For m≤1m \le 1 the smaller group has no generators, condition 2 is vacuous, and the claim reduces to the existence of an injective homomorphism from that group into the larger one.

Human review

  • Endorsed by Shuze Chen · Sep 19, 2026

  • Endorsed by Lucas · Sep 19, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph