Module

PerfectKernel.lean

Nyll.Yamaguchi26SolvableCoverings.GroupTheory.PerfectKernel

2 declarations indexed from sourceView source ↗

Module documentation

定理 2.5 に用いる位相的完全核の群論

連続全射 f : G → Q に対し、Q の任意の開正規部分群 H の逆像上でアーベル化の写像が単射ならば、ker f は位相的完全である。証明では有限商 q : G → S ごとに N = q(ker f) を作り、S/N への写像を Q に降ろす。その核を H とすると、局所アーベル化の単射性から N = [N,N] が従う。最後に閉集合への所属を有限商で検出して核の完全性を得る。

ここにはスキームに関する仮定や結論を新しい field として追加していない。幾何学的な定理 2.5 への適用には、有限 étale 被覆の基本群と開部分群との比較から局所アーベル化の単射性を実際に導く必要がある。

Imports4

Nyll.ProCGroups.FiniteStepSolvableQuotients.ProsolvableCriterion
Nyll.ProCGroups.FiniteStepSolvableQuotients.Commutators.Basic
Nyll.ProCGroups.ProC.OpenNormalSubgroups.Separation
Mathlib.GroupTheory.IsPerfect

Imported by2

theorem

isPerfect_kernel_image_of_openNormalAbelianizationInjective

L37 ↗

Yamaguchi26SolvableCoverings.isPerfect_kernel_image_of_openNormalAbelianizationInjective

Documentation

局所アーベル化が単射である全射の核は、任意の離散商の中で完全群を像に持つ。

Source context 5 commands

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

noncomputable section
open scoped ProCGroupsSolvableQuotients
namespace Yamaguchi26SolvableCoverings
open ProCGroups.FiniteStepSolvableQuotients
universe u

Lean source · statement

theorem isPerfect_kernel_image_of_openNormalAbelianizationInjective
    {G Q S : Type u}
    [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [CompactSpace G]
    [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q] [T2Space Q]
    [TopologicalSpace S] [Group S] [DiscreteTopology S]
    (f : G →ₜ* Q) (hf : Function.Surjective f)
    (hAb : OpenNormalAbelianizationInjective f)
    (q : G →ₜ* S) (hq : Function.Surjective q) :
    Group.IsPerfect (f.ker.map q.toMonoidHom)

theorem

kernel_topologicallyPerfect_of_openNormalAbelianizationInjective

L114 ↗

Yamaguchi26SolvableCoverings.kernel_topologicallyPerfect_of_openNormalAbelianizationInjective