ProCGroups/ProC/GroupPredicate.lean

1import Mathlib.Topology.Algebra.ContinuousMonoidHom

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/ProCGroups/ProC/GroupPredicate.lean

7translation_root: data/translation

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

9placement: after imports, never before imports

11/-!

12# Abstract pro-C predicates

14`ProCGroupPredicate` is the low-level wrapper for an abstract topological pro-`C` condition.

15For concrete finite quotient classes, the public entry point is

16`ProCGroups.ProC.IsProCGroup C G`; use this wrapper only when a theorem must quantify over an

17abstract predicate before its controlling finite quotient class has been fixed.

20namespace ProCGroups.ProC

22universe u

24/-- A predicate packaging the statement that a topological group belongs to a chosen pro-`C`

25class. -/

27 holds : {G : Type u} → [Group G] → [TopologicalSpace G] → [IsTopologicalGroup G] → Prop

31/-- A pro-`C` group predicate coerces to its underlying predicate on topological groups. -/

33 (fun _ => {G : Type u} → [Group G] → [TopologicalSpace G] → [IsTopologicalGroup G] → Prop) where

34 coe P := @P.holds

38end ProCGroups.ProC