Registry · Definition III.D11 tau-effective formalized

III.D11 — Boundary Character Space

Characters on L = S¹ ∨ S¹: Char(L) = Hom(π₁(L), S¹) ≅ S¹ × S¹. The character lattice ℤ² from H₁(L; ℤ) ≅ ℤ ⊕ ℤ. Every character indexed by (m,n) ∈ ℤ². The m-axis = multiplicative/Galois, n-axis = additive/automorphic.

Book III Part 2 Ch. 9

Dependency Graph

Depends on (1)

Depended on by (6)

Lean Formalization

Module: TauLib.BookIII.Sectors.BoundaryCharacters

Symbol: BoundaryCharacter