Skip to content

Commit e7ddc5c

Browse files
tsurumi-yizhoutsurumi-yizhou
committed
feat: 添加哈密顿量相关模块
实现哈密顿量计算的核心功能，包括： - 自旋操作与空间群元素作用 - 多项式与复数多项式表示 - 线性代数工具与不变量子计算 - 不变性分析与对称性检测
1 parent b1b9510 commit e7ddc5c

File tree

17 files changed

+1103
-304
lines changed

17 files changed

+1103
-304
lines changed

‎Demo/Altermagnet.lean‎

Lines changed: 32 additions & 81 deletions
Original file line numberDiff line numberDiff line change
@@ -4,108 +4,59 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yizhou Tong
55
-/
66
import SPG.Algebra.Basic
7-
import SPG.Algebra.Group
8-
import SPG.Geometry.SpatialOps
9-
import SPG.Geometry.SpinOps
10-
import SPG.Interface.Notation
117
import SPG.Physics.Hamiltonian
8+
import SPG.Data.MagneticGroups
129
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
1310

1411
namespace Demo.Altermagnet
1512

1613
open SPG
17-
open SPG.Geometry.SpatialOps
18-
open SPG.Geometry.SpinOps
19-
open SPG.Interface
20-
open SPG.Algebra
2114
open SPG.Physics.Hamiltonian
15+
open SPG.Data.MagneticGroups
2216

23-
-- 1. Generators for D4h altermagnet
24-
def mat_4_z : Matrix (Fin 3) (Fin 3) ℚ := ![![0, -1, 0], ![1, 0, 0], ![0, 0, 1]]
25-
def mat_inv : Matrix (Fin 3) (Fin 3) ℚ := ![![ -1, 0, 0], ![0, -1, 0], ![0, 0, -1]]
26-
-- mat_2_xy defined explicitly for clarity (rotation by 180 degrees about x+y axis)
27-
def mat_2_xy : Matrix (Fin 3) (Fin 3) ℚ := ![![0, 1, 0], ![1, 0, 0], ![0, 0, -1]]
28-
29-
-- Generators
30-
-- C4z * T : The key altermagnetic symmetry
31-
-- C2xy : Rotation about x+y axis
32-
-- I : Inversion
33-
def gen_C4z_TR : SPGElement := Op[mat_4_z, ^-1]
34-
def gen_C2xy : SPGElement := Op[mat_2_xy, ^1]
35-
def gen_Inv : SPGElement := Op[mat_inv, ^1]
36-
37-
def Altermagnet_Group : List SPGElement := generate_group [gen_C4z_TR, gen_C2xy, gen_Inv]
38-
39-
-- 2. ICE Symbol Output (Simplistic)
40-
-- We just print generators for now, as full ICE symbol logic is complex.
41-
def ice_symbol : String :=
42-
"4'22 (D4h magnetic)" -- Placeholder, deriving from generators
17+
def ice_symbol : String := "4'22 (D4h magnetic)"
4318

4419
end Demo.Altermagnet
4520

