ProCGroups.Boundary.restriction_eq_one_of_topological_generator_isConj_inv_of_coprime_two
A continuous map to an abelian Hausdorff group is trivial on a topologically cyclic inertia group when the image of a topological generator has order prime to two and its ambient image is conjugate to its inverse.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups.Boundary
universe u v wLean source · statement
theorem restriction_eq_one_of_topological_generator_isConj_inv_of_coprime_two
{I : Type u} {G : Type v} {A : Type w}
[Group I] [TopologicalSpace I] [IsTopologicalGroup I]
[Group G] [TopologicalSpace G]
[CommGroup A] [TopologicalSpace A] [T2Space A]
(inertiaMap : I →ₜ* G) (q : G →ₜ* A) {gamma : I}
(hGenerates :
Generation.TopologicallyGenerates (G := I) ({gamma} : Set I))
(hConj : IsConj (inertiaMap gamma) (inertiaMap gamma)⁻¹)
(hCoprime : Nat.Coprime (orderOf (q (inertiaMap gamma))) 2) :
q.comp inertiaMap = 1