ProCGroups/Topologies/FullSubgroupTopology/QuotientVariety.lean
1import ProCGroups.Topologies.FullSubgroupTopology.QuotientFormation
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/Topologies/FullSubgroupTopology/QuotientVariety.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Topological group constructions
14Topological subgroup, quotient, continuous homomorphism, continuous equivalence, conjugation, and full-subgroup-topology lemmas.
15-/
17open Set
18open scoped Topology
20namespace ProCGroups.Topologies
22universe u
24/-- A quotient variety is a quotient formation with the closure properties needed for varieties. -/
25structure QuotientVariety extends QuotientFormation where
26 comap_closed :
27 ∀ {G H : Type u} [Group G] [Group H] (f : G →* H) {N : Subgroup H},
28 toQuotientFormation.contains N → toQuotientFormation.contains (N.comap f)
30namespace QuotientVariety
32variable (C : QuotientVariety)
33variable {G H : Type u} [Group G] [Group H]
35/-- Abstract form of the fact that full pro-`C` openness pulls back along a homomorphism. -/
36theorem isOpenSubgroup_comap (f : G →* H) {K : Subgroup H}
37 (hK : C.toQuotientFormation.IsOpenSubgroup K) :
38 C.toQuotientFormation.IsOpenSubgroup (K.comap f) := by
39 rcases hK with ⟨N, hN, hNK⟩
40 refine ⟨N.comap f, C.comap_closed f hN, ?_⟩
41 intro x hx
42 exact hNK hx
46end ProCGroups.Topologies