The prescription property under topological isomorphisms

The twisted coefficient system I(χ)/pⁱ and the prescription property of a continuous p-adic character are intrinsic to the source topological group. If e : H ≃ₜ* G, then pullback along e identifies I(χ)/pⁱ with I(χ ∘ e)/pⁱ, compatibly with the reductions between levels (at the coefficient level any continuous homomorphism H →ₜ* G suffices). The resulting equivalences on explicit continuous H¹ show that χ has the prescription property exactly when χ ∘ e does.

This transport is the naturality input needed to define the canonical character of a Demushkin group using any of its normal-form presentations: uniqueness makes the transported character independent of the chosen presentation.

Main results

• TauCeti.ZModTwist.compEquiv: the coefficient equivalence I(χ)/pⁱ ≃ I(χ ∘ f)/pⁱ for a continuous homomorphism f : H →ₜ* G.
• TauCeti.ZModTwist.subgroupSubtypeHom: for a subgroup U ≤ G, the same equivalence along the inclusion of U, as a bijective U-equivariant homomorphism I(χ)/pⁱ →+[U] I(χ|_U)/pⁱ, where U acts on I(χ)/pⁱ through the inclusion.
• TauCeti.ZModTwist.explicitH1CompEquiv: the induced equivalence on explicit continuous H¹.
• TauCeti.HasPrescriptionProperty.comp_equiv: pullback along a topological group isomorphism preserves the prescription property.
• TauCeti.hasPrescriptionProperty_comp_equiv_iff: the corresponding equivalence.

Reduction compatibility

TauCeti.ZModTwist.explicitH1CompEquiv_reduce states that the equivalences on H¹ commute with every reduction map I(χ)/pⁱ → I(χ)/pʲ. Thus they identify the images of the reduction maps, so the prescription property is unchanged by pullback along a topological isomorphism. The related functoriality API is TauCeti.ContCohomology.explicitMap1Equiv, TauCeti.ContCohomology.explicitMap1_comp, TauCeti.ContCohomology.explicitMap1_congr_of_eq, and TauCeti.ContCohomology.explicitCoeff1_eq_explicitMap1.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, Proposition 6 and Theorem 4.

