ProCGroups.Categorical.QuotientPullbackEquivalences
This module supplies the topological part of the construction. It checks continuity and stagewise neighborhood properties so that the completed object inherits the required topology.
instance normal_iInf
{ι : Type*} {G : Type*} [Group G] (W : ι → Subgroup G)
[∀ i, (W i).Normal] :
(⨅ i, W i).Normal where
conj_mem := by
intro n hn g
rw [Subgroup.mem_iInf] at hn ⊢
intro i
exact (show (W i).Normal by infer_instance).conj_mem n (hn i) gAn infimum of normal subgroups is normal.
theorem isClosed_sup_of_isCompact_of_normal_right
{G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [T2Space G]
(U V : Subgroup G) [V.Normal]
(hU : IsCompact (U : Set G)) (hV : IsCompact (V : Set G)) :
IsClosed ((U ⊔ V : Subgroup G) : Set G)In a Hausdorff topological group, the join of a compact subgroup with a compact normal subgroup is closed.
Show proof
by
have hmul : Continuous (fun p : G × G => p.1 * p.2) :=
continuous_fst.mul continuous_snd
have hcompact :
IsCompact ((fun p : G × G => p.1 * p.2) '' ((U : Set G) ×ˢ (V : Set G))) :=
(hU.prod hV).image hmul
have hsup_eq_image :
((U ⊔ V : Subgroup G) : Set G) =
(fun p : G × G => p.1 * p.2) '' ((U : Set G) ×ˢ (V : Set G)) := by
ext g
constructor
· intro hg
rcases (Subgroup.mem_sup_of_normal_right (s := U) (t := V)).1 hg with
⟨u, hu, v, hv, huv⟩
exact ⟨(u, v), ⟨hu, hv⟩, by simp only [huv]⟩
· rintro ⟨p, hp, rfl⟩
exact (U ⊔ V).mul_mem
((le_sup_left : U ≤ U ⊔ V) hp.1)
((le_sup_right : V ≤ U ⊔ V) hp.2)
simpa [hsup_eq_image] using hcompact.isClosedProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□theorem isClosed_sup_of_normal
{G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [CompactSpace G]
[T2Space G]
(U V : Subgroup G) [V.Normal]
(hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
IsClosed ((U ⊔ V : Subgroup G) : Set G)In a compact Hausdorff topological group, the join of a closed subgroup with a closed normal subgroup is closed.
Show proof
isClosed_sup_of_isCompact_of_normal_right U V hUclosed.isCompact hVclosed.isCompactProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□def quotientMapOfLE (M N : Subgroup G) [M.Normal] [N.Normal] (hMN : M ≤ N) :
G ⧸ M →* G ⧸ N :=
QuotientGroup.map M N (MonoidHom.id G) (by
intro g hg
exact hMN hg)The quotient map induced by an inclusion of normal subgroups.
@[simp] theorem quotientMapOfLE_mk (M N : Subgroup G) [M.Normal] [N.Normal]
(hMN : M ≤ N) (g : G) :
quotientMapOfLE (G := G) M N hMN (QuotientGroup.mk g) = QuotientGroup.mk gThe quotient map induced by an inclusion sends a coset to its image coset.
Show proof
by
let hcomap : M ≤ Subgroup.comap (MonoidHom.id G) N := by
simpa using hMN
change QuotientGroup.map M N (MonoidHom.id G) hcomap (QuotientGroup.mk g) = QuotientGroup.mk g
simp only [QuotientGroup.map_mk, MonoidHom.id_apply]Proof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□def quotientIInfToCoordinate {ι : Type v} (W : ι → Subgroup G) [∀ i, (W i).Normal]
(i : ι) :
G ⧸ (⨅ j, W j) →* G ⧸ W i :=
quotientMapOfLE (G := G) (⨅ j, W j) (W i) (iInf_le W i)Coordinate map from the quotient by an indexed intersection of normal subgroups.
@[simp] theorem quotientIInfToCoordinate_mk {ι : Type v}
(W : ι → Subgroup G) [∀ i, (W i).Normal] (i : ι) (g : G) :
quotientIInfToCoordinate (G := G) W i (QuotientGroup.mk' (⨅ j, W j) g) =
QuotientGroup.mk' (W i) gThe map from the quotient by the infimum to a coordinate quotient sends a representative to its coordinate coset.
Show proof
by
simp only [quotientIInfToCoordinate, QuotientGroup.mk'_apply, quotientMapOfLE_mk]Proof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□theorem quotient_iInf_isLimit_finite {ι : Type v} [Fintype ι]
(W : ι → Subgroup G) [∀ i, (W i).Normal]
{x y : G ⧸ (⨅ i, W i)}
(hxy : ∀ i, quotientIInfToCoordinate (G := G) W i x =
quotientIInfToCoordinate (G := G) W i y) :
x = yShow proof
by
rcases QuotientGroup.mk'_surjective (⨅ i, W i) x with ⟨gx, rfl⟩
rcases QuotientGroup.mk'_surjective (⨅ i, W i) y with ⟨gy, rfl⟩
apply QuotientGroup.eq.2
rw [Subgroup.mem_iInf]
intro i
have hi := hxy i
simpa [quotientIInfToCoordinate] using (QuotientGroup.eq.1 hi)Proof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem ker_quotientMapOfLE_comp_mk (M N : Subgroup G) [M.Normal] [N.Normal]
(hMN : M ≤ N) :
((quotientMapOfLE (G := G) M N hMN).comp (QuotientGroup.mk' M)).ker = NKernel of the quotient map induced by M \(\le\) N, after precomposition with the quotient map from \(G\).
Show proof
by
ext g
simp only [quotientMapOfLE, MonoidHom.mem_ker, MonoidHom.coe_comp, QuotientGroup.coe_mk', Function.comp_apply,
QuotientGroup.map_mk, MonoidHom.id_apply, QuotientGroup.eq_one_iff]Proof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□def quotientInfToLeft : G ⧸ (U ⊓ V) →* G ⧸ U :=
quotientMapOfLE (G := G) (U ⊓ V) U inf_le_leftThe left-hand map in the quotient pullback square.
def quotientInfToRight : G ⧸ (U ⊓ V) →* G ⧸ V :=
quotientMapOfLE (G := G) (U ⊓ V) V inf_le_rightThe right-hand map in the quotient pullback square.
def quotientToSupLeft : G ⧸ U →* G ⧸ (U ⊔ V) :=
quotientMapOfLE (G := G) U (U ⊔ V) le_sup_leftThe bottom-left map in the quotient pullback square.
def quotientToSupRight : G ⧸ V →* G ⧸ (U ⊔ V) :=
quotientMapOfLE (G := G) V (U ⊔ V) le_sup_rightThe bottom-right map in the quotient pullback square.
@[simp] theorem ker_quotientToSupLeft_comp_mk :
((quotientToSupLeft (G := G) U V).comp (QuotientGroup.mk' U)).ker = U ⊔ VKernel of the left quotient-to-sup map after precomposition with the quotient map from \(G\).
Show proof
by
simp only [quotientToSupLeft, ker_quotientMapOfLE_comp_mk]Proof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem ker_quotientToSupRight_comp_mk :
((quotientToSupRight (G := G) U V).comp (QuotientGroup.mk' V)).ker = U ⊔ VThis lemma identifies the kernel of the right quotient-to-sup map after precomposition with the quotient map from \(G\).
Show proof
by
simp only [quotientToSupRight, ker_quotientMapOfLE_comp_mk]Proof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□def quotientMapOfLECont
{G : Type u} [Group G] [TopologicalSpace G]
(M N : Subgroup G) [M.Normal] [N.Normal] (hMN : M ≤ N) :
G ⧸ M →ₜ* G ⧸ N :=
QuotientGroup.mapₜ M N (ContinuousMonoidHom.id G) (by
intro g hg
exact hMN hg)The quotient map induced by an inclusion of normal subgroups is viewed as continuous.
@[simp] theorem quotientMapOfLECont_toMonoidHom
{G : Type u} [Group G] [TopologicalSpace G]
(M N : Subgroup G) [M.Normal] [N.Normal] (hMN : M ≤ N) :
(quotientMapOfLECont (G := G) M N hMN).toMonoidHom =
quotientMapOfLE (G := G) M N hMNThe quotient map sends the class of an element to the class of its image under the underlying group homomorphism.
Show proof
by
ext g
change quotientMapOfLECont (G := G) M N hMN (QuotientGroup.mk' M g) =
quotientMapOfLE (G := G) M N hMN (QuotientGroup.mk' M g)
simpa [quotientMapOfLECont, quotientMapOfLE] using
(QuotientGroup.mapₜ_apply_mk
(N := M) (M := N) (f := ContinuousMonoidHom.id G)
(hNM := by
intro g hg
exact hMN hg) g)Proof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem quotientMapOfLECont_mk
{G : Type u} [Group G] [TopologicalSpace G]
(M N : Subgroup G) [M.Normal] [N.Normal] (hMN : M ≤ N) (g : G) :
quotientMapOfLECont (G := G) M N hMN (QuotientGroup.mk g) = QuotientGroup.mk gEvaluation of the continuous quotient map induced by inclusion on a quotient class.
Show proof
by
change quotientMapOfLECont (G := G) M N hMN (QuotientGroup.mk' M g) =
QuotientGroup.mk' N g
simpa [quotientMapOfLECont] using
(QuotientGroup.mapₜ_apply_mk
(N := M) (M := N) (f := ContinuousMonoidHom.id G)
(hNM := by
intro g hg
exact hMN hg) g)Proof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□noncomputable def quotientInfToPullback :
G ⧸ (U ⊓ V) →*
FiberProduct.carrier (quotientToSupLeft (G := G) U V) (quotientToSupRight (G := G) U V) := by
refine FiberProduct.lift
(quotientToSupLeft (G := G) U V)
(quotientToSupRight (G := G) U V)
(quotientInfToLeft (G := G) U V)
(quotientInfToRight (G := G) U V) ?_
intro x
refine Quotient.inductionOn x ?_
intro g
rflThe canonical map from \(G/(U \cap V)\) to the concrete pullback of \(G/U\) and \(G/V\) over \(G/(UV)\).
@[simp] theorem quotientInfToPullback_mk (g : G) :
quotientInfToPullback (G := G) U V (QuotientGroup.mk g) =
⟨(QuotientGroup.mk g, QuotientGroup.mk g), rfl⟩The quotient-to-pullback map sends a coset to the corresponding pair of quotient cosets.
Show proof
by
rflProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem pullbackFst_quotientInfToPullback :
(FiberProduct.fst _ _).comp
(quotientInfToPullback (G := G) U V) =
quotientInfToLeft (G := G) U VThe first projection of the quotient-to-pullback map is the natural quotient map to \(G/U\).
Show proof
by
apply MonoidHom.ext
intro x
refine Quotient.inductionOn' x ?_
intro g
rflProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem pullbackSnd_quotientInfToPullback :
(FiberProduct.snd _ _).comp
(quotientInfToPullback (G := G) U V) =
quotientInfToRight (G := G) U VThe second projection of the quotient-to-pullback map is the natural quotient map to \(G/V\).
Show proof
by
apply MonoidHom.ext
intro x
refine Quotient.inductionOn' x ?_
intro g
rflProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□theorem quotientInfToPullback_injective :
Function.Injective (quotientInfToPullback (G := G) U V)The canonical map from \(G/(U \cap V)\) to the pullback of \(G/U\) and \(G/V\) over \(G/(UV)\) is injective.
Show proof
by
intro x y hxy
revert hxy
refine Quotient.inductionOn₂' x y ?_
intro g h hEq
apply QuotientGroup.eq.2
have hU :
QuotientGroup.mk' U g = QuotientGroup.mk' U h := by
simpa [quotientInfToPullback_mk] using
congrArg (fun z => FiberProduct.fst _ _ z) hEq
have hV :
QuotientGroup.mk' V g = QuotientGroup.mk' V h := by
simpa [quotientInfToPullback_mk] using
congrArg (fun z => FiberProduct.snd _ _ z) hEq
exact ⟨QuotientGroup.eq.1 hU, QuotientGroup.eq.1 hV⟩Proof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□theorem quotientInfToPullback_surjective :
Function.Surjective (quotientInfToPullback (G := G) U V)The canonical map from the quotient by \(U \cap V\) to the pullback of the quotients by \(U\) and \(V\) is surjective.
Show proof
by
intro x
rcases QuotientGroup.mk'_surjective U x.1.1 with ⟨a, ha⟩
rcases QuotientGroup.mk'_surjective V x.1.2 with ⟨b, hb⟩
have hsup :
QuotientGroup.mk' (U ⊔ V) a = QuotientGroup.mk' (U ⊔ V) b := by
calc
QuotientGroup.mk' (U ⊔ V) a =
quotientToSupLeft (G := G) U V x.1.1 := by
rw [← ha]
rfl
_ = quotientToSupRight (G := G) U V x.1.2 := x.2
_ = QuotientGroup.mk' (U ⊔ V) b := by
rw [← hb]
rfl
have hab : a⁻¹ * b ∈ U ⊔ V := QuotientGroup.eq.1 hsup
rcases (Subgroup.mem_sup_of_normal_right (s := U) (t := V)).1 hab with
⟨u, hu, v, hv, huv⟩
have hb_eq : b = (a * u) * v := by
calc
b = a * (a⁻¹ * b) := by simp only [mul_inv_cancel_left]
_ = a * (u * v) := by rw [← huv]
_ = (a * u) * v := by simp only [mul_assoc]
have hU : QuotientGroup.mk' U (a * u) = QuotientGroup.mk' U a := by
symm
apply QuotientGroup.eq.2
have hmem : a⁻¹ * (a * u) = u := by simp only [inv_mul_cancel_left]
simpa [hmem] using hu
have hV : QuotientGroup.mk' V (a * u) = QuotientGroup.mk' V b := by
apply QuotientGroup.eq.2
have hmem : (a * u)⁻¹ * b = v := by
calc
(a * u)⁻¹ * b = (a * u)⁻¹ * ((a * u) * v) := by rw [hb_eq]
_ = v := by simp only [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
rw [hmem]
exact hv
refine ⟨QuotientGroup.mk' (U ⊓ V) (a * u), ?_⟩
apply Subtype.ext
apply Prod.ext
· calc
(quotientInfToPullback (G := G) U V
(QuotientGroup.mk' (U ⊓ V) (a * u))).1.1 =
QuotientGroup.mk' U (a * u) := rfl
_ = QuotientGroup.mk' U a := hU
_ = x.1.1 := ha
· calc
(quotientInfToPullback (G := G) U V
(QuotientGroup.mk' (U ⊓ V) (a * u))).1.2 =
QuotientGroup.mk' V (a * u) := rfl
_ = QuotientGroup.mk' V b := hV
_ = x.1.2 := hbProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□theorem quotientInfToPullback_bijective :
Function.Bijective (quotientInfToPullback (G := G) U V)The canonical quotient-to-pullback map is bijective.
Show proof
by
exact ⟨quotientInfToPullback_injective (G := G) U V,
quotientInfToPullback_surjective (G := G) U V⟩Proof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□noncomputable def quotientInfPullbackEquiv :
G ⧸ (U ⊓ V) ≃*
FiberProduct.carrier (quotientToSupLeft (G := G) U V) (quotientToSupRight (G := G) U V) :=
MulEquiv.ofBijective (quotientInfToPullback (G := G) U V)
(quotientInfToPullback_bijective (G := G) U V)The quotient square is canonically isomorphic to the pullback.
@[simp] theorem quotientInfPullbackEquiv_fst :
(FiberProduct.fst _ _).comp (quotientInfPullbackEquiv (G := G) U V).toMonoidHom =
quotientInfToLeft (G := G) U VThe first coordinate of the quotient pullback equivalence is the natural map to \(G/U\).
Show proof
by
change (FiberProduct.fst _ _).comp (quotientInfToPullback (G := G) U V) =
quotientInfToLeft (G := G) U V
exact pullbackFst_quotientInfToPullback (G := G) U VProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem quotientInfPullbackEquiv_snd :
(FiberProduct.snd _ _).comp (quotientInfPullbackEquiv (G := G) U V).toMonoidHom =
quotientInfToRight (G := G) U VThe second coordinate of the quotient pullback equivalence is the natural map to \(G/V\).
Show proof
by
change (FiberProduct.snd _ _).comp (quotientInfToPullback (G := G) U V) =
quotientInfToRight (G := G) U V
exact pullbackSnd_quotientInfToPullback (G := G) U VProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□theorem quotientInf_isPullback :
IsPullbackSquare
(quotientInfToLeft (G := G) U V)
(quotientInfToRight (G := G) U V)
(quotientToSupLeft (G := G) U V)
(quotientToSupRight (G := G) U V)The quotient square is a pullback square.
Show proof
by
exact isPullbackSquare_of_bijective_toConcretePullback
(quotientInfToLeft (G := G) U V)
(quotientInfToRight (G := G) U V)
(quotientToSupLeft (G := G) U V)
(quotientToSupRight (G := G) U V)
(quotientInfToPullback (G := G) U V)
(quotientInfToPullback_bijective (G := G) U V)
(pullbackFst_quotientInfToPullback (G := G) U V)
(pullbackSnd_quotientInfToPullback (G := G) U V)Proof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□theorem isClosed_sup_of_normal
(hG : IsProfiniteGroup G)
(hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
IsClosed ((U ⊔ V : Subgroup G) : Set G)In a profinite group, the join of two closed normal subgroups is closed. This is the compactness input needed for the lower-right quotient in the quotient-pullback square.
Show proof
by
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
letI : T2Space G := IsProfiniteGroup.t2Space hG
exact Subgroup.isClosed_sup_of_normal U V hUclosed hVclosedProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□def quotientInfToLeftCont : G ⧸ (U ⊓ V) →ₜ* G ⧸ U :=
quotientMapOfLECont (G := G) (U ⊓ V) U inf_le_leftThe left map in the continuous quotient square.
def quotientInfToRightCont : G ⧸ (U ⊓ V) →ₜ* G ⧸ V :=
quotientMapOfLECont (G := G) (U ⊓ V) V inf_le_rightThe right map in the continuous quotient square.
def quotientToSupLeftCont : G ⧸ U →ₜ* G ⧸ (U ⊔ V) :=
quotientMapOfLECont (G := G) U (U ⊔ V) le_sup_leftThe bottom-left map in the continuous quotient square.
def quotientToSupRightCont : G ⧸ V →ₜ* G ⧸ (U ⊔ V) :=
quotientMapOfLECont (G := G) V (U ⊔ V) le_sup_rightThe bottom-right map in the continuous quotient square.
@[simp] theorem quotientInfToLeftCont_toMonoidHom :
(quotientInfToLeftCont (G := G) U V).toMonoidHom = quotientInfToLeft (G := G) U VForgetting continuity from the left continuous quotient-square map recovers the algebraic map.
Show proof
rflProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem quotientInfToRightCont_toMonoidHom :
(quotientInfToRightCont (G := G) U V).toMonoidHom = quotientInfToRight (G := G) U VForgetting continuity from the right continuous quotient-square map recovers the underlying algebraic map.
Show proof
rflProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem quotientToSupLeftCont_toMonoidHom :
(quotientToSupLeftCont (G := G) U V).toMonoidHom = quotientToSupLeft (G := G) U VForgetting continuity from the lower-left continuous quotient-square map recovers the algebraic map.
Show proof
rflProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem quotientToSupRightCont_toMonoidHom :
(quotientToSupRightCont (G := G) U V).toMonoidHom = quotientToSupRight (G := G) U VForgetting continuity from the lower-right continuous quotient-square map recovers the algebraic map.
Show proof
rflProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem quotientInfToLeftCont_mk (g : G) :
quotientInfToLeftCont (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk gEvaluation of the left continuous quotient-square map on a quotient class.
Show proof
by
simp only [quotientInfToLeftCont, quotientMapOfLECont_mk]Proof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem quotientInfToRightCont_mk (g : G) :
quotientInfToRightCont (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk gEvaluation of the right continuous quotient-square map on a quotient class.
Show proof
by
simp only [quotientInfToRightCont, quotientMapOfLECont_mk]Proof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem quotientToSupLeftCont_mk (g : G) :
quotientToSupLeftCont (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk gEvaluation of the lower-left continuous quotient-square map on a quotient class.
Show proof
by
simp only [quotientToSupLeftCont, quotientMapOfLECont_mk]Proof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem quotientToSupRightCont_mk (g : G) :
quotientToSupRightCont (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk gEvaluation of the lower-right continuous quotient-square map on a quotient class.
Show proof
by
simp only [quotientToSupRightCont, quotientMapOfLECont_mk]Proof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□def quotientInfToContinuousPullback :
G ⧸ (U ⊓ V) →ₜ*
TopologicalFiberProduct.carrier (quotientToSupLeftCont (G := G) U V) (quotientToSupRightCont (G := G) U V) := by
refine TopologicalFiberProduct.lift
(quotientToSupLeftCont (G := G) U V)
(quotientToSupRightCont (G := G) U V)
(quotientInfToLeftCont (G := G) U V)
(quotientInfToRightCont (G := G) U V) ?_
intro x
refine Quotient.inductionOn x ?_
intro g
rflThe canonical continuous map from \(G/(U \cap V)\) to the concrete continuous pullback of \(G/U\) and \(G/V\) over \(G/(UV)\).
@[simp] theorem quotientInfToContinuousPullback_toMonoidHom :
(quotientInfToContinuousPullback (G := G) U V).toMonoidHom =
quotientInfToPullback (G := G) U VForgetting continuity from the continuous quotient-to-pullback map recovers the algebraic one.
Show proof
by
apply MonoidHom.ext
intro x
refine Quotient.inductionOn' x ?_
intro g
exact Subtype.ext <| Prod.ext rfl rflProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem quotientInfToContinuousPullback_mk (g : G) :
quotientInfToContinuousPullback (G := G) U V (QuotientGroup.mk g) =
⟨(QuotientGroup.mk g, QuotientGroup.mk g), rfl⟩The quotient-to-continuous-pullback map sends a coset to the corresponding continuous pullback pair.
Show proof
by
rflProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem pullbackFstCont_quotientInfToContinuousPullback :
(TopologicalFiberProduct.fst _ _).comp (quotientInfToContinuousPullback (G := G) U V) =
quotientInfToLeftCont (G := G) U VThe first projection of the continuous quotient-to-pullback map is the natural quotient map to \(G/U\).
Show proof
by
apply ContinuousMonoidHom.ext
intro x
refine Quotient.inductionOn' x ?_
intro g
rflProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem pullbackSndCont_quotientInfToContinuousPullback :
(TopologicalFiberProduct.snd _ _).comp (quotientInfToContinuousPullback (G := G) U V) =
quotientInfToRightCont (G := G) U VThe second projection of the continuous quotient-to-pullback map is the natural quotient map to \(G/V\).
Show proof
by
apply ContinuousMonoidHom.ext
intro x
refine Quotient.inductionOn' x ?_
intro g
rflProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□theorem quotientInfToContinuousPullback_injective :
Function.Injective (quotientInfToContinuousPullback (G := G) U V)Injectivity of the continuous quotient-to-pullback map on the underlying groups.
Show proof
by
intro x y hxy
exact quotientInfToPullback_injective (G := G) U V <| by
simpa using hxyProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□theorem quotientInfToContinuousPullback_surjective :
Function.Surjective (quotientInfToContinuousPullback (G := G) U V)Surjectivity of the continuous quotient-to-pullback map on the underlying groups.
Show proof
by
intro x
rcases quotientInfToPullback_surjective (G := G) U V x with ⟨y, hy⟩
refine ⟨y, ?_⟩
simpa using hyProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□theorem quotientInfToContinuousPullback_bijective :
Function.Bijective (quotientInfToContinuousPullback (G := G) U V)The continuous quotient-to-pullback map is bijective on the underlying groups.
Show proof
by
exact ⟨quotientInfToContinuousPullback_injective (G := G) U V,
quotientInfToContinuousPullback_surjective (G := G) U V⟩Proof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□noncomputable def quotientInfContinuousPullbackEquiv
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
(hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
G ⧸ (U ⊓ V) ≃ₜ*
TopologicalFiberProduct.carrier (quotientToSupLeftCont (G := G) U V) (quotientToSupRightCont (G := G) U V) := by
let hG : IsProfiniteGroup G :=
⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
let hInfClosed : IsClosed (((U ⊓ V : Subgroup G) : Set G)) := hUclosed.inter hVclosed
let hSupClosed : IsClosed (((U ⊔ V : Subgroup G) : Set G)) :=
Subgroup.isClosed_sup_of_normal U V hUclosed hVclosed
let hQuotInf : IsProfiniteGroup (G ⧸ (U ⊓ V)) :=
ProCGroups.Generation.isProfinite_quotient_closedNormal (G := G) hG hInfClosed
let hQuotU : IsProfiniteGroup (G ⧸ U) :=
ProCGroups.Generation.isProfinite_quotient_closedNormal (G := G) hG hUclosed
let hQuotV : IsProfiniteGroup (G ⧸ V) :=
ProCGroups.Generation.isProfinite_quotient_closedNormal (G := G) hG hVclosed
let hQuotSup : IsProfiniteGroup (G ⧸ (U ⊔ V)) :=
ProCGroups.Generation.isProfinite_quotient_closedNormal (G := G) hG hSupClosed
let hPull :
IsProfiniteGroup
(TopologicalFiberProduct.carrier (quotientToSupLeftCont (G := G) U V) (quotientToSupRightCont (G := G) U V)) :=
TopologicalFiberProduct.isProfiniteGroup
(quotientToSupLeftCont (G := G) U V)
(quotientToSupRightCont (G := G) U V)
hQuotU hQuotV hQuotSup
letI : CompactSpace (G ⧸ (U ⊓ V)) := IsProfiniteGroup.compactSpace hQuotInf
letI : T2Space
(TopologicalFiberProduct.carrier (quotientToSupLeftCont (G := G) U V) (quotientToSupRightCont (G := G) U V)) :=
IsProfiniteGroup.t2Space hPull
exact ContinuousMulEquiv.ofBijectiveCompactToT2
(quotientInfToContinuousPullback (G := G) U V)
(quotientInfToContinuousPullback (G := G) U V).continuous_toFun
(quotientInfToContinuousPullback_bijective (G := G) U V)The quotient square is canonically isomorphic to the concrete profinite pullback.
@[simp] theorem quotientInfContinuousPullbackEquiv_toContinuousMonoidHom
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
(hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
(quotientInfContinuousPullbackEquiv
(G := G) (U := U) (V := V) hUclosed hVclosed).toContinuousMonoidHom =
quotientInfToContinuousPullback (G := G) U VThe quotient pullback equivalence is induced by the canonical comparison map.
Show proof
by
apply ContinuousMonoidHom.ext
intro x
exact Subtype.ext <| Prod.ext rfl rflProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem quotientInfContinuousPullbackEquiv_mk
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
(hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) (g : G) :
quotientInfContinuousPullbackEquiv (G := G) (U := U) (V := V) hUclosed hVclosed
(QuotientGroup.mk g) = ⟨(QuotientGroup.mk g, QuotientGroup.mk g), rfl⟩The continuous pullback equivalence sends a quotient coset to the corresponding pullback pair.
Show proof
by
change quotientInfToContinuousPullback (G := G) U V (QuotientGroup.mk g) = _
exact quotientInfToContinuousPullback_mk (G := G) U V gProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem quotientInfContinuousPullbackEquiv_fst
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
(hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
(TopologicalFiberProduct.fst _ _).comp
(quotientInfContinuousPullbackEquiv
(G := G) (U := U) (V := V) hUclosed hVclosed).toContinuousMonoidHom =
quotientInfToLeftCont (G := G) U VThe first coordinate of the continuous quotient pullback equivalence is the natural map to \(G/U\).
Show proof
by
rw [quotientInfContinuousPullbackEquiv_toContinuousMonoidHom
(G := G) (U := U) (V := V) hUclosed hVclosed]
exact pullbackFstCont_quotientInfToContinuousPullback (G := G) U VProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem quotientInfContinuousPullbackEquiv_snd
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
(hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
(TopologicalFiberProduct.snd _ _).comp
(quotientInfContinuousPullbackEquiv
(G := G) (U := U) (V := V) hUclosed hVclosed).toContinuousMonoidHom =
quotientInfToRightCont (G := G) U VThe second coordinate of the continuous quotient pullback equivalence is the natural map to \(G/V\).
Show proof
by
rw [quotientInfContinuousPullbackEquiv_toContinuousMonoidHom
(G := G) (U := U) (V := V) hUclosed hVclosed]
exact pullbackSndCont_quotientInfToContinuousPullback (G := G) U VProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□theorem quotientInf_hasProfiniteTestPullbackProperty
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
(hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
HasProfiniteTestPullbackProperty
(quotientInfToLeftCont (G := G) U V)
(quotientInfToRightCont (G := G) U V)
(quotientToSupLeftCont (G := G) U V)
(quotientToSupRightCont (G := G) U V)The quotient square is a pullback square in the category of profinite groups.
Show proof
by
exact hasProfiniteTestPullbackProperty_of_equiv_toConcretePullback
(quotientInfToLeftCont (G := G) U V)
(quotientInfToRightCont (G := G) U V)
(quotientToSupLeftCont (G := G) U V)
(quotientToSupRightCont (G := G) U V)
(quotientInfContinuousPullbackEquiv (G := G) (U := U) (V := V) hUclosed hVclosed)
(quotientInfContinuousPullbackEquiv_fst (G := G) (U := U) (V := V) hUclosed hVclosed)
(quotientInfContinuousPullbackEquiv_snd (G := G) (U := U) (V := V) hUclosed hVclosed)Proof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem infToLeft_mk (g : G) :
quotientInfToLeft (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk gThe map from the infimum quotient to the left quotient sends a coset to its left coordinate.
Show proof
rflProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem infToRight_mk (g : G) :
quotientInfToRight (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk gThe map from the infimum quotient to the right quotient sends a coset to its right coordinate.
Show proof
rflProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem leftToSup_mk (g : G) :
quotientToSupLeft (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk gThe map from the left quotient to the supremum quotient sends a coset to its image in the larger quotient.
Show proof
rflProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem rightToSup_mk (g : G) :
quotientToSupRight (G := G) U V (QuotientGroup.mk g) = QuotientGroup.mk gThe map from the right quotient to the supremum quotient sends a coset to its image in the larger quotient.
Show proof
rflProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□@[simp] theorem comparison_apply_mk (g : G) :
quotientInfToPullback (G := G) U V (QuotientGroup.mk g) =
⟨(QuotientGroup.mk g, QuotientGroup.mk g), rfl⟩The pullback comparison map sends a quotient representative to the corresponding pullback pair.
Show proof
quotientInfToPullback_mk (G := G) U V gProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□theorem comparison_bijective :
Function.Bijective (quotientInfToPullback (G := G) U V)The quotient-pullback comparison map is bijective.
Show proof
quotientInfToPullback_bijective (G := G) U VProof. Unfold the corresponding finite-stage, relator-set, or comparison construction. The claim follows by reading off the defining projection, relator family, deletion/replacement data, or inclusion map and checking the stated compatibility field.
□theorem isPullback :
IsPullbackSquare
(quotientInfToLeft (G := G) U V)
(quotientInfToRight (G := G) U V)
(quotientToSupLeft (G := G) U V)
(quotientToSupRight (G := G) U V)Namespaced form of the algebraic quotient-pullback theorem.
Show proof
quotientInf_isPullback (G := G) (U := U) (V := V)Proof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□theorem hasProfiniteTestPullbackProperty
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
(hUclosed : IsClosed (U : Set G)) (hVclosed : IsClosed (V : Set G)) :
HasProfiniteTestPullbackProperty
(quotientInfToLeftCont (G := G) U V)
(quotientInfToRightCont (G := G) U V)
(quotientToSupLeftCont (G := G) U V)
(quotientToSupRightCont (G := G) U V)A topological pullback square has the restricted profinite-source test property.
Show proof
quotientInf_hasProfiniteTestPullbackProperty (G := G) (U := U) (V := V) hUclosed hVclosedProof. Unfold the topological fiber product as the closed subspace of the product cut out by equality of the two continuous maps. The coordinate projections are continuous, the universal map into the fiber product is continuous because its product map is continuous and its image satisfies the pullback equation, and uniqueness follows from coordinate extensionality. Profinite and closedness claims follow from closed subspaces of compact Hausdorff profinite products.
□