ProCGroups.InverseSystems.CategoryBridge
This module studies category bridge for pro cgroups. The categorical TopCat diagram associated to a concrete inverse system. The TopCat functor associated to an inverse system sends an index morphism to the corresponding transition map.
import
- Mathlib.CategoryTheory.Category.Preorder
- Mathlib.Topology.Category.TopCat.Basic
- ProCGroups.InverseSystems.CompatibilityAndSurjectivity
Imported by
def toFunctor : Iᵒᵖ ⥤ TopCat.{v} where
obj i := TopCat.of (S.X i.unop)
map {i j} hij := TopCat.ofHom ⟨S.map hij.unop.le, S.continuous_map hij.unop.le⟩
map_id i := by
ext x
exact S.map_id_apply i.unop x
map_comp {i j k} hij hjk := by
ext x
exact (S.map_comp_apply hjk.unop.le hij.unop.le x).symmThe categorical TopCat diagram associated to a concrete inverse system.
@[simp] theorem toFunctor_map_apply {i j : Iᵒᵖ} (hij : i ⟶ j)
(x : S.X i.unop) :
S.toFunctor.map hij x = S.map hij.unop.le xThe TopCat functor associated to an inverse system sends an index morphism to the corresponding transition map.
Show proof
rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□def toNatTrans (Θ : S.Morphism T) : S.toFunctor ⟶ T.toFunctor where
app i := TopCat.ofHom ⟨Θ.map i.unop, Θ.continuous_map i.unop⟩
naturality {i j} hij := by
ext x
exact (Θ.comm_apply hij.unop.le x).symmA concrete morphism of inverse systems gives a natural transformation of the associated TopCat diagrams.
@[simp] theorem toNatTrans_app_apply (Θ : S.Morphism T) (i : Iᵒᵖ)
(x : S.X i.unop) :
Θ.toNatTrans.app i x = Θ.map i.unop xThe natural transformation associated to a morphism evaluates at a stage as that morphism's stage map.
Show proof
rflProof. Unfold the inverse-system data and argue componentwise at each index. Morphisms, transition maps, and comparison maps are defined by their stage maps, and the compatibility squares say exactly that these coordinates commute with refinement. For inverse-limit statements, equality is proved by projection extensionality; continuity is checked from the initial topology of the limit; and compactness, Hausdorffness, discreteness, density, and finite-stage factorization are inherited from the corresponding stagewise hypotheses.
□