ProCGroups/InverseSystems/CategoryBridge.lean
1import Mathlib.CategoryTheory.Category.Preorder
2import Mathlib.Topology.Category.TopCat.Basic
3import ProCGroups.InverseSystems.CompatibilityAndSurjectivity
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/InverseSystems/CategoryBridge.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Category bridge for concrete inverse systems
16The inverse-system API is a concrete, calculation-oriented wrapper for
17stagewise topological inverse limits. This file exposes the associated
18`TopCat` diagram without replacing the concrete API by a categorical one.
19-/
21open CategoryTheory
23namespace ProCGroups
24namespace InverseSystems
26universe u v
28section
30variable {I : Type u} [Preorder I]
32namespace InverseSystem
34variable (S : InverseSystem.{u, v} (I := I))
36/-- The categorical `TopCat` diagram associated to a concrete inverse system. -/
38 obj i := TopCat.of (S.X i.unop)
39 map {i j} hij := TopCat.ofHom ⟨S.map hij.unop.le, S.continuous_map hij.unop.le⟩
40 map_id i := by
41 ext x
42 exact S.map_id_apply i.unop x
43 map_comp {i j k} hij hjk := by
44 ext x
45 exact (S.map_comp_apply hjk.unop.le hij.unop.le x).symm
47@[simp] theorem toFunctor_map_apply {i j : Iᵒᵖ} (hij : i ⟶ j)
48 (x : S.X i.unop) :
49 S.toFunctor.map hij x = S.map hij.unop.le x :=
50 rfl
54variable {S}
55variable {T : InverseSystem.{u, v} (I := I)}
57/-- A concrete morphism of inverse systems gives a natural transformation of
58the associated `TopCat` diagrams. -/
59def toNatTrans (Θ : S.Morphism T) : S.toFunctor ⟶ T.toFunctor where
60 app i := TopCat.ofHom ⟨Θ.map i.unop, Θ.continuous_map i.unop⟩
61 naturality {i j} hij := by
62 ext x
63 exact (Θ.comm_apply hij.unop.le x).symm
65@[simp] theorem toNatTrans_app_apply (Θ : S.Morphism T) (i : Iᵒᵖ)
66 (x : S.X i.unop) :
67 Θ.toNatTrans.app i x = Θ.map i.unop x :=
68 rfl
72end InverseSystem
74end
76end InverseSystems
77end ProCGroups