Finite embedding problems

A finite embedding problem for a topological group G is a continuous surjection π : G ↠ Q onto a finite group together with a surjection α : E ↠ Q of finite groups. A solution is a continuous homomorphism β : G → E with α ∘ β = π. For homomorphisms into finite discrete groups, continuity is recorded as openness of the kernel. This equivalence uses the topological group structure on G.

A solution need not be surjective. For example, if G is cyclic of order p, Q = 1, and E = G × G, no homomorphism G → E is surjective.

A surjection φ : E ↠ F of finite groups and a homomorphism β : G → F with open kernel cut out an embedding problem, TauCeti.FiniteEmbeddingProblem.ofSurjective: the quotient is the range of β and the group to map into is its preimage under φ. Its solutions are exactly the lifts of β through φ with open kernel, and its kernel is the kernel of φ. This is the problem that appears when a solution modulo a normal subgroup is lifted one step further, and at each finite level of a lifting problem against a surjection of profinite groups.

Main definitions

• TauCeti.FiniteEmbeddingProblem: a finite embedding problem for G.
• TauCeti.FiniteEmbeddingProblem.IsSolution: a solution of a finite embedding problem.
• TauCeti.FiniteEmbeddingProblem.ofSurjective: the embedding problem cut out by a surjection φ : E ↠ F of finite groups and a homomorphism β : G → F with open kernel.

Main results

• TauCeti.FiniteEmbeddingProblem.ker_ofSurjective_α: the kernel of the problem cut out by φ and β is the kernel of φ.
• TauCeti.FiniteEmbeddingProblem.isSolution_ofSurjective_iff: its solutions are the lifts of β through φ with open kernel.

References

• J.-P. Serre, Galois Cohomology, Chapter I, §3.4 and §4.2.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, Chapter III, §5.

