The pullback extension of a finite embedding problem

For a finite embedding problem G → Q ← E, the pullback consists of pairs (g, e) with π g = α e. Its projection to G is an extension by ker α. A continuous splitting of this extension is equivalent to a solution of the embedding problem.

When ker α is abelian, conjugation descends to an action of Q on the kernel. Restricting along π gives the coefficient action of G induced by the pullback extension.

def TauCeti.FiniteEmbeddingProblem.pullback {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) : Subgroup (G × P.E)

The subgroup of compatible pairs in an embedding problem.

Equations

• P.pullback = (P.π.comp (MonoidHom.fst G P.E)).eqLocus (P.α.comp (MonoidHom.snd G P.E))

@[simp]

theorem TauCeti.FiniteEmbeddingProblem.mem_pullback {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) (x : G × P.E) : x ∈ P.pullback ↔ P.π x.1 = P.α x.2

def TauCeti.FiniteEmbeddingProblem.pullbackFst {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) : ↥P.pullback →* G

The projection of the pullback extension to its base.

Equations

• P.pullbackFst = (MonoidHom.fst G P.E).domRestrict P.pullback

def TauCeti.FiniteEmbeddingProblem.pullbackSnd {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) : ↥P.pullback →* P.E

The map from the pullback to the finite group of the embedding problem.

Equations

• P.pullbackSnd = (MonoidHom.snd G P.E).domRestrict P.pullback

@[simp]

theorem TauCeti.FiniteEmbeddingProblem.pullbackFst_apply {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) (x : ↥P.pullback) : P.pullbackFst x = (↑x).1

@[simp]

theorem TauCeti.FiniteEmbeddingProblem.pullbackSnd_apply {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) (x : ↥P.pullback) : P.pullbackSnd x = (↑x).2

theorem TauCeti.FiniteEmbeddingProblem.pullbackFst_surjective {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) : Function.Surjective ⇑P.pullbackFst

Surjectivity of α makes the pullback projection surjective.

def TauCeti.FiniteEmbeddingProblem.kernelEquivPullbackKer {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) : ↥P.α.ker ≃* ↥P.pullbackFst.ker

The kernel of the pullback projection is the original kernel, by e ↦ (1, e).

Equations

