An automorphism of a lattice with the eigenvalue one has infinite Reidemeister number (Lemma 4)
ProvedRInf.eigen_one_infIf the automorphism of the standard integer lattice of rank k has the eigenvalue one - some nonzero vector is fixed - then its Reidemeister number is infinite. On the abelian lattice the twisted conjugacy classes are the cosets of the image of the map taking z to z minus the image of z under the automorphism, and the index of this image is infinite because the determinant of one minus the automorphism vanishes at the eigenvalue one.
import Mathlib import Definitions.Def_RInf_alg import Definitions.Def_RInf_braid
namespace RInf
/-! Milestone 3 (Lemma 4, eigenvalue-one refinement): an automorphism of a
standard integer lattice with the eigenvalue one has infinite Reidemeister
number. If some nonzero vector is fixed by m, the Reidemeister number of m is
infinite: on the abelian lattice the twisted conjugacy classes are the
cosets of the image of the map taking z to z minus m z, whose determinant
vanishes at the eigenvalue one, so the index of the image is infinite. -/
theorem eigen_one_inf {k : Nat} (m : (Fin k → Int) ≃+ (Fin k → Int))
(h : HasEigenOne m) : ReidInfAdd m := by sorry
end RInf
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: if the automorphism m of the integer lattice of rank k has the eigenvalue one in the sense of the interface - a nonzero vector is fixed - then the Reidemeister number of m is infinite: there is an infinite sequence of pairwise non-twisted-conjugate lattice elements. Hypotheses: the eigenvalue-one property of m.