Registry · Definition IV.D55 tau-effective formalized

IV.D55 — Character on a Space

A character on a path-connected space X is a group homomorphism χ: π₁(X) → U(1). The set Char(X) := Hom(π₁(X), U(1)).

Book IV Part 3 Ch. 17

Dependency Graph

Depended on by (3)

IV.D56 IV.P11 IV.T33

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.QuantumCharacters

Symbol: Tau.BookIV.QuantumMechanics.CharacterOnASpace