Registry · Definition II.D61 established formalized

II.D61 — Moduli Space

The set of isomorphism classes of fibered products satisfying axioms K0-K5. By categoricity (II.T42), the moduli space is a singleton.

Book II Part 9 Ch. 52

Dependency Graph

Depends on (1)

II.T42

Depended on by (1)

II.C02

Lean Formalization

Module: TauLib.BookII.CentralTheorem.Categoricity

Symbol: Tau.BookII.CentralTheorem.moduli_singleton_check