4621
def main : IO Unit := do
47-
IO.println s!"Generated Group Size: {Demo.Altermagnet.Altermagnet_Group.length}"
22+
IO.println s!"Generated Group Size: {SPG.Data.MagneticGroups.Altermagnet_Group_D4h.length}"
4823
IO.println s!"ICE Symbol (Approx): {Demo.Altermagnet.ice_symbol}"
49-
IO.println "Allowed Hamiltonian Terms H(k) (up to quadratic):"
50-
51-
let invariants := SPG.Physics.Hamiltonian.find_invariants Demo.Altermagnet.Altermagnet_Group
52-
for (p, s) in invariants do
53-
let p_str := match p with
54-
| .const => "1"
55-
| .x => "kx" | .y => "ky" | .z => "kz"
56-
| .xx => "kx^2" | .yy => "ky^2" | .zz => "kz^2"
57-
| .xy => "kx ky" | .yz => "ky kz" | .zx => "kz kx"
58-
let s_str := match s with
59-
| .I => "I" | .x => "σx" | .y => "σy" | .z => "σz"
60-
IO.println s!" {p_str} * {s_str}"
61-
62-
-- Manually check d-wave altermagnet term: (kx^2 - ky^2) * sigma_z?
63-
-- Or kx ky * sigma_z ?
64-
-- Let's define a custom checker for kx^2 - ky^2
65-
let check_custom (f : SPG.Vec3 → ℚ) (s : SPG.Physics.Hamiltonian.SpinComp) : Bool :=
66-
let test_ks : List SPG.Vec3 := [![1, 0, 0], ![0, 1, 0], ![0, 0, 1], ![1, 1, 0], ![1, 0, 1], ![0, 1, 1], ![1, 2, 3]]
67-
test_ks.all fun k =>
68-
-- Re-implement loop
69-
Demo.Altermagnet.Altermagnet_Group.all fun g =>
70-
let val_gk := f (SPG.Physics.Hamiltonian.act_on_k g k)
71-
let val_k := f k
72-
-- Re-use projection logic from check_invariant
73-
if s == .I then
74-
val_gk == val_k
75-
else
76-
let s_prime := SPG.Physics.Hamiltonian.act_on_spin g s
77-
let coeff := SPG.Physics.Hamiltonian.project_spin s_prime s
78-
79-
-- Check eigenstate property (no mixing)
80-
let is_eigen :=
81-
(s == .x && s_prime 1 == 0 && s_prime 2 == 0) ||
82-
(s == .y && s_prime 0 == 0 && s_prime 2 == 0) ||
83-
(s == .z && s_prime 0 == 0 && s_prime 1 == 0)
84-
85-
if is_eigen then
86-
val_gk * coeff == val_k
87-
else
88-
false
89-
90-
let kx2_minus_ky2 (k : SPG.Vec3) : ℚ := k 0 * k 0 - k 1 * k 1
91-
let kx2_plus_ky2 (k : SPG.Vec3) : ℚ := k 0 * k 0 + k 1 * k 1
92-
let kx_ky (k : SPG.Vec3) : ℚ := k 0 * k 1
93-
94-
if check_custom kx2_minus_ky2 .z then
24+
IO.println "Invariant k·p Hamiltonians (basis by degree ≤ 2):"
25+
26+
let group := SPG.Data.MagneticGroups.Altermagnet_Group_D4h
27+
let blocks := SPG.Physics.Hamiltonian.invariants_vector_by_degree_solve group 2
28+
for (d, hs) in blocks do
29+
IO.println s!" degree {d}:"
30+
for h in hs do
31+
IO.println s!" {SPG.Physics.Hamiltonian.ham_to_string h}"
32+
33+
IO.println "Invariant complex k·p Hamiltonians (basis by degree ≤ 2):"
34+
let cblocks := SPG.Physics.Hamiltonian.invariants_vector_by_degree_solveC group 2
35+
for (d, hs) in cblocks do
36+
IO.println s!" degree {d}:"
37+
for h in hs do
38+
IO.println s!" {SPG.Physics.Hamiltonian.cham_to_string h}"
39+
40+
let p_dwave : SPG.Physics.Hamiltonian.Poly :=
41+
(SPG.Physics.Hamiltonian.kx * SPG.Physics.Hamiltonian.kx) -
42+
(SPG.Physics.Hamiltonian.ky * SPG.Physics.Hamiltonian.ky)
43+
let p_xy : SPG.Physics.Hamiltonian.Poly :=
44+
SPG.Physics.Hamiltonian.kx * SPG.Physics.Hamiltonian.ky
45+
let p_kin : SPG.Physics.Hamiltonian.Poly :=
46+
(SPG.Physics.Hamiltonian.kx * SPG.Physics.Hamiltonian.kx) +
47+
(SPG.Physics.Hamiltonian.ky * SPG.Physics.Hamiltonian.ky)
48+
49+
if SPG.Physics.Hamiltonian.isInvariantHam group (SPG.Physics.Hamiltonian.singleTerm p_dwave .z) then
9550
IO.println " (kx^2 - ky^2) * σz [d-wave altermagnetism (x^2-y^2 type)]"
9651
else
9752
IO.println " (kx^2 - ky^2) * σz [FORBIDDEN]"
98-
-- Analyze why it is forbidden (or allowed)
99-
let _ ← SPG.Physics.Hamiltonian.analyze_term_symmetry Demo.Altermagnet.Altermagnet_Group kx2_minus_ky2 .z "(kx^2 - ky^2)" "σz"
10053