noncomputable def TauCeti.ZModTwist.compEquiv {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (f : H →ₜ* G) (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : ZModTwist χ i ≃+ ZModTwist (χ.comp f) i

Pullback along a continuous group homomorphism f identifies the twisted coefficient modules for χ and χ ∘ f. On residue classes this is the identity.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ZModTwist.compEquiv_apply {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (f : H →ₜ* G) (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) (x : ZModTwist χ i) : ((compEquiv f χ i) x).val = x.val

@[simp]

theorem TauCeti.ZModTwist.compEquiv_symm_apply {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (f : H →ₜ* G) (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) (x : ZModTwist (χ.comp f) i) : ((compEquiv f χ i).symm x).val = x.val

@[simp]

theorem TauCeti.ZModTwist.compEquiv_smul {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (f : H →ₜ* G) (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) (h : H) (x : ZModTwist χ i) : (compEquiv f χ i) (f h • x) = h • (compEquiv f χ i) x

The coefficient equivalence for a pulled-back character is equivariant along the group homomorphism.

@[simp]

theorem TauCeti.ZModTwist.compEquiv_reduce {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (f : H →ₜ* G) (χ : G →ₜ* ℤ_[p]ˣ) {i j : ℕ} (h : j ≤ i) (x : ZModTwist χ i) : (compEquiv f χ j) ((reduce χ h) x) = (reduce (χ.comp f) h) ((compEquiv f χ i) x)

The coefficient equivalence for a pulled-back character commutes with reduction between levels.

noncomputable def TauCeti.ZModTwist.subgroupSubtypeHom {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (U : Subgroup G) (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : ZModTwist χ i →+[↥U] ZModTwist (χ.comp (ContinuousMonoidHom.subgroupSubtype U)) i

Pullback along the inclusion of a subgroup U ≤ G, as a U-equivariant homomorphism I(χ)/pⁱ →+[U] I(χ|_U)/pⁱ, where U acts on I(χ)/pⁱ through the inclusion. The underlying map is compEquiv (ContinuousMonoidHom.subgroupSubtype U) χ i, the identity on residue classes (val_subgroupSubtypeHom), so it is bijective (subgroupSubtypeHom_bijective). It is recorded as an equivariant homomorphism because that is the form in which the coefficient maps of continuous cohomology consume it.

Equations

• TauCeti.ZModTwist.subgroupSubtypeHom U χ i = { toFun := ⇑(TauCeti.ZModTwist.compEquiv (TauCeti.ContinuousMonoidHom.subgroupSubtype U) χ i), map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem TauCeti.ZModTwist.subgroupSubtypeHom_apply {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (U : Subgroup G) (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) (x : ZModTwist χ i) : (subgroupSubtypeHom U χ i) x = (compEquiv (ContinuousMonoidHom.subgroupSubtype U) χ i) x

@[simp]

theorem TauCeti.ZModTwist.val_subgroupSubtypeHom {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (U : Subgroup G) (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) (x : ZModTwist χ i) : ((subgroupSubtypeHom U χ i) x).val = x.val

theorem TauCeti.ZModTwist.subgroupSubtypeHom_bijective {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (U : Subgroup G) (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : Function.Bijective ⇑(subgroupSubtypeHom U χ i)

noncomputable def TauCeti.ZModTwist.explicitH1CompEquiv {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (e : H ≃ₜ* G) (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) : ContCohomology.H1 G (ZModTwist χ i) ≃+ ContCohomology.H1 H (ZModTwist (χ.comp ↑e) i)

Pullback along a topological group isomorphism identifies explicit continuous H¹ with twisted coefficients.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ZModTwist.explicitH1CompEquiv_apply {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (e : H ≃ₜ* G) (χ : G →ₜ* ℤ_[p]ˣ) (i : ℕ) (x : ContCohomology.H1 G (ZModTwist χ i)) : (explicitH1CompEquiv e χ i) x = (ContCohomology.explicitMap1 G (ZModTwist χ i) H (ZModTwist (χ.comp ↑e) i) (↑e) (compEquiv (↑e) χ i).toAddMonoidHom ⋯ ⋯) x

The equivalence on explicit continuous H¹ is pullback along the topological group isomorphism and the coefficient equivalence ZModTwist.compEquiv.

theorem TauCeti.ZModTwist.explicitH1CompEquiv_reduce {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (e : H ≃ₜ* G) (χ : G →ₜ* ℤ_[p]ˣ) {i j : ℕ} (h : j ≤ i) (x : ContCohomology.H1 G (ZModTwist χ i)) : (explicitH1CompEquiv e χ j) ((ContCohomology.explicitCoeff1 G (ZModTwist χ i) (reduce χ h) ⋯) x) = (ContCohomology.explicitCoeff1 H (ZModTwist (χ.comp ↑e) i) (reduce (χ.comp ↑e) h) ⋯) ((explicitH1CompEquiv e χ i) x)

The equivalences on explicit continuous H¹ commute with reduction between the levels of the twisted coefficient system.

theorem TauCeti.HasPrescriptionProperty.comp_equiv {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] {e : H ≃ₜ* G} {χ : G →ₜ* ℤ_[p]ˣ} (hχ : HasPrescriptionProperty χ) : HasPrescriptionProperty (χ.comp ↑e)

Pullback along a topological group isomorphism preserves the prescription property.

@[simp]

theorem TauCeti.hasPrescriptionProperty_comp_equiv_iff {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {H : Type v} [Group H] [TopologicalSpace H] (e : H ≃ₜ* G) (χ : G →ₜ* ℤ_[p]ˣ) : HasPrescriptionProperty (χ.comp ↑e) ↔ HasPrescriptionProperty χ

A character has the prescription property if and only if its pullback along a topological group isomorphism does.