feat(CondensedMatter): action of crystal symmetries on dual group

Physlib.lean

@@ -57,6 +57,7 @@ public import Physlib.CondensedMatter.Crystal.Bravais.Basic
 public import Physlib.CondensedMatter.Crystal.Embedding
 public import Physlib.CondensedMatter.Crystal.PeriodicGraph
 public import Physlib.CondensedMatter.Crystal.Symmetries
+public import Physlib.CondensedMatter.Crystal.Symmetry.Dual
 public import Physlib.CondensedMatter.Crystal.Symmetry.PointOperations
 public import Physlib.CondensedMatter.LatticeModels.Basic
 public import Physlib.CondensedMatter.ManyBody.Basic

Physlib/CondensedMatter/Crystal/Symmetry/Dual.lean

@@ -0,0 +1,146 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Physlib.CondensedMatter.Crystal.Symmetries
+public import Mathlib.Topology.Algebra.PontryaginDual
+
+/-!
+# Crystal momentum and translation characters
+
+Crystal symmetries act on the characters of the translations, which are the crystal momenta.
+
+## i. Overview
+
+A wave moving through a crystal picks up a phase whenever it is shifted by a lattice vector.
+For a Bloch wave, these phases encode its crystal momentum. Since momenta differing by a
+reciprocal lattice vector produce the same phases, crystal momentum naturally lives in the
+dual of the translation lattice: the Brillouin zone.
+
+Crystal symmetries also act on momentum. A symmetry transforms a translation by its lattice
+automorphism and consequently acts on characters by the inverse automorphism. Translations
+themselves leave momentum unchanged, so only the point-group part of a symmetry matters.
+This gives an action of the crystal symmetry group modulo translations on the Brillouin zone.
+
+This momentum space is `TranslationDual`, with the symmetry action and its quotient action
+`pointAction`. The translation lattice has the discrete topology, so every character is
+continuous.
+
+## ii. Key results
+
+- `TranslationDual` : the circle-valued characters of the translation group.
+- `Symmetry.smul_dual_apply` : the action evaluates a character at the inverse image of a step.
+- `Symmetry.smul_dual_lattice` : transforming a character and a step preserves the value.
+- `Symmetry.translation_smul_dual` : pure translations fix every character.
+- `pointAction` : the action of the symmetries modulo translations.
+- `mk_smul` : a symmetry class acts through any representative.
+
+## iii. Table of contents
+
+- A. Translation characters
+- B. Symmetry action
+- C. Action modulo translations
+
+## iv. References
+
+* N. W. Ashcroft and N. D. Mermin, *Solid State Physics*, Chapter 8.
+
+-/
+
+@[expose] public section
+
+namespace Physlib.CondensedMatter.Crystal
+
+variable {G : Type*} [AddCommGroup G] [AddGroup.FG G]
+  [TopologicalSpace G] [DiscreteTopology G]
+
+/-! ## A. Translation characters -/
+
+/-- Circle-valued characters of the translation group `G`, multiplied pointwise. -/
+abbrev TranslationDual (G : Type*) [AddCommGroup G] [TopologicalSpace G] :=
+  PontryaginDual (Multiplicative G)
+
+/-- Precompose `χ` with the lattice automorphism `A`. -/
+noncomputable def dualMap (A : G ≃+ G) (χ : TranslationDual G) : TranslationDual G :=
+  let f : Multiplicative G →ₜ* Multiplicative G :=
+    { toMonoidHom := (AddEquiv.toMultiplicative A).toMonoidHom
+      continuous_toFun := continuous_of_discreteTopology }
+  PontryaginDual.map f χ
+
+/-! ## B. Symmetry action -/
+
+/-- A symmetry acts on characters by precomposition with its inverse lattice automorphism. -/
+noncomputable instance (C : Crystal G) : MulDistribMulAction (Symmetry C) (TranslationDual G) where
+  smul s χ := dualMap s.lattice.symm χ
+  one_smul χ := by
+    ext a
+    rfl
+  mul_smul s t χ := by
+    ext a
+    rfl
+  smul_one s := by
+    ext a
+    rfl
+  smul_mul s χ ψ := by
+    ext a
+    rfl
+
+/-- The action evaluates `χ` at the inverse image of a lattice step. -/
+lemma Symmetry.smul_dual_apply {C : Crystal G} (s : Symmetry C) (χ : TranslationDual G) (a : G) :
+    (s • χ) (Multiplicative.ofAdd a) =
+      χ (Multiplicative.ofAdd (s.lattice.symm a)) := rfl
+
+/-- Transforming both a character and a lattice step preserves the character's value. -/
+lemma Symmetry.smul_dual_lattice {C : Crystal G} (s : Symmetry C) (χ : TranslationDual G) (a : G) :
+    (s • χ) (Multiplicative.ofAdd (s.lattice a)) = χ (Multiplicative.ofAdd a) := by
+  rw [Symmetry.smul_dual_apply, s.lattice.symm_apply_apply]
+
+/-- Pure translations fix every translation character. -/
+lemma Symmetry.translation_smul_dual (C : Crystal G) (a : G) (χ : TranslationDual G) :
+    Symmetry.translation C a • χ = χ := by
+  apply PontryaginDual.ext
+  intro b
+  simpa using Symmetry.smul_dual_lattice (Symmetry.translation C a) χ b.toAdd
+
+/-! ## C. Action modulo translations -/
+
+/-- The symmetry action as a homomorphism to automorphisms of the character group. -/
+noncomputable def symmetryAction (C : Crystal G) :
+    Symmetry C →* MulAut (TranslationDual G) :=
+  MulDistribMulAction.toMulAut (Symmetry C) (TranslationDual G)
+
+/-- Translations lie in the kernel of the action on characters. -/
+lemma translations_le_ker_symmetryAction (C : Crystal G) :
+    Symmetry.translations C ≤ (symmetryAction C).ker := by
+  rintro s ⟨a, rfl⟩
+  rw [MonoidHom.mem_ker]
+  ext χ : 1
+  exact Symmetry.translation_smul_dual C a.toAdd χ
+
+/-- The symmetry action factored through the quotient by translations. -/
+noncomputable def pointAction (C : Crystal G) :
+    (Symmetry C ⧸ Symmetry.translations C) →* MulAut (TranslationDual G) :=
+  QuotientGroup.lift _ (symmetryAction C) (translations_le_ker_symmetryAction C)
+
+/-- The quotient by translations acts on the character group. -/
+noncomputable instance (C : Crystal G) :
+    MulDistribMulAction (Symmetry C ⧸ Symmetry.translations C) (TranslationDual G) where
+  smul p χ := pointAction C p χ
+  one_smul χ := rfl
+  mul_smul p q χ := by
+    change pointAction C (p * q) χ = pointAction C p (pointAction C q χ)
+    rw [map_mul]
+    rfl
+  smul_one p := (pointAction C p).map_one
+  smul_mul p χ ψ := (pointAction C p).map_mul χ ψ
+
+/-- A symmetry class acts on characters through any representative. -/
+lemma mk_smul (C : Crystal G) (s : Symmetry C) (χ : TranslationDual G) :
+    (QuotientGroup.mk s : Symmetry C ⧸ Symmetry.translations C) • χ = s • χ := by
+  change pointAction C (QuotientGroup.mk s) χ = s • χ
+  rfl
+
+end Physlib.CondensedMatter.Crystal