101-
if check_custom kx_ky .z then
54+
if SPG.Physics.Hamiltonian.isInvariantHam group (SPG.Physics.Hamiltonian.singleTerm p_xy .z) then
10255
IO.println " kx ky * σz [d-wave altermagnetism (xy type)]"
10356
else
10457
IO.println " kx ky * σz [FORBIDDEN]"
105-
let _ ← SPG.Physics.Hamiltonian.analyze_term_symmetry Demo.Altermagnet.Altermagnet_Group kx_ky .z "kx ky" "σz"
10658

107-
if check_custom kx2_plus_ky2 .I then
59+
if SPG.Physics.Hamiltonian.isInvariantHam group (SPG.Physics.Hamiltonian.singleTerm p_kin .I) then
10860
IO.println " (kx^2 + ky^2) * I [Standard kinetic term]"
10961
else
11062
IO.println " (kx^2 + ky^2) * I [FORBIDDEN]"
111-
let _ ← SPG.Physics.Hamiltonian.analyze_term_symmetry Demo.Altermagnet.Altermagnet_Group kx2_plus_ky2 .I "(kx^2 + ky^2)" "I"

‎Demo/MagneticPhases.lean‎

Lines changed: 37 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ import SPG.Geometry.SpinOps
1010
import SPG.Interface.Notation
1111
import SPG.Physics.Hamiltonian
1212
import SPG.Data.MagneticGroups
13+
import SPG.Data.Tetragonal
1314
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
1415

1516
namespace Demo.MagneticPhases
@@ -21,6 +22,7 @@ open SPG.Interface
2122
open SPG.Algebra
2223
open SPG.Physics.Hamiltonian
2324
open SPG.Data.MagneticGroups
25+
open SPG.Data.Tetragonal
2426

2527
def check_linear_k_sigma (group : List SPGElement) : IO Unit := do
2628
IO.println " Checking linear spin-splitting terms (k * sigma):"
@@ -35,7 +37,7 @@ def check_linear_k_sigma (group : List SPGElement) : IO Unit := do
3537
if check_invariant group p s then
3638
IO.println s!" [ALLOWED] {name}"
3739
found := true
38-
40+
3941
if !found then
4042
IO.println " [NONE] No linear spin-splitting terms found."
4143

@@ -44,7 +46,28 @@ def analyze_phase (name : String) (group : List SPGElement) : IO Unit := do
4446
IO.println s!"Phase Analysis: {name}"
4547
IO.println s!"Group Order: {group.length}"
4648
IO.println "----------------------------------------"
47-
49+
50+
IO.println " Invariant k·p Hamiltonians (basis by degree ≤ 2):"
51+
let blocks := SPG.Physics.Hamiltonian.invariants_vector_by_degree_solve group 2
52+
for (d, hs) in blocks do
53+
IO.println s!" degree {d}:"
54+
for h in hs do
55+
IO.println s!" {SPG.Physics.Hamiltonian.ham_to_string h}"
56+
57+
IO.println " Invariant complex k·p Hamiltonians (basis by degree ≤ 2):"
58+
let cblocks := SPG.Physics.Hamiltonian.invariants_vector_by_degree_solveC group 2
59+
for (d, hs) in cblocks do
60+
IO.println s!" degree {d}:"
61+
for h in hs do
62+
IO.println s!" {SPG.Physics.Hamiltonian.cham_to_string h}"
63+
64+
IO.println " Invariant Hermitian complex k·p Hamiltonians (basis by degree ≤ 2):"
65+
let hcblocks := SPG.Physics.Hamiltonian.hermitian_invariants_vector_by_degree_solveC group 2
66+
for (d, hs) in hcblocks do
67+
IO.println s!" degree {d}:"
68+
for h in hs do
69+
IO.println s!" {SPG.Physics.Hamiltonian.cham_to_string h}"
70+
4871
-- Check Chemical Potential
4972
if check_invariant group .const .I then
5073
IO.println " [ALLOWED] Chemical Potential (1 * I)"
@@ -54,54 +77,28 @@ def analyze_phase (name : String) (group : List SPGElement) : IO Unit := do
5477
-- Check Standard Kinetic Energy (k^2)
5578
if check_invariant group .xx .I && check_invariant group .yy .I && check_invariant group .zz .I then
5679
IO.println " [ALLOWED] Standard Kinetic Terms (kx^2, ky^2, kz^2 * I)"
57-
80+
5881
-- Check Linear Spin Splitting (Rashba/Dresselhaus type)
5982
check_linear_k_sigma group
6083

