Descent of continuous group homomorphisms

A continuous group homomorphism descends through a quotient map precisely when its kernel contains the kernel of the quotient homomorphism. The construction uses ContinuousMonoidHom.quotientLift on the kernel quotient and Mathlib's QuotientGroup.quotientKerEquivOfSurjective to identify that quotient with the target. The quotient-map hypothesis ensures that the descended homomorphism is continuous.

Main results

• ContinuousMonoidHom.liftOfIsQuotientMap descends a continuous homomorphism through a quotient homomorphism.
• ContinuousMonoidHom.homEquivOfIsQuotientMap identifies continuous homomorphisms out of the quotient with continuous homomorphisms upstairs that kill the quotient kernel.

noncomputable def ContinuousMonoidHom.liftOfIsQuotientMap {G : Type u_1} {Q : Type u_2} {H : Type u_3} [Group G] [Group Q] [Monoid H] [TopologicalSpace G] [TopologicalSpace Q] [TopologicalSpace H] (p : G →ₜ* Q) (hp : Topology.IsQuotientMap ⇑p) (f : G →ₜ* H) (hf : (↑p).ker ≤ (↑f).ker) : Q →ₜ* H

Descend a continuous group homomorphism through a quotient homomorphism whose kernel it kills.

@[simp]

theorem ContinuousMonoidHom.liftOfIsQuotientMap_comp_apply {G : Type u_1} {Q : Type u_2} {H : Type u_3} [Group G] [Group Q] [Monoid H] [TopologicalSpace G] [TopologicalSpace Q] [TopologicalSpace H] (p : G →ₜ* Q) (hp : Topology.IsQuotientMap ⇑p) (f : G →ₜ* H) (hf : (↑p).ker ≤ (↑f).ker) (x : G) : (p.liftOfIsQuotientMap hp f hf) (p x) = f x

The descended continuous homomorphism agrees with the original homomorphism on every representative.

@[simp]

theorem ContinuousMonoidHom.liftOfIsQuotientMap_comp {G : Type u_1} {Q : Type u_2} {H : Type u_3} [Group G] [Group Q] [Monoid H] [TopologicalSpace G] [TopologicalSpace Q] [TopologicalSpace H] (p : G →ₜ* Q) (hp : Topology.IsQuotientMap ⇑p) (f : G →ₜ* H) (hf : (↑p).ker ≤ (↑f).ker) : (p.liftOfIsQuotientMap hp f hf).comp p = f

Composing the descended homomorphism with the quotient homomorphism recovers the original homomorphism.

theorem ContinuousMonoidHom.liftOfIsQuotientMap_unique {G : Type u_1} {Q : Type u_2} {H : Type u_3} [Group G] [Group Q] [Monoid H] [TopologicalSpace G] [TopologicalSpace Q] [TopologicalSpace H] (p : G →ₜ* Q) (hp : Topology.IsQuotientMap ⇑p) (f : G →ₜ* H) (hf : (↑p).ker ≤ (↑f).ker) (g : Q →ₜ* H) (hg : g.comp p = f) : g = p.liftOfIsQuotientMap hp f hf

A continuous homomorphism descended through a quotient homomorphism is uniquely determined by its composition with that quotient homomorphism.

noncomputable def ContinuousMonoidHom.homEquivOfIsQuotientMap {G : Type u_1} {Q : Type u_2} {H : Type u_3} [Group G] [Group Q] [Monoid H] [TopologicalSpace G] [TopologicalSpace Q] [TopologicalSpace H] (p : G →ₜ* Q) (hp : Topology.IsQuotientMap ⇑p) : (Q →ₜ* H) ≃ { f : G →ₜ* H // (↑p).ker ≤ (↑f).ker }

Precomposition with a quotient homomorphism identifies continuous homomorphisms on the quotient with continuous homomorphisms whose kernels contain the quotient kernel.

@[simp]

theorem ContinuousMonoidHom.homEquivOfIsQuotientMap_apply_coe {G : Type u_1} {Q : Type u_2} {H : Type u_3} [Group G] [Group Q] [Monoid H] [TopologicalSpace G] [TopologicalSpace Q] [TopologicalSpace H] (p : G →ₜ* Q) (hp : Topology.IsQuotientMap ⇑p) (f : Q →ₜ* H) : ↑((p.homEquivOfIsQuotientMap hp) f) = f.comp p

Evaluation of the forward quotient-homomorphism equivalence.

@[simp]

theorem ContinuousMonoidHom.homEquivOfIsQuotientMap_symm_apply {G : Type u_1} {Q : Type u_2} {H : Type u_3} [Group G] [Group Q] [Monoid H] [TopologicalSpace G] [TopologicalSpace Q] [TopologicalSpace H] (p : G →ₜ* Q) (hp : Topology.IsQuotientMap ⇑p) (f : { g : G →ₜ* H // (↑p).ker ≤ (↑g).ker }) : (p.homEquivOfIsQuotientMap hp).symm f = p.liftOfIsQuotientMap hp ↑f ⋯

Evaluation of the inverse quotient-homomorphism equivalence.