ProCGroups.Abelian.TopologicalAbelianization
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
import
- Mathlib.Topology.Algebra.Group.TopologicalAbelianization
- ProCGroups.Topologies.TopologicallyCharacteristicSubgroups
def mkₜ
(G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
G →ₜ* TopologicalAbelianization G :=
{ toMonoidHom := QuotientGroup.mk' (Subgroup.closedCommutator G)
continuous_toFun := QuotientGroup.continuous_mk }The natural continuous quotient map to the topological abelianization.
abbrev mk
(G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
G →* TopologicalAbelianization G :=
(mkₜ G).toMonoidHomThe natural quotient homomorphism to the topological abelianization.
theorem ker_mk
(G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
(mk G).ker =
Subgroup.closedCommutator GThe kernel of the topological abelianization map is the closed commutator subgroup.
Show proof
by
exact QuotientGroup.ker_mk' _Proof. Unfold the topological abelianization as the quotient by the closed commutator subgroup. The quotient map kills commutators and is continuous, and any continuous homomorphism to a commutative \(T_1\) topological group descends because its kernel contains the closed commutator subgroup. Functoriality, Hom equivalences, category structure, and inverse-limit comparisons are checked on quotient representatives and by quotient extensionality.
□theorem mk_eq_one_iff
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
{x : G} :
mk G x = 1 ↔
x ∈ Subgroup.closedCommutator GA representative maps to \(1\) in the topological abelianization exactly when it lies in the closed commutator subgroup.
Show proof
by
exact QuotientGroup.eq_one_iff (N := Subgroup.closedCommutator G) xProof. Unfold the topological abelianization as the quotient by the closed commutator subgroup. The quotient map kills commutators and is continuous, and any continuous homomorphism to a commutative \(T_1\) topological group descends because its kernel contains the closed commutator subgroup. Functoriality, Hom equivalences, category structure, and inverse-limit comparisons are checked on quotient representatives and by quotient extensionality.
□@[simp] theorem closedCommutator_eq_bot_of_commGroup_t1
(G : Type u) [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G] :
Subgroup.closedCommutator G = ⊥In a commutative \(T_1\) topological group, the closed commutator subgroup is trivial.
Show proof
by
have hcomm : commutator G = ⊥ := by
rw [commutator_eq_bot_iff_center_eq_top, CommGroup.center_eq_top]
rw [Subgroup.closedCommutator, hcomm]
ext x
change x ∈ closure ({(1 : G)} : Set G) ↔ x = 1
rw [closure_singleton]
simp only [Set.mem_singleton_iff]Proof. Unfold the topological abelianization as the quotient by the closed commutator subgroup. The quotient map kills commutators and is continuous, and any continuous homomorphism to a commutative \(T_1\) topological group descends because its kernel contains the closed commutator subgroup. Functoriality, Hom equivalences, category structure, and inverse-limit comparisons are checked on quotient representatives and by quotient extensionality.
□theorem surjective_mk
(G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
Function.Surjective (mk G)The canonical map to the topological abelianization is surjective.
Show proof
QuotientGroup.mk'_surjective (Subgroup.closedCommutator G)Proof. Unfold the topological abelianization as the quotient by the closed commutator subgroup. The quotient map kills commutators and is continuous, and any continuous homomorphism to a commutative \(T_1\) topological group descends because its kernel contains the closed commutator subgroup. Functoriality, Hom equivalences, category structure, and inverse-limit comparisons are checked on quotient representatives and by quotient extensionality.
□instance instT2SpaceTopologicalAbelianization
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
T2Space (TopologicalAbelianization G) := by
letI : IsClosed (((Subgroup.closedCommutator G : Subgroup G) : Set G)) :=
Subgroup.isClosed_closedCommutator G
infer_instanceThe topological abelianization is Hausdorff because it is a quotient by the closed commutator subgroup.
noncomputable def lift
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
{A : Type v} [TopologicalSpace A] [CommGroup A] [T1Space A]
(f : G →ₜ* A) :
TopologicalAbelianization G →ₜ* A := by
have hclosedCommutator_le_ker :
Subgroup.closedCommutator G ≤ f.toMonoidHom.ker := by
have hcomm : commutator G ≤ f.toMonoidHom.ker := by
rw [commutator_eq_closure]
rw [Subgroup.closure_le]
rintro x ⟨g, h, rfl⟩
change f ⁅g, h⁆ = 1
simp only [commutatorElement_def, mul_assoc, map_mul, map_inv, mul_inv_cancel_comm_assoc, mul_inv_cancel]
have hkerClosed : IsClosed (((f.toMonoidHom.ker : Subgroup G) : Set G)) := by
change IsClosed (f ⁻¹' ({1} : Set A))
simpa using isClosed_singleton.preimage f.continuous_toFun
exact Subgroup.topologicalClosure_minimal
(s := commutator G) (t := f.toMonoidHom.ker) hcomm hkerClosed
exact QuotientGroup.liftₜ (Subgroup.closedCommutator G) f hclosedCommutator_le_kerA continuous homomorphism to a commutative \(T_1\) topological group factors through the topological abelianization.
@[simp] theorem lift_apply_mk
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
{A : Type v} [TopologicalSpace A] [CommGroup A] [T1Space A]
(f : G →ₜ* A) (x : G) :
lift f (mk G x) = f xThe lift from the topological abelianization evaluates on a quotient class by applying the original homomorphism.
Show proof
by
rflProof. Unfold the topological abelianization as the quotient by the closed commutator subgroup. The quotient map kills commutators and is continuous, and any continuous homomorphism to a commutative \(T_1\) topological group descends because its kernel contains the closed commutator subgroup. Functoriality, Hom equivalences, category structure, and inverse-limit comparisons are checked on quotient representatives and by quotient extensionality.
□@[ext] theorem hom_ext
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
{A : Type v} [TopologicalSpace A] [Group A]
(φ ψ : TopologicalAbelianization G →ₜ* A)
(h : ∀ x : G, φ (mk G x) = ψ (mk G x)) :
φ = ψContinuous homomorphisms out of the topological abelianization are equal when they agree after the quotient map.
Show proof
by
apply ContinuousMonoidHom.toMonoidHom_injective
apply MonoidHom.ext
intro x
exact Quotient.inductionOn' x hProof. Unfold the topological abelianization as the quotient by the closed commutator subgroup. The quotient map kills commutators and is continuous, and any continuous homomorphism to a commutative \(T_1\) topological group descends because its kernel contains the closed commutator subgroup. Functoriality, Hom equivalences, category structure, and inverse-limit comparisons are checked on quotient representatives and by quotient extensionality.
□theorem lift_unique
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
{A : Type v} [TopologicalSpace A] [CommGroup A] [T1Space A]
(f : G →ₜ* A)
(φ : TopologicalAbelianization G →ₜ* A)
(hφ : ∀ x : G, φ (mk G x) = f x) :
φ = lift fThe lift from the topological abelianization is uniquely determined by its composition with the quotient map.
Show proof
by
apply hom_ext
intro x
simpa using hφ xProof. Unfold the topological abelianization as the quotient by the closed commutator subgroup. The quotient map kills commutators and is continuous, and any continuous homomorphism to a commutative \(T_1\) topological group descends because its kernel contains the closed commutator subgroup. Functoriality, Hom equivalences, category structure, and inverse-limit comparisons are checked on quotient representatives and by quotient extensionality.
□noncomputable def homEquiv
(G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
(A : Type v) [TopologicalSpace A] [CommGroup A] [T1Space A] :
(TopologicalAbelianization G →ₜ* A) ≃ (G →ₜ* A) where
toFun φ := φ.comp (mkₜ G)
invFun f := lift f
left_inv φ := by
apply hom_ext
intro x
rfl
right_inv f := by
ext x
rflThe universal property of topological abelianization as a Hom equivalence for commutative \(T_1\) targets.
@[simp] theorem homEquiv_apply
(G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
(A : Type v) [TopologicalSpace A] [CommGroup A] [T1Space A]
(φ : TopologicalAbelianization G →ₜ* A) :
homEquiv G A φ = φ.comp (mkₜ G)The Hom-equivalence is evaluated by composing a map out of the topological abelianization with the quotient map from the original group.
Show proof
rflProof. Unfold the topological abelianization as the quotient by the closed commutator subgroup. The quotient map kills commutators and is continuous, and any continuous homomorphism to a commutative \(T_1\) topological group descends because its kernel contains the closed commutator subgroup. Functoriality, Hom equivalences, category structure, and inverse-limit comparisons are checked on quotient representatives and by quotient extensionality.
□@[simp] theorem homEquiv_symm_apply_mk
(G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
(A : Type v) [TopologicalSpace A] [CommGroup A] [T1Space A]
(f : G →ₜ* A) (x : G) :
(homEquiv G A).symm f (mk G x) = f xThe inverse Hom equivalence evaluates on the abelianization class of \(x\) as the original continuous homomorphism evaluated at \(x\).
Show proof
rflProof. Unfold the topological abelianization as the quotient by the closed commutator subgroup. The quotient map kills commutators and is continuous, and any continuous homomorphism to a commutative \(T_1\) topological group descends because its kernel contains the closed commutator subgroup. Functoriality, Hom equivalences, category structure, and inverse-limit comparisons are checked on quotient representatives and by quotient extensionality.
□noncomputable def map
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
{H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
(f : G →ₜ* H) :
TopologicalAbelianization G →ₜ* TopologicalAbelianization H :=
lift ((mkₜ H).comp f)A continuous homomorphism induces a continuous homomorphism on topological abelianizations.
@[simp] theorem map_apply_mk
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
{H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
(f : G →ₜ* H) (x : G) :
map f (mk G x) =
mk H (f x)The induced map on topological abelianizations is evaluated on quotient representatives.
Show proof
by
rflProof. Unfold the topological abelianization as the quotient by the closed commutator subgroup. The quotient map kills commutators and is continuous, and any continuous homomorphism to a commutative \(T_1\) topological group descends because its kernel contains the closed commutator subgroup. Functoriality, Hom equivalences, category structure, and inverse-limit comparisons are checked on quotient representatives and by quotient extensionality.
□@[simp] theorem map_comp_mk
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
{H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
(f : G →ₜ* H) :
(map f).toMonoidHom.comp (mk G) =
(mk H).comp f.toMonoidHomComposing the abelianization map with the quotient map recovers the quotient map after applying the original homomorphism.
Show proof
by
ext x
rflProof. Unfold the topological abelianization as the quotient by the closed commutator subgroup. The quotient map kills commutators and is continuous, and any continuous homomorphism to a commutative \(T_1\) topological group descends because its kernel contains the closed commutator subgroup. Functoriality, Hom equivalences, category structure, and inverse-limit comparisons are checked on quotient representatives and by quotient extensionality.
□@[simp] theorem map_id
(G : Type u) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
map
(ContinuousMonoidHom.id G) =
ContinuousMonoidHom.id (TopologicalAbelianization G)The map induced by the identity homomorphism is the identity on the topological abelianization.
Show proof
by
apply hom_ext
intro g
rflProof. Unfold the topological abelianization as the quotient by the closed commutator subgroup. The quotient map kills commutators and is continuous, and any continuous homomorphism to a commutative \(T_1\) topological group descends because its kernel contains the closed commutator subgroup. Functoriality, Hom equivalences, category structure, and inverse-limit comparisons are checked on quotient representatives and by quotient extensionality.
□@[simp] theorem map_comp
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
{H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
{K : Type _} [TopologicalSpace K] [Group K] [IsTopologicalGroup K]
(g : H →ₜ* K) (f : G →ₜ* H) :
map (g.comp f) =
(map g).comp (map f)Induced maps on topological abelianizations compose functorially.
Show proof
by
apply hom_ext
intro a
rflProof. Unfold the topological abelianization as the quotient by the closed commutator subgroup. The quotient map kills commutators and is continuous, and any continuous homomorphism to a commutative \(T_1\) topological group descends because its kernel contains the closed commutator subgroup. Functoriality, Hom equivalences, category structure, and inverse-limit comparisons are checked on quotient representatives and by quotient extensionality.
□noncomputable def congr
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
{H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
(e : G ≃ₜ* H) :
TopologicalAbelianization G ≃ₜ* TopologicalAbelianization H := by
let f := map e.toContinuousMonoidHom
let g := map e.symm.toContinuousMonoidHom
exact ContinuousMulEquiv.ofHomInv f g
(by
intro x
refine Quotient.inductionOn' x ?_
intro a
change
map e.symm.toContinuousMonoidHom
(map e.toContinuousMonoidHom
(mk G a)) =
mk G a
rw [map_apply_mk, map_apply_mk]
simp only [ContinuousMonoidHom.coe_toMonoidHom, ContinuousMulEquiv.toContinuousMonoidHom_apply,
ContinuousMulEquiv.symm_apply_apply, MonoidHom.coe_coe])
(by
intro y
refine Quotient.inductionOn' y ?_
intro b
change
map e.toContinuousMonoidHom
(map e.symm.toContinuousMonoidHom
(mk H b)) =
mk H b
rw [map_apply_mk, map_apply_mk]
simp only [ContinuousMonoidHom.coe_toMonoidHom, ContinuousMulEquiv.toContinuousMonoidHom_apply,
ContinuousMulEquiv.apply_symm_apply, MonoidHom.coe_coe])A topological group isomorphism induces an isomorphism on topological abelianizations.
@[simp] theorem congr_apply_mk
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
{H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
(e : G ≃ₜ* H) (x : G) :
congr e (mk G x) =
mk H (e x)The abelianization congruence induced by a continuous equivalence sends representatives to representatives.
Show proof
by
rflProof. Unfold the topological abelianization as the quotient by the closed commutator subgroup. The quotient map kills commutators and is continuous, and any continuous homomorphism to a commutative \(T_1\) topological group descends because its kernel contains the closed commutator subgroup. Functoriality, Hom equivalences, category structure, and inverse-limit comparisons are checked on quotient representatives and by quotient extensionality.
□theorem surjective_map_of_surjective
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
{H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
(f : G →ₜ* H) (hf : Function.Surjective f) :
Function.Surjective (map f)Surjective homomorphisms induce surjective maps on topological abelianizations.
Show proof
by
intro y
refine Quotient.inductionOn' y ?_
intro h
rcases hf h with ⟨g, rfl⟩
exact ⟨QuotientGroup.mk' (Subgroup.closedCommutator G) g, rfl⟩Proof. Unfold the topological abelianization as the quotient by the closed commutator subgroup. The quotient map kills commutators and is continuous, and any continuous homomorphism to a commutative \(T_1\) topological group descends because its kernel contains the closed commutator subgroup. Functoriality, Hom equivalences, category structure, and inverse-limit comparisons are checked on quotient representatives and by quotient extensionality.
□theorem injective_mk_of_commGroup
{G : Type u} [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G] :
Function.Injective (mk G)In a commutative \(T_1\) topological group, the natural map to the topological abelianization is injective.
Show proof
by
rw [← MonoidHom.ker_eq_bot_iff]
rw [ker_mk, closedCommutator_eq_bot_of_commGroup_t1]Proof. Unfold the topological abelianization as the quotient by the closed commutator subgroup. The quotient map kills commutators and is continuous, and any continuous homomorphism to a commutative \(T_1\) topological group descends because its kernel contains the closed commutator subgroup. Functoriality, Hom equivalences, category structure, and inverse-limit comparisons are checked on quotient representatives and by quotient extensionality.
□noncomputable def continuousMulEquivOfCommGroup
(G : Type u) [TopologicalSpace G] [CommGroup G] [IsTopologicalGroup G] [T1Space G] :
_root_.TopologicalAbelianization G ≃ₜ* G := by
let e : G ≃* _root_.TopologicalAbelianization G :=
MulEquiv.ofBijective (mk G)
⟨injective_mk_of_commGroup (G := G),
QuotientGroup.mk'_surjective (Subgroup.closedCommutator G)⟩
refine
{ toMulEquiv := e.symm
continuous_toFun := ?_
continuous_invFun := ?_ }
· refine
(QuotientGroup.isQuotientMap_mk
(Subgroup.closedCommutator G)).continuous_iff.2 ?_
change Continuous fun x : G => e.symm (e x)
simpa using (continuous_id : Continuous fun x : G => x)
· change Continuous fun x : G => mk G x
exact QuotientGroup.continuous_mkThe canonical continuous equivalence for commutative \(T_1\) groups.