6184
-- Check Altermagnetic Terms (d-wave spin splitting)
6285
IO.println " Checking d-wave spin-splitting terms:"
63-
let kx2_m_ky2 (k : SPG.Vec3) : ℚ := k 0 * k 0 - k 1 * k 1
64-
let kx_ky (k : SPG.Vec3) : ℚ := k 0 * k 1
65-
66-
if check_invariant group .xx .z && check_invariant group .yy .z then
67-
-- This is loose checking, better to check the specific combination
68-
-- But here we use our custom checkers from the Hamiltonian module if we had them exposed as simple functions
69-
-- Since `check_invariant` takes PolyTerm, we can't directly check (kx^2 - ky^2).
70-
-- But we can check if kx^2 * sz and ky^2 * sz are allowed.
71-
-- Note: In d-wave AM, kx^2 * sz is NOT allowed alone usually, only the difference.
72-
-- Let's rely on the manual check helper logic from previous demo, adapted here.
73-
let _ := 0
74-
75-
-- We need to check (kx^2 - ky^2) * sz manually since it's a linear combination
76-
let check_custom (f : SPG.Vec3 → ℚ) (s : SpinComp) : Bool :=
77-
let test_ks : List SPG.Vec3 := [![1, 0, 0], ![0, 1, 0], ![0, 0, 1], ![1, 1, 0], ![1, 0, 1], ![0, 1, 1], ![1, 2, 3]]
78-
test_ks.all fun k =>
79-
group.all fun g =>
80-
let val_gk := f (act_on_k g k)
81-
let val_k := f k
82-
if s == .I then val_gk == val_k
83-
else
84-
let s_prime := act_on_spin g s
85-
let coeff := project_spin s_prime s
86-
let is_eigen :=
87-
(s == .x && s_prime 1 == 0 && s_prime 2 == 0) ||
88-
(s == .y && s_prime 0 == 0 && s_prime 2 == 0) ||
89-
(s == .z && s_prime 0 == 0 && s_prime 1 == 0)
90-
if is_eigen then val_gk * coeff == val_k else false
91-
92-
if check_custom kx2_m_ky2 .z then
86+
let p_dwave : Poly := (kx * kx) - (ky * ky)
87+
let p_xy : Poly := kx * ky
88+
89+
if isInvariantHam group (singleTerm p_dwave .z) then
9390
IO.println " [ALLOWED] (kx^2 - ky^2) * σz (d-wave)"
9491
else
9592
IO.println " [FORBIDDEN] (kx^2 - ky^2) * σz"
9693

97-
if check_custom kx_ky .z then
94+
if isInvariantHam group (singleTerm p_xy .z) then
9895
IO.println " [ALLOWED] kx ky * σz (d-wave)"
9996
else
10097
IO.println " [FORBIDDEN] kx ky * σz"
101-
98+
10299
-- Check Net Magnetization
103100
IO.println " Checking Net Magnetization (M):"
104-
if check_custom (fun _ => 1) .z then
101+
if isInvariantHam group (singleTerm (1 : Poly) .z) then
105102
IO.println " [ALLOWED] Ferromagnetism Mz (1 * σz)"
106103
else
107104
IO.println " [FORBIDDEN] Ferromagnetism Mz (1 * σz)"
@@ -112,3 +109,7 @@ def main : IO Unit := do
112109
Demo.MagneticPhases.analyze_phase "Ferromagnet (D4h, M || z)" SPG.Data.MagneticGroups.Ferromagnet_Group_D4h_z
113110
Demo.MagneticPhases.analyze_phase "Antiferromagnet (D4h, PT-symmetric)" SPG.Data.MagneticGroups.Antiferromagnet_Group_PT
114111
Demo.MagneticPhases.analyze_phase "Altermagnet (D4h)" SPG.Data.MagneticGroups.Altermagnet_Group_D4h
112+
let laue := SPG.Data.Tetragonal.Laue_D2d_gens
113+
let mag : List SPG.SPGElement := [SPG.Data.mk_ice_element SPG.Geometry.SpatialOps.mat_4bar_z true]
114+
let combined := SPG.Physics.Hamiltonian.group_from_laue_magnetic laue mag
115+
Demo.MagneticPhases.analyze_phase "Tetragonal Laue (D2d+I) + (4bar_z*T)" combined

