CompletedGroupAlgebra.InClassFunctoriality.ComapIndex
Completed Group Algebra / Functoriality Within a Class / Comap Index.
def completedGroupAlgebraComapIndexInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
CompletedGroupAlgebraIndexInClass G C :=
let φc : G →ₜ* H := { toMonoidHom := φ, continuous_toFun := hφ }
OrderDual.toDual
(OpenNormalSubgroupInClass.comap (C := C) (G := G) hHer φc (OrderDual.ofDual V))The inverse image of a \(C\)-quotient of \(H\) along a continuous homomorphism \(G\to H\), again as a \(C\)-quotient of \(G\), when \(C\) is hereditary.
theorem completedGroupAlgebraComapIndexInClass_subgroup
(C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
(((OrderDual.ofDual (completedGroupAlgebraComapIndexInClass
(G := G) (H := H) C hHer φ hφ V)).1 : OpenNormalSubgroup G) : Subgroup G) =
(((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H).comap φThe comap of an open normal subgroup along a continuous homomorphism is again open normal.
Show proof
rflProof. For a continuous homomorphism \(\varphi:G\to H\) and an open normal subgroup \(V\) of \(H\), the inverse image \(\varphi^{-1}(V)\) is open and normal in \(G\). If \(H/V\) lies in the class \(C\), heredity gives the corresponding \(C\)-quotient of \(G\). The induced quotient maps, monotonicity under refinement, surjectivity, and compatibility are checked directly on coset representatives.
□theorem completedGroupAlgebraComapIndexInClass_mono
(C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ)
{V W : CompletedGroupAlgebraIndexInClass H C} (hVW : V ≤ W) :
completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V ≤
completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ WComap indices are monotone with respect to refinement of open normal subgroups.
Show proof
by
change (((OrderDual.ofDual W).1 : OpenNormalSubgroup H) : Subgroup H).comap φ ≤
(((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H).comap φ
exact Subgroup.comap_mono hVWProof. For a continuous homomorphism \(\varphi:G\to H\) and an open normal subgroup \(V\) of \(H\), the inverse image \(\varphi^{-1}(V)\) is open and normal in \(G\). If \(H/V\) lies in the class \(C\), heredity gives the corresponding \(C\)-quotient of \(G\). The induced quotient maps, monotonicity under refinement, surjectivity, and compatibility are checked directly on coset representatives.
□def completedGroupAlgebraComapQuotientMapInClass
(C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
CompletedGroupAlgebraQuotientInClass G C
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) →*
CompletedGroupAlgebraQuotientInClass H C V :=
QuotientGroup.map _ _ φ (by
intro g hg
exact hg)The quotient homomorphism \(G/\varphi^{-1}(V) \to H/V\) for a \(C\)-indexed quotient.
theorem completedGroupAlgebraComapQuotientMapInClass_mk
(C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) (g : G) :
completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ V
(QuotientGroup.mk'
((((OrderDual.ofDual (completedGroupAlgebraComapIndexInClass
(G := G) (H := H) C hHer φ hφ V)).1 : OpenNormalSubgroup G) :
Subgroup G)) g) =
QuotientGroup.mk' ((((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H))
(φ g)The quotient map attached to a comap index sends a coset to the coset of its image.
Show proof
rflProof. For a continuous homomorphism \(\varphi:G\to H\) and an open normal subgroup \(V\) of \(H\), the inverse image \(\varphi^{-1}(V)\) is open and normal in \(G\). If \(H/V\) lies in the class \(C\), heredity gives the corresponding \(C\)-quotient of \(G\). The induced quotient maps, monotonicity under refinement, surjectivity, and compatibility are checked directly on coset representatives.
□theorem completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
(C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ) (hφsurj : Function.Surjective φ)
(V : CompletedGroupAlgebraIndexInClass H C) :
Function.Surjective
(completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ V)A surjective group homomorphism induces a surjective map on the corresponding finite quotients.
Show proof
by
intro q
rcases QuotientGroup.mk'_surjective
((((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H)) q with
⟨h, rfl⟩
rcases hφsurj h with ⟨g, rfl⟩
refine ⟨QuotientGroup.mk'
((((OrderDual.ofDual (completedGroupAlgebraComapIndexInClass
(G := G) (H := H) C hHer φ hφ V)).1 : OpenNormalSubgroup G) : Subgroup G)) g, ?_⟩
rw [completedGroupAlgebraComapQuotientMapInClass_mk]
@[simp]Proof. For a continuous homomorphism \(\varphi:G\to H\) and an open normal subgroup \(V\) of \(H\), the inverse image \(\varphi^{-1}(V)\) is open and normal in \(G\). If \(H/V\) lies in the class \(C\), heredity gives the corresponding \(C\)-quotient of \(G\). The induced quotient maps, monotonicity under refinement, surjectivity, and compatibility are checked directly on coset representatives.
□theorem completedGroupAlgebraComapQuotientMapInClass_compatible
(C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
(φ : G →* H) (hφ : Continuous φ)
{V W : CompletedGroupAlgebraIndexInClass H C} (hVW : V ≤ W) :
(OpenNormalSubgroupInClass.map
(C := C) (G := H)
(U := OrderDual.ofDual V) (V := OrderDual.ofDual W) hVW).comp
(completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ W) =
(completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ V).comp
(OpenNormalSubgroupInClass.map
(C := C) (G := G)
(U := OrderDual.ofDual
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V))
(V := OrderDual.ofDual
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ W))
(completedGroupAlgebraComapIndexInClass_mono
(G := G) (H := H) C hHer φ hφ hVW))The class-restricted completed group-algebra pullback quotient map is compatible with transition maps and coordinate projections for the completed group algebra.
Show proof
by
ext q
rcases QuotientGroup.mk'_surjective
((((OrderDual.ofDual
(completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ W)).1 :
OpenNormalSubgroup G) : Subgroup G)) q with ⟨g, rfl⟩
rflProof. For a continuous homomorphism \(\varphi:G\to H\) and an open normal subgroup \(V\) of \(H\), the inverse image \(\varphi^{-1}(V)\) is open and normal in \(G\). If \(H/V\) lies in the class \(C\), heredity gives the corresponding \(C\)-quotient of \(G\). The induced quotient maps, monotonicity under refinement, surjectivity, and compatibility are checked directly on coset representatives.
□