Yamaguchi Lean 4 Library
ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.Comap
ProCGroups/CompletedGroupAlgebra/AllFiniteFunctoriality/Comap

ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.Comap

4 Theorems | 2 Definitions

This module constructs the inverse-image finite quotient attached to a continuous group homomorphism and the induced quotient homomorphism. It is the index-level input for all-finite functoriality and has no dependency on augmentation theory.

import
Imported by

Declarations

Definition CompletedGroupAlgebra.completedGroupAlgebraComapIndex 
def completedGroupAlgebraComapIndex
    (φ : G →* H) (hφ : Continuous φ)
    (V : CompletedGroupAlgebraIndex H) : CompletedGroupAlgebraIndex G := by
  let V₀ : OpenNormalSubgroup H := (OrderDual.ofDual V).1
  let W : OpenNormalSubgroup G := ProCGroups.OpenNormalSubgroup.comap φ hφ V₀
  refine OrderDual.toDual ⟨W, ?_⟩
  let f : G ⧸ (W : Subgroup G) →* H ⧸ (V₀ : Subgroup H) :=
    QuotientGroup.map _ _ φ (by
      intro g hg
      simpa [W, V₀] using hg)
  have hf : Function.Injective f := by
    intro x y hxy
    rcases QuotientGroup.mk'_surjective (W : Subgroup G) x with ⟨a, rfl⟩
    rcases QuotientGroup.mk'_surjective (W : Subgroup G) y with ⟨b, rfl⟩
    apply QuotientGroup.eq.2
    change φ (a⁻¹ * b) ∈ (V₀ : Subgroup H)
    have hv : (φ a)⁻¹ * φ b ∈ (V₀ : Subgroup H) := QuotientGroup.eq.1 hxy
    simpa using hv
  letI : Finite (H ⧸ (V₀ : Subgroup H)) := (OrderDual.ofDual V).2
  exact Finite.of_injective f hf

The inverse image of an open-finite quotient of \(H\) along a continuous homomorphism \(G\to H\), regarded as an open-finite quotient of the profinite group \(G\). This is the index-level operation underlying Lemma 5.3.5(e)'s functoriality in the group variable.

Theorem CompletedGroupAlgebra.completedGroupAlgebraComapIndex_subgroup 
omit [IsTopologicalGroup G] [IsTopologicalGroup H] in
@[simp]
theorem completedGroupAlgebraComapIndex_subgroup
    (φ : G →* H) (hφ : Continuous φ)
    (V : CompletedGroupAlgebraIndex H) :
    (((OrderDual.ofDual (completedGroupAlgebraComapIndex (G := G) φ hφ V)).1 :
        OpenNormalSubgroup G) : Subgroup G) =
      (((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H).comap φ

The subgroup underlying the comap index is the subgroup-theoretic comap.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraComapIndex_mono 
omit [IsTopologicalGroup G] [IsTopologicalGroup H] in
theorem completedGroupAlgebraComapIndex_mono
    (φ : G →* H) (hφ : Continuous φ)
    {V W : CompletedGroupAlgebraIndex H} (hVW : V ≤ W) :
    completedGroupAlgebraComapIndex (G := G) φ hφ V ≤
      completedGroupAlgebraComapIndex (G := G) φ hφ W

Comap of all-finite completed-group-algebra indices is monotone.

Show Lean proof
Definition CompletedGroupAlgebra.completedGroupAlgebraComapQuotientMap 
def completedGroupAlgebraComapQuotientMap
    (φ : G →* H) (hφ : Continuous φ)
    (V : CompletedGroupAlgebraIndex H) :
    CompletedGroupAlgebraQuotient G (completedGroupAlgebraComapIndex (G := G) φ hφ V) →*
      CompletedGroupAlgebraQuotient H V :=
  QuotientGroup.map _ _ φ (by
    intro g hg
    exact hg)

The quotient homomorphism \(G/\varphi^{-1}(V) \to H/V\) induced by a continuous homomorphism \(\varphi: G \to H\).

Theorem CompletedGroupAlgebra.completedGroupAlgebraComapQuotientMap_mk 
@[simp]
theorem completedGroupAlgebraComapQuotientMap_mk
    (φ : G →* H) (hφ : Continuous φ)
    (V : CompletedGroupAlgebraIndex H) (g : G) :
    completedGroupAlgebraComapQuotientMap (G := G) φ hφ V
        (QuotientGroup.mk'
          ((((OrderDual.ofDual (completedGroupAlgebraComapIndex (G := G) φ hφ V)).1 :
            OpenNormalSubgroup G) : Subgroup G)) g) =
      QuotientGroup.mk'
        ((((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H)) (φ g)

The quotient map associated with the inverse-image subgroup sends the class of \(g\in G\) to the class of \(\varphi(g)\in H\).

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraComapQuotientMap_surjective 
theorem completedGroupAlgebraComapQuotientMap_surjective
    (φ : G →* H) (hφ : Continuous φ)
    (hφsurj : Function.Surjective φ) (V : CompletedGroupAlgebraIndex H) :
    Function.Surjective (completedGroupAlgebraComapQuotientMap (G := G) φ hφ V)

A surjective homomorphism induces a surjective map on the comap quotients.

Show Lean proof