‎SPG/Algebra/Actions.lean‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,11 +10,14 @@ import Mathlib.Data.Rat.Defs
1010
import Mathlib.Algebra.Ring.Basic
1111
import Mathlib.Algebra.Field.Defs
1212
import Mathlib.Algebra.Ring.Rat
13+
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
1314

1415
namespace SPG
1516

1617
def magnetic_action (g : SPGElement) (v : Vec3) : Vec3 :=
17-
Matrix.mulVec g.spin (Matrix.mulVec g.spatial v)
18+
let detR := Matrix.det g.spatial
19+
let rotated := Matrix.mulVec g.spatial v
20+
Matrix.mulVec g.spin (detR • rotated)
1821

1922
def electric_action (g : SPGElement) (v : Vec3) : Vec3 :=
2023
Matrix.mulVec g.spatial v

‎SPG/Algebra/Group.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,4 +26,7 @@ partial def generate_group (gens : List SPGElement) : List SPGElement :=
2626
loop combined
2727
loop gens
2828

29+
def combine_generators (gens₁ gens₂ : List SPGElement) : List SPGElement :=
30+
generate_group (gens₁ ++ gens₂)
31+
2932
end SPG.Algebra

‎SPG/Data/MagneticGroups.lean‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -18,10 +18,6 @@ open SPG.Interface
1818
open SPG.Algebra
1919

2020
-- Define common matrices
21-
def mat_id : Matrix (Fin 3) (Fin 3) ℚ := 1
22-
def mat_inv : Matrix (Fin 3) (Fin 3) ℚ := -1
23-
def mat_4_z : Matrix (Fin 3) (Fin 3) ℚ := ![![0, -1, 0], ![1, 0, 0], ![0, 0, 1]]
24-
def mat_2_x : Matrix (Fin 3) (Fin 3) ℚ := ![![1, 0, 0], ![0, -1, 0], ![0, 0, -1]]
2521
def mat_2_xy : Matrix (Fin 3) (Fin 3) ℚ := ![![0, 1, 0], ![1, 0, 0], ![0, 0, -1]]
2622

2723
-- 1. Ferromagnet (FM)

‎SPG/Data/Tetragonal.lean‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yizhou Tong
55
-/
66
import SPG.Data.ICE_Notation
7+
import SPG.Algebra.Group
78
import SPG.Geometry.SpatialOps
89

910
namespace SPG.Data.Tetragonal
1011

1112
open SPG.Geometry.SpatialOps
13+
open SPG.Algebra
1214

1315
-- Generators for CuFeS2 (Chalcopyrite structure, I-42d, #122)
1416
-- Using 4bar_z, 2_x, and m_xy (standard generators for D2d point group)
@@ -18,4 +20,10 @@ def gen1 : SPGElement := mk_ice_element mat_4bar_z false
1820
def gen2 : SPGElement := mk_ice_element mat_2_x false
1921
def gen3 : SPGElement := mk_ice_element mat_m_xy false
2022

23+
def D2d_gens : List SPGElement := [gen1, gen2, gen3]
24+
def D2d : List SPGElement := generate_group D2d_gens
25+
26+
def Laue_D2d_gens : List SPGElement := D2d_gens ++ [mk_ice_element mat_inv false]
27+
def Laue_D2d : List SPGElement := generate_group Laue_D2d_gens
28+
2129
end SPG.Data.Tetragonal

‎SPG/Geometry/SpatialOps.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,11 @@ import Mathlib.Data.Matrix.Basic
77

88
namespace SPG.Geometry.SpatialOps
99

10+
def mat_inv : Matrix (Fin 3) (Fin 3) ℚ := -1
11+
12+
def mat_4_z : Matrix (Fin 3) (Fin 3) ℚ :=
13+
![![0, -1, 0], ![1, 0, 0], ![0, 0, 1]]
14+
1015
def mat_4bar_z : Matrix (Fin 3) (Fin 3) ℚ :=
1116
![![0, 1, 0], ![-1, 0, 0], ![0, 0, -1]]
1217

0 commit comments

Comments
 (0)
⚡