ProCGroups.Topologies.QuotientMaps
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
- Mathlib.Topology.Algebra.Group.Quotient
- ProCGroups.Topologies.ContinuousMulEquiv
theorem comap_eq_of_map_eq_of_ker_le
(f : G →* H) {N : Subgroup G} {M : Subgroup H}
(hmap : N.map f = M) (hker : f.ker ≤ N) :
M.comap f = NThe comap of a quotient subgroup is determined by the representative-level map when the kernel condition holds.
Show proof
by
calc
M.comap f = (N.map f).comap f := by simp only [hmap]
_ = N ⊔ f.ker := by simpa using (Subgroup.comap_map_eq (f := f) (H := N))
_ = N := sup_eq_left.2 hkerProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□private theorem map_ker_eq_bot_of_map_eq_of_ker_le
(f : G →* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
(hNM : N ≤ M.comap f) (hmap : N.map f = M) (hker : f.ker ≤ N) :
(QuotientGroup.map (N := N) (M := M) (f := f) hNM).ker = ⊥Under the kernel condition, the induced quotient map has trivial kernel for the corresponding representative-level map.
Show proof
by
have hcomap : M.comap f = N := comap_eq_of_map_eq_of_ker_le f hmap hker
calc
(QuotientGroup.map (N := N) (M := M) (f := f) hNM).ker =
Subgroup.map (QuotientGroup.mk' N) (Subgroup.comap f M) := by
simpa using QuotientGroup.ker_map (N := N) (M := M) (f := f) hNM
_ = Subgroup.map (QuotientGroup.mk' N) N := by simp only [hcomap, map_mk'_self]
_ = ⊥ := by
refine (Subgroup.map_eq_bot_iff (f := QuotientGroup.mk' N) (H := N)).2 ?_
intro x hx
simpa using hxProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□noncomputable def mapMulEquivOfSurjective
(f : G →* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
(hf : Function.Surjective f) (hmap : N.map f = M) (hker : f.ker ≤ N) :
G ⧸ N ≃* H ⧸ M := by
have hNM : N ≤ M.comap f := by
intro x hx
change f x ∈ M
simpa [hmap] using (show f x ∈ N.map f from ⟨x, hx, rfl⟩)
let φ : G ⧸ N →* H ⧸ M :=
QuotientGroup.map (N := N) (M := M) (f := f) hNM
have hsurj : Function.Surjective φ := by
intro y
obtain ⟨h, rfl⟩ := QuotientGroup.mk'_surjective M y
rcases hf h with ⟨g, rfl⟩
exact ⟨QuotientGroup.mk' N g, rfl⟩
have hkerφ : φ.ker = ⊥ := by
dsimp [φ]
exact map_ker_eq_bot_of_map_eq_of_ker_le (f := f) hNM hmap hker
have hinj : Function.Injective φ :=
(MonoidHom.ker_eq_bot_iff (f := φ)).1 hkerφ
exact MulEquiv.ofBijective φ ⟨hinj, hsurj⟩A surjective homomorphism induces an isomorphism on quotients whenever it maps the source normal subgroup onto the target normal subgroup and its kernel is contained in the source normal subgroup. This is the algebraic core behind the usual snake-lemma argument for quotient diagrams.
@[simp] theorem mapMulEquivOfSurjective_apply_mk
(f : G →* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
(hf : Function.Surjective f) (hmap : N.map f = M) (hker : f.ker ≤ N) (g : G) :
mapMulEquivOfSurjective (G := G) (H := H) f hf hmap hker (QuotientGroup.mk' N g) =
QuotientGroup.mk' M (f g)A surjective homomorphism induces the expected multiplicative equivalence on quotient groups.
Show proof
by
rflProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□def liftₜ
(N : Subgroup G) [N.Normal] (f : G →ₜ* H)
(hN : N ≤ f.toMonoidHom.ker) :
G ⧸ N →ₜ* H := by
let φ : G ⧸ N →* H := QuotientGroup.lift N f.toMonoidHom hN
have hcomp : Continuous (fun x : G => φ (QuotientGroup.mk' N x)) := by
simpa [φ, QuotientGroup.lift_mk'] using f.continuous_toFun
have hcont : Continuous φ :=
(QuotientGroup.isQuotientMap_mk (G := G) (N := N)).continuous_iff.2 hcomp
exact
{ toMonoidHom := φ
continuous_toFun := hcont }The lifted continuous quotient map is induced by the quotient universal property.
def mapContinuousMonoidHom
(f : G →ₜ* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
(hNM : N ≤ M.comap f.toMonoidHom) :
G ⧸ N →ₜ* H ⧸ M := by
let φ : G ⧸ N →* H ⧸ M :=
QuotientGroup.map (N := N) (M := M) (f := f.toMonoidHom) hNM
have hcomp : Continuous (fun x : G => φ (QuotientGroup.mk' N x)) := by
dsimp [φ]
exact continuous_quotient_mk'.comp f.continuous_toFun
have hcont : Continuous φ :=
(QuotientGroup.isQuotientMap_mk (G := G) (N := N)).continuous_iff.2 hcomp
exact
{ toMonoidHom := φ
continuous_toFun := hcont }The continuous homomorphism induced on quotients by a continuous homomorphism.
def mapₜ
(N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
(f : G →ₜ* H) (hNM : N ≤ M.comap f.toMonoidHom) :
G ⧸ N →ₜ* H ⧸ M :=
mapContinuousMonoidHom (G := G) (H := H) f (N := N) (M := M) hNMContinuous version of the quotient-group map.
noncomputable def congrₜ
(N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
(e : G ≃ₜ* H) (h : N.map e.toMulEquiv.toMonoidHom = M) :
G ⧸ N ≃ₜ* H ⧸ M := by
let eAlg : G ⧸ N ≃* H ⧸ M :=
QuotientGroup.congr (G' := N) (H' := M) e.toMulEquiv h
refine
{ toMulEquiv := eAlg
continuous_toFun := ?_
continuous_invFun := ?_ }
· refine (QuotientGroup.isQuotientMap_mk N).continuous_iff.2 ?_
change Continuous fun x : G => eAlg (QuotientGroup.mk' N x)
simpa [eAlg, QuotientGroup.congr_mk'] using
(continuous_quotient_mk'.comp e.continuous_toFun)
· refine (QuotientGroup.isQuotientMap_mk M).continuous_iff.2 ?_
change Continuous fun y : H => eAlg.symm (QuotientGroup.mk' M y)
have hsymm : M.map e.symm.toMulEquiv.toMonoidHom = N :=
(Subgroup.map_symm_eq_iff_map_eq (K := N) (H := M) (e := e.toMulEquiv)).mpr h
simpa [eAlg, hsymm, QuotientGroup.congr_symm, QuotientGroup.congr_mk'] using
(continuous_quotient_mk'.comp e.symm.continuous_toFun)Continuous equivalence between quotients induced by a continuous multiplicative equivalence.
noncomputable def mapContinuousMulEquivOfSurjective
(f : G →ₜ* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
[CompactSpace (G ⧸ N)] [T2Space (H ⧸ M)]
(hf : Function.Surjective f) (hmap : N.map f.toMonoidHom = M)
(hker : f.toMonoidHom.ker ≤ N) :
G ⧸ N ≃ₜ* H ⧸ M := by
have hNM : N ≤ M.comap f.toMonoidHom := by
intro x hx
change f x ∈ M
rw [← hmap]
exact ⟨x, hx, rfl⟩
let φ := mapContinuousMonoidHom (G := G) (H := H) f (N := N) (M := M) hNM
have hsurj : Function.Surjective φ := by
intro y
obtain ⟨h, rfl⟩ := QuotientGroup.mk'_surjective M y
rcases hf h with ⟨g, rfl⟩
exact ⟨QuotientGroup.mk' N g, rfl⟩
have hkerφ : φ.toMonoidHom.ker = ⊥ := by
dsimp [φ, mapContinuousMonoidHom]
exact map_ker_eq_bot_of_map_eq_of_ker_le (f := f.toMonoidHom) hNM hmap hker
have hinj : Function.Injective φ :=
(MonoidHom.ker_eq_bot_iff (f := φ.toMonoidHom)).1 hkerφ
exact ContinuousMulEquiv.ofBijectiveCompactToT2
φ.toMonoidHom φ.continuous_toFun ⟨hinj, hsurj⟩Continuous version of the quotient-group multiplicative equivalence induced by a surjective map. The inverse is continuous by compact-to-Hausdorff automatic continuity, so the result is a topological-group isomorphism when the source quotient is compact and the target quotient is Hausdorff.
@[simp] theorem liftₜ_apply_mk
(N : Subgroup G) [N.Normal] (f : G →ₜ* H)
(hN : N ≤ f.toMonoidHom.ker) (g : G) :
liftₜ (G := G) (H := H) N f hN (QuotientGroup.mk' N g) = f gThe lifted continuous quotient map evaluates on quotient classes by applying the underlying map to representatives.
Show proof
by
rflProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□@[simp] theorem liftₜ_toMonoidHom
(N : Subgroup G) [N.Normal] (f : G →ₜ* H)
(hN : N ≤ f.toMonoidHom.ker) :
(liftₜ (G := G) (H := H) N f hN).toMonoidHom =
QuotientGroup.lift N f.toMonoidHom hNThe induced pro-\(C\) map agrees with the corresponding finite-quotient construction.
Show proof
by
rflProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□@[simp] theorem mapContinuousMonoidHom_apply_mk
(f : G →ₜ* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
(hNM : N ≤ M.comap f.toMonoidHom) (g : G) :
mapContinuousMonoidHom (G := G) (H := H) f (N := N) (M := M) hNM
(QuotientGroup.mk' N g) =
QuotientGroup.mk' M (f g)The induced continuous monoid homomorphism sends a quotient class to the class of its image.
Show proof
by
rflProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□@[simp] theorem mapₜ_apply_mk
(N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
(f : G →ₜ* H) (hNM : N ≤ M.comap f.toMonoidHom) (g : G) :
mapₜ (G := G) (H := H) N M f hNM (QuotientGroup.mk' N g) =
QuotientGroup.mk' M (f g)The induced pro-\(C\) map agrees with the corresponding finite-quotient construction.
Show proof
by
rflProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□@[simp] theorem mapₜ_toMonoidHom
(N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
(f : G →ₜ* H) (hNM : N ≤ M.comap f.toMonoidHom) :
(mapₜ (G := G) (H := H) N M f hNM).toMonoidHom =
QuotientGroup.map (N := N) (M := M) (f := f.toMonoidHom) hNMThe induced pro-\(C\) map agrees with the corresponding finite-quotient construction.
Show proof
by
rflProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□@[simp] theorem congrₜ_apply_mk
(N : Subgroup G) (M : Subgroup H) [N.Normal] [M.Normal]
(e : G ≃ₜ* H) (h : N.map e.toMulEquiv.toMonoidHom = M) (g : G) :
congrₜ (G := G) (H := H) N M e h (QuotientGroup.mk' N g) =
QuotientGroup.mk' M (e g)The continuous quotient congruence map evaluates on quotient classes by applying the underlying map to representatives.
Show proof
by
rflProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□@[simp 900] theorem mapContinuousMulEquivOfSurjective_apply_mk
(f : G →ₜ* H) {N : Subgroup G} {M : Subgroup H} [N.Normal] [M.Normal]
[CompactSpace (G ⧸ N)] [T2Space (H ⧸ M)]
(hf : Function.Surjective f) (hmap : N.map f.toMonoidHom = M)
(hker : f.toMonoidHom.ker ≤ N) (g : G) :
mapContinuousMulEquivOfSurjective (G := G) (H := H) f hf hmap hker
(QuotientGroup.mk' N g) =
QuotientGroup.mk' M (f g)The induced continuous multiplicative equivalence sends a quotient class to the class of its image.
Show proof
by
rflProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage.
□def restrictPreimage (f : G →ₜ* Q) (H : Subgroup Q) :
(H.comap f.toMonoidHom) →ₜ* H := by
refine
{ toMonoidHom :=
{ toFun := fun x => ⟨f x.1, x.2⟩
map_one' := by
ext
simp only [coe_toMonoidHom, OneMemClass.coe_one, map_one]
map_mul' := by
intro x y
ext
simp only [coe_toMonoidHom, Subgroup.coe_mul, map_mul]}
continuous_toFun := by
have hcont : Continuous (fun x : H.comap f.toMonoidHom => f x.1) :=
f.continuous.comp continuous_subtype_val
exact hcont.subtype_mk (by intro x; exact x.2) }A continuous homomorphism restricts to the preimage of a subgroup of the target.
theorem restrictPreimage_surjective (f : G →ₜ* Q) (hf : Function.Surjective f)
(H : Subgroup Q) :
Function.Surjective (f.restrictPreimage H)The restriction to a subgroup preimage is surjective if the original map is surjective.
Show proof
by
intro y
rcases hf y.1 with ⟨x, hx⟩
refine ⟨⟨x, ?_⟩, ?_⟩
· change f x ∈ H
simp only [hx, SetLike.coe_mem]
· exact Subtype.ext hxProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem restrictPreimage_eq_one_iff (f : G →ₜ* Q) (H : Subgroup Q)
(x : H.comap f.toMonoidHom) :
f.restrictPreimage H x = 1 ↔ f x.1 = 1The kernel of the restriction to a subgroup preimage is detected by the ambient map.
Show proof
by
constructor
· intro hx
exact congrArg Subtype.val hx
· intro hx
exact Subtype.ext hxProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□noncomputable def preimageSubgroupQuotientMulEquivOfSurjective
(f : G →ₜ* Q) (hf : Function.Surjective f) (H : Subgroup Q)
{N : Subgroup (H.comap f.toMonoidHom)} {M : Subgroup H} [N.Normal] [M.Normal]
(hmap : N.map (f.restrictPreimage H).toMonoidHom = M)
(hker : (f.restrictPreimage H).toMonoidHom.ker ≤ N) :
(H.comap f.toMonoidHom) ⧸ N ≃* H ⧸ M :=
QuotientGroup.mapMulEquivOfSurjective
(f.restrictPreimage H).toMonoidHom
(f.restrictPreimage_surjective hf H) hmap hkerNon-\(m\)-step quotient comparison for a subgroup preimage. This is the reusable form of the standard diagram/snake-lemma argument: if the restricted map sends N onto M and its kernel is absorbed by N, then the induced quotient map is an isomorphism.