• P.kernelEquivPullbackKer = { toFun := fun (n : ↥P.α.ker) => ⟨⟨(1, ↑n), ⋯⟩, ⋯⟩, invFun := fun (x : ↥P.pullbackFst.ker) => ⟨(↑↑x).2, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

def TauCeti.FiniteEmbeddingProblem.pullbackGroupExtension {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) : GroupExtension (↥P.α.ker) (↥P.pullback) G

The abstract extension of G by ker α obtained by pullback along π.

Equations

• P.pullbackGroupExtension = GroupExtension.ofMulEquivKer ⋯ P.kernelEquivPullbackKer

@[simp]

theorem TauCeti.FiniteEmbeddingProblem.pullbackGroupExtension_rightHom {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) : P.pullbackGroupExtension.rightHom = P.pullbackFst

@[simp]

theorem TauCeti.FiniteEmbeddingProblem.pullbackGroupExtension_inl {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) (n : ↥P.α.ker) : ↑(P.pullbackGroupExtension.inl n) = (1, ↑n)

theorem TauCeti.FiniteEmbeddingProblem.coe_pullbackGroupExtension_conjAct {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) (x : ↥P.pullback) (n : ↥P.α.ker) : ↑((P.pullbackGroupExtension.conjAct x) n) = (↑x).2 * ↑n * (↑x).2⁻¹

Conjugation in the pullback acts on its kernel through the second coordinate.

theorem TauCeti.FiniteEmbeddingProblem.continuous_π {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) [TopologicalSpace P.Q] : Continuous ⇑P.π

The quotient map of an embedding problem is continuous for any topology on Q.

theorem TauCeti.FiniteEmbeddingProblem.continuous_pullbackFst {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) [TopologicalSpace P.E] : Continuous ⇑P.pullbackFst

theorem TauCeti.FiniteEmbeddingProblem.continuous_pullbackSnd {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) [TopologicalSpace P.E] : Continuous ⇑P.pullbackSnd

theorem TauCeti.FiniteEmbeddingProblem.continuous_pullbackGroupExtension_inl {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) [TopologicalSpace P.E] : Continuous ⇑P.pullbackGroupExtension.inl

theorem TauCeti.FiniteEmbeddingProblem.isSolution_iff_continuous {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) [TopologicalSpace P.E] [DiscreteTopology P.E] (β : G →* P.E) : P.IsSolution β ↔ Continuous ⇑β ∧ P.α.comp β = P.π

For a discrete target, the open-kernel definition of a solution is continuity.

theorem TauCeti.FiniteEmbeddingProblem.exists_splitting_iff_hasSolution {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) [TopologicalSpace P.E] [DiscreteTopology P.E] : (∃ (s : P.pullbackGroupExtension.Splitting), Continuous ⇑s) ↔ ∃ (β : G →* P.E), P.IsSolution β

Continuous splittings of the pullback exist exactly when the embedding problem has a solution. The solution is not required to be surjective.

theorem TauCeti.FiniteEmbeddingProblem.isClosed_pullback {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) [TopologicalSpace P.E] [DiscreteTopology P.E] [TopologicalSpace P.Q] [DiscreteTopology P.Q] : IsClosed ↑P.pullback

The compatible-pair subgroup is closed in G × E.

theorem TauCeti.FiniteEmbeddingProblem.compactSpace_pullback {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) [TopologicalSpace P.E] [DiscreteTopology P.E] [TopologicalSpace P.Q] [DiscreteTopology P.Q] [CompactSpace G] : CompactSpace ↥P.pullback

Over a compact base the pullback group is compact.

theorem TauCeti.FiniteEmbeddingProblem.isMulCommutative_ker {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) (hcomm : ∀ x ∈ P.α.ker, ∀ y ∈ P.α.ker, x * y = y * x) : IsMulCommutative ↥P.α.ker

An abelian kernel is a commutative subgroup, so the scoped IsMulCommutative instances equip it with its bundled commutative group structure.

noncomputable def TauCeti.FiniteEmbeddingProblem.kernelConj {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) (hcomm : ∀ x ∈ P.α.ker, ∀ y ∈ P.α.ker, x * y = y * x) : P.Q →* MulAut ↥P.α.ker

Conjugation on the abelian kernel descends to the finite quotient Q.

Equations

• P.kernelConj hcomm = TauCeti.GroupExtension.conjActOfSection (GroupExtension.ofSurjective ⋯).surjInvRightHom

theorem TauCeti.FiniteEmbeddingProblem.coe_kernelConj {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) (hcomm : ∀ x ∈ P.α.ker, ∀ y ∈ P.α.ker, x * y = y * x) (e : P.E) (n : ↥P.α.ker) : ↑(((P.kernelConj hcomm) (P.α e)) n) = e * ↑n * e⁻¹

The action of the image of e is conjugation by e.

@[instance_reducible]

noncomputable def TauCeti.FiniteEmbeddingProblem.kernelAction {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) (hcomm : ∀ x ∈ P.α.ker, ∀ y ∈ P.α.ker, x * y = y * x) : MulDistribMulAction G ↥P.α.ker

The action on the kernel obtained by restricting conjugation along π.

Equations

• P.kernelAction hcomm = MulDistribMulAction.compHom (↥P.α.ker) ((P.kernelConj hcomm).comp P.π)

theorem TauCeti.FiniteEmbeddingProblem.kernelAction_smul {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) (hcomm : ∀ x ∈ P.α.ker, ∀ y ∈ P.α.ker, x * y = y * x) (g : G) (n : ↥P.α.ker) : g • n = ((P.kernelConj hcomm) (P.π g)) n

The kernel action evaluates the quotient action at π g.

theorem TauCeti.FiniteEmbeddingProblem.pullbackGroupExtension_inducesAction {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) (hcomm : ∀ x ∈ P.α.ker, ∀ y ∈ P.α.ker, x * y = y * x) : GroupExtension.InducesAction P.pullbackGroupExtension

The pullback extension induces the restricted conjugation action on its kernel.

theorem TauCeti.FiniteEmbeddingProblem.continuousSMul_kernelAction {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) (hcomm : ∀ x ∈ P.α.ker, ∀ y ∈ P.α.ker, x * y = y * x) [TopologicalSpace P.E] [DiscreteTopology P.E] [TopologicalSpace P.Q] [DiscreteTopology P.Q] : ContinuousSMul G ↥P.α.ker

The kernel action is continuous because it factors through the finite discrete quotient.

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteEmbeddingProblem.pullbackExtension {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (P : FiniteEmbeddingProblem G) (hcomm : ∀ x ∈ P.α.ker, ∀ y ∈ P.α.ker, x * y = y * x) [TopologicalSpace P.E] [DiscreteTopology P.E] [TopologicalSpace P.Q] [DiscreteTopology P.Q] [CompactSpace G] [TotallyDisconnectedSpace G] : ProfiniteGroupExtension G ↥P.α.ker

The profinite pullback extension of an embedding problem with abelian kernel, equipped with the conjugation action restricted along π.

Equations

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