FoxDifferential.Completed.DifferentialModule.Map.Stage
def primePowerCompletedGroupAlgebraMapStage
(ψ : ContinuousMonoidHom G H) (i : PrimePowerCompletedGroupAlgebraIndex H) :
PrimePowerCompletedGroupAlgebraStage ℓ G
(i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) →+*
PrimePowerCompletedGroupAlgebraStage ℓ H i :=
MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff (ℓ ^ i.1))
(completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ i.2)Coefficient change is performed stagewise: each coefficient is transported by the given ring homomorphism while the finite quotient support is left unchanged.
theorem primePowerCompletedGroupAlgebraMapStage_of
(ψ : ContinuousMonoidHom G H) (i : PrimePowerCompletedGroupAlgebraIndex H)
(q : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G
(completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)) :
primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
(MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1)) _ q) =
MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1)) _
(completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ i.2 q)Coefficient change is performed stagewise: each coefficient is transported by the given ring homomorphism while the finite quotient support is left unchanged.
Show proof
by
simp only [primePowerCompletedGroupAlgebraMapStage, MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk,
OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]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 primePowerCompletedGroupAlgebraMapStage_single
(ψ : ContinuousMonoidHom G H) (i : PrimePowerCompletedGroupAlgebraIndex H)
(q : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G
(completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2))
(a : ModNCompletedCoeff (ℓ ^ i.1)) :
primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
(MonoidAlgebra.single q a) =
MonoidAlgebra.single
(completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ i.2 q) aThe finite-stage component of the completed group-algebra map sends arbitrary group-ring basis coefficients by the pulled-back quotient map.
Show proof
by
simp only [primePowerCompletedGroupAlgebraMapStage, MonoidAlgebra.single,
MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]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 primePowerCompletedGroupAlgebraMapStage_surjective
(ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ)
(i : PrimePowerCompletedGroupAlgebraIndex H) :
Function.Surjective
(primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i)If \(\psi : G \to H\) is surjective, then every finite-stage group-algebra component of the completed map is surjective.
Show proof
by
intro x
induction x using Finsupp.induction with
| zero =>
exact ⟨0, by simp only [map_zero]⟩
| single_add q a x _ _ ih =>
rcases completedGroupAlgebraComapQuotientMap_surjective
(G := G) (H := H) ψ hψ i.2 q with
⟨q', hq'⟩
rcases ih with ⟨y, hy⟩
refine ⟨(MonoidAlgebra.single q' a :
PrimePowerCompletedGroupAlgebraStage ℓ G
(i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)) + y, ?_⟩
change primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
((MonoidAlgebra.single q' a :
PrimePowerCompletedGroupAlgebraStage ℓ G
(i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)) + y) =
(show PrimePowerCompletedGroupAlgebraStage ℓ H i from MonoidAlgebra.single q a) +
(show PrimePowerCompletedGroupAlgebraStage ℓ H i from x)
calc
primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
((MonoidAlgebra.single q' a :
PrimePowerCompletedGroupAlgebraStage ℓ G
(i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)) + y)
=
(show PrimePowerCompletedGroupAlgebraStage ℓ H i from
MonoidAlgebra.single
(completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ i.2 q') a) +
(show PrimePowerCompletedGroupAlgebraStage ℓ H i from
primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i y) := by
rw [map_add, primePowerCompletedGroupAlgebraMapStage_single]
_ =
(show PrimePowerCompletedGroupAlgebraStage ℓ H i from MonoidAlgebra.single q a) +
(show PrimePowerCompletedGroupAlgebraStage ℓ H i from x) := by
rw [hq', hy]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 primePowerCompletedGroupAlgebraMapStage_augmentation
(ψ : ContinuousMonoidHom G H) (i : PrimePowerCompletedGroupAlgebraIndex H)
(x : PrimePowerCompletedGroupAlgebraStage ℓ G
(i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)) :
modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) H i.2
(primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i x) =
modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G
(completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) xThe finite-stage component of a completed group-algebra map preserves augmentation.
Show proof
by
let leftMap :
PrimePowerCompletedGroupAlgebraStage ℓ G
(i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) →+*
ModNCompletedCoeff (ℓ ^ i.1) :=
(modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) H i.2).comp
(primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i)
let rightMap :
PrimePowerCompletedGroupAlgebraStage ℓ G
(i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) →+*
ModNCompletedCoeff (ℓ ^ i.1) :=
modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G
(completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)
change leftMap x = rightMap x
have hmaps : leftMap = rightMap := by
apply MonoidAlgebra.ringHom_ext
· intro r
rcases ZMod.intCast_surjective r with ⟨t, rfl⟩
simp only [modNCompletedGroupAlgebraStageAugmentation, primePowerCompletedGroupAlgebraMapStage,
MonoidAlgebra.mapDomainRingHom, RingHom.coe_comp, RingHom.coe_coe, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
Function.comp_apply, Finsupp.mapDomain_single, map_one, MonoidAlgebra.lift_single, smul_eq_mul,
mul_one, leftMap, rightMap]
· intro q
change leftMap
(MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1))
(_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G
(completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)) q) =
rightMap
(MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1))
(_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G
(completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)) q)
dsimp [leftMap, rightMap]
have hmap :=
primePowerCompletedGroupAlgebraMapStage_of
(ℓ := ℓ) (G := G) (H := H) ψ i q
rw [show
modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G
(completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)
(MonoidAlgebra.single q (1 : ModNCompletedCoeff (ℓ ^ i.1))) = 1 by
simpa [MonoidAlgebra.of, MonoidAlgebra.single] using
(modNCompletedGroupAlgebraStageAugmentation_of
(n := ℓ ^ i.1) (G := G)
(completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) q)]
calc
modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) H i.2
(primePowerCompletedGroupAlgebraMapStage
(ℓ := ℓ) (G := G) (H := H) ψ i (MonoidAlgebra.single q 1))
=
modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) H i.2
(MonoidAlgebra.single
(completedGroupAlgebraComapQuotientMap
(G := G) (H := H) ψ i.2 q) 1) := by
simpa [MonoidAlgebra.of, MonoidAlgebra.single] using
congrArg (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) H i.2) hmap
_ = 1 := by
simpa [MonoidAlgebra.of, MonoidAlgebra.single] using
(modNCompletedGroupAlgebraStageAugmentation_of
(n := ℓ ^ i.1) (G := H) i.2
(completedGroupAlgebraComapQuotientMap
(G := G) (H := H) ψ i.2 q))
rw [hmaps]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 primePowerCompletedGroupAlgebraMapStage_compatible
(ψ : ContinuousMonoidHom G H) {i j : PrimePowerCompletedGroupAlgebraIndex H} (hij : i ≤ j) :
(primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := H) hij).comp
(primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ j) =
(primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i).comp
(primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G)
(show
(i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) ≤
(j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2) from
⟨hij.1, completedGroupAlgebraComapIndex_mono (G := G) (H := H) ψ hij.2⟩))Coefficient change is performed stagewise: each coefficient is transported by the given ring homomorphism while the finite quotient support is left unchanged.
Show proof
by
apply RingHom.ext
intro x
refine MonoidAlgebra.induction_on
(p := fun x =>
((primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := H) hij).comp
(primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ j)) x =
((primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i).comp
(primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G)
(show
(i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) ≤
(j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2) from
⟨hij.1,
completedGroupAlgebraComapIndex_mono (G := G) (H := H) ψ hij.2⟩))) x)
x ?_ ?_ ?_
· intro q
rw [RingHom.comp_apply, RingHom.comp_apply,
primePowerCompletedGroupAlgebraMapStage_of,
primePowerCompletedGroupAlgebraTransition_of,
primePowerCompletedGroupAlgebraTransition_of]
change
MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1))
(_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H i.2)
((OpenNormalSubgroupInClass.map
(C := ProCGroups.FiniteGroupClass.allFinite) (G := H)
(U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2)
(completedGroupAlgebraComapQuotientMap (G := G) (H := H) ψ j.2 q)) =
primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
(MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1))
(_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G
(completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2))
((OpenNormalSubgroupInClass.map
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
(U := OrderDual.ofDual
(completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2))
(V := OrderDual.ofDual
(completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2))
(completedGroupAlgebraComapIndex_mono (G := G) (H := H) ψ hij.2)) q))
rw [primePowerCompletedGroupAlgebraMapStage_of]
exact congrArg (MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ i.1))
(_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient H i.2))
(congrFun
(congrArg DFunLike.coe
(completedGroupAlgebraComapQuotientMap_compatible
(G := G) (H := H) ψ hij.2)) q)
· intro x y hx hy
rw [map_add, map_add, hx, hy]
· intro a x hx
rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]
simp only [primePowerCompletedGroupAlgebraTransition, modNCompletedGroupAlgebraStageCoeffMap,
modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe, primePowerCompletedGroupAlgebraMapStage, map_intCast,
RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, MonoidAlgebra.mapDomainRingHom_apply]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.
□