NYLL
Module

EmbeddingProblems.lean

Nyll.ProCGroups.FreeProC.Characterization.EmbeddingProblems
6 declarations indexed from sourceView source ↗

Module documentation

Pro C Groups / Free pro-C / Characterization / Embedding Problems

This module defines topological embedding problems, their weak and proper solutions, and the finite split lifting properties used in freeness criteria.

Imports2
Imported by7

Declarations

structure

TopologicalEmbeddingProblem

L27 ↗
ProCGroups.FreeProC.Characterization.TopologicalEmbeddingProblem
Documentation

A topological embedding problem for a topological group. Finiteness and finite-class conditions are expressed by the predicates below instead of parallel wrapper structures.

Source context 4 commands

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

namespace ProCGroups.FreeProC.Characterization
open ProCGroups.FreeProC
universe u
section EmbeddingProblems
Lean source · full declaration
structure TopologicalEmbeddingProblem
    (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] where
  /-- The covering topological group through which a solution must lift. -/
  A : TopGrp.{u}
  /-- The common target of the embedding-problem epimorphism and the prescribed map from `G`. -/
  B : TopGrp.{u}
  /-- The continuous homomorphism from the covering group `A` onto `B`. -/
  α : A →ₜ* B
  /-- The covering homomorphism `α` is surjective. -/
  surjective_α : Function.Surjective α
  /-- The prescribed continuous homomorphism from `G` to the target group `B`. -/
  φ : G →ₜ* B
  /-- The prescribed map `φ` is surjective, so the embedding problem is epimorphic on both legs. -/
  surjective_φ : Function.Surjective φ
def

ProperSolution

L47 ↗
ProCGroups.FreeProC.Characterization.TopologicalEmbeddingProblem.ProperSolution
Documentation

A proper solution is a surjective weak solution.

Source context 6 commands

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

namespace ProCGroups.FreeProC.Characterization
open ProCGroups.FreeProC
universe u
section EmbeddingProblems
namespace TopologicalEmbeddingProblem
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def ProperSolution (P : TopologicalEmbeddingProblem G) : Type u
def

IsSplit

L52 ↗
ProCGroups.FreeProC.Characterization.TopologicalEmbeddingProblem.IsSplit
Documentation

The embedding problem is split: its epimorphism has a continuous section.

Source context 6 commands

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

namespace ProCGroups.FreeProC.Characterization
open ProCGroups.FreeProC
universe u
section EmbeddingProblems
namespace TopologicalEmbeddingProblem
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def IsSplit (P : TopologicalEmbeddingProblem G) : Prop
def

HasAtLeastProperSolutions

L59 ↗
ProCGroups.FreeProC.Characterization.TopologicalEmbeddingProblem.HasAtLeastProperSolutions
Documentation

An embedding problem has at least \(\kappa\) different solutions if there is a family of pairwise distinct continuous surjective lifts indexed by a set of cardinality \(\kappa\).

Source context 6 commands

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

namespace ProCGroups.FreeProC.Characterization
open ProCGroups.FreeProC
universe u
section EmbeddingProblems
namespace TopologicalEmbeddingProblem
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def HasAtLeastProperSolutions
    (P : TopologicalEmbeddingProblem G) (κ : Cardinal) : Prop
def

IsFiniteCEmbeddingProblem

L67 ↗
ProCGroups.FreeProC.Characterization.IsFiniteCEmbeddingProblem
Documentation

A finite embedding problem whose two finite target groups lie in the chosen finite class.

Source context 4 commands

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

namespace ProCGroups.FreeProC.Characterization
open ProCGroups.FreeProC
universe u
section EmbeddingProblems
Lean source · statement
def IsFiniteCEmbeddingProblem
    (C : ProCGroups.FiniteGroupClass.{u})
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (P : TopologicalEmbeddingProblem G) : Prop
def

IsFiniteSplitCEmbeddingProblem

L75 ↗
ProCGroups.FreeProC.Characterization.IsFiniteSplitCEmbeddingProblem
Documentation

A finite \(C\)-embedding problem with a continuous section.

Source context 4 commands

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

namespace ProCGroups.FreeProC.Characterization
open ProCGroups.FreeProC
universe u
section EmbeddingProblems
Lean source · statement
def IsFiniteSplitCEmbeddingProblem
    (C : ProCGroups.FiniteGroupClass.{u})
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (P : TopologicalEmbeddingProblem G) : Prop

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