ProCGroups.Abelian.TopologicalAbelianizationFunctoriality
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
structure T1CommTopGrp where
carrier : Type uBundled commutative \(T_1\) topological groups with continuous homomorphisms.
instance instCoeSort : CoeSort T1CommTopGrp (Type u) where
coe G := G.carrierThe category object coerces to its underlying type.
abbrev of (G : Type u) [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G]
[T1Space G] : T1CommTopGrp where
carrier := GBundle an unbundled commutative \(T_1\) topological group.
structure Hom (G H : T1CommTopGrp.{u}) where
hom' : G →ₜ* HMorphisms of commutative \(T_1\) topological groups are continuous homomorphisms.
instance instCategory : Category T1CommTopGrp where
Hom G H := Hom G H
id G := ⟨ContinuousMonoidHom.id G⟩
comp f g := ⟨g.hom'.comp f.hom'⟩Commutative topological groups form a category.
instance instConcreteCategory : ConcreteCategory T1CommTopGrp (fun G H => G →ₜ* H) where
hom f := f.hom'
ofHom f := ⟨f⟩The category of \(T_1\) commutative topological groups has the concrete category structure inherited from its underlying type.
abbrev Hom.hom {G H : T1CommTopGrp.{u}} (f : G ⟶ H) : G →ₜ* H :=
ConcreteCategory.hom (C := T1CommTopGrp) fThe underlying continuous homomorphism of a morphism.
instance instCoeFunHom {G H : T1CommTopGrp.{u}} : CoeFun (G ⟶ H) (fun _ => G → H) where
coe f := f.homA morphism coerces to its underlying continuous homomorphism.
@[simp] theorem hom_id {G : T1CommTopGrp.{u}} :
(𝟙 G : G ⟶ G).hom = ContinuousMonoidHom.id GThe underlying homomorphism of the identity morphism is the identity continuous homomorphism.
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 hom_comp {G H K : T1CommTopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) :
(f ≫ g).hom = g.hom.comp f.homThe underlying homomorphism of a composite is the composite of underlying homomorphisms.
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 comp_apply {G H K : T1CommTopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) (x : G) :
(f ≫ g) x = g (f x)The composite map is computed pointwise by applying the constituent coordinate formulas in succession.
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.
□@[ext] theorem hom_ext {G H : T1CommTopGrp.{u}} {f g : G ⟶ H} (h : f.hom = g.hom) :
f = gMorphisms in T1CommTopGrp are equal when their underlying continuous homomorphisms are equal.
Show proof
Hom.ext 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.
□abbrev ofHom {G H : Type u}
[CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] [T1Space G]
[CommGroup H] [TopologicalSpace H] [IsTopologicalGroup H] [T1Space H]
(f : G →ₜ* H) : of G ⟶ of H :=
ConcreteCategory.ofHom fBundle a continuous homomorphism as a commutative \(T_1\) topological-group morphism.
def t1CommTopGrpForgetToTopGrp : T1CommTopGrp.{u} ⥤ TopGrp.{u} where
obj G := TopGrp.of G
map f := TopGrp.ofHom f.hom
map_id G := by
apply TopGrp.hom_ext
rfl
map_comp f g := by
apply TopGrp.hom_ext
rflForget the \(T_1\) and commutativity structure of a bundled commutative \(T_1\) topological group.
def t1CommTopGrpForgetToCommTopGrp : T1CommTopGrp.{u} ⥤ CommTopGrp.{u} where
obj G := CommTopGrp.of G
map f := CommTopGrp.ofHom f.hom
map_id G := by
apply CommTopGrp.hom_ext
rfl
map_comp f g := by
apply CommTopGrp.hom_ext
rflForget only the \(T_1\) structure of a bundled commutative \(T_1\) topological group.
noncomputable def topologicalAbelianizationFunctor : TopGrp.{u} ⥤ CommTopGrp.{u} where
obj G := CommTopGrp.of (TopologicalAbelianization G)
map {G H} f := CommTopGrp.ofHom (TopologicalAbelianization.map f.hom)
map_id G := by
apply CommTopGrp.hom_ext
exact TopologicalAbelianization.map_id G
map_comp f g := by
apply CommTopGrp.hom_ext
exact TopologicalAbelianization.map_comp g.hom f.homTopological abelianization as a functor from topological groups to commutative topological groups.
@[simp] theorem topologicalAbelianizationFunctor_map_apply_mk
{G H : TopGrp.{u}} (f : G ⟶ H) (x : G) :
topologicalAbelianizationFunctor.map f (TopologicalAbelianization.mk G x) =
TopologicalAbelianization.mk H (f x)The induced map on topological abelianizations sends a representative class to the class of its image.
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 topologicalAbelianizationT1Functor : TopGrp.{u} ⥤ T1CommTopGrp.{u} where
obj G := T1CommTopGrp.of (TopologicalAbelianization G)
map {G H} f := T1CommTopGrp.ofHom (TopologicalAbelianization.map f.hom)
map_id G := by
apply T1CommTopGrp.hom_ext
exact TopologicalAbelianization.map_id G
map_comp f g := by
apply T1CommTopGrp.hom_ext
exact TopologicalAbelianization.map_comp g.hom f.homTopological abelianization as a functor from topological groups to commutative \(T_1\) topological groups.
@[simp] theorem topologicalAbelianizationT1Functor_map_apply_mk
{G H : TopGrp.{u}} (f : G ⟶ H) (x : G) :
topologicalAbelianizationT1Functor.map f (TopologicalAbelianization.mk G x) =
TopologicalAbelianization.mk H (f x)The induced map on topological abelianizations sends a representative class to the class of its image.
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 topologicalAbelianizationHomEquiv
(G : TopGrp.{u}) (A : CommTopGrp.{u}) [T1Space A] :
(topologicalAbelianizationFunctor.obj G ⟶ A) ≃
(G ⟶ commTopGrpForgetToTopGrp.obj A) where
toFun φ := TopGrp.ofHom (φ.hom.comp (TopologicalAbelianization.mkₜ G))
invFun f := CommTopGrp.ofHom (TopologicalAbelianization.lift f.hom)
left_inv φ := by
apply CommTopGrp.hom_ext
apply TopologicalAbelianization.hom_ext
intro x
rfl
right_inv f := by
apply TopGrp.hom_ext
ext x
rflCategory-level Hom equivalence expressing the universal property of topological abelianization for commutative \(T_1\) targets.
@[simp] theorem topologicalAbelianizationHomEquiv_apply_hom
(G : TopGrp.{u}) (A : CommTopGrp.{u}) [T1Space A]
(φ : topologicalAbelianizationFunctor.obj G ⟶ A) :
(topologicalAbelianizationHomEquiv G A φ).hom =
φ.hom.comp (TopologicalAbelianization.mkₜ G)The topological-abelianization hom equivalence evaluates a homomorphism by its induced map on representatives.
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 topologicalAbelianizationHomEquiv_symm_apply_mk
(G : TopGrp.{u}) (A : CommTopGrp.{u}) [T1Space A]
(f : G ⟶ commTopGrpForgetToTopGrp.obj A) (x : G) :
(topologicalAbelianizationHomEquiv G A).symm f
(TopologicalAbelianization.mk G x) = f xThe inverse topological-abelianization hom equivalence sends a coset representative to the corresponding homomorphism value.
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 topologicalAbelianizationTopMulEquiv
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
TopologicalAbelianization ↥((⊤ : OpenSubgroup G) : Subgroup G) ≃ₜ*
TopologicalAbelianization G :=
TopologicalAbelianization.congr
(G := ↥((⊤ : OpenSubgroup G) : Subgroup G))
(H := G)
(OpenSubgroup.topContinuousMulEquiv G)The topological abelianization of the \(\top\) open subgroup is canonically the same as the topological abelianization of the ambient group.
@[simp] theorem topologicalAbelianizationTopMulEquiv_apply_mk
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
(x : ↥((⊤ : OpenSubgroup G) : Subgroup G)) :
topologicalAbelianizationTopMulEquiv
(G := G) (TopologicalAbelianization.mk ↥((⊤ : OpenSubgroup G) : Subgroup G) x) =
TopologicalAbelianization.mk G x.1The abelianization equivalence for a topological group equivalence sends representatives to representatives.
Show proof
by
simpa [topologicalAbelianizationTopMulEquiv] using
(TopologicalAbelianization.congr_apply_mk
(OpenSubgroup.topContinuousMulEquiv G) x)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 quotientConjugationTopologicalAbelianizationMap
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
(N : Subgroup G) [N.Normal] :
(G ⧸ N) →* MulAut (TopologicalAbelianization N) := by
let K : Subgroup N := Subgroup.closedCommutator N
have hKchar : K.TopologicallyCharacteristic :=
Subgroup.closedCommutator_topologicallyCharacteristic (G := N)
exact ProCGroups.Topologies.quotientConjugationOnTopologicallyCharacteristicQuotient
(G := G) N K
(fun n x => by
have hcomm :
⁅n, x⁆ ∈ Subgroup.closedCommutator N :=
Subgroup.commutator_le_closedCommutator N
(Subgroup.commutator_mem_commutator (Subgroup.mem_top n) (Subgroup.mem_top x))
have hconj : (MulAut.conjNormal (n : G)) x = n * x * n⁻¹ := by
ext
simp only [MulAut.conjNormal_apply, Subgroup.coe_mul, InvMemClass.coe_inv]
rw [hconj]
simpa [K, commutatorElement_def, mul_assoc] using hcomm)The quotient G/N acts on the topological abelianization of N by conjugation.
noncomputable def conjugationTopologicalAbelianizationContinuousAut
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
(N : Subgroup G) [N.Normal] (g : G) :
TopologicalAbelianization N ≃ₜ* TopologicalAbelianization N :=
TopologicalAbelianization.congr (Subgroup.conjNormalContinuousMulEquiv (G := G) N g)The continuous self-equivalence of topological abelianization induced by conjugation by a representative.
@[simp] theorem conjugationTopologicalAbelianizationContinuousAut_toMulAut_apply_mk
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
(N : Subgroup G) [N.Normal] (g : G) (n : N) :
conjugationTopologicalAbelianizationContinuousAut (G := G) N g
(TopologicalAbelianization.mk N n) =
quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
(QuotientGroup.mk' N g) (TopologicalAbelianization.mk N n)The representative-wise continuous automorphism has the same underlying algebraic action as quotientConjugationTopologicalAbelianizationMap.
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 quotientConjugationTopologicalAbelianizationMap_mk_apply_mk
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
(N : Subgroup G) [N.Normal] (g : G) (n : N) :
quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
(QuotientGroup.mk' N g) (TopologicalAbelianization.mk N n) =
TopologicalAbelianization.mk N ((MulAut.conjNormal g) n)The conjugation action on a quotient induces the expected map on topological abelianization representatives.
Show proof
by
dsimp [quotientConjugationTopologicalAbelianizationMap, TopologicalAbelianization.mk,
TopologicalAbelianization.mkₜ]
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 quotientConjugationTopologicalAbelianizationMap_mk_eq_one_of_commutator_mem_closure
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
(N : Subgroup G) [N.Normal] {x : G}
(hx :
∀ n : N,
(((MulAut.conjNormal x) n) * n⁻¹ : N) ∈ Subgroup.closedCommutator N) :
quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
(QuotientGroup.mk' N x) = 1If every commutator correction lies in the closed commutator subgroup, the induced conjugation action on the topological abelianization is trivial.
Show proof
by
ext a
obtain ⟨n, rfl⟩ := QuotientGroup.mk'_surjective (Subgroup.closedCommutator N) a
exact
(QuotientGroup.eq_iff_div_mem (N := Subgroup.closedCommutator N)
(x := (MulAut.conjNormal x) n) (y := n)).2 (by
simpa [div_eq_mul_inv] using hx n)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 quotientConjugationTopologicalAbelianizationMap_mk_apply_mk_eq_iff
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
(N : Subgroup G) [N.Normal] {x : G} {n : N} :
quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
(QuotientGroup.mk' N x) (TopologicalAbelianization.mk N n) =
TopologicalAbelianization.mk N n ↔
(((MulAut.conjNormal x) n) * n⁻¹ : N) ∈ Subgroup.closedCommutator NThe conjugation action fixes a representative exactly when the correction term lies in the closed commutator subgroup.
Show proof
by
rw [quotientConjugationTopologicalAbelianizationMap_mk_apply_mk]
simpa [div_eq_mul_inv] using
(QuotientGroup.eq_iff_div_mem
(N := Subgroup.closedCommutator N)
(x := (MulAut.conjNormal x) n) (y := n))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 quotientConjugationTopologicalAbelianizationMap_mk_eq_one_iff
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
(N : Subgroup G) [N.Normal] {x : G} :
quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
(QuotientGroup.mk' N x) = 1 ↔
∀ n : N,
(((MulAut.conjNormal x) n) * n⁻¹ : N) ∈ Subgroup.closedCommutator NThe induced conjugation action is trivial exactly when every correction term lies in the closed commutator subgroup.
Show proof
by
constructor
· intro h n
have hpoint :=
congrArg
(fun φ : MulAut (TopologicalAbelianization N) => φ (TopologicalAbelianization.mk N n))
h
exact
(quotientConjugationTopologicalAbelianizationMap_mk_apply_mk_eq_iff
(G := G) (N := N) (x := x) (n := n)).1 (by simpa using hpoint)
· intro hx
exact quotientConjugationTopologicalAbelianizationMap_mk_eq_one_of_commutator_mem_closure
(G := G) (N := N) (x := x) hxProof. 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 quotientConjugationTopologicalAbelianizationMap_mk_eq_one_of_mem_center
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
(N : Subgroup G) [N.Normal] {x : G} (hx : x ∈ Subgroup.center G) :
quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
(QuotientGroup.mk' N x) = 1Central elements act trivially on the topological abelianization of a normal subgroup.
Show proof
by
apply quotientConjugationTopologicalAbelianizationMap_mk_eq_one_of_commutator_mem_closure
(G := G) (N := N)
intro n
have hxn : x * (n : G) = (n : G) * x := by
exact (Subgroup.mem_center_iff.mp hx (n : G)).symm
have hconj : MulAut.conjNormal x n = n := by
ext
rw [MulAut.conjNormal_apply]
simp only [hxn, mul_assoc, mul_inv_cancel, mul_one]
simp only [hconj, mul_inv_cancel, one_mem]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 quotientConjAbMap_apply_mk_of_commute
{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
(N : Subgroup G) [N.Normal] {g : G} {x : N}
(hgx : g * (x : G) = (x : G) * g) :
quotientConjugationTopologicalAbelianizationMap (G := G) (N := N)
(QuotientGroup.mk' N g) (TopologicalAbelianization.mk N x) =
TopologicalAbelianization.mk N xIf a representative commutes with an element of N, then the induced action fixes its class in the topological abelianization.
Show proof
by
have hconj : (MulAut.conjNormal g) x = x := by
ext
rw [MulAut.conjNormal_apply]
simp only [hgx, mul_assoc, mul_inv_cancel, mul_one]
rw [quotientConjugationTopologicalAbelianizationMap_mk_apply_mk, hconj]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 subgroupImageInTopologicalAbelianization
{Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
(S : Subgroup Q) (U : OpenNormalSubgroup Q) :
Subgroup (TopologicalAbelianization ↥(U : Subgroup Q)) :=
(((S ⊓ (U : Subgroup Q)).subgroupOf (U : Subgroup Q)).map
(TopologicalAbelianization.mk ↥(U : Subgroup Q)))The image of \(S\cap U\) in the topological abelianization of \(U\).
@[simp] theorem mem_subgroupImageInTopologicalAbelianization_iff
{Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
(S : Subgroup Q) (U : OpenNormalSubgroup Q)
(y : TopologicalAbelianization ↥(U : Subgroup Q)) :
y ∈ subgroupImageInTopologicalAbelianization (Q := Q) S U ↔
∃ x : ↥(U : Subgroup Q), (x : Q) ∈ S ∧ TopologicalAbelianization.mk _ x = yMembership in the subgroup image inside the topological abelianization is equivalent to the displayed coordinate condition.
Show proof
by
simp only [subgroupImageInTopologicalAbelianization, ContinuousMonoidHom.coe_toMonoidHom,
Subgroup.inf_subgroupOf_right, Subgroup.mem_map, Subgroup.mem_subgroupOf, MonoidHom.coe_coe, Subtype.exists,
OpenSubgroup.mem_toSubgroup, exists_and_left]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 subgroupImageInTopologicalAbelianization_mono_left
{Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
{S T : Subgroup Q} (hST : S ≤ T) (U : OpenNormalSubgroup Q) :
subgroupImageInTopologicalAbelianization (Q := Q) S U ≤
subgroupImageInTopologicalAbelianization (Q := Q) T UEnlarging the ambient subgroup \(S\) enlarges its image in the abelianization of \(U\).
Show proof
by
intro y hy
rcases (mem_subgroupImageInTopologicalAbelianization_iff (Q := Q) S U y).1 hy with
⟨x, hxS, hxy⟩
exact (mem_subgroupImageInTopologicalAbelianization_iff (Q := Q) T U y).2
⟨x, hST hxS, hxy⟩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 topologicalAbelianizationMapOfOpenNormalSubgroupLe
{Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
{U V : OpenNormalSubgroup Q} (hUV : (U : Subgroup Q) ≤ (V : Subgroup Q)) :
TopologicalAbelianization ↥(U : Subgroup Q) →ₜ*
TopologicalAbelianization ↥(V : Subgroup Q) :=
TopologicalAbelianization.map
{ toMonoidHom := Subgroup.inclusion hUV
continuous_toFun := by
apply Continuous.subtype_mk
exact continuous_subtype_val }An inclusion of open normal subgroups induces the corresponding map on topological abelianizations.
@[simp] theorem topologicalAbelianizationMapOfOpenNormalSubgroupLe_apply_mk
{Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
{U V : OpenNormalSubgroup Q} (hUV : (U : Subgroup Q) ≤ (V : Subgroup Q))
(x : ↥(U : Subgroup Q)) :
topologicalAbelianizationMapOfOpenNormalSubgroupLe (Q := Q) hUV
(TopologicalAbelianization.mk ↥(U : Subgroup Q) x) =
TopologicalAbelianization.mk ↥(V : Subgroup Q) ⟨x.1, hUV x.2⟩The induced map on topological abelianizations sends a representative class to the class of its image.
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.
□theorem subgroupImageInTopologicalAbelianization_map_le_of_openNormalSubgroup_le
{Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
(S : Subgroup Q) {U V : OpenNormalSubgroup Q}
(hUV : (U : Subgroup Q) ≤ (V : Subgroup Q)) :
(subgroupImageInTopologicalAbelianization (Q := Q) S U).map
(topologicalAbelianizationMapOfOpenNormalSubgroupLe (Q := Q) hUV).toMonoidHom ≤
subgroupImageInTopologicalAbelianization (Q := Q) S VUnder an inclusion U \(\leq\) V, the image from U maps into the image from V.
Show proof
by
intro y hy
rcases hy with ⟨x, hx, rfl⟩
rcases (mem_subgroupImageInTopologicalAbelianization_iff (Q := Q) S U x).1 hx with
⟨a, haS, hax⟩
rw [← hax]
exact (mem_subgroupImageInTopologicalAbelianization_iff (Q := Q) S V _).2
⟨⟨a.1, hUV a.2⟩, haS, 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 subgroupImageInTopologicalAbelianization_le_comap_of_openNormalSubgroup_le
{Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
(S : Subgroup Q) {U V : OpenNormalSubgroup Q}
(hUV : (U : Subgroup Q) ≤ (V : Subgroup Q)) :
subgroupImageInTopologicalAbelianization (Q := Q) S U ≤
(subgroupImageInTopologicalAbelianization (Q := Q) S V).comap
(topologicalAbelianizationMapOfOpenNormalSubgroupLe (Q := Q) hUV).toMonoidHomComap form of subgroupImageInTopologicalAbelianization_map_le_of_openNormalSubgroup_le.
Show proof
Subgroup.map_le_iff_le_comap.mp
(subgroupImageInTopologicalAbelianization_map_le_of_openNormalSubgroup_le
(Q := Q) S hUV)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.
□def FiniteAbstractIndex
{Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
(S K : Subgroup Q) : Prop :=
∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
Finite
((TopologicalAbelianization ↥(U : Subgroup Q)) ⧸
subgroupImageInTopologicalAbelianization (Q := Q) S U)The image of \(S\) has finite abstract index in the topological abelianization of every open normal supergroup of \(K\).
noncomputable def closedSubgroupImageInTopologicalAbelianization
{Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
(S : Subgroup Q) (U : OpenNormalSubgroup Q) :
Subgroup (TopologicalAbelianization ↥(U : Subgroup Q)) :=
(subgroupImageInTopologicalAbelianization (Q := Q) S U).topologicalClosureThe topological closure of the image of \(S \cap U\) in the topological abelianization of \(U\).
@[simp] theorem closedSubgroupImageInTopologicalAbelianization_eq_topologicalClosure
{Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
(S : Subgroup Q) (U : OpenNormalSubgroup Q) :
closedSubgroupImageInTopologicalAbelianization (Q := Q) S U =
(subgroupImageInTopologicalAbelianization (Q := Q) S U).topologicalClosureThe image of a closed subgroup in the topological abelianization is the corresponding topological closure.
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.
□def OpenClosure
{Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
(S K : Subgroup Q) : Prop :=
∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
IsOpen
((closedSubgroupImageInTopologicalAbelianization (Q := Q) S U :
Subgroup (TopologicalAbelianization ↥(U : Subgroup Q))) : Set
(TopologicalAbelianization ↥(U : Subgroup Q)))The closed image of \(S\) is open in every open normal supergroup of \(K\).
def FiniteTopologicalIndex
{Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
(S K : Subgroup Q) : Prop :=
∀ U : OpenNormalSubgroup Q, K ≤ (U : Subgroup Q) →
IsClosed
((subgroupImageInTopologicalAbelianization (Q := Q) S U :
Subgroup (TopologicalAbelianization ↥(U : Subgroup Q))) : Set
(TopologicalAbelianization ↥(U : Subgroup Q))) ∧
Finite
((TopologicalAbelianization ↥(U : Subgroup Q)) ⧸
subgroupImageInTopologicalAbelianization (Q := Q) S U)The image of \(S\) is closed and has finite quotient in every open normal supergroup of \(K\).
theorem finiteAbstractIndex_of_finiteTopologicalIndex
{Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
{S K : Subgroup Q}
(h : FiniteTopologicalIndex (Q := Q) S K) :
FiniteAbstractIndex (Q := Q) S KFinite topological index includes finite abstract index as its quotient-size component.
Show proof
fun U hKU => (h U hKU).2Proof. 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.
□