Module

FiniteInvariantQuotients.lean

Nyll.ProCGroups.Abelian.FiniteInvariantQuotients

9 declarations indexed from sourceView source ↗

Module documentation

Finite invariant quotients

A finite group of continuous automorphisms admits arbitrarily small invariant open normal subgroups. The construction is the kernel of the product of the translated finite quotient maps; in particular, invariance is proved from the given action rather than supplied as additional data.

Imports3

Nyll.ProCGroups.ProC.OpenNormalSubgroups.Basic
Nyll.ProCGroups.ProC.OpenNormalSubgroups.BasisAtOne
Mathlib.Topology.Constructions

Imported by4

def

invariantOpenNormalCore

L31 ↗

ProCGroups.Abelian.invariantOpenNormalCore

Documentation

The intersection of all translates of an open normal subgroup under a finite continuous action, constructed as a continuous kernel.

Source context 5 commands

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

open scoped Topology
namespace ProCGroups.Abelian
universe u v
variable {C : Type u} [Group C] [Finite C]
variable {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]

Lean source · statement

def invariantOpenNormalCore
    (ρ : C →* MulAut A) (hρ : ∀ c : C, Continuous (ρ c))
    (U : OpenNormalSubgroup A) : OpenNormalSubgroup A

theorem

mem_invariantOpenNormalCore_iff

L53 ↗

ProCGroups.Abelian.mem_invariantOpenNormalCore_iff

Documentation

Membership in the invariant core is membership of every translate in the original open normal subgroup.

Source context 5 commands

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

open scoped Topology
namespace ProCGroups.Abelian
universe u v
variable {C : Type u} [Group C] [Finite C]
variable {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]

Lean source · statement

theorem mem_invariantOpenNormalCore_iff
    (ρ : C →* MulAut A) (hρ : ∀ c : C, Continuous (ρ c))
    (U : OpenNormalSubgroup A) (x : A) :
    x ∈ invariantOpenNormalCore ρ hρ U ↔ ∀ c : C, ρ c x ∈ U

theorem

invariantOpenNormalCore_le

L67 ↗

ProCGroups.Abelian.invariantOpenNormalCore_le

Documentation

The invariant core refines the original subgroup.

Source context 5 commands

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

open scoped Topology
namespace ProCGroups.Abelian
universe u v
variable {C : Type u} [Group C] [Finite C]
variable {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]

Lean source · statement

theorem invariantOpenNormalCore_le
    (ρ : C →* MulAut A) (hρ : ∀ c : C, Continuous (ρ c))
    (U : OpenNormalSubgroup A) :
    (invariantOpenNormalCore ρ hρ U : Subgroup A) ≤ (U : Subgroup A)

theorem

action_mem_invariantOpenNormalCore

L77 ↗

ProCGroups.Abelian.action_mem_invariantOpenNormalCore

Documentation

Every element of the acting group preserves the invariant core.

Source context 5 commands

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

open scoped Topology
namespace ProCGroups.Abelian
universe u v
variable {C : Type u} [Group C] [Finite C]
variable {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]

Lean source · statement

theorem action_mem_invariantOpenNormalCore
    (ρ : C →* MulAut A) (hρ : ∀ c : C, Continuous (ρ c))
    (U : OpenNormalSubgroup A) (c : C) {x : A}
    (hx : x ∈ invariantOpenNormalCore ρ hρ U) :
    ρ c x ∈ invariantOpenNormalCore ρ hρ U

theorem

map_invariantOpenNormalCore

L88 ↗

ProCGroups.Abelian.map_invariantOpenNormalCore

Documentation

An automorphism in the action maps the invariant core onto itself.

Source context 5 commands

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

open scoped Topology
namespace ProCGroups.Abelian
universe u v
variable {C : Type u} [Group C] [Finite C]
variable {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]

Lean source · statement

theorem map_invariantOpenNormalCore
    (ρ : C →* MulAut A) (hρ : ∀ c : C, Continuous (ρ c))
    (U : OpenNormalSubgroup A) (c : C) :
    (invariantOpenNormalCore ρ hρ U : Subgroup A).map (ρ c).toMonoidHom =
      (invariantOpenNormalCore ρ hρ U : Subgroup A)

def

invariantOpenNormalQuotientAction

L103 ↗

ProCGroups.Abelian.invariantOpenNormalQuotientAction

Documentation

The action induced on the quotient by the invariant open normal core.

