Source: ProCGroups.ProC.Quotients.LeftQuotientMaps
1import ProCGroups.ProC.Subgroups.Products
3/-!
4# Maps between left quotients
6This file defines the canonical projection \(G/L \to G/H\) for nested subgroups and proves its
7formula, continuity, surjectivity, functoriality, and compatibility with the quotient action.
8-/
10open Set
11open scoped Topology Pointwise
13namespace ProCGroups.ProC
15universe u v
17open InverseSystems
19/--
20The natural projection \(G/K \to G/H\) for closed subgroups K \(\leq\) H is viewed as a
21quotient-space map on left cosets.
22-/
23def leftQuotientProjection
24 {G : Type u} [Group G] (K H : Subgroup G) (hKH : K ≤ H) :
25 G ⧸ K → G ⧸ H :=
26 Quotient.map' id <| by
27 intro a b hab
28 rw [QuotientGroup.leftRel_apply] at hab ⊢
29 exact hKH hab
31variable {G : Type u} [Group G]
33/--
34The projection on left quotients sends the class of \(g\) modulo \(K\) to the class of \(g\)
35modulo \(H\).
36-/
37@[simp] theorem leftQuotientProjection_mk
38 (K H : Subgroup G) (hKH : K ≤ H) (g : G) :
39 leftQuotientProjection K H hKH (QuotientGroup.mk (s := K) g) =
40 QuotientGroup.mk (s := H) g := by
41 rfl
43/-- The natural map between nested left quotients is continuous. -/
44theorem continuous_leftQuotientProjection
45 [TopologicalSpace G]
46 (K H : Subgroup G) (hKH : K ≤ H) :
47 Continuous (leftQuotientProjection K H hKH : G ⧸ K → G ⧸ H) := by
48 refine (QuotientGroup.isQuotientMap_mk K).continuous_iff.2 ?_
49 change Continuous (QuotientGroup.mk (s := H) : G → G ⧸ H)
50 exact QuotientGroup.continuous_mk
52/-- The left-quotient projection to itself is the identity. -/
53@[simp] theorem leftQuotientProjection_id
54 (K : Subgroup G) :
55 leftQuotientProjection K K le_rfl = id := by
56 funext x
57 refine Quotient.inductionOn x ?_
58 intro g
59 rfl
61/-- Left-quotient projections compose along chains of subgroup inclusions. -/
62@[simp] theorem leftQuotientProjection_comp
63 (K H L : Subgroup G) (hKH : K ≤ H) (hHL : H ≤ L) :
64 leftQuotientProjection H L hHL ∘ leftQuotientProjection K H hKH =
65 leftQuotientProjection K L (hKH.trans hHL) := by
66 funext x
67 refine Quotient.inductionOn x ?_
68 intro g
69 rfl
71/--
72Applying the projection map to a completed element returns its corresponding finite-stage
73coordinate.
74-/
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. -/
83theorem leftQuotientProjection_comp_apply_symm
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. -/
90theorem surjective_leftQuotientProjection
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