structure TauCeti.FiniteEmbeddingProblem (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Type (max (max u (v + 1)) (w + 1))

A finite embedding problem for a topological group G: a continuous surjection π : G ↠ Q onto a finite group, together with a surjection α : E ↠ Q of finite groups. Continuity of π is recorded as openness of its kernel, which is what continuity into a finite discrete group amounts to.

• Q : Type v

  The finite quotient of G the problem sits over.

• groupQ : Group self.Q
• finiteQ : Finite self.Q
• E : Type w

  The finite group into which a solution maps.

• groupE : Group self.E
• finiteE : Finite self.E
• π : G →* self.Q

  The continuous surjection G ↠ Q.

• isOpen_ker_π : IsOpen ↑self.π.ker

  Continuity of π, as openness of its kernel.

• π_surjective : Function.Surjective ⇑self.π

  Surjectivity of π.

• α : self.E →* self.Q

  The surjection of finite groups E ↠ Q.

• α_surjective : Function.Surjective ⇑self.α

  Surjectivity of α.

def TauCeti.FiniteEmbeddingProblem.IsSolution {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) (β : G →* P.E) : Prop

A solution of a finite embedding problem P: a homomorphism β : G → E with open kernel (that is, continuous for the discrete topology on E) such that α ∘ β = π. A solution need not be surjective.

Equations

• P.IsSolution β = (IsOpen ↑β.ker ∧ ∀ (g : G), P.α (β g) = P.π g)

@[simp]

theorem TauCeti.FiniteEmbeddingProblem.isSolution_iff {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {P : FiniteEmbeddingProblem G} {β : G →* P.E} : P.IsSolution β ↔ IsOpen ↑β.ker ∧ P.α.comp β = P.π

A homomorphism solves P exactly when its kernel is open and α ∘ β = π.

theorem TauCeti.FiniteEmbeddingProblem.IsSolution.isOpen_ker {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {P : FiniteEmbeddingProblem G} {β : G →* P.E} (hβ : P.IsSolution β) : IsOpen ↑β.ker

A solution of a finite embedding problem has open kernel.

theorem TauCeti.FiniteEmbeddingProblem.IsSolution.comp_eq {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {P : FiniteEmbeddingProblem G} {β : G →* P.E} (hβ : P.IsSolution β) : P.α.comp β = P.π

A solution of a finite embedding problem lifts π through α.

The embedding problem cut out by a surjection and a homomorphism with open kernel

@[reducible, inline]

abbrev TauCeti.FiniteEmbeddingProblem.ofSurjective {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {E : Type w} {F : Type v} [Group E] [Finite E] [Group F] (φ : E →* F) (hφ : Function.Surjective ⇑φ) (β : G →* F) (hβ : IsOpen ↑β.ker) : FiniteEmbeddingProblem G

The finite embedding problem cut out by a surjection φ : E ↠ F of finite groups and a homomorphism β : G → F with open kernel: the quotient is the range β(G), the group to map into is its preimage φ⁻¹(β(G)), and the two surjections are the restrictions of β and of φ. Its kernel is the kernel of φ (TauCeti.FiniteEmbeddingProblem.ker_ofSurjective_α), and its solutions are the lifts of β through φ with open kernel (TauCeti.FiniteEmbeddingProblem.isSolution_ofSurjective_iff).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.FiniteEmbeddingProblem.coe_ofSurjective_α_apply {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {E : Type w} {F : Type v} [Group E] [Finite E] [Group F] {φ : E →* F} {hφ : Function.Surjective ⇑φ} {β : G →* F} {hβ : IsOpen ↑β.ker} (x : ↥(Subgroup.comap φ β.range)) : ↑((ofSurjective φ hφ β hβ).α x) = φ ↑x

@[simp]

theorem TauCeti.FiniteEmbeddingProblem.coe_ofSurjective_π_apply {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {E : Type w} {F : Type v} [Group E] [Finite E] [Group F] {φ : E →* F} {hφ : Function.Surjective ⇑φ} {β : G →* F} {hβ : IsOpen ↑β.ker} (g : G) : ↑((ofSurjective φ hφ β hβ).π g) = β g

@[simp]

theorem TauCeti.FiniteEmbeddingProblem.ker_ofSurjective_α {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {E : Type w} {F : Type v} [Group E] [Finite E] [Group F] {φ : E →* F} {hφ : Function.Surjective ⇑φ} {β : G →* F} {hβ : IsOpen ↑β.ker} : (ofSurjective φ hφ β hβ).α.ker = φ.ker.subgroupOf (Subgroup.comap φ β.range)

The kernel of the embedding problem cut out by φ and β is the kernel of φ.

theorem TauCeti.FiniteEmbeddingProblem.isSolution_ofSurjective_iff {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {E : Type w} {F : Type v} [Group E] [Finite E] [Group F] {φ : E →* F} {hφ : Function.Surjective ⇑φ} {β : G →* F} {hβ : IsOpen ↑β.ker} {β' : G →* ↥(Subgroup.comap φ β.range)} : (ofSurjective φ hφ β hβ).IsSolution β' ↔ IsOpen ↑β'.ker ∧ φ.comp ((Subgroup.comap φ β.range).subtype.comp β') = β

A solution of the embedding problem cut out by φ and β is a lift of β through φ with open kernel.

theorem TauCeti.FiniteEmbeddingProblem.IsSolution.isOpen_ker_subtype_comp {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {E : Type w} {F : Type v} [Group E] [Finite E] [Group F] {φ : E →* F} {hφ : Function.Surjective ⇑φ} {β : G →* F} {hβ : IsOpen ↑β.ker} {β' : G →* ↥(Subgroup.comap φ β.range)} (h : (ofSurjective φ hφ β hβ).IsSolution β') : IsOpen ↑((Subgroup.comap φ β.range).subtype.comp β').ker

A solution of the embedding problem cut out by φ and β, composed with the inclusion of φ⁻¹(β(G)) into E, has open kernel.

theorem TauCeti.FiniteEmbeddingProblem.IsSolution.comp_subtype_comp {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {E : Type w} {F : Type v} [Group E] [Finite E] [Group F] {φ : E →* F} {hφ : Function.Surjective ⇑φ} {β : G →* F} {hβ : IsOpen ↑β.ker} {β' : G →* ↥(Subgroup.comap φ β.range)} (h : (ofSurjective φ hφ β hβ).IsSolution β') : φ.comp ((Subgroup.comap φ β.range).subtype.comp β') = β

A solution of the embedding problem cut out by φ and β, composed with the inclusion of φ⁻¹(β(G)) into E, lifts β through φ.