ProCGroups.FiniteGeneration.CharacteristicChainsAndIndices
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
Imported by
- ProCGroups
- ProCGroups.Completion.SameFiniteQuotients
- ProCGroups.FiniteGeneration
- ProCGroups.FiniteStepSolvableQuotients.Commutators.Width
- ProCGroups.FreeProC.Basic
- ProCGroups.LocalWeight.CardinalInvariantsAndLocalWeight
- ProCGroups.LocalWeight.MetrizabilityAndQuotients
- ReidemeisterSchreier.Profinite.OpenSubgroups.FinitePermutationTargets
structure CharacteristicOpenChain where
toSubgroup : ℕ → Subgroup G
zero_eq_top : toSubgroup 0 = ⊤
antitone : Antitone toSubgroup
isOpen' : ∀ n, IsOpen ((toSubgroup n : Set G))
isTopologicallyCharacteristic' : ∀ n, IsTopologicallyCharacteristic G (toSubgroup n)A countable descending chain of open characteristic subgroups. This packages the standard bounded-index characteristic-chain data.
structure FiniteIndexSubgroup (G : Type u) [Group G] where
subgroup : Subgroup G
quotient_finite : Finite (G ⧸ subgroup)A subgroup together with evidence that its quotient has finite cardinality.
noncomputable def index (H : FiniteIndexSubgroup G) : Nat :=
haveI := H.quotient_finite
Nat.card (G ⧸ H.subgroup)The index attached to a finite-index subgroup is finite.
structure OpenSubgroupOfFiniteIndex (G : Type u) [Group G] [TopologicalSpace G] where
subgroup : OpenSubgroup G
quotient_finite : Finite (G ⧸ (subgroup : Subgroup G))An open subgroup together with evidence that its quotient has finite cardinality.
noncomputable def index (H : OpenSubgroupOfFiniteIndex G) : Nat :=
haveI := H.quotient_finite
Nat.card (G ⧸ (H.subgroup : Subgroup G))The index of an open finite-index subgroup.
def toFiniteIndex [IsTopologicalGroup G] [CompactSpace G] (U : OpenSubgroup G) :
OpenSubgroupOfFiniteIndex G where
subgroup := U
quotient_finite :=
Subgroup.quotient_finite_of_isOpen (U : Subgroup G) (openSubgroup_isOpen (G := G) U)In a compact topological group, an open subgroup has finite index.
def OpenSubgroupsOfIndexLE (G : Type u) [Group G] [TopologicalSpace G]
(n : ℕ) : Set (Subgroup G) :=
{ H | IsOpen (H : Set G) ∧ Finite (G ⧸ H) ∧ Nat.card (G ⧸ H) ≤ n }The open subgroups of index at most \(n\). This is the bounded-index family whose intersection defines the characteristic core.
def OpenNormalSubgroupsOfIndex (G : Type u) [Group G] [TopologicalSpace G]
(n : ℕ) : Set (Subgroup G) :=
{ U | U.Normal ∧ IsOpen (U : Set G) ∧ Finite (G ⧸ U) ∧ Nat.card (G ⧸ U) = n }The open normal subgroups of index exactly n. This is the fixed-index family used in the Hopfian finite-quotient argument.
@[simp] theorem mem_openSubgroupsOfIndexLE {n : ℕ} {H : Subgroup G} :
H ∈ OpenSubgroupsOfIndexLE (G := G) n ↔
IsOpen (H : Set G) ∧ Finite (G ⧸ H) ∧ Nat.card (G ⧸ H) ≤ nMembership criterion for the finite set of open subgroups of index at most \(n\).
Show proof
Iff.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. 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 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. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□@[simp] theorem mem_openNormalSubgroupsOfIndex {n : ℕ} {U : Subgroup G} :
U ∈ OpenNormalSubgroupsOfIndex (G := G) n ↔
U.Normal ∧ IsOpen (U : Set G) ∧ Finite (G ⧸ U) ∧ Nat.card (G ⧸ U) = nMembership criterion for the finite set of open normal subgroups of a fixed index.
Show proof
Iff.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. 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 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. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□def CharacteristicIndexIntersection (G : Type u) [Group G] [TopologicalSpace G]
(n : ℕ) : Subgroup G :=
sInf (OpenSubgroupsOfIndexLE (G := G) n)The canonical bounded-index intersection \(V_n = \bigcap {H \leq G | H open and [G: H] \leq n}\).
@[simp] theorem characteristicIndexIntersection_def (n : ℕ) :
CharacteristicIndexIntersection (G := G) n =
sInf (OpenSubgroupsOfIndexLE (G := G) n)The characteristic index intersection is the infimum of all open subgroups of bounded index.
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. 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 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. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□structure CharacteristicIndexIntersectionSpec where
isOpen' : ∀ n, IsOpen ((CharacteristicIndexIntersection (G := G) n : Set G))
isTopologicallyCharacteristic' : ∀ n, IsTopologicallyCharacteristic G (CharacteristicIndexIntersection (G := G) n)
antitone' : Antitone (CharacteristicIndexIntersection (G := G))
cofinal' :
∀ U : Subgroup G, IsOpen (U : Set G) →
∃ n, CharacteristicIndexIntersection (G := G) n ≤ UBasic bounded-index intersection package: the canonical bounded-index intersections are open, characteristic, descending, and cofinal among open subgroups.
def HasFiniteOpenSubgroupsOfIndex (G : Type u) [Group G] [TopologicalSpace G]
: Prop :=
∀ n, Set.Finite
{ H : Subgroup G | IsOpen (H : Set G) ∧ Finite (G ⧸ H) ∧ Nat.card (G ⧸ H) = n }A group has only finitely many open subgroups of each prescribed index.
def HasFiniteOpenNormalSubgroupsOfIndex (G : Type u) [Group G] [TopologicalSpace G]
: Prop :=
∀ n,
Set.Finite
{ U : Subgroup G |
U.Normal ∧ IsOpen (U : Set G) ∧ Finite (G ⧸ U) ∧ Nat.card (G ⧸ U) = n }Normal-subgroup version of fixed-index finiteness.
theorem HasFiniteOpenSubgroupsOfIndex.toHasFiniteOpenNormalSubgroupsOfIndex
(h : HasFiniteOpenSubgroupsOfIndex G) :
HasFiniteOpenNormalSubgroupsOfIndex GFiniteness of open subgroups of each index implies finiteness of open normal subgroups of each index.
Show proof
by
intro n
refine (h n).subset ?_
intro U hU
exact ⟨hU.2.1, hU.2.2.1, hU.2.2.2⟩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. 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.
□theorem continuousMonoidHom_eq_of_eqOn_topologicalGenerators
[IsTopologicalGroup G]
{R : Type v} [Group R] [TopologicalSpace R] [T2Space R]
{s : Finset G} (hsgen : TopologicallyGenerates (G := G) (↑s : Set G))
{f g : ContinuousMonoidHom G R}
(hfg : ∀ x ∈ (↑s : Set G), f x = g x) :
f = gContinuous homomorphisms are equal when they agree on a topological generating set.
Show proof
by
let K : Subgroup G := {
carrier := { x | f x = g x }
one_mem' := by simp only [mem_setOf_eq, map_one]
mul_mem' := by
intro a b ha hb
change f (a * b) = g (a * b)
rw [map_mul, map_mul, ha, hb]
inv_mem' := by
intro a ha
simpa using congrArg Inv.inv ha
}
have hKclosed : IsClosed ((K : Subgroup G) : Set G) := by
change IsClosed { x | f x = g x }
exact isClosed_eq f.continuous_toFun g.continuous_toFun
have hsub : Subgroup.closure (↑s : Set G) ≤ K := by
rw [Subgroup.closure_le]
intro x hx
exact hfg x hx
have htop : (⊤ : Subgroup G) ≤ K := by
have hcl :
(Subgroup.closure (↑s : Set G)).topologicalClosure ≤ K :=
Subgroup.topologicalClosure_minimal _ hsub hKclosed
rw [TopologicallyGenerates] at hsgen
simpa [hsgen] using hcl
ext x
simpa [K] using htop (show x ∈ (⊤ : Subgroup G) from by simp only [Subgroup.mem_top])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 pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem finite_continuousMonoidHom_to_finite_of_topologicallyFinitelyGenerated
[IsTopologicalGroup G]
{R : Type v} [Group R] [TopologicalSpace R] [T2Space R] [Finite R]
(hG : TopologicallyFinitelyGenerated G) :
Finite (ContinuousMonoidHom G R)A finitely generated profinite group admits only finitely many continuous homomorphisms into a fixed finite discrete target.
Show proof
by
classical
rcases hG with ⟨s, hsgen⟩
let eval : ContinuousMonoidHom G R → ((↑s : Set G) → R) := fun φ x => φ x.1
have heval : Function.Injective eval := by
intro φ ψ hφψ
apply continuousMonoidHom_eq_of_eqOn_topologicalGenerators (G := G) hsgen
intro x hx
exact congrArg (fun k => k ⟨x, hx⟩) hφψ
exact Finite.of_injective eval hevalProof. 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 openSubgroupIndexEquiv
(H : Subgroup G) (hHfinite : Finite (G ⧸ H)) {n : ℕ}
(hn : Nat.card (G ⧸ H) = n) :
(G ⧸ H) ≃ Fin n := by
classical
letI : Finite (G ⧸ H) := hHfinite
letI : Fintype (G ⧸ H) := Fintype.ofFinite (G ⧸ H)
refine Finite.equivFinOfCardEq ?_
simpa [Nat.card_eq_fintype_card] using hnnoncomputable def openSubgroupIndexAction
(H : Subgroup G) (hHfinite : Finite (G ⧸ H)) {n : ℕ}
(hn : Nat.card (G ⧸ H) = n) :
G →* Equiv.Perm (Fin n) := by
classical
let e := openSubgroupIndexEquiv (G := G) H hHfinite hn
exact e.permCongrHom.toMonoidHom.comp (MulAction.toPermHom G (G ⧸ H))The coset action of \(G\) on the \(n\) cosets of an index-\(n\) subgroup, transported to \(\operatorname{Fin} n\).
noncomputable def openSubgroupIndexBasepoint
(H : Subgroup G) (hHfinite : Finite (G ⧸ H)) {n : ℕ}
(hn : Nat.card (G ⧸ H) = n) : Fin n :=
openSubgroupIndexEquiv (G := G) H hHfinite hn (QuotientGroup.mk 1)The image of the identity coset under the chosen \(\operatorname{Fin} n\) identification.
instance instTopologicalSpaceFinitePerm (n : ℕ) : TopologicalSpace (Equiv.Perm (Fin n)) :=
⊥The finite permutation type has its canonical topological space structure.
instance instDiscreteTopologyFinitePerm (n : ℕ) : DiscreteTopology (Equiv.Perm (Fin n)) :=
⟨rfl⟩The finite permutation type carries the discrete topology.
instance instIsTopologicalGroupFinitePerm (n : ℕ) : IsTopologicalGroup (Equiv.Perm (Fin n)) := by
infer_instanceThe finite permutation group is a topological group with the discrete topology.
instance instFiniteFinitePerm (n : ℕ) : Finite (Equiv.Perm (Fin n)) := by
infer_instanceThe finite permutation type is finite.
noncomputable def openSubgroupIndexContinuousHom
[IsTopologicalGroup G] [CompactSpace G]
(H : Subgroup G) (hH : IsOpen (H : Set G)) {n : ℕ}
(hHfinite : Finite (G ⧸ H)) (hn : Nat.card (G ⧸ H) = n) :
G →ₜ* Equiv.Perm (Fin n) := by
classical
let φ : G →* Equiv.Perm (Fin n) := openSubgroupIndexAction (G := G) H hHfinite hn
have hφker :
IsOpen ((φ.ker : Subgroup G) : Set G) := by
let e := openSubgroupIndexEquiv (G := G) H hHfinite hn
have hker :
φ.ker = (MulAction.toPermHom G (G ⧸ H)).ker := by
ext g
change e.permCongr (MulAction.toPerm g) = 1 ↔ MulAction.toPerm g = 1
have hperm_one :
e.permCongr (1 : Equiv.Perm (G ⧸ H)) = (1 : Equiv.Perm (Fin n)) := by
ext x
simp only [Equiv.permCongr_apply, Equiv.Perm.coe_one, id_eq, Equiv.apply_symm_apply]
rw [← hperm_one]
exact e.permCongr.injective.eq_iff
letI : Finite (G ⧸ H) := Subgroup.quotient_finite_of_isOpen H hH
letI : H.FiniteIndex := Subgroup.finiteIndex_of_finite_quotient (H := H)
have hHclosed : IsClosed ((H : Subgroup G) : Set G) :=
Subgroup.isClosed_of_isOpen H hH
letI : H.normalCore.FiniteIndex := Subgroup.finiteIndex_normalCore (H := H)
have hopenCore : IsOpen (((H.normalCore : Subgroup G) : Set G)) :=
H.normalCore.isOpen_of_isClosed_of_finiteIndex (H.normalCore_isClosed hHclosed)
simpa [hker, Subgroup.normalCore_eq_ker (H := H)] using hopenCore
have hφcont : Continuous φ := by
letI : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
letI : UniformSpace (Equiv.Perm (Fin n)) :=
IsTopologicalGroup.rightUniformSpace (Equiv.Perm (Fin n))
have hφuc :
UniformContinuous φ :=
(IsUniformGroup.uniformContinuous_iff_isOpen_ker (f := φ)).2 hφker
exact hφuc.continuous
exact
{ toMonoidHom := φ
continuous_toFun := hφcont }The finite coset action is viewed as a continuous homomorphism into a discrete permutation group.
theorem mem_openSubgroup_iff_indexAction_fix_basepoint
{H : Subgroup G} (hHfinite : Finite (G ⧸ H)) {n : ℕ}
(hn : Nat.card (G ⧸ H) = n) {g : G} :
g ∈ H ↔
openSubgroupIndexAction (G := G) H hHfinite hn g
(openSubgroupIndexBasepoint (G := G) H hHfinite hn) =
openSubgroupIndexBasepoint (G := G) H hHfinite hnMembership in an open subgroup is equivalent to fixing the basepoint in its coset action.
Show proof
by
classical
let e := openSubgroupIndexEquiv (G := G) H hHfinite hn
constructor
· intro hg
have hq : QuotientGroup.mk (s := H) g = QuotientGroup.mk (s := H) 1 := by
simpa [QuotientGroup.eq] using hg
simpa [openSubgroupIndexAction, openSubgroupIndexBasepoint, e] using congrArg e hq
· intro hg
have hq :
QuotientGroup.mk (s := H) g = QuotientGroup.mk (s := H) 1 := by
apply e.injective
simpa [openSubgroupIndexAction, openSubgroupIndexBasepoint, e] using hg
simpa [QuotientGroup.eq] using hqProof. 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. 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. 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.
□theorem hasFiniteOpenSubgroupsOfIndex_of_topologicallyFinitelyGenerated
[IsTopologicalGroup G] [CompactSpace G]
(hG : TopologicallyFinitelyGenerated G) :
HasFiniteOpenSubgroupsOfIndex GFinitely generated profinite groups have only finitely many open subgroups of each index.
Show proof
by
intro n
classical
let S : Type u :=
{ H : Subgroup G // IsOpen (H : Set G) ∧ Finite (G ⧸ H) ∧ Nat.card (G ⧸ H) = n }
letI : TopologicalSpace (Equiv.Perm (Fin n)) := ⊥
letI : DiscreteTopology (Equiv.Perm (Fin n)) := ⟨rfl⟩
letI : IsTopologicalGroup (Equiv.Perm (Fin n)) := by infer_instance
letI : Finite (Equiv.Perm (Fin n)) := by infer_instance
let code : S → ContinuousMonoidHom G (Equiv.Perm (Fin n)) × Fin n := fun H =>
let φ := openSubgroupIndexAction (G := G) H.1 H.2.2.1 H.2.2.2
let e := openSubgroupIndexEquiv (G := G) H.1 H.2.2.1 H.2.2.2
let hφker :
IsOpen ((φ.ker : Subgroup G) : Set G) := by
letI : Finite (G ⧸ H.1) := H.2.2.1
letI : H.1.FiniteIndex := Subgroup.finiteIndex_of_finite_quotient (H := H.1)
have hHclosed : IsClosed ((H.1 : Subgroup G) : Set G) :=
Subgroup.isClosed_of_isOpen H.1 H.2.1
have hker :
φ.ker = (MulAction.toPermHom G (G ⧸ H.1)).ker := by
ext g
change
e.permCongr (MulAction.toPerm g) = 1 ↔ MulAction.toPerm g = 1
have hperm_one : e.permCongr (1 : Equiv.Perm (G ⧸ H.1)) = (1 : Equiv.Perm (Fin n)) := by
ext x
simp only [Equiv.permCongr_apply, Equiv.Perm.coe_one, id_eq, Equiv.apply_symm_apply]
rw [← hperm_one]
exact e.permCongr.injective.eq_iff
letI : H.1.normalCore.FiniteIndex := Subgroup.finiteIndex_normalCore (H := H.1)
have hopenCore : IsOpen (((H.1).normalCore : Subgroup G) : Set G) :=
(H.1).normalCore.isOpen_of_isClosed_of_finiteIndex ((H.1).normalCore_isClosed hHclosed)
simpa [hker, Subgroup.normalCore_eq_ker (H := H.1)] using hopenCore
let hφcont :
Continuous φ := by
letI : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
letI : UniformSpace (Equiv.Perm (Fin n)) :=
IsTopologicalGroup.rightUniformSpace (Equiv.Perm (Fin n))
have hφuc :
UniformContinuous φ :=
(IsUniformGroup.uniformContinuous_iff_isOpen_ker (f := φ)).2 hφker
exact hφuc.continuous
({ toMonoidHom := φ
continuous_toFun := hφcont },
openSubgroupIndexBasepoint (G := G) H.1 H.2.2.1 H.2.2.2)
have hhomfinite : Finite (ContinuousMonoidHom G (Equiv.Perm (Fin n))) :=
finite_continuousMonoidHom_to_finite_of_topologicallyFinitelyGenerated
(G := G) hG
let _ : Finite (ContinuousMonoidHom G (Equiv.Perm (Fin n)) × Fin n) := by
infer_instance
have hcode : Function.Injective code := by
intro H K hHK
apply Subtype.ext
ext g
rw [mem_openSubgroup_iff_indexAction_fix_basepoint (G := G) (H := H.1) H.2.2.1 H.2.2.2
(g := g),
mem_openSubgroup_iff_indexAction_fix_basepoint (G := G) (H := K.1) K.2.2.1 K.2.2.2
(g := g)]
exact Iff.of_eq <| by
simpa [code] using congrArg
(fun p : ContinuousMonoidHom G (Equiv.Perm (Fin n)) × Fin n => p.1 g p.2 = p.2) hHK
have hSfinite :
Finite
{ H : Subgroup G //
IsOpen (H : Set G) ∧ Finite (G ⧸ H) ∧ Nat.card (G ⧸ H) = n } := by
simpa [S] using (Finite.of_injective code hcode)
exact @Set.toFinite (Subgroup G)
{ H : Subgroup G | IsOpen (H : Set G) ∧ Finite (G ⧸ H) ∧ Nat.card (G ⧸ H) = n }
hSfiniteProof. 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.
□theorem finite_openSubgroupsOfIndexLE_of_hasFiniteOpenSubgroupsOfIndex
(hfin : HasFiniteOpenSubgroupsOfIndex G) (n : ℕ) :
Set.Finite (OpenSubgroupsOfIndexLE (G := G) n)Bounding the index by \(n\) still yields only finitely many open subgroups.
Show proof
by
classical
refine Set.Finite.subset ((Set.finite_le_nat n).biUnion fun m hm => hfin m) ?_
intro H hH
exact Set.mem_iUnion.2
⟨Nat.card (G ⧸ H), Set.mem_iUnion.2 ⟨hH.2.2, ⟨hH.1, hH.2.1, 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. 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. 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.
□theorem Subgroup.isOpen_sInf_of_finite
{S : Set (Subgroup G)} (hS : S.Finite)
(hopen : ∀ H ∈ S, IsOpen (H : Set G)) :
IsOpen ((sInf S : Subgroup G) : Set G)The infimum of a finite family of open subgroups is open.
Show proof
by
classical
induction S, hS using Set.Finite.induction_on with
| empty =>
simp only [sInf_empty, Subgroup.coe_top, isOpen_univ]
| @insert H S hHS hS ih =>
rw [sInf_insert]
exact (hopen H (by simp only [mem_insert_iff, true_or])).inter (ih fun K hK => hopen K (by simp only [mem_insert_iff, hK, or_true]))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. 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.
□theorem characteristicIndexIntersection_isOpen_of_hasFiniteOpenSubgroupsOfIndex
(hfin : HasFiniteOpenSubgroupsOfIndex G) (n : ℕ) :
IsOpen ((CharacteristicIndexIntersection (G := G) n : Set G))The bounded-index characteristic intersection is open once the bounded-index family is finite.
Show proof
by
apply Subgroup.isOpen_sInf_of_finite
· exact finite_openSubgroupsOfIndexLE_of_hasFiniteOpenSubgroupsOfIndex (G := G) hfin n
· intro H hH
exact hH.1Proof. 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. 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.
□theorem characteristicIndexIntersection_antitone :
Antitone (CharacteristicIndexIntersection (G := G))The bounded-index characteristic intersections form a descending chain.
Show proof
by
intro m n hmn x hx
simp only [CharacteristicIndexIntersection, Subgroup.mem_sInf] at hx ⊢
intro H hH
exact hx H ⟨hH.1, hH.2.1, le_trans hH.2.2 hmn⟩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. 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 pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□theorem characteristicIndexIntersection_isTopologicallyCharacteristic
[IsTopologicalGroup G] [CompactSpace G]
(n : ℕ) :
IsTopologicallyCharacteristic G (CharacteristicIndexIntersection (G := G) n)The finite-index characteristic intersection is characteristic.
Show proof
by
have hforward :
∀ φ : G ≃ₜ* G, ∀ g : G,
g ∈ CharacteristicIndexIntersection (G := G) n →
φ g ∈ CharacteristicIndexIntersection (G := G) n := by
intro φ g hg
simp only [CharacteristicIndexIntersection, Subgroup.mem_sInf] at hg ⊢
intro H hH
have hcomap :
Subgroup.comap φ.toMonoidHom H ∈ OpenSubgroupsOfIndexLE (G := G) n := by
have hcomapOpen : IsOpen ((Subgroup.comap φ.toMonoidHom H : Subgroup G) : Set G) :=
hH.1.preimage φ.continuous_toFun
have hcomapFinite : Finite (G ⧸ Subgroup.comap φ.toMonoidHom H) :=
Subgroup.quotient_finite_of_isOpen (Subgroup.comap φ.toMonoidHom H) hcomapOpen
refine ⟨hcomapOpen, hcomapFinite, ?_⟩
simpa [Subgroup.index_eq_card] using
(Subgroup.index_comap_of_surjective (H := H) φ.surjective).le.trans hH.2.2
exact hg _ hcomap
intro φ g
constructor
· intro hg
simpa using hforward φ.symm (φ g) hg
· exact hforward φ gProof. 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 characteristicIndexIntersection_cofinal_of_openSubgroup
[IsTopologicalGroup G] [CompactSpace G]
(U : Subgroup G) (hU : IsOpen (U : Set G)) :
∃ n, CharacteristicIndexIntersection (G := G) n ≤ UCharacteristic index intersections are cofinal among open subgroups.
Show proof
by
have hUfinite : Finite (G ⧸ U) :=
Subgroup.quotient_finite_of_isOpen U hU
refine ⟨Nat.card (G ⧸ U), ?_⟩
intro x hx
simp only [CharacteristicIndexIntersection, Subgroup.mem_sInf] at hx
exact hx U ⟨hU, hUfinite, le_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. 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. 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.
□theorem characteristicIndexIntersectionSpec_of_hasFiniteOpenSubgroupsOfIndex
[IsTopologicalGroup G] [CompactSpace G]
(hfin : HasFiniteOpenSubgroupsOfIndex G) :
CharacteristicIndexIntersectionSpec (G := G) where
isOpen'Fixed-index finiteness yields the full characteristic-intersection package.
Show proof
characteristicIndexIntersection_isOpen_of_hasFiniteOpenSubgroupsOfIndex
(G := G) hfin
isTopologicallyCharacteristic' :=
characteristicIndexIntersection_isTopologicallyCharacteristic
(G := G)
antitone' := characteristicIndexIntersection_antitone (G := G)
cofinal' := characteristicIndexIntersection_cofinal_of_openSubgroup (G := 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. 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. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□def CharacteristicIndexIntersectionSpec.toCharacteristicOpenChain
(hV : CharacteristicIndexIntersectionSpec (G := G)) :
CharacteristicOpenChain G where
toSubgroup
| 0 => ⊤
| n + 1 => CharacteristicIndexIntersection (G := G) n
zero_eq_top := rfl
antitone := by
intro m n hmn
cases m with
| zero =>
exact le_top
| succ m =>
cases n with
| zero =>
cases Nat.not_succ_le_zero m hmn
| succ n =>
exact hV.antitone' (Nat.succ_le_succ_iff.mp hmn)
isOpen' := by
intro n
cases n with
| zero =>
simp only [Subgroup.coe_top, isOpen_univ]
| succ n =>
exact hV.isOpen' n
isTopologicallyCharacteristic' := by
intro n
cases n with
| zero =>
simp only [IsTopologicallyCharacteristic.top]
| succ n =>
exact hV.isTopologicallyCharacteristic' nConvert characteristic index-intersection data into a characteristic open chain.
theorem CharacteristicIndexIntersectionSpec.exists_subset_of_open_one_mem
[IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
(hV : CharacteristicIndexIntersectionSpec (G := G))
{U : Set G} (hUopen : IsOpen U) (h1U : (1 : G) ∈ U) :
∃ n, ((CharacteristicIndexIntersection (G := G) n : Subgroup G) : Set G) ⊆ UA characteristic-intersection package produces a basis element inside any open neighborhood of \(1\).
Show proof
by
rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hUopen h1U with ⟨N, hNU⟩
rcases hV.cofinal' (N : Subgroup G) (openNormalSubgroup_isOpen (G := G) N) with ⟨n, hn⟩
exact ⟨n, Set.Subset.trans hn hNU⟩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. 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 pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□theorem exists_characteristicOpenBasis_of_characteristicIndexIntersectionSpec
[IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
(hV : CharacteristicIndexIntersectionSpec (G := G)) :
∃ V : ℕ → Subgroup G,
V 0 = ⊤ ∧
Antitone V ∧
(∀ n, IsOpen ((V n : Subgroup G) : Set G)) ∧
(∀ n, IsTopologicallyCharacteristic G (V n)) ∧
∀ U : Set G, U ∈ 𝓝 (1 : G) → ∃ n, ((V n : Subgroup G) : Set G) ⊆ UA characteristic-intersection package yields a countable characteristic open basis at the identity.
Show proof
by
let V := hV.toCharacteristicOpenChain
refine ⟨V.toSubgroup, V.zero_eq_top, V.antitone, V.isOpen', V.isTopologicallyCharacteristic', ?_⟩
intro U hU
rcases mem_nhds_iff.mp hU with ⟨W, hWU, hWopen, h1W⟩
rcases hV.exists_subset_of_open_one_mem hWopen h1W with ⟨n, hn⟩
exact ⟨n + 1, Set.Subset.trans hn hWU⟩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. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□theorem exists_characteristicOpenBasis_of_topologicallyFinitelyGenerated
[IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
: TopologicallyFinitelyGenerated G →
∃ V : ℕ → Subgroup G,
V 0 = ⊤ ∧
Antitone V ∧
(∀ n, IsOpen ((V n : Subgroup G) : Set G)) ∧
(∀ n, IsTopologicallyCharacteristic G (V n)) ∧
∀ U : Set G, U ∈ 𝓝 (1 : G) → ∃ n, ((V n : Subgroup G) : Set G) ⊆ UTopologically finitely generated profinite groups have a countable characteristic open basis at the identity.
Show proof
by
intro hG
exact exists_characteristicOpenBasis_of_characteristicIndexIntersectionSpec (G := G)
(characteristicIndexIntersectionSpec_of_hasFiniteOpenSubgroupsOfIndex (G := G)
(hasFiniteOpenSubgroupsOfIndex_of_topologicallyFinitelyGenerated (G := G) 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. 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 finiteIndexOpenSubgroups_and_charBasis_of_tfg
[IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G]
(hG : TopologicallyFinitelyGenerated G) :
HasFiniteOpenSubgroupsOfIndex G ∧
∃ V : ℕ → Subgroup G,
V 0 = ⊤ ∧
Antitone V ∧
(∀ n, IsOpen ((V n : Subgroup G) : Set G)) ∧
(∀ n, IsTopologicallyCharacteristic G (V n)) ∧
∀ U : Set G, U ∈ 𝓝 (1 : G) → ∃ n, ((V n : Subgroup G) : Set G) ⊆ UFinitely generated profinite groups have finite fixed-index open-subgroup sets and a countable characteristic open basis at the identity.
Show proof
by
exact ⟨hasFiniteOpenSubgroupsOfIndex_of_topologicallyFinitelyGenerated (G := G) hG,
exists_characteristicOpenBasis_of_topologicallyFinitelyGenerated (G := G) 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. 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.
□theorem Finite.surjOn_of_injOn_mapsTo {α : Type*} {s : Set α}
(hs : s.Finite) {f : α → α}
(hf : MapsTo f s s) (hinj : InjOn f s) :
SurjOn f s sAn injective self-map of a finite set is automatically surjective on that set.
Show proof
by
classical
let g : s → s := fun x => ⟨f x.1, hf x.2⟩
have hg_inj : Function.Injective g := by
intro x y hxy
apply Subtype.ext
exact hinj x.2 y.2 (congrArg Subtype.val hxy)
haveI := hs.to_subtype
have hg_surj : Function.Surjective g := Finite.surjective_of_injective hg_inj
intro y hy
rcases hg_surj ⟨y, hy⟩ with ⟨x, hx⟩
refine ⟨x.1, x.2, ?_⟩
exact congrArg Subtype.val 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. 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. For injectivity, suppose two source elements have the same image. After projecting to every finite quotient stage the corresponding finite-stage map is injective, or the equality is simply equality of subtype carriers; hence all source coordinates agree, and the inverse-limit extensionality principle identifies the original elements.
□def OpenNormalSeparatesPoints (G : Type u) [Group G] [TopologicalSpace G]
: Prop :=
∀ x : G, x ≠ 1 → ∃ U : Subgroup G, U.Normal ∧ IsOpen (U : Set G) ∧ x ∉ UOpen normal subgroups separate the identity from every nontrivial element. This is the abstract separation input behind the fixed-index Hopfian argument.
theorem injective_of_ker_le_every_openNormal
{φ : ContinuousMonoidHom G G}
(hker : ∀ U : Subgroup G, U.Normal → IsOpen (U : Set G) → φ.ker ≤ U)
(hsep : OpenNormalSeparatesPoints G) :
Function.Injective φKernel-separation criterion for Hopfian arguments. If every kernel element lies in every open normal subgroup, and open normal subgroups separate points, then the endomorphism is injective.
Show proof
by
intro x y hxy
have hmem : x * y⁻¹ ∈ φ.ker := by
simp only [ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.mem_ker, MonoidHom.coe_coe, map_mul, hxy, map_inv,
mul_inv_cancel]
have hone : x * y⁻¹ = 1 := by
by_contra hne
obtain ⟨U, hU_normal, hU_open, hnotU⟩ := hsep (x * y⁻¹) hne
exact hnotU (hker U hU_normal hU_open hmem)
have hmul := congrArg (fun z => z * y) hone
simpa [mul_assoc] using hmulProof. 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. 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. For injectivity, suppose two source elements have the same image. After projecting to every finite quotient stage the corresponding finite-stage map is injective, or the equality is simply equality of subtype carriers; hence all source coordinates agree, and the inverse-limit extensionality principle identifies the original elements. 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.
□def PreimagePreservesOpenNormalSubgroupsOfIndex
(φ : ContinuousMonoidHom G G) : Prop :=
∀ n,
Set.MapsTo (fun U : Subgroup G => Subgroup.comap φ.toMonoidHom U)
(OpenNormalSubgroupsOfIndex (G := G) n)
(OpenNormalSubgroupsOfIndex (G := G) n)The preimage operator preserves the fixed-index family of open normal subgroups.
theorem subgroupComap_injective_of_surjective
{H : Type v} [Group H]
(f : G →* H) (hf : Function.Surjective f) :
Function.Injective (Subgroup.comap f)Comap along a surjective homomorphism is injective on subgroups.
Show proof
by
intro U V hUV
ext y
constructor <;> intro hy
· rcases hf y with ⟨x, rfl⟩
change x ∈ Subgroup.comap f V
have hx : x ∈ Subgroup.comap f U := hy
simpa [hUV] using hx
· rcases hf y with ⟨x, rfl⟩
change x ∈ Subgroup.comap f U
have hx : x ∈ Subgroup.comap f V := hy
simpa [hUV] 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. 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. 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.
□theorem preimage_injectiveOn_openNormalSubgroupsOfIndex
{φ : ContinuousMonoidHom G G}
(hφsurj : Function.Surjective φ) (n : ℕ) :
Set.InjOn (fun U : Subgroup G => Subgroup.comap φ.toMonoidHom U)
(OpenNormalSubgroupsOfIndex (G := G) n)Preimage under a surjective endomorphism is injective on each fixed-index open-normal family.
Show proof
by
intro U hU V hV hEq
exact subgroupComap_injective_of_surjective (G := G) φ.toMonoidHom hφsurj hEqProof. 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. 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. For injectivity, suppose two source elements have the same image. After projecting to every finite quotient stage the corresponding finite-stage map is injective, or the equality is simply equality of subtype carriers; hence all source coordinates agree, and the inverse-limit extensionality principle identifies the original elements.
□def PreimageSurjectiveOnOpenNormalSubgroupsOfIndex
(φ : ContinuousMonoidHom G G) : Prop :=
∀ n,
Set.SurjOn (fun U : Subgroup G => Subgroup.comap φ.toMonoidHom U)
(OpenNormalSubgroupsOfIndex (G := G) n)
(OpenNormalSubgroupsOfIndex (G := G) n)Surjectivity of the preimage operator on each family of open normal subgroups of index \(n\). This is exactly the conclusion obtained from the finiteness of the family \(U_n\).
theorem preimageSurjectiveOn_openNormalSubgroupsOfIndex_of_finite
{φ : ContinuousMonoidHom G G}
(hfin : HasFiniteOpenNormalSubgroupsOfIndex G)
(hφsurj : Function.Surjective φ)
(hpres : PreimagePreservesOpenNormalSubgroupsOfIndex (G := G) φ) :
PreimageSurjectiveOnOpenNormalSubgroupsOfIndex (G := G) φFor finite groups, preimage along a surjective endomorphism is surjective on open normal subgroups of fixed index.
Show proof
by
intro n
exact Set.Finite.surjOn_of_injOn_mapsTo
(hs := hfin n)
(f := fun U : Subgroup G => Subgroup.comap φ.toMonoidHom U)
(hpres n)
(preimage_injectiveOn_openNormalSubgroupsOfIndex (G := G) hφsurj n)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. 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. 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.
□theorem ker_le_every_openNormal_of_preimageSurjectiveOn_index
[IsTopologicalGroup G] [CompactSpace G]
{φ : ContinuousMonoidHom G G}
(hφ : PreimageSurjectiveOnOpenNormalSubgroupsOfIndex (G := G) φ) :
∀ U : Subgroup G, U.Normal → IsOpen (U : Set G) → φ.ker ≤ UIf the preimage map is surjective on every fixed-index open-normal family, then \(\ker \varphi \le U\) for every open normal subgroup \(U\).
Show proof
by
intro U hU_normal hU_open
have hUfinite : Finite (G ⧸ U) :=
Subgroup.quotient_finite_of_isOpen U hU_open
let n : ℕ := Nat.card (G ⧸ U)
have hU : U ∈ OpenNormalSubgroupsOfIndex (G := G) n := by
exact ⟨hU_normal, hU_open, hUfinite, rfl⟩
rcases hφ n hU with ⟨V, hV, hEq⟩
rw [← hEq]
intro x hx
change φ x ∈ V
have hx1 : φ x = 1 := by
change φ x = 1 at hx
exact hx
rw [hx1]
exact V.one_memProof. 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. 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. 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. 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.
□theorem injective_of_preimageSurjectiveOn_openNormalIndex
[IsTopologicalGroup G] [CompactSpace G]
{φ : ContinuousMonoidHom G G}
(hφ : PreimageSurjectiveOnOpenNormalSubgroupsOfIndex (G := G) φ)
(hsep : OpenNormalSeparatesPoints G) :
Function.Injective φThe injectivity step in the fixed-index Hopfian argument, abstracted away from the finiteness argument.
Show proof
by
apply injective_of_ker_le_every_openNormal
· exact ker_le_every_openNormal_of_preimageSurjectiveOn_index (G := G) hφ
· exact hsepProof. 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 ContinuousHopfian (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
∀ φ : ContinuousMonoidHom G G, Function.Surjective φ → Function.Injective φA topological group is continuously Hopfian if every surjective continuous endomorphism is injective.
def SurjectiveContinuousEndomorphismsAreAutomorphisms
(G : Type u) [Group G] [TopologicalSpace G] : Prop :=
∀ φ : ContinuousMonoidHom G G, Function.Surjective φ →
∃ e : G ≃ₜ* G, ∀ x : G, e x = φ xEvery surjective continuous endomorphism is induced by a continuous automorphism.
noncomputable def ContinuousMonoidHom.toContinuousMulEquivOfBijective
[CompactSpace G] [T2Space G]
(φ : ContinuousMonoidHom G G) (hφ : Function.Bijective φ) :
G ≃ₜ* G := by
let e : G ≃ G := Equiv.ofBijective φ hφ
let eh : G ≃ₜ G :=
e.toHomeomorphOfContinuousClosed φ.continuous_toFun
(Continuous.isClosedMap φ.continuous_toFun)
exact ContinuousMulEquiv.mk' eh (by
intro x y
exact φ.map_mul x y)Upgrade a continuous bijective endomorphism of a compact Hausdorff topological group to a continuous automorphism.
theorem surjectiveContinuousEndomorphismsAreAutomorphisms_of_continuousHopfian
[CompactSpace G] [T2Space G]
(hhopf : ContinuousHopfian G) :
SurjectiveContinuousEndomorphismsAreAutomorphisms GA continuously Hopfian group has all surjective continuous endomorphisms invertible.
Show proof
by
intro φ hφsurj
let e := ContinuousMonoidHom.toContinuousMulEquivOfBijective
(G := G) φ ⟨hhopf φ hφsurj, hφsurj⟩
refine ⟨e, ?_⟩
intro x
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. 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 continuousHopfian_of_preimageSurjectiveOn_openNormalIndex
[IsTopologicalGroup G] [CompactSpace G]
(hsep : OpenNormalSeparatesPoints G)
(hpre : ∀ φ : ContinuousMonoidHom G G, Function.Surjective φ →
PreimageSurjectiveOnOpenNormalSubgroupsOfIndex (G := G) φ) :
ContinuousHopfian GOnce the preimage-surjectivity statement on fixed-index open normal subgroups is available for all surjective continuous endomorphisms, the Hopfian conclusion follows mathematically.
Show proof
by
intro φ hφsurj
exact injective_of_preimageSurjectiveOn_openNormalIndex (G := G) (hpre φ hφsurj) hsepProof. 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 continuousHopfian_of_finiteOpenNormalSubgroupsOfIndex
[IsTopologicalGroup G] [CompactSpace G]
(hsep : OpenNormalSeparatesPoints G)
(hfin : HasFiniteOpenNormalSubgroupsOfIndex G)
(hpres :
∀ φ : ContinuousMonoidHom G G, Function.Surjective φ →
PreimagePreservesOpenNormalSubgroupsOfIndex (G := G) φ) :
ContinuousHopfian GFiniteness of open normal subgroups of each index implies the continuous Hopfian property.
Show proof
by
apply continuousHopfian_of_preimageSurjectiveOn_openNormalIndex (G := G) hsep
intro φ hφsurj
exact preimageSurjectiveOn_openNormalSubgroupsOfIndex_of_finite
(G := G) hfin hφsurj (hpres φ hφsurj)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.
□theorem surjContinuousEndomorphismsAreAutomorphisms_of_finiteOpenNormalSubgroupsOfIndex
[IsTopologicalGroup G] [CompactSpace G] [T2Space G]
(hsep : OpenNormalSeparatesPoints G)
(hfin : HasFiniteOpenNormalSubgroupsOfIndex G)
(hpres :
∀ φ : ContinuousMonoidHom G G, Function.Surjective φ →
PreimagePreservesOpenNormalSubgroupsOfIndex (G := G) φ) :
SurjectiveContinuousEndomorphismsAreAutomorphisms GFixed-index finiteness of open normal subgroups implies the profinite Hopfian conclusion.
Show proof
by
apply surjectiveContinuousEndomorphismsAreAutomorphisms_of_continuousHopfian
exact continuousHopfian_of_finiteOpenNormalSubgroupsOfIndex (G := G) hsep hfin hpresProof. 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.
□theorem openNormalSeparatesPoints_of_profinite
[IsTopologicalGroup G] [CompactSpace G] [T1Space G] [TotallyDisconnectedSpace G] :
OpenNormalSeparatesPoints GIn a profinite group, open normal subgroups separate the identity from every nontrivial element.
Show proof
by
intro x hx
let U : Set G := ({x} : Set G)ᶜ
have hUopen : IsOpen U := isClosed_singleton.isOpen_compl
have h1U : (1 : G) ∈ U := by
simpa [U, eq_comm] using hx
rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hUopen h1U with ⟨N, hNU⟩
refine ⟨N, N.isNormal', openNormalSubgroup_isOpen (G := G) N, ?_⟩
intro hxN
have hxU : x ∈ U := hNU hxN
simp only [mem_compl_iff, mem_singleton_iff, not_true_eq_false, U] at hxUProof. 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 preimagePreservesOpenNormalSubgroupsOfIndex_of_surjective
[IsTopologicalGroup G] [CompactSpace G]
{φ : ContinuousMonoidHom G G} (hφsurj : Function.Surjective φ) :
PreimagePreservesOpenNormalSubgroupsOfIndex (G := G) φPreimage along a surjective continuous endomorphism preserves open normal subgroups of fixed index.
Show proof
by
intro n U hU
refine ⟨?_, ?_, ?_, ?_⟩
· exact hU.1.comap φ.toMonoidHom
· exact hU.2.1.preimage φ.continuous_toFun
· exact Subgroup.quotient_finite_of_isOpen
(Subgroup.comap φ.toMonoidHom U) (hU.2.1.preimage φ.continuous_toFun)
· simpa [Subgroup.index_eq_card] using
(Subgroup.index_comap_of_surjective (H := U) hφsurj).trans hU.2.2.2Proof. 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. 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.
□theorem surjContinuousEndomorphismsAreAutomorphisms_of_topologicallyFinitelyGenerated
[IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
: TopologicallyFinitelyGenerated G →
∀ φ : ContinuousMonoidHom G G, Function.Surjective φ →
∃ e : G ≃ₜ* G, ∀ x : G, e x = φ xA surjective continuous endomorphism of a topologically finitely generated profinite group is automatically a continuous automorphism.
Show proof
by
intro hG
apply surjContinuousEndomorphismsAreAutomorphisms_of_finiteOpenNormalSubgroupsOfIndex
· exact openNormalSeparatesPoints_of_profinite (G := G)
· exact HasFiniteOpenSubgroupsOfIndex.toHasFiniteOpenNormalSubgroupsOfIndex
(h := hasFiniteOpenSubgroupsOfIndex_of_topologicallyFinitelyGenerated (G := G) hG)
· intro φ hφsurj
exact preimagePreservesOpenNormalSubgroupsOfIndex_of_surjective (G := G) hφsurjProof. 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.
□