theorem primePowerCompletedGroupAlgebraMap_surjective
(ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ) :
Function.Surjective
(primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ)If \(\psi : G \to H\) is surjective, then the induced map of prime-power completed group algebras is surjective.
Show proof
by
classical
let S := primePowerCompletedGroupAlgebraSystem ℓ H
let T := primePowerCompletedGroupAlgebraSystem ℓ G
let f : PrimePowerCompletedGroupAlgebra ℓ G → PrimePowerCompletedGroupAlgebra ℓ H :=
primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ
letI : Nonempty (PrimePowerCompletedGroupAlgebraIndex H) :=
⟨(0, _root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex H)⟩
letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex H, TopologicalSpace (S.X i) :=
fun i => S.topologicalSpace i
letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex H, DiscreteTopology (S.X i) :=
fun _ => ⟨rfl⟩
letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex H, CompactSpace (S.X i) :=
fun i => by
letI : Finite (S.X i) := by
dsimp [S, primePowerCompletedGroupAlgebraSystem]
infer_instance
letI : Fintype (S.X i) := Fintype.ofFinite _
infer_instance
letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex H, T2Space (S.X i) :=
fun _ => inferInstance
letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, TopologicalSpace (T.X i) :=
fun i => T.topologicalSpace i
letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, DiscreteTopology (T.X i) :=
fun _ => ⟨rfl⟩
letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, CompactSpace (T.X i) :=
fun i => by
letI : Finite (T.X i) := by
dsimp [T, primePowerCompletedGroupAlgebraSystem]
infer_instance
letI : Fintype (T.X i) := Fintype.ofFinite _
infer_instance
letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, T2Space (T.X i) :=
fun _ => inferInstance
letI : CompactSpace (PrimePowerCompletedGroupAlgebra ℓ G) :=
inferInstance
letI : T2Space (PrimePowerCompletedGroupAlgebra ℓ H) :=
S.t2Space_inverseLimit
have hf_continuous : Continuous f :=
continuous_primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ
have hclosed : IsClosed (Set.range f) :=
(isCompact_range hf_continuous).isClosed
have hprojection_images :
∀ i : PrimePowerCompletedGroupAlgebraIndex H,
S.projection i '' Set.range f =
S.projection i '' (Set.univ : Set (PrimePowerCompletedGroupAlgebra ℓ H)) := by
intro i
apply Set.Subset.antisymm
· rintro z ⟨y, _hy, rfl⟩
exact ⟨y, trivial, rfl⟩
· rintro z ⟨y, _hy, rfl⟩
rcases primePowerCompletedGroupAlgebraMapStage_surjective
(ℓ := ℓ) (G := G) (H := H) ψ hψ i (S.projection i y) with
⟨c, hc⟩
let sourceIndex : PrimePowerCompletedGroupAlgebraIndex G :=
(i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)
rcases primePowerCompletedGroupAlgebraProjection_surjective
(ℓ := ℓ) (G := G) sourceIndex c with
⟨x, hx⟩
refine ⟨f x, ⟨x, rfl⟩, ?_⟩
change primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := H) i
(primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ x) =
S.projection i y
rw [primePowerCompletedGroupAlgebraProjection_map]
change primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
(primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) sourceIndex x) =
S.projection i y
rw [hx, hc]
have hclosure :
closure (Set.range f) =
(Set.univ : Set (PrimePowerCompletedGroupAlgebra ℓ H)) := by
have hclosure' :
closure (Set.range f) =
closure (Set.univ : Set (PrimePowerCompletedGroupAlgebra ℓ H)) :=
S.closure_eq_of_projection_images_eq_of_subsets
(directed_primePowerCompletedGroupAlgebraIndex (G := H))
(Set.range f)
(Set.univ : Set (PrimePowerCompletedGroupAlgebra ℓ H))
hprojection_images
simpa using hclosure'
intro y
have hy_closure : y ∈ closure (Set.range f) := by
rw [hclosure]
simp only [Set.mem_univ]
have hy_range : y ∈ Set.range f := by
rwa [hclosed.closure_eq] at hy_closure
rcases hy_range with ⟨x, hx⟩
exact ⟨x, hx⟩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.
□def primePowerCompletedGroupAlgebraMapLiftOfSurjective
(ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ)
(a : PrimePowerCompletedGroupAlgebra ℓ H) :
PrimePowerCompletedGroupAlgebra ℓ G :=
Classical.choose
(primePowerCompletedGroupAlgebraMap_surjective
(ℓ := ℓ) (G := G) (H := H) ψ hψ a)A choice of a lift along a surjective completed group-algebra map. This is intentionally kept at the completed group-algebra level: it uses the already-proved surjectivity of \(\Lambda_G \to \Lambda_H\), and does not touch the displayed differential premodule topology.
theorem primePowerCompletedGroupAlgebraMap_liftOfSurjective
(ψ : ContinuousMonoidHom G H) (hψ : Function.Surjective ψ)
(a : PrimePowerCompletedGroupAlgebra ℓ H) :
primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ
(primePowerCompletedGroupAlgebraMapLiftOfSurjective
(ℓ := ℓ) (G := G) (H := H) ψ hψ a) = aThe chosen lift maps back to the target coefficient.
Show proof
Classical.choose_spec
(primePowerCompletedGroupAlgebraMap_surjective
(ℓ := ℓ) (G := G) (H := H) ψ hψ a)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.
□