Source: ProCGroups.Topologies.FullSubgroupTopology.QuotientVariety
1import ProCGroups.Topologies.FullSubgroupTopology.QuotientFormation
3/-!
4# Quotient varieties
6A quotient variety is a quotient formation stable under pullback along group homomorphisms. This
7file shows that the corresponding notion of open subgroup is likewise preserved by comap.
8-/
10open Set
11open scoped Topology
13namespace ProCGroups.Topologies
15universe u
17/-- A quotient variety is a quotient formation with the closure properties needed for varieties. -/
18structure QuotientVariety extends QuotientFormation where
19 /-- Admissible quotient kernels are closed under pullback along group homomorphisms. -/
20 comap_closed :
21 ∀ {G H : Type u} [Group G] [Group H] (f : G →* H) {N : Subgroup H},
22 toQuotientFormation.contains N → toQuotientFormation.contains (N.comap f)
24namespace QuotientVariety
26variable (C : QuotientVariety)
27variable {G H : Type u} [Group G] [Group H]
29/-- Abstract form of the fact that full pro-\(C\) openness pulls back along a homomorphism. -/
30theorem isOpenSubgroup_comap (f : G →* H) {K : Subgroup H}
31 (hK : C.toQuotientFormation.IsOpenSubgroup K) :
32 C.toQuotientFormation.IsOpenSubgroup (K.comap f) := by
33 rcases hK with ⟨N, hN, hNK⟩
34 refine ⟨N.comap f, C.comap_closed f hN, ?_⟩
35 intro x hx
36 exact hNK hx
38end QuotientVariety
40end ProCGroups.Topologies