ProCGroups.Topologies.TopologicallyCharacteristicSubgroups
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.
import
- Mathlib.Topology.Algebra.ContinuousMonoidHom
- Mathlib.Topology.Algebra.Group.Quotient
- Mathlib.GroupTheory.Commutator.Basic
- ProCGroups.Topologies.QuotientMaps
Imported by
- ProCGroups.Abelian.TopologicalAbelianization
- ProCGroups.FiniteStepSolvableQuotients.Commutators.DerivedSeriesAndQuotients
- ProCGroups.FreeProC.Criteria.InverseLimitsAndFiniteSubsets
- ProCGroups.Presentations.Profinite
- ProCGroups.Topologies
- ProCGroups.Topologies.Conjugation
- ReidemeisterSchreier.Profinite.OpenSubgroups.BasisTheorems
lemma image_subtype_eq_map
{G : Type u} [Group G]
{H : Type _} [Group H]
(f : G →* H) (K : Subgroup G) :
(fun x : G => f x) '' (K : Set G) = ((K.map f : Subgroup H) : Set H)Identify the image of a subgroup with its Subgroup.map.
Show proof
by
ext y
constructor
· rintro ⟨x, hx, rfl⟩
exact ⟨x, hx, rfl⟩
· rintro ⟨x, hx, rfl⟩
exact ⟨x, hx, rfl⟩Proof. 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. 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.
□lemma map_symm_toMonoidHom_eq_comap
{G : Type u} [Group G] (K : Subgroup G) (e : G ≃* G) :
K.map e.symm.toMonoidHom = K.comap e.toMonoidHomMapping a subgroup by the inverse of an automorphism agrees with comapping along the automorphism itself.
Show proof
by
ext x
constructor
· rintro ⟨y, hy, rfl⟩
change e (e.symm y) ∈ K
simpa using hy
· intro hx
have hx' : e x ∈ K := by
simpa [Subgroup.mem_comap] using hx
exact ⟨e x, hx', by simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, MulEquiv.symm_apply_apply]⟩Proof. 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.
□theorem map_topologicalClosure_le_of_map_le
{G H : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
[TopologicalSpace H] [Group H] [IsTopologicalGroup H]
{A : Subgroup G} {B : Subgroup H} {f : G →* H}
(hf : Continuous f) (hAB : A.map f ≤ B) (hB : IsClosed (B : Set H)) :
A.topologicalClosure.map f ≤ BContinuous maps send the topological closure of a subgroup into a closed subgroup whenever they send the subgroup itself into that closed subgroup.
Show proof
by
have hMapsTo : Set.MapsTo (fun x : G => f x) (A : Set G) (B : Set H) := by
intro x hx
exact hAB ⟨x, hx, rfl⟩
have hMapsTo_cl :
Set.MapsTo (fun x : G => f x) (_root_.closure (A : Set G)) (B : Set H) :=
Set.MapsTo.closure_left hMapsTo hf hB
rintro y ⟨x, hx, rfl⟩
exact hMapsTo_cl 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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.
□theorem map_topologicalClosure_eq_of_continuousMulEquiv
{G H : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
[TopologicalSpace H] [Group H] [IsTopologicalGroup H]
(e : G ≃ₜ* H) (A : Subgroup G) :
A.topologicalClosure.map e.toMulEquiv.toMonoidHom =
(A.map e.toMulEquiv.toMonoidHom).topologicalClosureHomeomorphic group equivalences commute with topological closure of subgroups.
Show proof
by
apply SetLike.coe_injective
calc
((A.topologicalClosure.map e.toMulEquiv.toMonoidHom : Subgroup H) : Set H) =
e.toHomeomorph '' ((A.topologicalClosure : Subgroup G) : Set G) := by
symm
exact TopologicalGroup.image_subtype_eq_map
(f := e.toMulEquiv.toMonoidHom) (K := A.topologicalClosure)
_ = e.toHomeomorph '' (_root_.closure ((A : Subgroup G) : Set G)) := by
rw [show ((A.topologicalClosure : Subgroup G) : Set G) =
_root_.closure ((A : Set G)) by
exact topologicalClosure_coe]
_ = _root_.closure (e.toHomeomorph '' ((A : Subgroup G) : Set G)) := by
exact e.toHomeomorph.image_closure ((A : Subgroup G) : Set G)
_ = _root_.closure (((A.map e.toMulEquiv.toMonoidHom : Subgroup H) : Set H)) := by
exact congrArg _root_.closure
(TopologicalGroup.image_subtype_eq_map
(f := e.toMulEquiv.toMonoidHom) (K := A))
_ = (((A.map e.toMulEquiv.toMonoidHom).topologicalClosure : Subgroup H) : Set H) := by
symm
exact topologicalClosure_coeProof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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.
□abbrev closedCommutator (G : Type*) [TopologicalSpace G] [Group G]
[IsTopologicalGroup G] : Subgroup G :=
(_root_.commutator G).topologicalClosureThe closed commutator subgroup of a topological group.
@[simp] theorem isClosed_closedCommutator
(G : Type*) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
IsClosed (closedCommutator G : Set G)The closed commutator subgroup is closed.
Show proof
isClosed_topologicalClosure (s := _root_.commutator G)Proof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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.
□theorem commutator_le_closedCommutator
(G : Type*) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
_root_.commutator G ≤ closedCommutator GThe abstract commutator subgroup is contained in the closed commutator subgroup.
Show proof
le_topologicalClosure (_root_.commutator G)Proof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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. 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 topologicalClosure_eq_self_of_discrete
(H : Subgroup G) [DiscreteTopology G] :
H.topologicalClosure = HIn a discrete topological group, the topological closure of a subgroup is the subgroup itself.
Show proof
by
apply SetLike.coe_injective
rw [topologicalClosure_coe, closure_discrete]Proof. 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.
□@[simp] theorem closedCommutator_eq_commutator_of_discrete
(G : Type*) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
[DiscreteTopology G] :
closedCommutator G = _root_.commutator GFor a discrete group, the closed commutator subgroup agrees with the ordinary commutator subgroup.
Show proof
by
simp only [closedCommutator, topologicalClosure_eq_self_of_discrete]Proof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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.
□theorem closedCommutator_map_le
{G H : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
[TopologicalSpace H] [Group H] [IsTopologicalGroup H]
(f : G →ₜ* H) :
(closedCommutator G).map f.toMonoidHom ≤ closedCommutator HContinuous homomorphisms send closed commutator subgroups into closed commutator subgroups.
Show proof
by
have hcomm : (_root_.commutator G).map f.toMonoidHom ≤ closedCommutator H := by
have hmap : (_root_.commutator G).map f.toMonoidHom ≤ _root_.commutator H := by
rw [_root_.map_commutator_eq]
exact Subgroup.commutator_mono le_top le_top
exact hmap.trans (commutator_le_closedCommutator H)
exact map_topologicalClosure_le_of_map_le
(f := f.toMonoidHom) f.continuous_toFun hcomm (isClosed_closedCommutator H)Proof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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.
□theorem closedCommutator_map_eq_of_equiv
{G H : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
[TopologicalSpace H] [Group H] [IsTopologicalGroup H]
(e : G ≃ₜ* H) :
(closedCommutator G).map e.toMulEquiv.toMonoidHom = closedCommutator HContinuous group equivalences map the closed commutator subgroup onto the closed commutator subgroup.
Show proof
by
apply le_antisymm
· exact closedCommutator_map_le
{ toMonoidHom := e.toMulEquiv.toMonoidHom
continuous_toFun := e.continuous_toFun }
· intro y hy
have hy' :
e.symm y ∈
(closedCommutator H).map e.symm.toMulEquiv.toMonoidHom := ⟨y, hy, rfl⟩
exact
⟨e.symm y,
closedCommutator_map_le
{ toMonoidHom := e.symm.toMulEquiv.toMonoidHom
continuous_toFun := e.symm.continuous_toFun } hy',
e.apply_symm_apply y⟩Proof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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.
□theorem closedCommutator_characteristic
{G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
∀ e : G ≃ₜ* G,
(closedCommutator G).map e.toMulEquiv.toMonoidHom = closedCommutator GThe closed commutator subgroup is invariant under continuous automorphisms.
Show proof
fun e => closedCommutator_map_eq_of_equiv eProof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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.
□structure TopologicallyCharacteristic
(H : Subgroup G) : Prop where
comap_eq : ∀ e : G ≃ₜ* G, H.comap e.toMulEquiv.toMonoidHom = HA subgroup is topologically characteristic if every continuous automorphism preserves it.
instance topologicallyCharacteristic_of_characteristic
[H.Characteristic] :
H.TopologicallyCharacteristic := by
refine ⟨?_⟩
intro e
simpa using
(Subgroup.characteristic_iff_comap_eq.mp (show H.Characteristic by infer_instance)
e.toMulEquiv)Every abstractly characteristic subgroup is invariant under continuous automorphisms.
theorem topologicallyCharacteristic_iff_comap_eq :
H.TopologicallyCharacteristic ↔
∀ e : G ≃ₜ* G, H.comap e.toMulEquiv.toMonoidHom = HTopological characteristicity is equivalent to invariance under comap by every continuous automorphism.
Show proof
⟨TopologicallyCharacteristic.comap_eq, TopologicallyCharacteristic.mk⟩Proof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem topologicallyCharacteristic_iff_comap_le :
H.TopologicallyCharacteristic ↔
∀ e : G ≃ₜ* G, H.comap e.toMulEquiv.toMonoidHom ≤ HA subgroup is topologically characteristic exactly when every automorphism comap is contained in it.
Show proof
topologicallyCharacteristic_iff_comap_eq.trans
⟨fun h e => le_of_eq (h e), fun h e =>
le_antisymm (h e) fun g hg =>
h e.symm ((congrArg (fun x => x ∈ H) (e.symm_apply_apply g)).mpr hg)⟩Proof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem topologicallyCharacteristic_iff_le_comap :
H.TopologicallyCharacteristic ↔
∀ e : G ≃ₜ* G, H ≤ H.comap e.toMulEquiv.toMonoidHomA subgroup is topologically characteristic exactly when it is contained in every automorphism comap.
Show proof
topologicallyCharacteristic_iff_comap_eq.trans
⟨fun h e => ge_of_eq (h e), fun h e =>
le_antisymm
(fun g hg =>
(congrArg (fun x => x ∈ H) (e.symm_apply_apply g)).mp (h e.symm hg))
(h e)⟩Proof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem topologicallyCharacteristic_iff_map_eq :
H.TopologicallyCharacteristic ↔
∀ e : G ≃ₜ* G, H.map e.toMulEquiv.toMonoidHom = HTopological characteristicity is equivalent to invariance under image by every continuous automorphism.
Show proof
by
simp_rw [map_equiv_eq_comap_symm']
exact topologicallyCharacteristic_iff_comap_eq.trans
⟨fun h e => h e.symm, fun h e => h e.symm⟩Proof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem closedCommutator_topologicallyCharacteristic
{G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
(closedCommutator G).TopologicallyCharacteristicThe closed commutator subgroup is topologically characteristic.
Show proof
by
rw [topologicallyCharacteristic_iff_map_eq]
exact closedCommutator_characteristicProof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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.
□theorem topologicallyCharacteristic_iff_le_map :
H.TopologicallyCharacteristic ↔
∀ e : G ≃ₜ* G, H ≤ H.map e.toMulEquiv.toMonoidHomA subgroup is topologically characteristic exactly when it is contained in every automorphism image.
Show proof
by
simp_rw [map_equiv_eq_comap_symm']
exact topologicallyCharacteristic_iff_le_comap.trans
⟨fun h e => h e.symm, fun h e => h e.symm⟩Proof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□lemma map_eq
(hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) :
H.map (e.toMulEquiv.toMonoidHom) = HA topologically characteristic subgroup is fixed by the image of every continuous automorphism.
Show proof
by
calc
H.map (e.toMulEquiv.toMonoidHom)
= H.comap (e.symm.toMulEquiv.toMonoidHom) := by
simpa using
TopologicalGroup.map_symm_toMonoidHom_eq_comap (K := H) (e := e.symm.toMulEquiv)
_ = H := hH.comap_eq e.symmProof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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. 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.
□lemma apply_mem_iff
(hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) {g : G} :
e g ∈ H ↔ g ∈ HMembership in a topologically characteristic subgroup is invariant under applying a continuous automorphism.
Show proof
by
change g ∈ H.comap e.toMulEquiv.toMonoidHom ↔ g ∈ H
rw [hH.comap_eq e]Proof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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.
□theorem inf
(hH : H.TopologicallyCharacteristic) (hK : K.TopologicallyCharacteristic) :
(H ⊓ K).TopologicallyCharacteristicIntersections of topologically characteristic subgroups are topologically characteristic.
Show proof
by
rw [topologicallyCharacteristic_iff_comap_eq]
intro e
calc
(H ⊓ K).comap e.toMulEquiv.toMonoidHom =
H.comap e.toMulEquiv.toMonoidHom ⊓ K.comap e.toMulEquiv.toMonoidHom := by
simpa using Subgroup.comap_inf H K e.toMulEquiv.toMonoidHom
_ = H ⊓ K := by rw [hH.comap_eq e, hK.comap_eq e]Proof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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.
□theorem sup
(hH : H.TopologicallyCharacteristic) (hK : K.TopologicallyCharacteristic) :
(H ⊔ K).TopologicallyCharacteristicSupremums of topologically characteristic subgroups are topologically characteristic.
Show proof
by
rw [topologicallyCharacteristic_iff_map_eq]
intro e
calc
(H ⊔ K).map e.toMulEquiv.toMonoidHom = H.map e.toMulEquiv.toMonoidHom ⊔
K.map e.toMulEquiv.toMonoidHom := by
simpa using Subgroup.map_sup H K e.toMulEquiv.toMonoidHom
_ = H ⊔ K := by rw [map_eq hH e, map_eq hK e]Proof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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.
□theorem sInf
{S : Set (Subgroup G)}
(hS : ∀ L ∈ S, L.TopologicallyCharacteristic) :
(sInf S).TopologicallyCharacteristicArbitrary intersections of topologically characteristic subgroups are topologically characteristic.
Show proof
by
rw [topologicallyCharacteristic_iff_comap_eq]
intro e
ext g
rw [Subgroup.mem_comap, Subgroup.mem_sInf, Subgroup.mem_sInf]
constructor
· intro hg L hL
exact (apply_mem_iff (hS L hL) e (g := g)).1 (hg L hL)
· intro hg L hL
exact (apply_mem_iff (hS L hL) e (g := g)).2 (hg L hL)Proof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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.
□theorem iInf
{ι : Sort*} {S : ι → Subgroup G}
(hS : ∀ i, (S i).TopologicallyCharacteristic) :
(⨅ i, S i).TopologicallyCharacteristicIndexed intersections of topologically characteristic subgroups are topologically characteristic.
Show proof
by
rw [topologicallyCharacteristic_iff_comap_eq]
intro e
ext g
rw [Subgroup.mem_comap, Subgroup.mem_iInf, Subgroup.mem_iInf]
constructor
· intro hg i
exact (apply_mem_iff (hS i) e (g := g)).1 (hg i)
· intro hg i
exact (apply_mem_iff (hS i) e (g := g)).2 (hg i)Proof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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.
□theorem iSup
{ι : Sort*} {S : ι → Subgroup G}
(hS : ∀ i, (S i).TopologicallyCharacteristic) :
(⨆ i, S i).TopologicallyCharacteristicIndexed supremums of topologically characteristic subgroups are topologically characteristic.
Show proof
by
rw [topologicallyCharacteristic_iff_map_eq]
intro e
calc
(⨆ i, S i).map e.toMulEquiv.toMonoidHom = ⨆ i, (S i).map e.toMulEquiv.toMonoidHom := by
simpa using Subgroup.map_iSup e.toMulEquiv.toMonoidHom S
_ = ⨆ i, S i := by
simpa using iSup_congr (fun i => map_eq (hS i) e)Proof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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.
□theorem topologicalClosure
(hH : H.TopologicallyCharacteristic) :
H.topologicalClosure.TopologicallyCharacteristicThe topological closure of a topologically characteristic subgroup is topologically characteristic.
Show proof
by
rw [topologicallyCharacteristic_iff_map_eq]
intro e
apply SetLike.coe_injective
calc
(((H.topologicalClosure).map e.toMulEquiv.toMonoidHom : Subgroup G) : Set G) =
e.toHomeomorph '' ((H.topologicalClosure : Subgroup G) : Set G) := by
symm
exact TopologicalGroup.image_subtype_eq_map
(f := e.toMulEquiv.toMonoidHom) (K := H.topologicalClosure)
_ = e.toHomeomorph '' (_root_.closure ((H : Subgroup G) : Set G)) := by
rw [show (((H.topologicalClosure : Subgroup G) : Set G)) = _root_.closure ((H : Set G)) by
exact Subgroup.topologicalClosure_coe]
_ = _root_.closure (e.toHomeomorph '' ((H : Subgroup G) : Set G)) := by
exact e.toHomeomorph.image_closure ((H : Subgroup G) : Set G)
_ = _root_.closure (((H.map e.toMulEquiv.toMonoidHom : Subgroup G) : Set G)) := by
exact congrArg _root_.closure
(TopologicalGroup.image_subtype_eq_map
(f := e.toMulEquiv.toMonoidHom) (K := H))
_ = _root_.closure ((H : Subgroup G) : Set G) := by
simpa using congrArg _root_.closure
(congrArg (fun L : Subgroup G => (L : Set G)) (map_eq hH e))
_ = ((H.topologicalClosure : Subgroup G) : Set G) := by
symm
exact Subgroup.topologicalClosure_coeProof. 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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. 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.
□instance botTopologicallyCharacteristic :
(⊥ : Subgroup G).TopologicallyCharacteristic := inferInstanceThe bottom subgroup is topologically characteristic.
instance topTopologicallyCharacteristic :
(⊤ : Subgroup G).TopologicallyCharacteristic := inferInstanceThe top subgroup is topologically characteristic.
instance commutatorTopologicallyCharacteristic
[H.TopologicallyCharacteristic] [K.TopologicallyCharacteristic] :
(⁅H, K⁆).TopologicallyCharacteristic := by
refine topologicallyCharacteristic_iff_le_map.mpr ?_
intro e
have hHle :
H ≤ H.map e.toMulEquiv.toMonoidHom :=
topologicallyCharacteristic_iff_le_map.mp
(show H.TopologicallyCharacteristic by infer_instance) e
have hKle :
K ≤ K.map e.toMulEquiv.toMonoidHom :=
topologicallyCharacteristic_iff_le_map.mp
(show K.TopologicallyCharacteristic by infer_instance) e
exact Subgroup.commutator_le_map_commutator
hHle hKleCommutators of topologically characteristic subgroups are topologically characteristic.
instance centerTopologicallyCharacteristic :
(center G).TopologicallyCharacteristic := inferInstanceThe center is topologically characteristic.
instance topologicallyCharacteristic_centralizerInst
[hH : H.TopologicallyCharacteristic] :
(centralizer (H : Set G)).TopologicallyCharacteristic := by
refine topologicallyCharacteristic_iff_comap_le.mpr ?_
intro e g hg
have hg' : e g ∈ centralizer (H : Set G) := hg
rw [Subgroup.mem_centralizer_iff]
intro h hh
apply e.toMulEquiv.injective
rw [e.toMulEquiv.map_mul, e.toMulEquiv.map_mul]
exact
hg' (e h) ((TopologicallyCharacteristic.apply_mem_iff (hH := inferInstance) e (g := h)).2 hh)The centralizer of a topologically characteristic subgroup is again topologically characteristic.
instance topologicallyCharacteristic_normalInst
[H.TopologicallyCharacteristic] :
H.Normal := by
refine ⟨?_⟩
intro x hx g
let e : G ≃ₜ* G :=
{ toMulEquiv := MulAut.conj g
continuous_toFun := by
dsimp [MulAut.conj_apply]
exact IsTopologicalGroup.continuous_conj (G := G) g
continuous_invFun := by
simpa [MulAut.conj_inv_apply] using
(IsTopologicalGroup.continuous_conj (G := G) (g := g⁻¹)) }
have hmap : H.map (e.toMulEquiv.toMonoidHom) = H :=
TopologicallyCharacteristic.map_eq (hH := inferInstance) e
have hxmap : e x ∈ H.map (e.toMulEquiv.toMonoidHom) := ⟨x, hx, rfl⟩
rw [hmap] at hxmap
simpa [e, MulAut.conj_apply] using hxmapTopologically characteristic subgroups are normal.
noncomputable def quotientMulEquiv
(hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) :
G ⧸ H ≃* G ⧸ H := by
letI : H.Normal := by infer_instance
exact QuotientGroup.congr H H e.toMulEquiv (map_eq hH e)A continuous automorphism descends to the quotient by a topologically characteristic subgroup.
@[simp] theorem quotientMulEquiv_mk
(hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) (g : G) :
hH.quotientMulEquiv e (QuotientGroup.mk' H g) =
QuotientGroup.mk' H (e g)The quotient equivalence induced by a topologically characteristic subgroup sends representatives 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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. 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.
□noncomputable def quotientContinuousMulEquiv
(hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) :
G ⧸ H ≃ₜ* G ⧸ H := by
letI : H.Normal := by infer_instance
exact QuotientGroup.congrₜ H H e (map_eq hH e)A topologically characteristic subgroup induces the corresponding continuous multiplicative equivalence on quotients.
@[simp] theorem quotientContinuousMulEquiv_mk
(hH : H.TopologicallyCharacteristic) (e : G ≃ₜ* G) (g : G) :
hH.quotientContinuousMulEquiv e (QuotientGroup.mk' H g) =
QuotientGroup.mk' H (e g)The continuous quotient equivalence induced by a topologically characteristic subgroup sends representatives 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. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). 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. 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.
□