Source context 5 commands

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

open scoped Topology
namespace ProCGroups.Abelian
universe u v
variable {C : Type u} [Group C] [Finite C]
variable {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]

Lean source · full declaration

def invariantOpenNormalQuotientAction
    (ρ : C →* MulAut A) (hρ : ∀ c : C, Continuous (ρ c))
    (U : OpenNormalSubgroup A) :
    C →* MulAut (A ⧸ (invariantOpenNormalCore ρ hρ U : Subgroup A)) where
  toFun c := QuotientGroup.congr
    (invariantOpenNormalCore ρ hρ U : Subgroup A)
    (invariantOpenNormalCore ρ hρ U : Subgroup A)
    (ρ c) (map_invariantOpenNormalCore ρ hρ U c)
  map_one' := by
    apply MulEquiv.ext
    intro q
    refine QuotientGroup.induction_on q ?_
    intro x
    change QuotientGroup.mk' (invariantOpenNormalCore ρ hρ U : Subgroup A) (ρ 1 x) =
      QuotientGroup.mk' (invariantOpenNormalCore ρ hρ U : Subgroup A) x
    rw [map_one, MulAut.one_apply]
  map_mul' := by
    intro c d
    apply MulEquiv.ext
    intro q
    refine QuotientGroup.induction_on q ?_
    intro x
    change QuotientGroup.mk' (invariantOpenNormalCore ρ hρ U : Subgroup A)
        (ρ (c * d) x) =
      QuotientGroup.mk' (invariantOpenNormalCore ρ hρ U : Subgroup A)
        (ρ c (ρ d x))
    rw [map_mul, MulAut.mul_apply]

theorem

invariantOpenNormalQuotientAction_apply_mk

L132 ↗

ProCGroups.Abelian.invariantOpenNormalQuotientAction_apply_mk

Documentation

The quotient projection is equivariant for the induced finite action.

Source context 5 commands

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

open scoped Topology
namespace ProCGroups.Abelian
universe u v
variable {C : Type u} [Group C] [Finite C]
variable {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]

Lean source · statement

theorem invariantOpenNormalQuotientAction_apply_mk
    (ρ : C →* MulAut A) (hρ : ∀ c : C, Continuous (ρ c))
    (U : OpenNormalSubgroup A) (c : C) (x : A) :
    invariantOpenNormalQuotientAction ρ hρ U c
        (QuotientGroup.mk' (invariantOpenNormalCore ρ hρ U : Subgroup A) x) =
      QuotientGroup.mk' (invariantOpenNormalCore ρ hρ U : Subgroup A) (ρ c x)

theorem

exists_invariantOpenNormalCore_not_mem

L145 ↗

ProCGroups.Abelian.exists_invariantOpenNormalCore_not_mem

Documentation

A nonidentity element of a profinite group can be excluded from an invariant open normal subgroup for any finite continuous action.

Source context 5 commands

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

open scoped Topology
namespace ProCGroups.Abelian
universe u v
variable {C : Type u} [Group C] [Finite C]
variable {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]

Lean source · statement

theorem exists_invariantOpenNormalCore_not_mem
    [CompactSpace A] [TotallyDisconnectedSpace A]
    (ρ : C →* MulAut A) (hρ : ∀ c : C, Continuous (ρ c))
    {x : A} (hx : x ≠ 1) :
    ∃ U : OpenNormalSubgroup A, x ∉ invariantOpenNormalCore ρ hρ U

theorem

exists_faithful_invariantOpenNormalQuotientAction

L162 ↗

ProCGroups.Abelian.exists_faithful_invariantOpenNormalQuotientAction

Documentation

A faithful finite continuous action on a profinite group remains faithful on a finite quotient by an invariant open normal subgroup. No commutativity of the original group is required.

Source context 5 commands

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

open scoped Topology
namespace ProCGroups.Abelian
universe u v
variable {C : Type u} [Group C] [Finite C]
variable {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A]

Lean source · statement

theorem exists_faithful_invariantOpenNormalQuotientAction
    [CompactSpace A] [TotallyDisconnectedSpace A]
    (ρ : C →* MulAut A) (hρ : ∀ c : C, Continuous (ρ c))
    (hfaithful : Function.Injective ρ) :
    ∃ U : OpenNormalSubgroup A,
      Function.Injective (invariantOpenNormalQuotientAction ρ hρ U)

Module documentation

Finite invariant quotients

Declarations