ProCGroups/ProC/Quotients/LeftQuotientMaps.lean
1import ProCGroups.ProC.Subgroups.Products
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/ProC/Quotients/LeftQuotientMaps.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Pro-C groups and open normal quotients
14Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.
15-/
17open Set
18open scoped Topology Pointwise
20namespace ProCGroups.ProC
22universe u v
24open InverseSystems
26/-- The natural projection `G/K → G/H` for closed subgroups `K ≤ H`, viewed as a quotient-space
27map on left cosets. -/
29 {G : Type u} [Group G] (K H : Subgroup G) (hKH : K ≤ H) :
30 G ⧸ K → G ⧸ H :=
31 Quotient.map' id <| by
32 intro a b hab
33 rw [QuotientGroup.leftRel_apply] at hab ⊢
34 exact hKH hab
36variable {G : Type u} [Group G]
38/-- The projection on left quotients sends the class of `g` modulo `K` to the class of `g`
39modulo `H`. -/
40@[simp] theorem leftQuotientProjection_mk
41 (K H : Subgroup G) (hKH : K ≤ H) (g : G) :
42 leftQuotientProjection K H hKH (QuotientGroup.mk (s := K) g) =
43 QuotientGroup.mk (s := H) g := by
44 rfl
46/-- The natural map between nested left quotients is continuous. -/
48 [TopologicalSpace G]
49 (K H : Subgroup G) (hKH : K ≤ H) :
50 Continuous (leftQuotientProjection K H hKH : G ⧸ K → G ⧸ H) := by
51 refine (QuotientGroup.isQuotientMap_mk K).continuous_iff.2 ?_
52 simpa [Function.comp, leftQuotientProjection_mk] using
53 (QuotientGroup.continuous_mk : Continuous (QuotientGroup.mk (s := H) : G → G ⧸ H))
55/-- The left-quotient projection to itself is the identity. -/
56@[simp] theorem leftQuotientProjection_id
57 (K : Subgroup G) :
58 leftQuotientProjection K K le_rfl = id := by
59 funext x
60 refine Quotient.inductionOn x ?_
61 intro g
62 rfl
64/-- Left-quotient projections compose along chains of subgroup inclusions. -/
65@[simp] theorem leftQuotientProjection_comp
66 (K H L : Subgroup G) (hKH : K ≤ H) (hHL : H ≤ L) :
67 leftQuotientProjection H L hHL ∘ leftQuotientProjection K H hKH =
68 leftQuotientProjection K L (hKH.trans hHL) := by
69 funext x
70 refine Quotient.inductionOn x ?_
71 intro g
72 rfl
74/-- Pointwise form of the composition law for left-quotient projections. -/
75@[simp] theorem leftQuotientProjection_comp_apply
76 (K H L : Subgroup G) (hKH : K ≤ H) (hHL : H ≤ L) (x : G ⧸ K) :
77 leftQuotientProjection H L hHL (leftQuotientProjection K H hKH x) =
78 leftQuotientProjection K L (hKH.trans hHL) x := by
79 simpa using congrArg (fun f => f x) (leftQuotientProjection_comp (K := K) (H := H) (L := L)
80 hKH hHL)
82/-- Symmetric pointwise form of the composition law for left-quotient projections. -/
84 (K H L : Subgroup G) (hKH : K ≤ H) (hHL : H ≤ L) (x : G ⧸ K) :
85 leftQuotientProjection K L (hKH.trans hHL) x =
86 leftQuotientProjection H L hHL (leftQuotientProjection K H hKH x) := by
87 exact (leftQuotientProjection_comp_apply (K := K) (H := H) (L := L) hKH hHL x).symm
89/-- The natural map between nested left quotients is surjective. -/
91 (K H : Subgroup G) (hKH : K ≤ H) :
92 Function.Surjective (leftQuotientProjection K H hKH : G ⧸ K → G ⧸ H) := by
93 intro x
94 refine Quotient.inductionOn x ?_
95 intro g
96 exact ⟨QuotientGroup.mk (s := K) g, rfl⟩
98/-- Left-quotient projections are equivariant for the ambient left action of `G`. -/
99@[simp] theorem leftQuotientProjection_smul
100 (K H : Subgroup G) (hKH : K ≤ H) (g : G) (x : G ⧸ K) :
101 leftQuotientProjection K H hKH (g • x) =
102 g • leftQuotientProjection K H hKH x := by
103 refine Quotient.inductionOn x ?_
104 intro y
105 rfl
107end ProCGroups.ProC