Permutation representations on lattice norm shells

Self-isometries of an integral lattice permute its vectors of any specified norm. If those vectors span the rational ambient space, this permutation representation is faithful. It represents the full lattice isometry group, not merely a subgroup generated by selected isometries.

The construction restricts the native carrier equivalence of a lattice isometry; faithfulness uses LinearMap.ext_on on the rational span of the shell.

def TauCeti.IntegralLattice.Isometry.normShellHom {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (n : ℚ) : L.Isometry L →* Equiv.Perm ↑(L.vectorsOfNorm n)

The permutation representation of the full lattice isometry group on a norm shell.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.coe_normShellHom_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (e : L.Isometry L) (n : ℚ) (x : ↑(L.vectorsOfNorm n)) : ↑↑(((normShellHom L n) e) x) = e ↑↑x

On ambient vectors, the shell permutation is the original lattice isometry.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.coe_normShellHom_symm_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (e : L.Isometry L) (n : ℚ) (x : ↑(L.vectorsOfNorm n)) : ↑↑((Equiv.symm ((normShellHom L n) e)) x) = e.symm ↑↑x

On ambient vectors, the inverse shell permutation is the inverse lattice isometry.

theorem TauCeti.IntegralLattice.Isometry.normShellHom_injective {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (n : ℚ) (hspan : Submodule.span ℚ (Subtype.val '' L.vectorsOfNorm n) = ⊤) : Function.Injective ⇑(normShellHom L n)

Isometries are determined by a norm shell that spans their rational ambient space.