ProCGroups/Categorical.lean

1import ProCGroups.Categorical.AlgebraicPullbacks

2import ProCGroups.Categorical.ProfinitePullbacks

3import ProCGroups.Categorical.PullbackComparison

4import ProCGroups.Categorical.PushoutSquares

5import ProCGroups.Categorical.QuotientPullbackEquivalences

7/-

8PUBLIC_PAGE_SNAPSHOT

9generated_at: 2026-05-27T09:47:29+09:00

10lean_source: lean4/ProCGroups/Categorical.lean

11translation_root: data/translation

12purpose: identifies the local data snapshot used to build pages/

13placement: after imports, never before imports

15/-!

16# Categorical pullback and pushout API

18This module re-exports the public categorical constructions for algebraic

19fiber products, topological/profinite pullbacks, pullback comparison maps, and

20pushout squares used by the pro-C library.