Registry · Definition I.D56 tau-effective formalized

I.D56 — Tau-Site

The tau-site: Cat_tau equipped with primorial coverage. At each depth k, the covering family for object X consists of the CRT residues mod primes p_1, ..., p_k. Encodes arithmetic structure categorically.

Book I Part 14 Ch. 55

Dependency Graph

Depends on (2)

Depended on by (1)

Lean Formalization

Module: TauLib.BookI.Topos.LimitsSites

Symbol: Tau.Topos.TauSite