ProCGroups.FreeProC.Characterization.EmbeddingProblems
This module studies embedding problems for pro cgroups. A subgroup is minimal normal if it is nontrivial, normal, and has no proper nontrivial normal subgroup below it. A topological embedding problem for a topological group.
def IsMinimalNormalSubgroup
{A : Type u} [Group A] (N : Subgroup A) : Prop :=
N.Normal ∧ N ≠ ⊥ ∧
∀ M : Subgroup A, M.Normal → M ≤ N → M = ⊥ ∨ M = NA subgroup is minimal normal if it is nontrivial, normal, and has no proper nontrivial normal subgroup below it.
structure TopologicalEmbeddingProblem
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] where
A : Type u
instGroupA : Group A
instTopologicalSpaceA : TopologicalSpace A
instIsTopologicalGroupA : IsTopologicalGroup A
B : Type u
instGroupB : Group B
instTopologicalSpaceB : TopologicalSpace B
instIsTopologicalGroupB : IsTopologicalGroup B
α : A →* B
continuous_α : Continuous α
surjective_α : Function.Surjective α
φ : G →* B
continuous_φ : Continuous φ
surjective_φ : Function.Surjective φA topological embedding problem for a topological group. No finiteness or pro-\(C\) condition is built into this structure; those are supplied by FiniteEmbeddingProblem and ProCEmbeddingProblem below.
structure FiniteEmbeddingProblem
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
extends TopologicalEmbeddingProblem G where
finiteA : Finite A
finiteB : Finite BA topological embedding problem whose two finite target groups are finite.
structure ProCEmbeddingProblem
(ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
extends TopologicalEmbeddingProblem G where
isProCA : @ProCGroups.ProC.ProCGroupPredicate.holds ProC A _ _ _
isProCB : @ProCGroups.ProC.ProCGroupPredicate.holds ProC B _ _ _A topological embedding problem whose two finite target groups lie in the chosen pro-\(C\) predicate.
def kernel (P : TopologicalEmbeddingProblem G) : Subgroup P.A :=
P.α.kerThe kernel of a topological embedding problem is the kernel of its epimorphism to the target group.
def WeakSolution (P : TopologicalEmbeddingProblem G) : Type u :=
{ φbar : G →* P.A // Continuous φbar ∧ P.α.comp φbar = P.φ }A weak solution is a continuous lift commuting with the embedding-problem square.
def ProperSolution (P : TopologicalEmbeddingProblem G) : Type u :=
{ φbar : WeakSolution P // Function.Surjective φbar.1 }A proper solution is a surjective weak solution.
def HasWeakSolution (P : TopologicalEmbeddingProblem G) : Prop :=
∃ φbar : G →* P.A, Continuous φbar ∧ P.α.comp φbar = P.φWeak solvability of an embedding problem.
def HasSolution (P : TopologicalEmbeddingProblem G) : Prop :=
∃ φbar : G →* P.A,
Continuous φbar ∧ Function.Surjective φbar ∧ P.α.comp φbar = P.φThe free pro-\(C\) embedding-problem construction has a continuous surjective lift commuting with the specified maps.
def HasFiniteMinimalNormalKernel (P : TopologicalEmbeddingProblem G) : Prop :=
Finite P.kernel ∧ IsMinimalNormalSubgroup P.kernelThe finite minimal normal kernel condition.
def IsSplit (P : TopologicalEmbeddingProblem G) : Prop :=
∃ σ : P.B →* P.A, Continuous σ ∧ P.α.comp σ = MonoidHom.id P.BThe embedding problem is split: its epimorphism has a continuous section.
def HasAtLeastProperSolutions
(P : TopologicalEmbeddingProblem G) (κ : Cardinal) : Prop :=
∃ I : Type u, Cardinal.mk I = κ ∧
∃ ψ : I → P.ProperSolution, Function.Injective ψ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\).
abbrev EmbeddingProblemPredicate :=
{G : Type u} → [Group G] → [TopologicalSpace G] → [IsTopologicalGroup G] →
TopologicalEmbeddingProblem G → PropA global class of embedding problems, varying with the ambient source group.
def IsProCEmbeddingProblem
(ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(P : TopologicalEmbeddingProblem G) : Prop :=
@ProCGroups.ProC.ProCGroupPredicate.holds ProC P.A _ _ _ ∧
@ProCGroups.ProC.ProCGroupPredicate.holds ProC P.B _ _ _An embedding problem whose source and target both lie in the chosen pro-\(C\) class.
def IsFiniteCEmbeddingProblem
(C : ProCGroups.FiniteGroupClass.{u})
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(P : TopologicalEmbeddingProblem G) : Prop :=
Finite P.A ∧ Finite P.B ∧
ProCGroups.ProC.IsProCGroup C P.A ∧ ProCGroups.ProC.IsProCGroup C P.Bdef IsFiniteSplitCEmbeddingProblem
(C : ProCGroups.FiniteGroupClass.{u})
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(P : TopologicalEmbeddingProblem G) : Prop :=
IsFiniteCEmbeddingProblem C P ∧ P.IsSplitA finite \(C\)-embedding problem with a continuous section.
def HasWeakLiftingPropertyOver
(E : EmbeddingProblemPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop :=
∀ P : TopologicalEmbeddingProblem G, E P → P.HasWeakSolutionWeak lifting property over a class of embedding problems.
def HasStrongLiftingPropertyAt
(E : EmbeddingProblemPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(κ : Cardinal) : Prop :=
∀ P : TopologicalEmbeddingProblem G, E P →
Generation.topologicalRank P.B < κ →
Generation.topologicalRank P.A ≤ κ →
P.HasSolutionStrong lifting property over a class of embedding problems, with the ambient cardinal bound exposed explicitly.