Module

TopologicalGeneration.lean

Nyll.GaloisCohomology.ProfiniteIntegers.TopologicalGeneration

10 declarations indexed from sourceView source ↗

Module documentation

normalized degree and Frobenius theory: topological generation

This file contains the small amount of topological-generation theory used in the construction of Frobenius fixed fields, next to its sole application.

Imports2

Mathlib.Topology.Algebra.ClopenNhdofOne
Mathlib.Topology.Algebra.ContinuousMonoidHom

Imported by6

def

TopologicallyGenerates

L32 ↗

ClassFormation.TopologicallyGenerates

Documentation

A set topologically generates a group when the closure of the abstract subgroup it generates is the whole group.

Source context 6 commands

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

namespace ClassFormation
open Set
open scoped Topology Pointwise
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def TopologicallyGenerates (X : Set G) : Prop

theorem

topologicallyGenerates_iff_dense

L37 ↗

ClassFormation.topologicallyGenerates_iff_dense

Documentation

Topological generation is equivalently density of the generated abstract subgroup.

Source context 6 commands

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

namespace ClassFormation
open Set
open scoped Topology Pointwise
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem topologicallyGenerates_iff_dense {X : Set G} :
    TopologicallyGenerates (G := G) X ↔
      Dense ((Subgroup.closure X : Subgroup G) : Set G)

def

closedSubgroupGenerated

L44 ↗

ClassFormation.closedSubgroupGenerated

Documentation

The closed subgroup topologically generated by a set.

Source context 6 commands

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

namespace ClassFormation
open Set
open scoped Topology Pointwise
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · full declaration

def closedSubgroupGenerated (X : Set G) : ClosedSubgroup G where
  toSubgroup := (Subgroup.closure X).topologicalClosure
  isClosed' := Subgroup.isClosed_topologicalClosure _

def

closedSubgroupGeneratedMap

L49 ↗

ClassFormation.closedSubgroupGeneratedMap

Documentation

The canonical family in the closed subgroup that it generates.

Source context 6 commands

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

namespace ClassFormation
open Set
open scoped Topology Pointwise
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

def closedSubgroupGeneratedMap {A : Type v} (φ : A → G) :
    A → (closedSubgroupGenerated (G := G) (Set.range φ) : Subgroup G)

theorem

closedSubgroupGeneratedMap_topologicallyGenerates

L57 ↗

ClassFormation.closedSubgroupGeneratedMap_topologicallyGenerates

Documentation

The canonical family topologically generates its closed generated subgroup.

Source context 6 commands

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

namespace ClassFormation
open Set
open scoped Topology Pointwise
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem closedSubgroupGeneratedMap_topologicallyGenerates {A : Type v}
    (φ : A → G) :
    TopologicallyGenerates
      (G := (closedSubgroupGenerated (G := G) (Set.range φ) : Subgroup G))
      (Set.range (closedSubgroupGeneratedMap (G := G) φ))

theorem

map_mem_closedSubgroupGenerated_image

L105 ↗

ClassFormation.map_mem_closedSubgroupGenerated_image

Documentation

Membership in a closed generated subgroup is preserved by a continuous homomorphism after mapping the generating set.

Source context 6 commands

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

namespace ClassFormation
open Set
open scoped Topology Pointwise
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem map_mem_closedSubgroupGenerated_image
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (φ : G →ₜ* H) {X : Set G} {y : G}
    (hy : y ∈ (closedSubgroupGenerated (G := G) X : Subgroup G)) :
    φ y ∈ (closedSubgroupGenerated (G := H) (φ '' X) : Subgroup H)

theorem

map_mem_closedSubgroupGenerated_singleton

L127 ↗

ClassFormation.map_mem_closedSubgroupGenerated_singleton

Documentation

The singleton form of functoriality of closed topological generation.

Source context 6 commands

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

namespace ClassFormation
open Set
open scoped Topology Pointwise
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem map_mem_closedSubgroupGenerated_singleton
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (φ : G →ₜ* H) (x : G) {y : G}
    (hy : y ∈
      (closedSubgroupGenerated (G := G) ({x} : Set G) : Subgroup G)) :
    φ y ∈
      (closedSubgroupGenerated (G := H) ({φ x} : Set H) : Subgroup H)

theorem

topologicallyGenerates_singleton_of_denseRange_mint

L140 ↗

ClassFormation.topologicallyGenerates_singleton_of_denseRange_mint

Documentation

A dense image of the infinite cyclic group is topologically generated by the image of 1.

Source context 6 commands

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

namespace ClassFormation
open Set
open scoped Topology Pointwise
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem topologicallyGenerates_singleton_of_denseRange_mint
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (f : Multiplicative ℤ →* H) (hf : DenseRange f) :
    TopologicallyGenerates
      (G := H) ({f (Multiplicative.ofAdd 1)} : Set H)

theorem

topologicallyGenerates_image_of_continuousSurjective

L174 ↗

ClassFormation.topologicallyGenerates_image_of_continuousSurjective

Documentation

Topological generation pushes forward along a continuous surjective homomorphism.

Source context 6 commands

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

namespace ClassFormation
open Set
open scoped Topology Pointwise
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem topologicallyGenerates_image_of_continuousSurjective
    {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (f : G →* H) (hf : Continuous f) (hfsurj : Function.Surjective f)
    {X : Set G} (hX : TopologicallyGenerates (G := G) X) :
    TopologicallyGenerates (G := H) (f '' X)

theorem

topologicallyGenerates_quotient_image

L191 ↗

ClassFormation.topologicallyGenerates_quotient_image

Documentation

Topological generation descends to a quotient by a normal subgroup.

Source context 6 commands

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

namespace ClassFormation
open Set
open scoped Topology Pointwise
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem topologicallyGenerates_quotient_image
    (N : Subgroup G) [N.Normal]
    {X : Set G} (hX : TopologicallyGenerates (G := G) X) :
    TopologicallyGenerates
      (G := G ⧸ N) ((QuotientGroup.mk' N) '' X)

Module documentation

normalized degree and Frobenius theory: topological generation

Declarations