NYLL
Module

ClosedNormalGeneration.lean

Nyll.EtaleFundamentalGroups.Inertia.ClosedNormalGeneration
2 declarations indexed from sourceView source ↗

Module documentation

閉正規生成部分群と、それを殺す有限商

profinite 群の部分集合 s が生成する閉正規部分群は、s を含む全ての開正規部分群の 共通部分である。開正規部分群は有限商への核なので、これは「生成元を殺す有限商の 核を交わす」という記述との比較である。

惰性群の和集合を s に取ると、原稿1.1の閉正規生成部分群に適用できる。 ただし、この群論だけで strict henselization の基本群の像を正規化の固定部分群と 同一視できるわけではなく、その幾何学的比較は別途必要である。

Imports5
Imported by2

Declarations

theorem

topologicalClosure_normalClosure_eq_iInf_openNormal

L33 ↗
EtaleFundamentalGroups.Inertia.topologicalClosure_normalClosure_eq_iInf_openNormal
Documentation

A closed normal subgroup generated by s is determined by the finite quotients that kill every element of s.

Source context 3 commands

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

open CategoryTheory CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u
Lean source · statement
theorem topologicalClosure_normalClosure_eq_iInf_openNormal
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (s : Set G) :
    (Subgroup.normalClosure s).topologicalClosure =
      ⨅ (N : OpenNormalSubgroup G) (_hs : s ⊆ (N : Set G)), (N : Subgroup G)
theorem

topologicalClosure_normalClosure_eq_iInf_galoisQuotient

L65 ↗
EtaleFundamentalGroups.Inertia.topologicalClosure_normalClosure_eq_iInf_galoisQuotient
Documentation

In a Galois category, the same closed normal subgroup is the intersection of the kernels of pointed Galois quotients that kill its generators. This uses the actual correspondence between open normal subgroups and pointed Galois objects, with no restriction on the universe of the fiber functor.

Source context 3 commands

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

open CategoryTheory CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups.Inertia
universe u
Lean source · full declaration
theorem topologicalClosure_normalClosure_eq_iInf_galoisQuotient
    {C : Type*} [Category C] [GaloisCategory C]
    (F : C ⥤ FintypeCat) [FiberFunctor F]
    (s : Set (Aut F)) :
    (Subgroup.normalClosure s).topologicalClosure =
      ⨅ (A : C) (hA : IsGalois A) (a : F.obj A),
        letI : IsGalois A := hA
        ⨅ (_hs : s ⊆
          (galoisObjectQuotientMonoidHom
            F (Aut F) A a).ker),
          (galoisObjectQuotientMonoidHom
            F (Aut F) A a).ker := by
  apply le_antisymm
  · apply le_iInf
    intro A
    apply le_iInf
    intro hA
    let : IsGalois A := hA
    apply le_iInf
    intro a
    apply le_iInf
    intro hs
    apply Subgroup.topologicalClosure_minimal (Subgroup.normalClosure s)
      (Subgroup.normalClosure_le_normal hs)
    rw [galoisObjectQuotientMonoidHom_ker]
    exact Subgroup.isClosed_of_isOpen _
      (stabilizer_isOpen (Aut F) a)
  · rw [topologicalClosure_normalClosure_eq_iInf_openNormal]
    apply le_iInf
    intro U
    apply le_iInf
    intro hsU g hg
    obtain ⟨A, hA, a, ha⟩ :=
      exists_galois_object_point_stabilizer_eq_any_universe F U
    let : IsGalois A := hA
    have hker :
        (galoisObjectQuotientMonoidHom
          F (Aut F) A a).ker = (U : Subgroup (Aut F)) :=
      (galoisObjectQuotientMonoidHom_ker
        F (Aut F) A a).trans ha
    have hs : s ⊆
        (galoisObjectQuotientMonoidHom
          F (Aut F) A a).ker := by
      rw [hker]
      exact hsU
    simp only [Subgroup.mem_iInf] at hg
    have hgker := hg A hA a hs
    rw [hker] at hgker
    exact hgker

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.