ProCGroups.Topologies.ContinuousMulEquiv
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.GroupTheory.QuotientGroup.Basic
- Mathlib.Topology.Algebra.ContinuousMonoidHom
- ProCGroups.Topologies.ContinuousMonoidHom
def toContinuousMonoidHom (e : G ≃ₜ* H) : G →ₜ* H :=
{ toMonoidHom := e.toMulEquiv.toMonoidHom
continuous_toFun := e.continuous_toFun }The forward continuous homomorphism on inverse limits induced by a stagewise isomorphism.
@[simp] theorem toContinuousMonoidHom_apply (e : G ≃ₜ* H) (g : G) :
e.toContinuousMonoidHom g = e gThe continuous equivalence is evaluated by the corresponding comparison formula.
Show proof
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. 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. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums.
□noncomputable def ofHomInv
(f : G →ₜ* H) (g : H →ₜ* G)
(hleft : Function.LeftInverse g f)
(hright : Function.RightInverse g f) :
G ≃ₜ* H :=
{ toMulEquiv :=
{ toFun := f
invFun := g
left_inv := hleft
right_inv := hright
map_mul' := f.map_mul }
continuous_toFun := f.continuous_toFun
continuous_invFun := g.continuous_toFun }Build a continuous multiplicative equivalence from inverse continuous homomorphisms.
@[simp] theorem ofHomInv_apply
(f : G →ₜ* H) (g : H →ₜ* G)
(hleft : Function.LeftInverse g f)
(hright : Function.RightInverse g f) (x : G) :
ofHomInv f g hleft hright x = f xThe continuous equivalence is evaluated by the corresponding comparison formula.
Show proof
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.
□noncomputable def ofBijectiveCompactToT2
{G : Type u} {H : Type v}
[Group G] [TopologicalSpace G]
[Group H] [TopologicalSpace H]
[CompactSpace G] [T2Space H]
(φ : G →* H) (hφcont : Continuous φ)
(hφ : Function.Bijective φ) :
G ≃ₜ* H := by
let e : G ≃ H := Equiv.ofBijective φ hφ
let eh : G ≃ₜ H :=
e.toHomeomorphOfContinuousClosed hφcont (Continuous.isClosedMap hφcont)
exact ContinuousMulEquiv.mk' eh (by
intro x y
exact φ.map_mul x y)Upgrade a bijective continuous homomorphism from a compact topological group to a Hausdorff topological group to a continuous multiplicative equivalence.
@[simp 900] theorem ofBijectiveCompactToT2_apply
{G : Type u} {H : Type v}
[Group G] [TopologicalSpace G]
[Group H] [TopologicalSpace H]
[CompactSpace G] [T2Space H]
(φ : G →* H) (hφcont : Continuous φ)
(hφ : Function.Bijective φ) (x : G) :
ofBijectiveCompactToT2 φ hφcont hφ x = φ xThe composite map is computed pointwise by applying the constituent coordinate formulas in succession.
Show proof
by
unfold ofBijectiveCompactToT2
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. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums.
□noncomputable def quotientKerContinuousMulEquivRange
{G : Type u} {H : Type v}
[Group G] [TopologicalSpace G] [CompactSpace G]
[Group H] [TopologicalSpace H] [T2Space H]
(f : G →ₜ* H) :
(G ⧸ (f.toMonoidHom.ker : Subgroup G)) ≃ₜ* f.toMonoidHom.range := by
let φ : (G ⧸ (f.toMonoidHom.ker : Subgroup G)) →* f.toMonoidHom.range :=
(QuotientGroup.quotientKerEquivRange f.toMonoidHom).toMonoidHom
have hφcont : Continuous φ := by
refine (QuotientGroup.isQuotientMap_mk f.toMonoidHom.ker).continuous_iff.2 ?_
simpa [φ, ContinuousMonoidHom.rangeRestrict] using f.rangeRestrict.continuous_toFun
exact ContinuousMulEquiv.ofBijectiveCompactToT2 φ hφcont
(QuotientGroup.quotientKerEquivRange f.toMonoidHom).bijectiveThe first isomorphism theorem for continuous monoid homomorphisms from a compact group to a Hausdorff group, with the quotient and range carrying their induced topologies.
@[simp] theorem quotientKerContinuousMulEquivRange_mk
{G : Type u} {H : Type v}
[Group G] [TopologicalSpace G] [CompactSpace G]
[Group H] [TopologicalSpace H] [T2Space H]
(f : G →ₜ* H) (g : G) :
quotientKerContinuousMulEquivRange f
(QuotientGroup.mk' (f.toMonoidHom.ker : Subgroup G) g) =
f.toMonoidHom.rangeRestrict gThe quotient-by-kernel equivalence to the range sends a representative to its image.
Show proof
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. 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.
□@[simp] theorem coe_quotientKerContinuousMulEquivRange_mk
{G : Type u} {H : Type v}
[Group G] [TopologicalSpace G] [CompactSpace G]
[Group H] [TopologicalSpace H] [T2Space H]
(f : G →ₜ* H) (g : G) :
(quotientKerContinuousMulEquivRange f
(QuotientGroup.mk' (f.toMonoidHom.ker : Subgroup G) g) : H) = f gCoercing the quotient-by-kernel equivalence to the codomain gives the original homomorphism value.
Show proof
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. 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.
□