FoxDifferential.Completed.DifferentialModule.Map.Comap
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
def completedGroupAlgebraComapIndex
(ψ : ContinuousMonoidHom G H) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H) :
_root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G := by
let V : OpenNormalSubgroup H := (OrderDual.ofDual U).1
let W : OpenNormalSubgroup G := OpenNormalSubgroup.comap ψ.toMonoidHom ψ.continuous_toFun V
refine OrderDual.toDual ⟨W, ?_⟩
let q : G →* H ⧸ (V : Subgroup H) :=
(QuotientGroup.mk' (V : Subgroup H)).comp ψ.toMonoidHom
let f : G ⧸ (W : Subgroup G) → H ⧸ (V : Subgroup H) :=
QuotientGroup.map _ _ ψ.toMonoidHom (by
intro g hg
simpa [W] 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 U).2
exact Finite.of_injective f hftheorem completedGroupAlgebraComapIndex_subgroup
(ψ : ContinuousMonoidHom G H) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H) :
(((OrderDual.ofDual (completedGroupAlgebraComapIndex (G := G) (H := H) ψ U)).1 :
OpenNormalSubgroup G) : Subgroup G) =
Subgroup.comap ψ.toMonoidHom
(((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H)The subgroup underlying the comap index is the subgroup-theoretic comap.
Show proof
by
rflProof. Use the completed group-algebra map induced stagewise by the relevant quotient, comap, target, or coefficient map. At each finite stage, supports are sent by the finite quotient homomorphism and coefficients are transported by the given coefficient map when present. Compatibility with refinements gives a map of inverse limits; formulas, group-like elements, augmentation, linearity, and surjectivity are checked on singleton basis elements and extended by finite support and linearity.
□def completedGroupAlgebraComapQuotientMap
(ψ : ContinuousMonoidHom G H) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H) :
_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G
(completedGroupAlgebraComapIndex (G := G) (H := H) ψ U) →*
_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H U :=
QuotientGroup.map _ _ ψ.toMonoidHom (by
intro g hg
simpa [completedGroupAlgebraComapIndex] using hg)The quotient map from the pulled-back source quotient to the target quotient induced by the original homomorphism.
theorem completedGroupAlgebraComapQuotientMap_mk
(ψ : ContinuousMonoidHom G H) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H) (g : G) :
completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ U
(QuotientGroup.mk' _ g) =
QuotientGroup.mk' (((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H) (ψ g)The pullback quotient map sends the class of a source element to the class of its image in the target quotient in the Fox differential construction.
Show proof
by
rflProof. Use the completed group-algebra map induced stagewise by the relevant quotient, comap, target, or coefficient map. At each finite stage, supports are sent by the finite quotient homomorphism and coefficients are transported by the given coefficient map when present. Compatibility with refinements gives a map of inverse limits; formulas, group-like elements, augmentation, linearity, and surjectivity are checked on singleton basis elements and extended by finite support and linearity.
□theorem completedGroupAlgebraComapQuotientMap_surjective
(ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ)
(U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H) :
Function.Surjective
(completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ U)Show proof
by
intro q
rcases QuotientGroup.mk'_surjective
((((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H)) q with
⟨h, rfl⟩
rcases hψ h with ⟨g, rfl⟩
refine ⟨QuotientGroup.mk'
((((OrderDual.ofDual
(completedGroupAlgebraComapIndex (G := G) (H := H) ψ U)).1 :
OpenNormalSubgroup G) : Subgroup G)) g, ?_⟩
rw [completedGroupAlgebraComapQuotientMap_mk]Proof. Use the completed group-algebra map induced stagewise by the relevant quotient, comap, target, or coefficient map. At each finite stage, supports are sent by the finite quotient homomorphism and coefficients are transported by the given coefficient map when present. Compatibility with refinements gives a map of inverse limits; formulas, group-like elements, augmentation, linearity, and surjectivity are checked on singleton basis elements and extended by finite support and linearity.
□theorem completedGroupAlgebraComapIndex_mono
(ψ : ContinuousMonoidHom G H) {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H} (hUV : U ≤ V) :
completedGroupAlgebraComapIndex (G := G) (H := H) ψ U ≤
completedGroupAlgebraComapIndex (G := G) (H := H) ψ VComap of all-finite completed-group-algebra indices is monotone.
Show proof
by
change
Subgroup.comap ψ.toMonoidHom
(((OrderDual.ofDual V).1 : OpenNormalSubgroup H) : Subgroup H) ≤
Subgroup.comap ψ.toMonoidHom
(((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H)
exact Subgroup.comap_mono hUVProof. Use the completed group-algebra map induced stagewise by the relevant quotient, comap, target, or coefficient map. At each finite stage, supports are sent by the finite quotient homomorphism and coefficients are transported by the given coefficient map when present. Compatibility with refinements gives a map of inverse limits; formulas, group-like elements, augmentation, linearity, and surjectivity are checked on singleton basis elements and extended by finite support and linearity.
□theorem completedGroupAlgebraComapQuotientMap_compatible
(ψ : ContinuousMonoidHom G H) {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex H} (hUV : U ≤ V) :
(OpenNormalSubgroupInClass.map
(C := ProCGroups.FiniteGroupClass.allFinite) (G := H)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV).comp
(completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ V) =
(completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ U).comp
(OpenNormalSubgroupInClass.map
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
(U := OrderDual.ofDual
(completedGroupAlgebraComapIndex (G := G) (H := H) ψ U))
(V := OrderDual.ofDual
(completedGroupAlgebraComapIndex (G := G) (H := H) ψ V))
(completedGroupAlgebraComapIndex_mono (G := G) (H := H) ψ hUV))The comap quotient maps are compatible with refinement of finite quotients.
Show proof
by
ext q
rcases QuotientGroup.mk'_surjective
((((OrderDual.ofDual
(completedGroupAlgebraComapIndex (G := G) (H := H) ψ V)).1 :
OpenNormalSubgroup G) : Subgroup G)) q with ⟨g, rfl⟩
rflProof. Unfold the completed group-algebra comap system. An open normal subgroup of the target pulls back to an open normal subgroup of the source, the quotient map sends a source class to the corresponding target class, and compatibility follows by comparing the induced maps under refinement.
□