Registry · Definition IV.D56 tau-effective formalized

IV.D56 — Character Variety of T²

Char(T²) := Hom(Z×Z, U(1)) ≅ U(1)×U(1) = T². The address book of quantum states is itself a torus — Pontryagin duality.

Book IV Part 3 Ch. 17

Dependency Graph

Depends on (2)

Depended on by (1)

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.QuantumCharacters

Symbol: Tau.BookIV.QuantumMechanics.CharacterVarietyOfT