ProCGroups.Order.Basic
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
import
instance instTopClosedSubgroup : Top (ClosedSubgroup G) :=
⟨{ toSubgroup := ⊤, isClosed' := isClosed_univ }⟩Closed subgroups have a top element: the whole group.
instance instBotClosedSubgroup [T1Space G] : Bot (ClosedSubgroup G) :=
⟨{ toSubgroup := ⊥
isClosed' := by
change IsClosed ({(1 : G)} : Set G)
exact isClosed_singleton }⟩Closed subgroups have a bottom element: the trivial subgroup, closed in a \(T_1\) topological group.
noncomputable def map [CompactSpace G] [T2Space K] (H : ClosedSubgroup G)
(φ : G →* K) (hφ : Continuous φ) : ClosedSubgroup K where
toSubgroup := (H : Subgroup G).map φ
isClosed' := by
let f : H → K := fun x => φ x
have hcont : Continuous f := hφ.comp continuous_subtype_val
have hcompact : IsCompact (Set.range f) := isCompact_range hcont
have hEq : Set.range f = ((H : Subgroup G).map φ : Set K) := by
ext y
constructor
· rintro ⟨x, rfl⟩
exact (Subgroup.mem_map).2 ⟨x.1, x.2, rfl⟩
· intro hy
rcases (Subgroup.mem_map).1 hy with ⟨x, hx, rfl⟩
exact ⟨⟨x, hx⟩, rfl⟩
simpa [hEq] using hcompact.isClosedThe image of a closed subgroup under a continuous homomorphism from a compact domain into a Hausdorff codomain.
theorem toSubgroup_map [CompactSpace G] [T2Space K] (H : ClosedSubgroup G)
(φ : G →* K) (hφ : Continuous φ) :
((map H φ hφ : ClosedSubgroup K) : Subgroup K) = (H : Subgroup G).map φThe underlying subgroup of the image closed subgroup is the image of the underlying subgroup.
Show proof
rflProof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem mem_map [CompactSpace G] [T2Space K] {H : ClosedSubgroup G}
{φ : G →* K} (hφ : Continuous φ) {y : K} :
y ∈ map H φ hφ ↔ ∃ x ∈ (H : Subgroup G), φ x = yMembership in the image closed subgroup is membership in the subgroup map.
Show proof
by
rflProof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem map_id [CompactSpace G] [T2Space G] (H : ClosedSubgroup G) :
map H (MonoidHom.id G) continuous_id = HMapping a closed subgroup along the identity homomorphism gives the same closed subgroup.
Show proof
by
apply ClosedSubgroup.toSubgroup_injective
ext x
constructor
· rintro ⟨y, hy, rfl⟩
exact hy
· intro hx
exact ⟨x, hx, rfl⟩Proof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem map_comp
{L : Type w} [Group L] [TopologicalSpace L]
[CompactSpace G] [T2Space K] [CompactSpace K] [T2Space L]
(H : ClosedSubgroup G) (φ : G →* K) (hφ : Continuous φ)
(ψ : K →* L) (hψ : Continuous ψ) :
map (map H φ hφ) ψ hψ = map H (ψ.comp φ) (hψ.comp hφ)Images of closed subgroups compose under composition of continuous homomorphisms.
Show proof
by
apply ClosedSubgroup.toSubgroup_injective
ext z
constructor
· rintro ⟨y, hy, rfl⟩
rcases (Subgroup.mem_map).1 hy with ⟨x, hx, rfl⟩
exact ⟨x, hx, rfl⟩
· rintro ⟨x, hx, rfl⟩
exact ⟨φ x, (Subgroup.mem_map).2 ⟨x, hx, rfl⟩, rfl⟩Proof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem map_mono [CompactSpace G] [T2Space K] {H H' : ClosedSubgroup G}
(hHH' : (H : Subgroup G) ≤ (H' : Subgroup G))
(φ : G →* K) (hφ : Continuous φ) :
((map H φ hφ : ClosedSubgroup K) : Subgroup K) ≤
((map H' φ hφ : ClosedSubgroup K) : Subgroup K)The image construction on closed subgroups is monotone.
Show proof
Subgroup.map_mono hHH'Proof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem map_bot [CompactSpace G] [T1Space G] [T2Space K]
(φ : G →* K) (hφ : Continuous φ) :
map (⊥ : ClosedSubgroup G) φ hφ = (⊥ : ClosedSubgroup K)The image of the bottom closed subgroup is the bottom closed subgroup.
Show proof
by
apply ClosedSubgroup.toSubgroup_injective
ext y
constructor
· rintro ⟨x, hx, rfl⟩
simpa using congrArg φ (show x = 1 from by simpa using hx)
· intro hy
refine ⟨1, by simp only [SetLike.mem_coe, one_mem], ?_⟩
simpa using (show y = 1 from by simpa using hy).symmProof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem map_eq_top_of_surjective [CompactSpace G] [T2Space K] (H : ClosedSubgroup G)
(φ : G →* K) (hφ : Continuous φ)
(hφH : ∀ y : K, ∃ x ∈ (H : Subgroup G), φ x = y) :
map H φ hφ = (⊤ : ClosedSubgroup K)The image of the top closed subgroup under a surjective homomorphism is top.
Show proof
by
apply ClosedSubgroup.toSubgroup_injective
ext y
constructor
· intro _
trivial
· intro _
exact hφH yProof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem map_le_iff_le_comap [CompactSpace G] [T2Space K]
{H : ClosedSubgroup G} {L : ClosedSubgroup K}
{φ : G →* K} (hφ : Continuous φ) :
((map H φ hφ : ClosedSubgroup K) : Subgroup K) ≤ (L : Subgroup K) ↔
(H : Subgroup G) ≤ Subgroup.comap φ (L : Subgroup K)Image containment for closed subgroups is equivalent to containment in the comap.
Show proof
by
constructor
· intro h x hx
exact h ((Subgroup.mem_map).2 ⟨x, hx, rfl⟩)
· intro h y hy
rcases (Subgroup.mem_map).1 hy with ⟨x, hx, rfl⟩
exact h hxProof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□def IsSurjectiveInverseSystem {I : Type v} [Preorder I]
(S : ProCGroups.InverseSystems.InverseSystem (I := I)) : Prop :=
∀ ⦃i j : I⦄ (hij : i ≤ j), Function.Surjective (S.map hij)The surjectivity hypothesis for transition maps in a group-valued inverse system.
noncomputable def inverseLimitProjectionImage
{I : Type v} [Preorder I]
(S : ProCGroups.InverseSystems.InverseSystem (I := I))
[∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
[∀ i, TopologicalSpace (S.X i)] [∀ i, T2Space (S.X i)]
[CompactSpace S.inverseLimit]
(H : ClosedSubgroup S.inverseLimit) (i : I) : ClosedSubgroup (S.X i) :=
let πi : S.inverseLimit →* S.X i := {
toFun := fun x => S.projection i x
map_one' := rfl
map_mul' := by
intro x y
rfl
}
have hπi : Continuous (fun x : S.inverseLimit => S.projection i x) := by
exact (continuous_apply i).comp continuous_subtype_val
ClosedSubgroup.map H πi hπiThe image of a closed subgroup under a projection from a group-valued inverse limit.
noncomputable def quotientImage [CompactSpace G] (H : ClosedSubgroup G)
(U : OpenNormalSubgroup G) : ClosedSubgroup (G ⧸ (U : Subgroup G)) :=
ClosedSubgroup.map H (QuotientGroup.mk' (U : Subgroup G)) continuous_quotient_mk'The image of a closed subgroup in an open-normal finite quotient.
theorem toSubgroup_quotientImage [CompactSpace G] (H : ClosedSubgroup G)
(U : OpenNormalSubgroup G) :
((quotientImage (G := G) H U : ClosedSubgroup (G ⧸ (U : Subgroup G))) :
Subgroup (G ⧸ (U : Subgroup G))) =
(H : Subgroup G).map (QuotientGroup.mk' (U : Subgroup G))The subgroup underlying a quotient image is the image of the closed subgroup in the quotient.
Show proof
rflProof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem mem_quotientImage [CompactSpace G] {H : ClosedSubgroup G}
{U : OpenNormalSubgroup G} {y : G ⧸ (U : Subgroup G)} :
y ∈ quotientImage (G := G) H U ↔
∃ x ∈ (H : Subgroup G), QuotientGroup.mk' (U : Subgroup G) x = yMembership in a quotient image is membership in the image of the underlying closed subgroup.
Show proof
by
rflProof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem mem_closedSubgroup_iff_forall_quotientImage_mem [CompactSpace G]
(hG : IsProfiniteGroup G) {H : ClosedSubgroup G} {x : G} :
x ∈ H ↔
∀ U : OpenNormalSubgroup G,
OpenNormalSubgroup.quotientProj U x ∈
(quotientImage (G := G) H U : Subgroup (G ⧸ (U : Subgroup G)))Membership in a closed subgroup of a profinite group can be checked after all open-normal finite quotients.
Show proof
by
constructor
· intro hx U
exact (Subgroup.mem_map).2 ⟨x, hx, rfl⟩
· intro hx
letI : T2Space G := IsProfiniteGroup.t2Space hG
letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
have hxOpen :
∀ N : Subgroup G, IsOpen (N : Set G) ∧ (H : Subgroup G) ≤ N → x ∈ N := by
intro N hN
let V : OpenSubgroup G := ⟨N, hN.1⟩
rcases exists_openNormalSubgroup_mul_subset_openSubgroup (G := G) H V hN.2 with
⟨U, hHU⟩
have hxImg :
QuotientGroup.mk' (U : Subgroup G) x ∈
(quotientImage (G := G) H U : Subgroup (G ⧸ (U : Subgroup G))) := by
simpa [OpenNormalSubgroup.quotientProj] using hx U
have hxSup : x ∈ (H : Subgroup G) ⊔ (U : Subgroup G) := by
have hEq :
(H : Subgroup G) ⊔ (U : Subgroup G) =
Subgroup.comap (QuotientGroup.mk' (U : Subgroup G))
((quotientImage (G := G) H U :
ClosedSubgroup (G ⧸ (U : Subgroup G))) :
Subgroup (G ⧸ (U : Subgroup G))) := by
calc
(H : Subgroup G) ⊔ (U : Subgroup G) =
(H : Subgroup G) ⊔ (QuotientGroup.mk' (U : Subgroup G)).ker := by
rw [QuotientGroup.ker_mk']
_ = Subgroup.comap (QuotientGroup.mk' (U : Subgroup G))
(((H : Subgroup G).map (QuotientGroup.mk' (U : Subgroup G))) :
Subgroup (G ⧸ (U : Subgroup G))) := by
rw [← Subgroup.comap_map_eq]
_ = Subgroup.comap (QuotientGroup.mk' (U : Subgroup G))
((quotientImage (G := G) H U :
ClosedSubgroup (G ⧸ (U : Subgroup G))) :
Subgroup (G ⧸ (U : Subgroup G))) := by
rfl
rw [hEq]
exact hxImg
rcases
(Subgroup.mem_sup_of_normal_right (s := (H : Subgroup G)) (t := (U : Subgroup G))).1
hxSup with
⟨h, hhH, u, huU, hhu⟩
have hxV : x ∈ (V : Set G) := hHU ⟨h, hhH, u, huU, hhu⟩
simpa [V] using hxV
have hxInf :
x ∈ sInf {N : Subgroup G | IsOpen (N : Set G) ∧ (H : Subgroup G) ≤ N} := by
simp only [Subgroup.mem_sInf, Set.mem_setOf_eq]
intro N hN
exact hxOpen N hN
change x ∈ (H : Subgroup G)
exact (closedSubgroup_eq_sInf_open (G := G) H).symm ▸ hxInfProof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem closedSubgroup_le_iff_forall_quotientImages_le [CompactSpace G]
(hG : IsProfiniteGroup G) {H K : ClosedSubgroup G} :
(H : Subgroup G) ≤ (K : Subgroup G) ↔
∀ U : OpenNormalSubgroup G,
(quotientImage (G := G) H U : Subgroup (G ⧸ (U : Subgroup G))) ≤
(quotientImage (G := G) K U : Subgroup (G ⧸ (U : Subgroup G)))Inclusion of closed subgroups of a profinite group can be checked on all open-normal finite quotients.
Show proof
by
constructor
· intro hHK U y hy
rcases (Subgroup.mem_map).1 hy with ⟨x, hx, rfl⟩
exact (Subgroup.mem_map).2 ⟨x, hHK hx, rfl⟩
· intro hHK x hx
exact (mem_closedSubgroup_iff_forall_quotientImage_mem (G := G) hG (H := K)).2 (by
intro U
exact hHK U ((Subgroup.mem_map).2 ⟨x, hx, rfl⟩))Proof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem closedSubgroup_eq_of_quotientImages_eq [CompactSpace G]
(hG : IsProfiniteGroup G) {H K : ClosedSubgroup G}
(hHK : ∀ U : OpenNormalSubgroup G,
quotientImage (G := G) H U = quotientImage (G := G) K U) :
H = KTwo closed subgroups are equal if their images agree in every finite quotient.
Show proof
by
letI : T2Space G := IsProfiniteGroup.t2Space hG
letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
have hle :
∀ {A B : ClosedSubgroup G},
(∀ U : OpenNormalSubgroup G,
quotientImage (G := G) A U = quotientImage (G := G) B U) →
(A : Subgroup G) ≤ B := by
intro A B hAB x hxA
have hxOpen :
∀ N : Subgroup G, IsOpen (N : Set G) ∧ (B : Subgroup G) ≤ N → x ∈ N := by
intro N hN
let V : OpenSubgroup G := ⟨N, hN.1⟩
rcases exists_openNormalSubgroup_mul_subset_openSubgroup (G := G) B V hN.2 with
⟨U, hBU⟩
have hxImgA :
QuotientGroup.mk' (U : Subgroup G) x ∈ (quotientImage (G := G) A U : Subgroup _) := by
exact (Subgroup.mem_map).2 ⟨x, hxA, rfl⟩
have hxImgB :
QuotientGroup.mk' (U : Subgroup G) x ∈ (quotientImage (G := G) B U : Subgroup _) := by
rw [← hAB U]
exact hxImgA
have hxSup : x ∈ (B : Subgroup G) ⊔ (U : Subgroup G) := by
have hEq :
(B : Subgroup G) ⊔ (U : Subgroup G) =
Subgroup.comap (QuotientGroup.mk' (U : Subgroup G))
((quotientImage (G := G) B U :
ClosedSubgroup (G ⧸ (U : Subgroup G))) :
Subgroup (G ⧸ (U : Subgroup G))) := by
calc
(B : Subgroup G) ⊔ (U : Subgroup G) =
(B : Subgroup G) ⊔ (QuotientGroup.mk' (U : Subgroup G)).ker := by
rw [QuotientGroup.ker_mk']
_ = Subgroup.comap (QuotientGroup.mk' (U : Subgroup G))
(((B : Subgroup G).map (QuotientGroup.mk' (U : Subgroup G))) :
Subgroup (G ⧸ (U : Subgroup G))) := by
rw [← Subgroup.comap_map_eq]
_ = Subgroup.comap (QuotientGroup.mk' (U : Subgroup G))
((quotientImage (G := G) B U :
ClosedSubgroup (G ⧸ (U : Subgroup G))) :
Subgroup (G ⧸ (U : Subgroup G))) := by
rfl
rw [hEq]
exact hxImgB
rcases
(Subgroup.mem_sup_of_normal_right (s := (B : Subgroup G)) (t := (U : Subgroup G))).1
hxSup with
⟨b, hbB, u, huU, hbu⟩
have hxV : x ∈ (V : Set G) := hBU ⟨b, hbB, u, huU, hbu⟩
simpa [V] using hxV
have hxB :
x ∈ sInf {N : Subgroup G | IsOpen (N : Set G) ∧ (B : Subgroup G) ≤ N} := by
simp only [Subgroup.mem_sInf, Set.mem_setOf_eq]
intro N hN
exact hxOpen N hN
exact (closedSubgroup_eq_sInf_open (G := G) B).symm ▸ hxB
exact le_antisymm (hle hHK) (hle (fun U => (hHK U).symm))Proof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□instance instTopologicalSpaceXCompat (i : I) :
TopologicalSpace (S.X i) :=
S.topologicalSpace iThe constructed object carries the topological space structure inherited from its construction.
instance instTopologicalSpaceXCompatFun :
∀ i, TopologicalSpace (S.X i) :=
S.topologicalSpaceThe constructed object carries the topological space structure inherited from its construction.
instance instCompactSpaceXCompatFun : ∀ i, CompactSpace (S.X i) := by
intro i
infer_instanceThe constructed object carries the compact space structure inherited from its profinite construction.
instance instT2SpaceXCompatFun : ∀ i, T2Space (S.X i) := by
intro i
infer_instanceThe constructed object is Hausdorff, with its \(T_2\) structure inherited from the profinite construction.
def inverseSystemStageHom {i j : I} (hij : i ≤ j) : S.X j →* S.X i where
toFun := S.map hij
map_one' := ProCGroups.InverseSystems.IsGroupSystem.map_one (S := S) hij
map_mul' := ProCGroups.InverseSystems.IsGroupSystem.map_mul (S := S) hijThe transition map of a group-valued inverse system is viewed as a homomorphism.
theorem inverseSystemStageHom_continuous {i j : I} (hij : i ≤ j) :
Continuous (inverseSystemStageHom (S := S) hij)The stage homomorphism associated to a group-valued inverse system is continuous.
Show proof
by
simpa [inverseSystemStageHom] using (S.continuous_map hij :
Continuous (fun x : S.X j => S.map hij x))Proof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□def compatibleClosedSubgroupSystem
(L : ∀ i, ClosedSubgroup (S.X i))
(hcompat : ∀ {i j : I} (hij : i ≤ j),
((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
(inverseSystemStageHom_continuous (S := S) hij) :
ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
(L i : Subgroup (S.X i))) :
ProCGroups.InverseSystems.InverseSystem (I := I) where
X := fun i => L i
topologicalSpace := fun i => inferInstance
map := fun {i j} hij x =>
⟨S.map hij x.1, by
have hx :
S.map hij x.1 ∈
((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
(inverseSystemStageHom_continuous (S := S) hij) :
ClosedSubgroup (S.X i)) : Subgroup (S.X i)) := by
exact (Subgroup.mem_map).2 ⟨x.1, x.2, rfl⟩
rw [hcompat hij] at hx
exact hx⟩
continuous_map := fun {i j} hij =>
Continuous.subtype_mk
((inverseSystemStageHom_continuous (S := S) hij).comp continuous_subtype_val) (fun x => by
have hx :
S.map hij x.1 ∈
((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
(inverseSystemStageHom_continuous (S := S) hij) :
ClosedSubgroup (S.X i)) : Subgroup (S.X i)) := by
exact (Subgroup.mem_map).2 ⟨x.1, x.2, rfl⟩
rw [hcompat hij] at hx
exact hx)
map_id := fun i => by
funext x
apply Subtype.ext
simp only [InverseSystem.map_id_apply, id_eq]
map_comp := fun {i j k} hij hjk => by
funext x
apply Subtype.ext
simp only [Function.comp_apply, InverseSystem.map_comp_apply]The inverse system obtained by restricting an ambient inverse system to a compatible family of closed subgroups.
instance compatibleClosedSubgroupSystem_group
(L : ∀ i, ClosedSubgroup (S.X i))
(hcompat : ∀ {i j : I} (hij : i ≤ j),
((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
(inverseSystemStageHom_continuous (S := S) hij) :
ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
(L i : Subgroup (S.X i)))
(i : I) :
Group ((compatibleClosedSubgroupSystem (S := S) L hcompat).X i) := by
dsimp [compatibleClosedSubgroupSystem]
infer_instanceEach stage of a compatible closed-subgroup system is a group.
instance compatibleClosedSubgroupSystem_isGroupSystem
(L : ∀ i, ClosedSubgroup (S.X i))
(hcompat : ∀ {i j : I} (hij : i ≤ j),
((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
(inverseSystemStageHom_continuous (S := S) hij) :
ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
(L i : Subgroup (S.X i))) :
ProCGroups.InverseSystems.IsGroupSystem (compatibleClosedSubgroupSystem (S := S) L hcompat) where
map_one := by
intro i j hij
apply Subtype.ext
simpa [compatibleClosedSubgroupSystem, inverseSystemStageHom] using
(ProCGroups.InverseSystems.IsGroupSystem.map_one (S := S) hij)
map_mul := by
intro i j hij x y
apply Subtype.ext
simpa [compatibleClosedSubgroupSystem, inverseSystemStageHom] using
(ProCGroups.InverseSystems.IsGroupSystem.map_mul (S := S) hij x.1 y.1)
map_inv := by
intro i j hij x
apply Subtype.ext
simpa [compatibleClosedSubgroupSystem, inverseSystemStageHom] using
(ProCGroups.InverseSystems.IsGroupSystem.map_inv (S := S) hij x.1)A compatible closed-subgroup system is a group-valued inverse system.
def compatibleClosedSubgroupInclusion
(L : ∀ i, ClosedSubgroup (S.X i))
(hcompat : ∀ {i j : I} (hij : i ≤ j),
((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
(inverseSystemStageHom_continuous (S := S) hij) :
ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
(L i : Subgroup (S.X i))) :
(compatibleClosedSubgroupSystem (S := S) L hcompat).Morphism S where
map := fun i => Subtype.val
continuous_map := fun i => by
dsimp [compatibleClosedSubgroupSystem]
exact continuous_subtype_val
comm := fun {i j} hij => by
funext x
rflThe canonical coordinatewise inclusion of a compatible subgroup system into the ambient system.
noncomputable def compatibleClosedSubgroupLimHom
(L : ∀ i, ClosedSubgroup (S.X i))
(hcompat : ∀ {i j : I} (hij : i ≤ j),
((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
(inverseSystemStageHom_continuous (S := S) hij) :
ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
(L i : Subgroup (S.X i))) :
(compatibleClosedSubgroupSystem (S := S) L hcompat).inverseLimit →* S.inverseLimit where
toFun :=
(compatibleClosedSubgroupSystem (S := S) L hcompat).limMap
(compatibleClosedSubgroupInclusion (S := S) L hcompat)
map_one' := by
apply S.ext
intro i
rfl
map_mul' := by
intro x y
apply S.ext
intro i
rflThe induced homomorphism from the inverse limit of a compatible subgroup family into the ambient inverse limit.
noncomputable def closedSubgroupFromCompatibleFamily
(L : ∀ i, ClosedSubgroup (S.X i))
(hcompat : ∀ {i j : I} (hij : i ≤ j),
((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
(inverseSystemStageHom_continuous (S := S) hij) :
ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
(L i : Subgroup (S.X i))) :
ClosedSubgroup S.inverseLimit where
toSubgroup := (compatibleClosedSubgroupLimHom (S := S) L hcompat).range
isClosed' := by
let T := compatibleClosedSubgroupSystem (S := S) L hcompat
letI : ∀ i, TopologicalSpace (S.X i) := S.topologicalSpace
letI : ∀ i, T2Space (S.X i) := instT2SpaceXCompatFun (S := S)
letI : ∀ i, CompactSpace (T.X i) := fun i => by
dsimp [T, compatibleClosedSubgroupSystem]
infer_instance
letI : ∀ i, T2Space (T.X i) := fun i => by
dsimp [T, compatibleClosedSubgroupSystem]
infer_instance
letI : CompactSpace T.inverseLimit := inferInstance
letI : T2Space S.inverseLimit := S.t2Space_inverseLimit
let φ := compatibleClosedSubgroupLimHom (S := S) L hcompat
have hφcont :
Continuous (φ : T.inverseLimit → S.inverseLimit) := by
change Continuous (T.limMap (compatibleClosedSubgroupInclusion (S := S) L hcompat))
exact T.continuous_limMap (compatibleClosedSubgroupInclusion (S := S) L hcompat)
simpa [φ] using (isCompact_range hφcont).isClosedClosed subgroup of the ambient inverse limit obtained from a compatible family of closed subgroups with surjective transition maps.
theorem inverseLimitProjectionImage_closedSubgroupFromCompatibleFamily
[CompactSpace S.inverseLimit]
(hdir : Directed (· ≤ ·) (id : I → I))
(L : ∀ i, ClosedSubgroup (S.X i))
(hcompat : ∀ {i j : I} (hij : i ≤ j),
((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
(inverseSystemStageHom_continuous (S := S) hij) :
ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
(L i : Subgroup (S.X i))) (i : I) :
inverseLimitProjectionImage S (closedSubgroupFromCompatibleFamily (S := S) L hcompat) i =
L iProjection images of a closed subgroup recovered from a compatible family match the given family.
Show proof
by
let T := compatibleClosedSubgroupSystem (S := S) L hcompat
let incl := compatibleClosedSubgroupInclusion (S := S) L hcompat
let φ := compatibleClosedSubgroupLimHom (S := S) L hcompat
have hTsurj : ∀ {i j : I} (hij : i ≤ j), Function.Surjective (T.map hij) := by
intro i j hij y
have hy :
y.1 ∈
((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
(inverseSystemStageHom_continuous (S := S) hij) :
ClosedSubgroup (S.X i)) : Subgroup (S.X i)) := by
exact (hcompat hij).symm ▸ (show y.1 ∈ (L i : Subgroup (S.X i)) from y.2)
rcases (Subgroup.mem_map).1 hy with ⟨x, hx, hxy⟩
refine ⟨⟨x, hx⟩, ?_⟩
apply Subtype.ext
simpa [T, compatibleClosedSubgroupSystem] using hxy
letI : ∀ i, CompactSpace (T.X i) := fun i => by
dsimp [T, compatibleClosedSubgroupSystem]
infer_instance
letI : ∀ i, T2Space (T.X i) := fun i => by
dsimp [T, compatibleClosedSubgroupSystem]
infer_instance
letI : CompactSpace T.inverseLimit := inferInstance
letI : T2Space T.inverseLimit := T.t2Space_inverseLimit
ext y
constructor
· intro hy
rcases (Subgroup.mem_map).1 hy with ⟨x, hx, hxy⟩
rcases hx with ⟨z, rfl⟩
have hcoord :
S.projection i ((φ : T.inverseLimit →* S.inverseLimit) z) = (T.projection i z).1 := by
simpa [φ, compatibleClosedSubgroupInclusion] using congrFun (T.π_comp_limMap (Θ := incl) i) z
have hmem : (T.projection i z).1 ∈ (L i : Subgroup (S.X i)) := by
exact (T.projection i z).2
have hmem' : S.projection i ((φ : T.inverseLimit →* S.inverseLimit) z) ∈ (L i : Subgroup (S.X i)) := by
exact hcoord ▸ hmem
exact hxy ▸ hmem'
· intro hy
have hπsurj : Function.Surjective (T.projection i) := T.surjective_π hdir hTsurj i
rcases hπsurj ⟨y, hy⟩ with ⟨z, hz⟩
refine (Subgroup.mem_map).2 ?_
refine ⟨φ z, ⟨z, rfl⟩, ?_⟩
have hcoord :
S.projection i ((φ : T.inverseLimit →* S.inverseLimit) z) = y := by
simpa [φ, compatibleClosedSubgroupLimHom, compatibleClosedSubgroupInclusion,
compatibleClosedSubgroupSystem] using congrArg Subtype.val hz
exact hcoordProof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem map_inverseLimitProjectionImage
[CompactSpace S.inverseLimit]
(H : ClosedSubgroup S.inverseLimit) {i j : I} (hij : i ≤ j) :
((ClosedSubgroup.map (inverseLimitProjectionImage S H j) (inverseSystemStageHom (S := S) hij)
(inverseSystemStageHom_continuous (S := S) hij) :
ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
(inverseLimitProjectionImage S H i : Subgroup (S.X i))Projection images commute with mapping a closed subgroup along a compatible inverse-limit morphism.
Show proof
by
ext x
constructor
· intro hx
rcases (Subgroup.mem_map).1 hx with ⟨y, hy, hxy⟩
rcases (Subgroup.mem_map).1 hy with ⟨z, hz, hzy⟩
refine (Subgroup.mem_map).2 ⟨z, hz, ?_⟩
calc
S.projection i z = S.map hij (S.projection j z) := by
symm
simpa using z.2 i j hij
_ = S.map hij y := by simpa using congrArg (S.map hij) hzy
_ = x := hxy
· intro hx
rcases (Subgroup.mem_map).1 hx with ⟨z, hz, hzx⟩
refine (Subgroup.mem_map).2 ⟨S.projection j z, ?_, ?_⟩
· exact (Subgroup.mem_map).2 ⟨z, hz, rfl⟩
· calc
S.map hij (S.projection j z) = S.projection i z := by
simpa using z.2 i j hij
_ = x := hzxProof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem map_inverseLimitProjectionImage_closed
[CompactSpace S.inverseLimit]
(H : ClosedSubgroup S.inverseLimit) {i j : I} (hij : i ≤ j) :
ClosedSubgroup.map (inverseLimitProjectionImage S H j)
(inverseSystemStageHom (S := S) hij)
(inverseSystemStageHom_continuous (S := S) hij) =
inverseLimitProjectionImage S H iThe stage-transition compatibility of projection images, repackaged as an equality of closed subgroups.
Show proof
by
ext x
simpa using congrArg (fun K : Subgroup (S.X i) => x ∈ K)
(map_inverseLimitProjectionImage (S := S) H hij)Proof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem inverseLimitProjectionImage_bot
[CompactSpace S.inverseLimit] (i : I) :
inverseLimitProjectionImage S (⊥ : ClosedSubgroup S.inverseLimit) i = ⊥The projection image of the trivial closed subgroup is trivial.
Show proof
by
ext x
constructor
· intro hx
rcases (Subgroup.mem_map).1 hx with ⟨y, hy, hyx⟩
have hy1 : y = 1 := by simpa using hy
cases hy1
simpa using hyx.symm
· intro hx
have hx1 : x = 1 := by simpa using hx
refine (Subgroup.mem_map).2 ⟨1, by simp only [one_mem], ?_⟩
rw [hx1]
rflProof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem inverseLimitProjectionImage_top
[CompactSpace S.inverseLimit]
(hdir : Directed (· ≤ ·) (id : I → I))
(hsurj : IsSurjectiveInverseSystem S) (i : I) :
inverseLimitProjectionImage S (⊤ : ClosedSubgroup S.inverseLimit) i = ⊤Under surjective transition maps, the projection image of the whole inverse limit is the whole stage group.
Show proof
by
ext x
constructor
· intro _
change x ∈ (⊤ : Subgroup (S.X i))
simp only [Subgroup.mem_top]
· intro _
have hπsurj : Function.Surjective (S.projection i) :=
S.surjective_π hdir (fun {i j} hij => hsurj hij) i
rcases hπsurj x with ⟨y, hy⟩
refine (Subgroup.mem_map).2 ⟨y, ?_, hy⟩
change y ∈ (⊤ : Subgroup S.inverseLimit)
simp only [Subgroup.mem_top]Proof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem inverseLimitProjectionImage_mono
[CompactSpace S.inverseLimit]
{H K : ClosedSubgroup S.inverseLimit}
(hHK : (H : Subgroup S.inverseLimit) ≤ K) (i : I) :
(inverseLimitProjectionImage S H i : Subgroup (S.X i)) ≤
(inverseLimitProjectionImage S K i : Subgroup (S.X i))Projection images are monotone in the closed subgroup argument.
Show proof
by
intro x hx
rcases (Subgroup.mem_map).1 hx with ⟨y, hy, rfl⟩
exact (Subgroup.mem_map).2 ⟨y, hHK hy, rfl⟩Proof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem closedSubgroup_le_of_projectionImages_le
[Nonempty I] [CompactSpace S.inverseLimit]
[TotallyDisconnectedSpace S.inverseLimit] [IsTopologicalGroup S.inverseLimit]
[∀ i, TotallyDisconnectedSpace (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I))
(H K : ClosedSubgroup S.inverseLimit)
(hproj : ∀ i,
(inverseLimitProjectionImage S H i : Subgroup (S.X i)) ≤
(inverseLimitProjectionImage S K i : Subgroup (S.X i))) :
(H : Subgroup S.inverseLimit) ≤ (K : Subgroup S.inverseLimit)Closed subgroups of an inverse limit are determined by their stagewise projection images.
Show proof
by
intro x hx
have hx' :
x ∈ sInf {N : Subgroup S.inverseLimit |
IsOpen (N : Set S.inverseLimit) ∧ (K : Subgroup S.inverseLimit) ≤ N} := by
simp only [Subgroup.mem_sInf, Set.mem_setOf_eq]
intro N hN
let V : OpenSubgroup S.inverseLimit := ⟨N, hN.1⟩
rcases exists_openNormalSubgroup_mul_subset_openSubgroup (G := S.inverseLimit) K V hN.2 with
⟨U, hKU⟩
letI : Finite (S.inverseLimit ⧸ (U : Subgroup S.inverseLimit)) :=
openNormalSubgroup_finiteQuotient (G := S.inverseLimit) U
letI : DiscreteTopology (S.inverseLimit ⧸ (U : Subgroup S.inverseLimit)) :=
QuotientGroup.discreteTopology (openNormalSubgroup_isOpen (G := S.inverseLimit) U)
let β : S.inverseLimit →* S.inverseLimit ⧸ (U : Subgroup S.inverseLimit) :=
QuotientGroup.mk' (U : Subgroup S.inverseLimit)
rcases ProCGroups.InverseSystems.InverseSystem.factors_through_projection_finite_group_hom
(S := S) hdir β continuous_quotient_mk' with ⟨k, βk, hβkcont, hβfac⟩
have hxk : S.projection k x ∈ (inverseLimitProjectionImage S H k : Subgroup (S.X k)) := by
exact (Subgroup.mem_map).2 ⟨x, hx, rfl⟩
have hxkK : S.projection k x ∈ (inverseLimitProjectionImage S K k : Subgroup (S.X k)) := hproj k hxk
rcases (Subgroup.mem_map).1 hxkK with ⟨z, hzK, hzxk⟩
have hβz : β z = βk (S.projection k z) := by
simpa [Function.comp] using
congrArg (fun f : S.inverseLimit → S.inverseLimit ⧸ (U : Subgroup S.inverseLimit) =>
f z) hβfac
have hβx : β x = βk (S.projection k x) := by
simpa [Function.comp] using
congrArg (fun f : S.inverseLimit → S.inverseLimit ⧸ (U : Subgroup S.inverseLimit) =>
f x) hβfac
have hzxu : z⁻¹ * x ∈ (U : Subgroup S.inverseLimit) := by
apply (QuotientGroup.eq_one_iff (N := (U : Subgroup S.inverseLimit)) (z⁻¹ * x)).1
have hβeq : β z = β x := by
calc
β z = βk (S.projection k z) := hβz
_ = βk (S.projection k x) := by simpa using congrArg βk hzxk
_ = β x := hβx.symm
calc
β (z⁻¹ * x) = (β z)⁻¹ * β x := by simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_mul, QuotientGroup.mk_inv, β]
_ = 1 := by simp only [hβeq, inv_mul_cancel]
have hxKU : x ∈ (((K : Subgroup S.inverseLimit) : Set S.inverseLimit) *
(((U : Subgroup S.inverseLimit) : Set S.inverseLimit))) := by
refine ⟨z, hzK, z⁻¹ * x, hzxu, ?_⟩
simp only [mul_inv_cancel_left]
exact hKU hxKU
exact (closedSubgroup_eq_sInf_open (G := S.inverseLimit) K).symm ▸ hx'Proof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem closedSubgroup_eq_of_projectionImages_eq
[Nonempty I] [CompactSpace S.inverseLimit]
[TotallyDisconnectedSpace S.inverseLimit] [IsTopologicalGroup S.inverseLimit]
[∀ i, TotallyDisconnectedSpace (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I))
(H K : ClosedSubgroup S.inverseLimit)
(hproj : ∀ i, inverseLimitProjectionImage S H i = inverseLimitProjectionImage S K i) :
H = KStagewise equality of projection images determines a closed subgroup of an inverse limit.
Show proof
by
have hHK : (H : Subgroup S.inverseLimit) ≤ (K : Subgroup S.inverseLimit) :=
closedSubgroup_le_of_projectionImages_le (S := S) hdir H K (fun i => by
exact
le_of_eq <|
congrArg (fun (L : ClosedSubgroup (S.X i)) => (L : Subgroup (S.X i))) (hproj i))
have hKH : (K : Subgroup S.inverseLimit) ≤ (H : Subgroup S.inverseLimit) :=
closedSubgroup_le_of_projectionImages_le (S := S) hdir K H (fun i => by
exact
le_of_eq <|
congrArg (fun (L : ClosedSubgroup (S.X i)) => (L : Subgroup (S.X i))) (hproj i).symm)
apply SetLike.ext'
exact Set.ext fun x => ⟨fun hx => hHK hx, fun hx => hKH hx⟩Proof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem closedSubgroup_eq_bot_of_projectionImages_eq_bot
[Nonempty I] [CompactSpace S.inverseLimit]
[TotallyDisconnectedSpace S.inverseLimit] [IsTopologicalGroup S.inverseLimit]
[∀ i, TotallyDisconnectedSpace (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I))
(H : ClosedSubgroup S.inverseLimit)
(hproj : ∀ i, inverseLimitProjectionImage S H i = ⊥) :
H = ⊥If every stagewise projection image is trivial, then the closed subgroup itself is trivial.
Show proof
by
apply closedSubgroup_eq_of_projectionImages_eq (S := S) hdir H ⊥
intro i
rw [hproj i, inverseLimitProjectionImage_bot (S := S) (i := i)]Proof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□theorem closedSubgroup_eq_top_of_projectionImages_eq_top
[Nonempty I] [CompactSpace S.inverseLimit]
[TotallyDisconnectedSpace S.inverseLimit] [IsTopologicalGroup S.inverseLimit]
[∀ i, TotallyDisconnectedSpace (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I))
(hsurj : IsSurjectiveInverseSystem S)
(H : ClosedSubgroup S.inverseLimit)
(hproj : ∀ i, inverseLimitProjectionImage S H i = ⊤) :
H = ⊤If every stagewise projection image is the whole stage group, then the closed subgroup itself is the whole inverse limit.
Show proof
by
apply closedSubgroup_eq_of_projectionImages_eq (S := S) hdir H ⊤
intro i
rw [hproj i, inverseLimitProjectionImage_top (S := S) hdir hsurj i]Proof. Unfold closed subgroups as subgroups equipped with closedness data. Bottom, top, infimum, image, comap, and order relations are computed on the underlying subgroups, while closedness follows from the relevant topological facts: the trivial subgroup is closed in a \(T_1\) group, the whole group is closed, compact images in Hausdorff groups are closed, and intersections of closed sets are closed. Stagewise projection-image statements use inverse-limit extensionality for closed subgroups.
□