Module

Normalizer.lean

Nyll.AnabelianGeometry.CuspidalInertia.Normalizer

1 declaration indexed from sourceView source ↗

Module documentation

Normalizers detected by abelian images

If a subgroup embeds into an abelian image of the ambient group, its normalizer centralizes it. This supplies the abelianization step in self-normalization arguments for boundary inertia. No assertion about centralizers of free profinite generators is assumed to have been proved here.

Imports1

Mathlib.GroupTheory.Subgroup.Centralizer

Imported by1

Nyll.AnabelianGeometry.CuspidalInertia.All

theorem

normalizer_eq_centralizer_of_injective_abelian_image

L25 ↗

AnabelianGeometry.CuspidalInertia.normalizer_eq_centralizer_of_injective_abelian_image

Documentation

An injective abelian image forces each normalizing element to act trivially.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AnabelianGeometry.CuspidalInertia
universe u v
variable {G : Type u} [Group G] {A : Type v} [CommGroup A]

Lean source · statement

theorem normalizer_eq_centralizer_of_injective_abelian_image
    (I : Subgroup G) (f : G →* A) (hf : Set.InjOn f (I : Set G)) :
    Subgroup.normalizer (I : Set G) = Subgroup.centralizer (I : Set G)

Module documentation

Normalizers detected by abelian images

Declarations

normalizer_eq_centralizer_of_injective_abelian_image